@[simp]

theorem AP.mkSymFs_symm {ft : PointZ ≃ PointZ} : (mkSymFs ft).symm = mkSymFs ft.symm

@[simp]

theorem AP.ft_mkSym {ft : PointZ ≃ PointZ} : (mkSym ft).ft = ft

@[simp]

theorem AP.ft'_mkSym {ft : PointZ ≃ PointZ} : (mkSym ft).ft' = ft.symm

@[simp]

theorem AP.fs_mkSym {ft : PointZ ≃ PointZ} : (mkSym ft).fs = mkSymFs ft

@[simp]

theorem AP.fs'_mkSym {ft : PointZ ≃ PointZ} : (mkSym ft).fs' = mkSymFs ft.symm

@[simp]

theorem AP.mkSymFs_apply {ft : PointZ ≃ PointZ} {s : State} : (mkSymFs ft) s = mkSymFsAux (⇑ft) s

@[simp]

theorem AP.pw_mkSymFsAux {ft : PointZ → PointZ} {s : State} : (mkSymFsAux ft s).pw = s.pw

@[simp]

theorem AP.taken_mkSymFsAux {ft : PointZ → PointZ} {s : State} : (mkSymFsAux ft s).taken = s.taken.map ft

@[simp]

theorem AP.aPos_mkSymFsAux {ft : PointZ → PointZ} {s : State} : (mkSymFsAux ft s).aPos = ft s.aPos

@[simp]

theorem AP.aTurn_mkSymFsAux {ft : PointZ → PointZ} {s : State} : (mkSymFsAux ft s).aTurn = s.aTurn

@[simp]

theorem AP.hist_mkSymFsAux {ft : PointZ → PointZ} {s : State} : (mkSymFsAux ft s).hist = List.map ft s.hist

@[simp]

theorem AP.aPos₀_mkSymFsAux {ft : PointZ → PointZ} {s : State} [hs : sys.WF s] : (mkSymFsAux ft s).aPos₀ = ft s.aPos₀

theorem AP.aPos₀_mkSymFsAux_eq_ite {ft : PointZ → PointZ} {s : State} : (mkSymFsAux ft s).aPos₀ = if s.hist = [] then s.aPos₀ else ft s.aPos₀

@[simp]

theorem AP.aTurn_sym_fs {s : State} {sym : sys.Symmetry} [hs : sys.WF s] [H : sym.WF] : (sym.fs s).aTurn = s.aTurn

@[simp]

theorem AP.aTurn_sym_fs' {s : State} {sym : sys.Symmetry} [hs : sys.WF s] [H : sym.WF] : (sym.fs' s).aTurn = s.aTurn

def AP.AStrat.sym (a : AStrat) (sym : sys.Symmetry) : AStrat

Equations

• a.sym sym = { f := sym.simFn a.f }

def AP.DStrat.sym (d : DStrat) (sym : sys.Symmetry) : DStrat

Equations

• d.sym sym = { f := sym.simFn d.f }

def AP.Strat.sym (st : Strat) (sym : sys.Symmetry) : Strat

Equations

• st.sym sym = { a := st.a.sym sym, d := st.d.sym sym }

@[simp]

instance AP.AState.sym_fs {s : State} {sym : sys.Symmetry} [hs : AState s] [H : sym.WF] : AState (sym.fs s)

@[simp]

instance AP.AState.sym_fs' {s : State} {sym : sys.Symmetry} [hs : AState s] [H : sym.WF] : AState (sym.fs' s)

@[simp]

instance AP.DState.sym_fs {s : State} {sym : sys.Symmetry} [hs : DState s] [H : sym.WF] : DState (sym.fs s)

@[simp]

instance AP.DState.sym_fs' {s : State} {sym : sys.Symmetry} [hs : DState s] [H : sym.WF] : DState (sym.fs' s)

@[simp]

instance AP.instWFSymOfWFStatePointZ {a : AStrat} {sym : sys.Symmetry} [ha : a.WF] [H : sym.WF] : (a.sym sym).WF

@[simp]

instance AP.instWFSymOfWFStatePointZ_1 {d : DStrat} {sym : sys.Symmetry} [hd : d.WF] [H : sym.WF] : (d.sym sym).WF

@[simp]

instance AP.instSimFnStatePointZSysFSymOfWFOfWF {st : Strat} {sym : sys.Symmetry} [hst : st.WF] [H : sym.WF] : sys.SimFn (st.sym sym).f

theorem AP.Strat.f_sym_eq {st : Strat} {s : State} {sym : sys.Symmetry} [hs : sys.WF s] [H : sym.WF] : (st.sym sym).f s = sym.simFn st.f s

theorem AP.Strat.simulate_sym_eq {st : Strat} {s : State} {n : ℕ} {sym : sys.Symmetry} [hst : st.WF] [hs : sys.WF s] [H : sym.WF] : sys.simulate (st.sym sym).f s n = sys.simulate (sym.simFn st.f) s n

