Equations
- LO.FirstOrder.newVar Γ = List.foldr max 0 (List.map LO.FirstOrder.Semiformula.upper Γ)
Instances For
theorem
LO.FirstOrder.not_fvar?_newVar
{L : LO.FirstOrder.Language}
{p : LO.FirstOrder.SyntacticFormula L}
{Γ : LO.FirstOrder.Sequent L}
(h : p ∈ Γ)
:
def
LO.FirstOrder.Derivation.allNvar
{L : LO.FirstOrder.Language}
{T : LO.FirstOrder.Theory L}
{Δ : LO.FirstOrder.Sequent L}
{p : LO.FirstOrder.SyntacticSemiformula L (0 + 1)}
(h : ∀' p ∈ Δ)
:
T ⟹ (LO.FirstOrder.Rew.substs ![LO.FirstOrder.Semiterm.fvar (LO.FirstOrder.newVar Δ)]).hom p :: Δ → T ⟹ Δ
Equations
- LO.FirstOrder.Derivation.allNvar h b = let b := LO.FirstOrder.Derivation.genelalizeByNewver ⋯ ⋯ b; LO.Tait.wk b ⋯
Instances For
def
LO.FirstOrder.Derivation.id
{L : LO.FirstOrder.Language}
{T : LO.FirstOrder.Theory L}
{Δ : LO.FirstOrder.Sequent L}
{p : LO.FirstOrder.SyntacticFormula L}
(hp : p ∈ T)
:
T ⟹ ∼LO.FirstOrder.Semiformula.close p :: Δ → T ⟹ Δ
Equations
Instances For
- 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
Instances For
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.
Instances For
instance
LO.FirstOrder.System.instEncodableCode
{L : LO.FirstOrder.Language}
[(k : ℕ) → Encodable (L.Func k)]
[(k : ℕ) → Encodable (L.Rel k)]
:
Equations
- One or more equations did not get rendered due to their size.