def Hex.PermGroup.Chain.programSize {n : Nat} (c : Chain n) : c.Choice → Nat

Compute the exact membership-program allocation from existing program sizes and chain choices, without constructing the translated programs.

Equations

• One or more equations did not get rendered due to their size.
• (Hex.PermGroup.Chain.leaf generators words).programSize x_2 = 1

theorem Hex.PermGroup.Chain.program_size {n : Nat} (c : Chain n) (base : Nat) (h : c.checkFrom base = true) (digits : c.Choice) : (c.program base h digits).val.nodes.size = c.programSize digits

def Hex.PermGroup.Group.programSize {n : Nat} (G : Group n) (digits : G.chain.Choice) : Nat

Equations

• G.programSize digits = 1 + (List.map (fun (w : Hex.PermGroup.Program) => w.nodes.size) G.chain.words.toList).sum + G.chain.programSize digits

theorem Hex.PermGroup.Group.program_size {n : Nat} (G : Group n) (digits : G.chain.Choice) : (G.program digits).nodes.size = G.programSize digits