@[simp]

instance AP.instWFSymOfWFStatePointZ_2 {st : Strat} {sym : sys.Symmetry} [hst : st.WF] [H : sym.WF] : (st.sym sym).WF

theorem AP.State.aHws_sym_of {s : State} {sym : sys.Symmetry} [hs : sys.WF s] [H : sym.WF] (h : s.aHws) : (sym.fs s).aHws

theorem AP.State.aHws_iff_sym {s : State} {sym : sys.Symmetry} [hs : sys.WF s] [H : sym.WF] : s.aHws ↔ (sym.fs s).aHws

theorem AP.State.dHws_iff_sym {s : State} {sym : sys.Symmetry} {hs : sys.WF s} [H : sym.WF] : s.dHws ↔ (sym.fs s).dHws

@[simp]

theorem AP.mkSymFsAux_initState {ft : PointZ → PointZ} {pw : ℕ} {p : PointZ} : mkSymFsAux ft (initState pw p) = initState pw (ft p)

@[simp]

theorem AP.mkSymFsAux_id : mkSymFsAux id = id

@[simp]

theorem AP.mkSym_one : mkSym 1 = 1

@[simp]

instance AP.instBasicSymOfNatSymmetryStatePointZSys : BasicSym 1

@[simp]

instance AP.instBasicSymInvSymmetryStatePointZSys {sym : sys.Symmetry} [H : BasicSym sym] : BasicSym sym⁻¹

@[simp]

instance AP.instBasicSymHPowSymmetryStatePointZSysNat {sym : sys.Symmetry} {n : ℕ} [H : BasicSym sym] : BasicSym (sym ^ n)

@[simp]

instance AP.instBasicSymHPowSymmetryStatePointZSysInt {sym : sys.Symmetry} {z : ℤ} [H : BasicSym sym] : BasicSym (sym ^ z)

@[simp]

theorem AP.aPos₀_sym_of_basicSym {sym : sys.Symmetry} {s : State} [H : BasicSym sym] [hs : sys.WF s] : (sym.fs s).aPos₀ = sym.ft s.aPos₀

@[simp]

theorem AP.aPos₀_sym_of_basicSym' {sym : sys.Symmetry} {s : State} [H : BasicSym sym] [hs : sys.WF s] : (sym.fs' s).aPos₀ = sym.ft' s.aPos₀

@[simp]

theorem AP.aPos_sym_of_basicSym {sym : sys.Symmetry} {s : State} [H : BasicSym sym] : (sym.fs s).aPos = sym.ft s.aPos

@[simp]

theorem AP.aPos_sym_of_basicSym' {sym : sys.Symmetry} {s : State} [H : BasicSym sym] : (sym.fs' s).aPos = sym.ft' s.aPos

@[simp]

theorem AP.taken_sym_of_basicSym {sym : sys.Symmetry} {s : State} [H : BasicSym sym] : (sym.fs s).taken = s.taken.map ⇑sym.ft

@[simp]

theorem AP.taken_sym_of_basicSym' {sym : sys.Symmetry} {s : State} [H : BasicSym sym] : (sym.fs' s).taken = s.taken.map ⇑sym.ft'

theorem AP.ft_eq_iff {sym : sys.Symmetry} {p₁ p₂ : PointZ} : sym.ft p₁ = p₂ ↔ p₁ = sym.ft' p₂

theorem AP.ft'_eq_iff {sym : sys.Symmetry} {p₁ p₂ : PointZ} : sym.ft' p₁ = p₂ ↔ p₁ = sym.ft p₂

theorem AP.fs_eq_iff {sym : sys.Symmetry} {s₁ s₂ : State} : sym.fs s₁ = s₂ ↔ s₁ = sym.fs' s₂

theorem AP.fs'_eq_iff {sym : sys.Symmetry} {s₁ s₂ : State} : sym.fs' s₁ = s₂ ↔ s₁ = sym.fs s₂

theorem AP.ext_iff_of_basicSym {sym₁ sym₂ : sys.Symmetry} [H₁ : BasicSym sym₁] [H₂ : BasicSym sym₂] : sym₁ = sym₂ ↔ ∀ (p : PointZ), sym₁.ft p = sym₂.ft p

@[simp]

instance AP.instBasicSymHMulSymmetryStatePointZSys {sym₁ sym₂ : sys.Symmetry} [H₁ : BasicSym sym₁] [H₂ : BasicSym sym₂] : BasicSym (sym₁ * sym₂)

@[simp]

theorem AP.pw_fs_of_basicSym {s : State} {sym : sys.Symmetry} [H : BasicSym sym] : (sym.fs s).pw = s.pw

@[simp]

theorem AP.pw_fs'_of_basicSym {s : State} {sym : sys.Symmetry} [H : BasicSym sym] : (sym.fs' s).pw = s.pw