def LO.FirstOrder.newVar {L : LO.FirstOrder.Language} (Γ : LO.FirstOrder.Sequent L) : ℕ

Equations

• LO.FirstOrder.newVar Γ = List.foldr max 0 (List.map LO.FirstOrder.Semiformula.fvSup Γ)

theorem LO.FirstOrder.not_fvar?_newVar {L : LO.FirstOrder.Language} {φ : LO.FirstOrder.SyntacticFormula L} {Γ : LO.FirstOrder.Sequent L} (h : φ ∈ Γ) : ¬LO.FirstOrder.Semiformula.FVar? φ (LO.FirstOrder.newVar Γ)

def LO.FirstOrder.Derivation.allNvar {L : LO.FirstOrder.Language} {T : LO.FirstOrder.Theory L} {Δ : LO.FirstOrder.Sequent L} {φ : LO.FirstOrder.SyntacticSemiformula L (0 + 1)} (h : ∀' φ ∈ Δ) : T ⟹ φ/[LO.FirstOrder.Semiterm.fvar (LO.FirstOrder.newVar Δ)] :: Δ → T ⟹ Δ

Equations

• LO.FirstOrder.Derivation.allNvar h b = LO.Tait.wk (LO.FirstOrder.Derivation.genelalizeByNewver ⋯ ⋯ b) ⋯

def LO.FirstOrder.Derivation.id {L : LO.FirstOrder.Language} {T : LO.FirstOrder.Theory L} {Δ : LO.FirstOrder.Sequent L} {φ : LO.FirstOrder.SyntacticFormula L} (hp : φ ∈ T) : T ⟹ ∼LO.FirstOrder.Semiformula.close φ :: Δ → T ⟹ Δ

Equations

• LO.FirstOrder.Derivation.id hp b = LO.Tait.cut (LO.Tait.wk (LO.FirstOrder.Derivation.toClose (LO.FirstOrder.Derivation.root hp)) ⋯) b

inductive LO.FirstOrder.System.Code (L : LO.FirstOrder.Language) : Type u

• axL: {L : LO.FirstOrder.Language} → {k : ℕ} → L.Rel k → (Fin k → LO.FirstOrder.SyntacticTerm L) → LO.FirstOrder.System.Code L
• verum: {L : LO.FirstOrder.Language} → LO.FirstOrder.System.Code L
• and: {L : LO.FirstOrder.Language} → LO.FirstOrder.SyntacticFormula L → LO.FirstOrder.SyntacticFormula L → LO.FirstOrder.System.Code L
• or: {L : LO.FirstOrder.Language} → LO.FirstOrder.SyntacticFormula L → LO.FirstOrder.SyntacticFormula L → LO.FirstOrder.System.Code L
• all: {L : LO.FirstOrder.Language} → LO.FirstOrder.SyntacticSemiformula L 1 → LO.FirstOrder.System.Code L
• ex: {L : LO.FirstOrder.Language} → LO.FirstOrder.SyntacticSemiformula L 1 → LO.FirstOrder.SyntacticTerm L → LO.FirstOrder.System.Code L
• id: {L : LO.FirstOrder.Language} → LO.FirstOrder.SyntacticFormula L → LO.FirstOrder.System.Code L

def LO.FirstOrder.System.Code.equiv (L : LO.FirstOrder.Language) : LO.FirstOrder.System.Code L ≃ (k : ℕ) × L.Rel k × (Fin k → LO.FirstOrder.SyntacticTerm L) ⊕ Unit ⊕ LO.FirstOrder.SyntacticFormula L × LO.FirstOrder.SyntacticFormula L ⊕ LO.FirstOrder.SyntacticFormula L × LO.FirstOrder.SyntacticFormula L ⊕ LO.FirstOrder.SyntacticSemiformula L 1 ⊕ LO.FirstOrder.SyntacticSemiformula L 1 × LO.FirstOrder.SyntacticTerm L ⊕ LO.FirstOrder.SyntacticFormula L

Equations

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

instance LO.FirstOrder.System.instEncodableCodeOfDecidableEqOfFuncOfRel {L : LO.FirstOrder.Language} [(k : ℕ) → DecidableEq (L.Func k)] [(k : ℕ) → DecidableEq (L.Rel k)] [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] : Encodable (LO.FirstOrder.System.Code L)

Equations

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