@[simp]

theorem System.Symmetry.ft_mk {S T : Type u} {sys : System S T} {ft : T ≃ T} {fs : S ≃ S} : { ft := ft, fs := fs }.ft = ft

@[simp]

theorem System.Symmetry.ft'_mk {S T : Type u} {sys : System S T} {ft : T ≃ T} {fs : S ≃ S} : { ft := ft, fs := fs }.ft' = ft.symm

@[simp]

theorem System.Symmetry.fs_mk {S T : Type u} {sys : System S T} {ft : T ≃ T} {fs : S ≃ S} : { ft := ft, fs := fs }.fs = fs

@[simp]

theorem System.Symmetry.fs'_mk {S T : Type u} {sys : System S T} {ft : T ≃ T} {fs : S ≃ S} : { ft := ft, fs := fs }.fs' = fs.symm

@[simp]

theorem System.Symmetry.ft'_ft {S T : Type u} {sys : System S T} {sym : sys.Symmetry} {t : T} : sym.ft' (sym.ft t) = t

@[simp]

theorem System.Symmetry.ft_ft' {S T : Type u} {sys : System S T} {sym : sys.Symmetry} {t : T} : sym.ft (sym.ft' t) = t

@[simp]

theorem System.Symmetry.fs'_fs {S T : Type u} {sys : System S T} {sym : sys.Symmetry} {s : S} : sym.fs' (sym.fs s) = s

@[simp]

theorem System.Symmetry.fs_fs' {S T : Type u} {sys : System S T} {sym : sys.Symmetry} {s : S} : sym.fs (sym.fs' s) = s

@[simp]

theorem System.Symmetry.ft_symm {S T : Type u} {sys : System S T} {sym : sys.Symmetry} : sym.ft.symm = sym.ft'

@[simp]

theorem System.Symmetry.ft'_symm {S T : Type u} {sys : System S T} {sym : sys.Symmetry} : sym.ft'.symm = sym.ft

@[simp]

theorem System.Symmetry.fs_symm {S T : Type u} {sys : System S T} {sym : sys.Symmetry} : sym.fs.symm = sym.fs'

@[simp]

theorem System.Symmetry.fs'_symm {S T : Type u} {sys : System S T} {sym : sys.Symmetry} : sym.fs'.symm = sym.fs

@[simp]

theorem System.Symmetry.initial_fs_iff {S T : Type u} {sys : System S T} {sym : sys.Symmetry} [wf : sym.WF] {s : S} : sys.Initial (sym.fs s) ↔ sys.Initial s

@[simp]

theorem System.Symmetry.initial_fs'_iff {S T : Type u} {sys : System S T} {sym : sys.Symmetry} [wf : sym.WF] {s : S} : sys.Initial (sym.fs' s) ↔ sys.Initial s

theorem System.Symmetry.tr_eq {S T : Type u} {sys : System S T} {sym : sys.Symmetry} [wf : sym.WF] {s : S} {t : T} : sys.tr s t = Option.map (⇑sym.fs') (sys.tr (sym.fs s) (sym.ft t))

theorem System.Symmetry.tr_eq' {S T : Type u} {sys : System S T} {sym : sys.Symmetry} [wf : sym.WF] {s : S} {t : T} : sys.tr s t = Option.map (⇑sym.fs) (sys.tr (sym.fs' s) (sym.ft' t))

theorem System.Symmetry.reachable_of {S T : Type u} {sys : System S T} {sym : sys.Symmetry} [wf : sym.WF] {s s' : S} (h : sys.Reachable s s') : sys.Reachable (sym.fs s) (sym.fs s')

theorem System.Symmetry.reachable'_of {S T : Type u} {sys : System S T} {sym : sys.Symmetry} [wf : sym.WF] {s s' : S} (h : sys.Reachable s s') : sys.Reachable (sym.fs' s) (sym.fs' s')

theorem System.Symmetry.reachable_iff {S T : Type u} {sys : System S T} {sym : sys.Symmetry} [wf : sym.WF] {s s' : S} : sys.Reachable s s' ↔ sys.Reachable (sym.fs s) (sym.fs s')

theorem System.Symmetry.reachable_iff' {S T : Type u} {sys : System S T} {sym : sys.Symmetry} [wf : sym.WF] {s s' : S} : sys.Reachable s s' ↔ sys.Reachable (sym.fs' s) (sym.fs' s')

@[simp]

theorem System.Symmetry.wf_fs_iff {S T : Type u} {sys : System S T} {sym : sys.Symmetry} [wf : sym.WF] {s : S} : sys.WF (sym.fs s) ↔ sys.WF s

@[simp]

theorem System.Symmetry.wf_fs'_iff {S T : Type u} {sys : System S T} {sym : sys.Symmetry} [wf : sym.WF] {s : S} : sys.WF (sym.fs' s) ↔ sys.WF s

