def Hex.PermGroup.Program.shift (offset : Nat) : Node → Node

Relocate node references when appending an independent program. Generator indices address the same input array and are left unchanged.

Equations

• Hex.PermGroup.Program.shift offset Hex.PermGroup.Node.id = Hex.PermGroup.Node.id
• Hex.PermGroup.Program.shift offset (Hex.PermGroup.Node.generator i) = Hex.PermGroup.Node.generator i
• Hex.PermGroup.Program.shift offset (Hex.PermGroup.Node.inv i) = Hex.PermGroup.Node.inv (offset + i)
• Hex.PermGroup.Program.shift offset (Hex.PermGroup.Node.comp i j) = Hex.PermGroup.Node.comp (offset + i) (offset + j)

theorem Hex.PermGroup.Program.evalNode_shift {n : Nat} (S : Array (Perm n)) (pre values : Array { p : Perm n // Generated S p }) (node : Node) : evalNode S (pre ++ values) (shift pre.size node) = evalNode S values node

theorem Hex.PermGroup.Program.evalNodes_shift {n : Nat} (S : Array (Perm n)) (nodes : List Node) (pre values : Array { p : Perm n // Generated S p }) : evalNodes S (List.map (shift pre.size) nodes) (pre ++ values) = Option.map (fun (x : Array { p : Perm n // Generated S p }) => pre ++ x) (evalNodes S nodes values)

theorem Hex.PermGroup.Program.evalNodes_get {n : Nat} {S : Array (Perm n)} {nodes : List Node} {values result : Array { p : Perm n // Generated S p }} (h : evalNodes S nodes values = some result) (i : Fin values.size) : result[↑i]? = some values[↑i]

Every prefix of a successful evaluation retains its cached values.

theorem Hex.PermGroup.Program.eval_values {n : Nat} {S : Array (Perm n)} {w : Program} {p : Perm n} (h : eval S w = some p) : ∃ (values : Array { p : Perm n // Generated S p }), evalNodes S w.nodes.toList #[] = some values ∧ ∃ (hi : w.root < values.size), values[w.root].val = p

def Hex.PermGroup.Program.inv (w : Program) : Program

Append an inverse node without expanding the program's expression.

Equations

• w.inv = { nodes := w.nodes.push (Hex.PermGroup.Node.inv w.root), root := w.nodes.size }

theorem Hex.PermGroup.Program.eval_inv {n : Nat} {S : Array (Perm n)} {w : Program} {p : Perm n} (h : eval S w = some p) : eval S w.inv = some p.inv

def Hex.PermGroup.Program.comp (u v : Program) : Program

Compose programs by relocating the right program, then adding one product node. Each input DAG is copied once; its internal shared references stay shared.

Equations

• One or more equations did not get rendered due to their size.

theorem Hex.PermGroup.Program.eval_comp {n : Nat} {S : Array (Perm n)} {u v : Program} {p q : Perm n} (hu : eval S u = some p) (hv : eval S v = some q) : eval S (u.comp v) = some (p.comp q)