Measures

def lengthOfProgram : Program → ℕ

Equations

• lengthOfProgram (·a) = 1
• lengthOfProgram (α;'β) = 1 + lengthOfProgram α + lengthOfProgram β
• lengthOfProgram (α⋓β) = 1 + lengthOfProgram α + lengthOfProgram β
• lengthOfProgram (∗α) = 1 + lengthOfProgram α
• lengthOfProgram (?'φ) = 2 + lengthOfFormula φ

def lengthOfFormula : Formula → ℕ

Equations

• lengthOfFormula Formula.bottom = 1
• lengthOfFormula (·a) = 1
• lengthOfFormula (~φ) = 1 + lengthOfFormula φ
• lengthOfFormula (φ⋀ψ) = 1 + lengthOfFormula φ + lengthOfFormula ψ
• lengthOfFormula (⌈α⌉φ) = 1 + lengthOfProgram α + lengthOfFormula φ

class HasLength (α : Type) : Type

• lengthOf : α → ℕ

instance formulaHasLength : HasLength Formula

Equations

• formulaHasLength = { lengthOf := lengthOfFormula }

instance setFormulaHasLength : HasLength (Finset Formula)

Equations

• setFormulaHasLength = { lengthOf := fun (X : Finset Formula) => X.sum lengthOfFormula }

instance listFormulaHasLength : HasLength (List Formula)

Equations

• listFormulaHasLength = { lengthOf := fun (X : List Formula) => (List.map lengthOfFormula X).sum }

instance programHasLength : HasLength Program

Equations

• programHasLength = { lengthOf := lengthOfProgram }

instance setProgramHasLength : HasLength (Finset Program)

Equations

• setProgramHasLength = { lengthOf := fun (X : Finset Program) => X.sum lengthOfProgram }