instance System.Symmetry.instWFCoeEquivFs {S T : Type u} {sys : System S T} {sym : sys.Symmetry} [wf : sym.WF] {s : S} [hs : sys.WF s] : sys.WF (sym.fs s)

instance System.Symmetry.instWFCoeEquivFs' {S T : Type u} {sys : System S T} {sym : sys.Symmetry} [wf : sym.WF] {s : S} [hs : sys.WF s] : sys.WF (sym.fs' s)

theorem System.Symmetry.validTr_iff {S T : Type u} {sys : System S T} {sym : sys.Symmetry} [wf : sym.WF] {s : S} {t : T} : sys.validTr s t ↔ sys.validTr (sym.fs s) (sym.ft t)

theorem System.Symmetry.validTr_iff' {S T : Type u} {sys : System S T} {sym : sys.Symmetry} [wf : sym.WF] {s : S} {t : T} : sys.validTr s t ↔ sys.validTr (sym.fs' s) (sym.ft' t)

theorem System.Symmetry.hasTr_iff {S T : Type u} {sys : System S T} {sym : sys.Symmetry} [wf : sym.WF] {s : S} : sys.hasTr s ↔ sys.hasTr (sym.fs s)

theorem System.Symmetry.hasTr_iff' {S T : Type u} {sys : System S T} {sym : sys.Symmetry} [wf : sym.WF] {s : S} : sys.hasTr s ↔ sys.hasTr (sym.fs' s)

@[simp]

theorem System.Symmetry.hasTr_fs_iff {S T : Type u} {sys : System S T} {sym : sys.Symmetry} [wf : sym.WF] {s : S} : sys.hasTr (sym.fs s) ↔ sys.hasTr s

@[simp]

theorem System.Symmetry.hasTr_fs'_iff {S T : Type u} {sys : System S T} {sym : sys.Symmetry} [wf : sym.WF] {s : S} : sys.hasTr (sym.fs' s) ↔ sys.hasTr s

@[simp]

theorem System.Symmetry.ft_one {S T : Type u} {sys : System S T} {t : T} : (ft 1) t = t

@[simp]

theorem System.Symmetry.ft'_one {S T : Type u} {sys : System S T} {t : T} : (ft' 1) t = t

@[simp]

theorem System.Symmetry.fs_one {S T : Type u} {sys : System S T} {s : S} : (fs 1) s = s

@[simp]

theorem System.Symmetry.fs'_one {S T : Type u} {sys : System S T} {s : S} : (fs' 1) s = s

@[simp]

instance System.Symmetry.instWFOfNat {S T : Type u} {sys : System S T} : WF 1

instance System.Symmetry.instSimFnSimFn {S T : Type u} {sys : System S T} {sym : sys.Symmetry} [wf : sym.WF] {f : S → T} [hf : sys.SimFn f] : sys.SimFn (sym.simFn f)

@[simp]

theorem System.Symmetry.ft_inv {S T : Type u} {sys : System S T} {sym : sys.Symmetry} : sym⁻¹.ft = sym.ft'

@[simp]

theorem System.Symmetry.ft'_inv {S T : Type u} {sys : System S T} {sym : sys.Symmetry} : sym⁻¹.ft' = sym.ft

@[simp]

theorem System.Symmetry.fs_inv {S T : Type u} {sys : System S T} {sym : sys.Symmetry} : sym⁻¹.fs = sym.fs'

@[simp]

theorem System.Symmetry.fs'_inv {S T : Type u} {sys : System S T} {sym : sys.Symmetry} : sym⁻¹.fs' = sym.fs

