def AP.mkSymFsAux (f : PointZ → PointZ) (s : State) : State

Equations

• AP.mkSymFsAux f s = { pw := s.pw, taken := s.taken.map f, aPos := f s.aPos, aTurn := s.aTurn, hist := List.map f s.hist }

def AP.mkSymFs (ft : PointZ ≃ PointZ) : State ≃ State

Equations

• AP.mkSymFs ft = { toFun := AP.mkSymFsAux ⇑ft, invFun := AP.mkSymFsAux ⇑ft.symm, left_inv := ⋯, right_inv := ⋯ }

def AP.mkSym (ft : PointZ ≃ PointZ) : sys.Symmetry

Equations

• AP.mkSym ft = { ft := ft, fs := AP.mkSymFs ft }

class AP.BasicSym (sym : sys.Symmetry) extends sym.WF : Prop

• initial_fs_iff {s : AP.State} : AP.sys.Initial (sym.fs s) ↔ AP.sys.Initial s
• tr_eq {s : AP.State} {t : PointZ} : AP.sys.tr s t = Option.map (⇑sym.fs') (AP.sys.tr (sym.fs s) (sym.ft t))
• exi_mkSym : ∃ (ft : PointZ ≃ PointZ), mkSym ft = sym