def freshVarForm : Formula → ℕ

Get a fresh atomic proposition x not occuring in ψ.

Equations

• freshVarForm Formula.bottom = 0
• freshVarForm (·c) = c + 1
• freshVarForm (~φ) = freshVarForm φ
• freshVarForm (φ1⋀φ2) = freshVarForm φ1 ⊔ freshVarForm φ2
• freshVarForm (⌈α⌉φ) = freshVarProg α ⊔ freshVarForm φ

def freshVarProg : Program → ℕ

Get a fresh atomic proposition x not occuring in α.

Equations

• freshVarProg (·a) = 0
• freshVarProg (α;'β) = freshVarProg α ⊔ freshVarProg β
• freshVarProg (α⋓β) = freshVarProg α ⊔ freshVarProg β
• freshVarProg (∗α) = freshVarProg α
• freshVarProg (?'φ) = freshVarForm φ

theorem freshVarForm_is_larger (φ : Formula) (n : ℕ) : n ∈ φ.voc.atomProps → n < freshVarForm φ

theorem freshVarProg_is_larger (α : Program) (n : ℕ) : n ∈ α.voc.atomProps → n < freshVarProg α

theorem freshVarForm_is_fresh (φ : Formula) : Sum.inl (freshVarForm φ) ∉ φ.voc

theorem freshVarProg_is_fresh (α : Program) : Sum.inl (freshVarProg α) ∉ α.voc