instance System.Symmetry.instWFInv {S T : Type u} {sys : System S T} {sym : sys.Symmetry} [wf : sym.WF] : sym⁻¹.WF

@[simp]

theorem System.Symmetry.inv_inv {S T : Type u} {sys : System S T} {sym : sys.Symmetry} : sym⁻¹⁻¹ = sym

@[simp]

theorem System.Symmetry.ft_mul {S T : Type u} {sys : System S T} {sym₁ sym₂ : sys.Symmetry} {t : T} : (sym₁ * sym₂).ft t = sym₁.ft (sym₂.ft t)

@[simp]

theorem System.Symmetry.ft'_mul {S T : Type u} {sys : System S T} {sym₁ sym₂ : sys.Symmetry} {t : T} : (sym₁ * sym₂).ft' t = sym₂.ft' (sym₁.ft' t)

@[simp]

theorem System.Symmetry.fs_mul {S T : Type u} {sys : System S T} {sym₁ sym₂ : sys.Symmetry} {s : S} : (sym₁ * sym₂).fs s = sym₁.fs (sym₂.fs s)

@[simp]

theorem System.Symmetry.fs'_mul {S T : Type u} {sys : System S T} {sym₁ sym₂ : sys.Symmetry} {s : S} : (sym₁ * sym₂).fs' s = sym₂.fs' (sym₁.fs' s)

instance System.Symmetry.instWFHMul {S T : Type u} {sys : System S T} {sym₁ sym₂ : sys.Symmetry} [wf₁ : sym₁.WF] [wf₂ : sym₂.WF] : (sym₁ * sym₂).WF

instance System.Symmetry.instWFHDiv {S T : Type u} {sys : System S T} {sym₁ sym₂ : sys.Symmetry} [wf₁ : sym₁.WF] [wf₂ : sym₂.WF] : (sym₁ / sym₂).WF

@[simp]

theorem System.Symmetry.inv_mul_cancel {S T : Type u} {sys : System S T} {sym : sys.Symmetry} : sym⁻¹ * sym = 1

@[simp]

theorem System.Symmetry.inv_eq_of_mul {S T : Type u} {sys : System S T} {sym₁ sym₂ : sys.Symmetry} (h : sym₁ * sym₂ = 1) : sym₁⁻¹ = sym₂

@[instance_reducible]

instance System.Symmetry.instGroup {S T : Type u} {sys : System S T} : Group sys.Symmetry

Equations

• System.Symmetry.instGroup = { toMul := System.Symmetry.instMul, mul_assoc := ⋯, toOne := System.Symmetry.instOne, one_mul := ⋯, mul_one := ⋯, npow := npowRecAuto, npow_zero := ⋯, npow_succ := ⋯, toInv := System.Symmetry.instInv, toDiv := System.Symmetry.instDiv, zpow := zpowRec, div_eq_mul_inv := ⋯, zpow_zero' := ⋯, zpow_succ' := ⋯, zpow_neg' := ⋯, inv_mul_cancel := ⋯ }

@[instance_reducible]

instance System.Symmetry.instDivisionMonoid {S T : Type u} {sys : System S T} : DivisionMonoid sys.Symmetry

Equations

• System.Symmetry.instDivisionMonoid = { toDivInvMonoid := System.Symmetry.instGroup.toDivInvMonoid, inv_inv := ⋯, mul_inv_rev := ⋯, inv_eq_of_mul := ⋯ }

theorem System.Symmetry.npow_def {S T : Type u} {sys : System S T} {sym : sys.Symmetry} {n : ℕ} : sym ^ n = npow n sym

instance System.Symmetry.instWFHPowNat {S T : Type u} {sys : System S T} {sym : sys.Symmetry} [wf : sym.WF] {n : ℕ} : (sym ^ n).WF

theorem System.Symmetry.zpow_def {S T : Type u} {sys : System S T} {sym : sys.Symmetry} {z : ℤ} : sym ^ z = zpow z sym

instance System.Symmetry.instWFHPowInt {S T : Type u} {sys : System S T} {sym : sys.Symmetry} [wf : sym.WF] {z : ℤ} : (sym ^ z).WF

@[simp]

theorem System.Symmetry.simFn'_simFn {S T : Type u} {sys : System S T} {sym : sys.Symmetry} {f : S → T} : sym.simFn' (sym.simFn f) = f

@[simp]

theorem System.Symmetry.simFn_simFn' {S T : Type u} {sys : System S T} {sym : sys.Symmetry} {f : S → T} : sym.simFn (sym.simFn' f) = f

