def LO.FirstOrder.LT.le {L : LO.FirstOrder.Language} [LO.FirstOrder.Semiformula.Operator.Eq L] [LO.FirstOrder.Semiformula.Operator.LT L] : LO.FirstOrder.Semiformula.Operator L 2

Equations

• LO.FirstOrder.LT.le = op(=).or op(<)

theorem LO.FirstOrder.le_eq {L : LO.FirstOrder.Language} [LO.FirstOrder.Semiformula.Operator.Eq L] [LO.FirstOrder.Semiformula.Operator.LT L] {μ : Type u_1} {n : ℕ} (t₁ : LO.FirstOrder.Semiterm L μ n) (t₂ : LO.FirstOrder.Semiterm L μ n) : LO.FirstOrder.LT.le.operator ![t₁, t₂] = (“(!!t₁ = !!t₂ ∨ !!t₁ < !!t₂)”)

noncomputable def LO.FirstOrder.Order.leIffEqOrLt {L : LO.FirstOrder.Language} [LO.FirstOrder.Semiformula.Operator.Eq L] [LO.FirstOrder.Semiformula.Operator.LT L] {T : LO.FirstOrder.Theory L} : T ⊢! (“∀' ∀' (!!(LO.FirstOrder.Semiterm.bvar 1) ≤ !!(LO.FirstOrder.Semiterm.bvar 0) ↔ (!!(LO.FirstOrder.Semiterm.bvar 1) = !!(LO.FirstOrder.Semiterm.bvar 0) ∨ !!(LO.FirstOrder.Semiterm.bvar 1) < !!(LO.FirstOrder.Semiterm.bvar 0)))”)

Equations

• ⋯ = ⋯

theorem LO.FirstOrder.Order.provOf {L : LO.FirstOrder.Language} [LO.FirstOrder.Semiformula.Operator.Eq L] [LO.FirstOrder.Semiformula.Operator.LT L] {T : LO.FirstOrder.Theory L} [𝐄𝐐 ≼ T] (p : LO.FirstOrder.SyntacticFormula L) (H : ∀ (M : Type (max u w)) [inst : Nonempty M] [inst_1 : LT M] [inst_2 : LO.FirstOrder.Structure L M] [inst_3 : LO.FirstOrder.Structure.Eq L M] [inst_4 : LO.FirstOrder.Structure.LT L M] [inst_5 : M ⊧ₘ* T], M ⊧ₘ p) : T ⊨ p