NF weak partition development: NFCompactLeafSemanticAdapters.

theorem NFChoice.Compiler.NFCompactLeafSemanticAdapters.holds_syn_csn {S : Fol.Structure Foundation.LNF} (v : SemanticCore.Var → S.carrier) (A : SemanticCore.Class) (s : S.carrier) : SemanticCore.Class.Holds S v (CompactSourceSyntax.synCsn A) s ↔ ∀ (a : S.carrier), SemanticCore.Mem S a s ↔ SemanticCore.Class.Holds S v A a

Semantic membership in the compact singleton constructor.

theorem NFChoice.Compiler.NFCompactLeafSemanticAdapters.holds_syn_cnin {S : Fol.Structure Foundation.LNF} (hExt : SemanticCore.Extensional S) (v : SemanticCore.Var → S.carrier) (A B : SemanticCore.Class) (s : S.carrier) : SemanticCore.Class.Holds S v (CompactSourceSyntax.synCnin A B) s ↔ ¬(SemanticCore.Class.Holds S v A s ∧ SemanticCore.Class.Holds S v B s)

Semantic NAND law for the compact class intersection-complement primitive.

theorem NFChoice.Compiler.NFCompactLeafSemanticAdapters.holds_syn_ccompl {S : Fol.Structure Foundation.LNF} (hExt : SemanticCore.Extensional S) (v : SemanticCore.Var → S.carrier) (A : SemanticCore.Class) (s : S.carrier) : SemanticCore.Class.Holds S v (CompactSourceSyntax.synCcompl A) s ↔ ¬SemanticCore.Class.Holds S v A s

theorem NFChoice.Compiler.NFCompactLeafSemanticAdapters.holds_syn_cun {S : Fol.Structure Foundation.LNF} (hExt : SemanticCore.Extensional S) (v : SemanticCore.Var → S.carrier) (A B : SemanticCore.Class) (s : S.carrier) : SemanticCore.Class.Holds S v (CompactSourceSyntax.synCun A B) s ↔ SemanticCore.Class.Holds S v A s ∨ SemanticCore.Class.Holds S v B s

theorem NFChoice.Compiler.NFCompactLeafSemanticAdapters.holds_syn_cpr {S : Fol.Structure Foundation.LNF} (hExt : SemanticCore.Extensional S) (v : SemanticCore.Var → S.carrier) (A B : SemanticCore.Class) (s : S.carrier) : SemanticCore.Class.Holds S v (CompactSourceSyntax.synCpr A B) s ↔ (∀ (a : S.carrier), SemanticCore.Mem S a s ↔ SemanticCore.Class.Holds S v A a) ∨ ∀ (a : S.carrier), SemanticCore.Mem S a s ↔ SemanticCore.Class.Holds S v B a

theorem NFChoice.Compiler.NFCompactLeafSemanticAdapters.holds_syn_copk {S : Fol.Structure Foundation.LNF} (hExt : SemanticCore.Extensional S) (v : SemanticCore.Var → S.carrier) (A B : SemanticCore.Class) (p : S.carrier) : SemanticCore.Class.Holds S v (CompactSourceSyntax.synCopk A B) p ↔ (∀ (u : S.carrier), SemanticCore.Mem S u p ↔ ∀ (a : S.carrier), SemanticCore.Mem S a u ↔ SemanticCore.Class.Holds S v A a) ∨ ∀ (u : S.carrier), SemanticCore.Mem S u p ↔ (∀ (a : S.carrier), SemanticCore.Mem S a u ↔ SemanticCore.Class.Holds S v A a) ∨ ∀ (a : S.carrier), SemanticCore.Mem S a u ↔ SemanticCore.Class.Holds S v B a

The compact ordered-pair constructor, stated without unfolding its syntax DAG.

theorem NFChoice.Compiler.NFCompactLeafSemanticAdapters.formulaHolds_disj {S : Fol.Structure Foundation.LNF} {n : ℕ} {xs : DVec S.carrier n} {p q : Foundation.Formula n} : SemanticCore.Lowering.FormulaHolds S xs (p.disj q) ↔ SemanticCore.Lowering.FormulaHolds S xs p ∨ SemanticCore.Lowering.FormulaHolds S xs q

theorem NFChoice.Compiler.NFCompactLeafSemanticAdapters.formulaHolds_renameVars {S : Fol.Structure Foundation.LNF} {n m : ℕ} (rho : Fin n → Fin m) (ys : DVec S.carrier m) (xs : DVec S.carrier n) (p : Foundation.Formula n) (hlookup : ∀ (i : Fin n), SemanticCore.Lowering.lookup ys (rho i) = SemanticCore.Lowering.lookup xs i) : SemanticCore.Lowering.FormulaHolds S ys (Foundation.ExactLiteralTrial.Formula.renameVars rho p) ↔ SemanticCore.Lowering.FormulaHolds S xs p

Renaming a formula agrees with reindexing its bounded valuation.

theorem NFChoice.Compiler.NFCompactLeafSemanticAdapters.formulaHolds_liftClassPredicate {S : Fol.Structure Foundation.LNF} {n : ℕ} (xs : DVec S.carrier n) (candidate inserted : S.carrier) (p : Foundation.Formula (n + 1)) : SemanticCore.Lowering.FormulaHolds S (DVec.cons candidate (DVec.cons inserted xs)) (Foundation.ExactLiteralTrial.Formula.liftClassPredicate p) ↔ SemanticCore.Lowering.FormulaHolds S (DVec.cons candidate xs) p

liftClassPredicate merely inserts the represented set at index one.

theorem NFChoice.Compiler.NFCompactLeafSemanticAdapters.formulaHolds_eqCandidateToPredicate {S : Fol.Structure Foundation.LNF} {n : ℕ} (xs : DVec S.carrier n) (candidate : S.carrier) (p : Foundation.Formula (n + 1)) : SemanticCore.Lowering.FormulaHolds S (DVec.cons candidate xs) (Foundation.ExactLiteralTrial.Formula.eqCandidateToPredicate p) ↔ ∀ (a : S.carrier), SemanticCore.Mem S a candidate ↔ SemanticCore.Lowering.FormulaHolds S (DVec.cons a xs) p

def NFChoice.Compiler.NFCompactLeafSemanticAdapters.LiteralClassSem {S : Fol.Structure Foundation.LNF} {n : ℕ} (xs : DVec S.carrier n) : Foundation.ExactLiteralTrial.LiteralClass n → S.carrier → Prop

Direct model semantics of an exact literal class expression.

Equations

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

theorem NFChoice.Compiler.NFCompactLeafSemanticAdapters.formulaHolds_literalClass_membership {S : Fol.Structure Foundation.LNF} {n : ℕ} (xs : DVec S.carrier n) (A : Foundation.ExactLiteralTrial.LiteralClass n) (candidate : S.carrier) : SemanticCore.Lowering.FormulaHolds S (DVec.cons candidate xs) A.membership ↔ LiteralClassSem xs A candidate

The exact literal membership formula denotes LiteralClassSem.