@[simp]

theorem System.Symmetry.simFn_inv {S T : Type u} {sys : System S T} {sym : sys.Symmetry} : sym⁻¹.simFn = sym.simFn'

theorem System.Symmetry.tr_fs_ft {S T : Type u} {sys : System S T} {sym : sys.Symmetry} [wf : sym.WF] {s : S} {t : T} : sys.tr (sym.fs s) (sym.ft t) = Option.map (⇑sym.fs) (sys.tr s t)

theorem System.Symmetry.tr_fs'_ft' {S T : Type u} {sys : System S T} {sym : sys.Symmetry} [wf : sym.WF] {s : S} {t : T} : sys.tr (sym.fs' s) (sym.ft' t) = Option.map (⇑sym.fs') (sys.tr s t)

theorem System.Symmetry.trs_eq {S T : Type u} {sys : System S T} {sym : sys.Symmetry} [wf : sym.WF] {s : S} {ts : List T} : sys.trs s ts = Prod.map (⇑sym.fs') (fun (x : List T) => List.map (⇑sym.ft') x) (sys.trs (sym.fs s) (List.map (⇑sym.ft) ts))

theorem System.Symmetry.trs_eq' {S T : Type u} {sys : System S T} {sym : sys.Symmetry} [wf : sym.WF] {s : S} {ts : List T} : sys.trs s ts = Prod.map (⇑sym.fs) (fun (x : List T) => List.map (⇑sym.ft) x) (sys.trs (sym.fs' s) (List.map (⇑sym.ft') ts))

theorem System.Symmetry.simulate_eq {S T : Type u} {sys : System S T} {sym : sys.Symmetry} [wf : sym.WF] {f : S → T} {s : S} {n : ℕ} : sys.simulate f s n = Prod.map (⇑sym.fs') id (sys.simulate (sym.simFn f) (sym.fs s) n)

theorem System.Symmetry.simulate_eq' {S T : Type u} {sys : System S T} {sym : sys.Symmetry} [wf : sym.WF] {f : S → T} {s : S} {n : ℕ} : sys.simulate f s n = Prod.map (⇑sym.fs) id (sys.simulate (sym.simFn' f) (sym.fs' s) n)

@[simp]

theorem System.Symmetry.snd_simulate_eq {S T : Type u} {sys : System S T} {sym : sys.Symmetry} [wf : sym.WF] {f : S → T} {s : S} {n : ℕ} : (sys.simulate (sym.simFn f) s n).2 = (sys.simulate f (sym.fs' s) n).2

@[simp]

theorem System.Symmetry.snd_simulate_eq' {S T : Type u} {sys : System S T} {sym : sys.Symmetry} [wf : sym.WF] {f : S → T} {s : S} {n : ℕ} : (sys.simulate (sym.simFn' f) s n).2 = (sys.simulate f (sym.fs s) n).2

@[simp]

theorem System.Symmetry.SelfInverse.inv_eq_self' {S T : Type u} {sys : System S T} {sym : sys.Symmetry} [H : sym.SelfInverse] : sym⁻¹ = sym

@[simp]

theorem System.Symmetry.SelfInverse.ft'_eq_ft {S T : Type u} {sys : System S T} {sym : sys.Symmetry} [H : sym.SelfInverse] : sym.ft' = sym.ft

@[simp]

theorem System.Symmetry.SelfInverse.fs'_eq_fs {S T : Type u} {sys : System S T} {sym : sys.Symmetry} [H : sym.SelfInverse] : sym.fs' = sym.fs

@[simp]

theorem System.Symmetry.SelfInverse.ft_ft {S T : Type u} {sys : System S T} {sym : sys.Symmetry} [H : sym.SelfInverse] {t : T} : sym.ft (sym.ft t) = t

@[simp]

theorem System.Symmetry.SelfInverse.fs_fs {S T : Type u} {sys : System S T} {sym : sys.Symmetry} [H : sym.SelfInverse] {s : S} : sym.fs (sym.fs s) = s