NF weak partition development: NFCompactLeafEndpoints.

theorem NFChoice.Compiler.NFCompactLeafEndpoints.formulaHolds_setEqClass {S : Fol.Structure Foundation.LNF} {n : ℕ} (xs : DVec S.carrier n) (r : Fin n) (A : Foundation.ExactLiteralTrial.LiteralClass n) : SemanticCore.Lowering.FormulaHolds S xs (Foundation.ExactLiteralTrial.LiteralClass.setEqClass r A) ↔ ∀ (z : S.carrier), SemanticCore.Mem S z (SemanticCore.Lowering.lookup xs r) ↔ NFCompactLeafSemanticAdapters.LiteralClassSem xs A z

theorem NFChoice.Compiler.NFCompactLeafEndpoints.formulaHolds_classMemSet {S : Fol.Structure Foundation.LNF} {n : ℕ} (xs : DVec S.carrier n) (A : Foundation.ExactLiteralTrial.LiteralClass n) (r : Fin n) : SemanticCore.Lowering.FormulaHolds S xs (A.classMemSet r) ↔ ∃ (p : S.carrier), (∀ (z : S.carrier), SemanticCore.Mem S z p ↔ NFCompactLeafSemanticAdapters.LiteralClassSem xs A z) ∧ SemanticCore.Mem S p (SemanticCore.Lowering.lookup xs r)

theorem NFChoice.Compiler.NFCompactLeafEndpoints.holds_syn_csn_literal {S : Fol.Structure Foundation.LNF} {n : ℕ} (v : SemanticCore.Var → S.carrier) (xs : DVec S.carrier n) (A : SemanticCore.Class) (LA : Foundation.ExactLiteralTrial.LiteralClass n) (hA : ∀ (a : S.carrier), SemanticCore.Class.Holds S v A a ↔ NFCompactLeafSemanticAdapters.LiteralClassSem xs LA a) (s : S.carrier) : SemanticCore.Class.Holds S v (CompactSourceSyntax.synCsn A) s ↔ NFCompactLeafSemanticAdapters.LiteralClassSem xs LA.singleton s

theorem NFChoice.Compiler.NFCompactLeafEndpoints.holds_syn_cpr_literal {S : Fol.Structure Foundation.LNF} {n : ℕ} (hExt : SemanticCore.Extensional S) (v : SemanticCore.Var → S.carrier) (xs : DVec S.carrier n) (A B : SemanticCore.Class) (LA LB : Foundation.ExactLiteralTrial.LiteralClass n) (hA : ∀ (a : S.carrier), SemanticCore.Class.Holds S v A a ↔ NFCompactLeafSemanticAdapters.LiteralClassSem xs LA a) (hB : ∀ (a : S.carrier), SemanticCore.Class.Holds S v B a ↔ NFCompactLeafSemanticAdapters.LiteralClassSem xs LB a) (p : S.carrier) : SemanticCore.Class.Holds S v (CompactSourceSyntax.synCpr A B) p ↔ NFCompactLeafSemanticAdapters.LiteralClassSem xs (LA.unorderedPair LB) p

theorem NFChoice.Compiler.NFCompactLeafEndpoints.holds_syn_copk_literal {S : Fol.Structure Foundation.LNF} {n : ℕ} (hExt : SemanticCore.Extensional S) (v : SemanticCore.Var → S.carrier) (xs : DVec S.carrier n) (A B : SemanticCore.Class) (LA LB : Foundation.ExactLiteralTrial.LiteralClass n) (hA : ∀ (a : S.carrier), SemanticCore.Class.Holds S v A a ↔ NFCompactLeafSemanticAdapters.LiteralClassSem xs LA a) (hB : ∀ (a : S.carrier), SemanticCore.Class.Holds S v B a ↔ NFCompactLeafSemanticAdapters.LiteralClassSem xs LB a) (p : S.carrier) : SemanticCore.Class.Holds S v (CompactSourceSyntax.synCopk A B) p ↔ NFCompactLeafSemanticAdapters.LiteralClassSem xs (LA.kPair LB) p

theorem NFChoice.Compiler.NFCompactLeafEndpoints.holds_classEq_cv_literal {S : Fol.Structure Foundation.LNF} {n : ℕ} (v : SemanticCore.Var → S.carrier) (xs : DVec S.carrier n) (x : SemanticCore.Var) (r : Fin n) (A : SemanticCore.Class) (LA : Foundation.ExactLiteralTrial.LiteralClass n) (hx : v x = SemanticCore.Lowering.lookup xs r) (hA : ∀ (a : S.carrier), SemanticCore.Class.Holds S v A a ↔ NFCompactLeafSemanticAdapters.LiteralClassSem xs LA a) : SemanticCore.Wff.Holds S v (SemanticCore.Wff.classEq (SemanticCore.Class.cv x) A) ↔ SemanticCore.Lowering.FormulaHolds S xs (Foundation.ExactLiteralTrial.LiteralClass.setEqClass r LA)

theorem NFChoice.Compiler.NFCompactLeafEndpoints.holds_classMem_cv_literal {S : Fol.Structure Foundation.LNF} {n : ℕ} (v : SemanticCore.Var → S.carrier) (xs : DVec S.carrier n) (x : SemanticCore.Var) (r : Fin n) (A : SemanticCore.Class) (LA : Foundation.ExactLiteralTrial.LiteralClass n) (hx : v x = SemanticCore.Lowering.lookup xs r) (hA : ∀ (a : S.carrier), SemanticCore.Class.Holds S v A a ↔ NFCompactLeafSemanticAdapters.LiteralClassSem xs LA a) : SemanticCore.Wff.Holds S v (SemanticCore.Wff.classMem A (SemanticCore.Class.cv x)) ↔ SemanticCore.Lowering.FormulaHolds S xs (LA.classMemSet r)

theorem NFChoice.Compiler.NFCompactLeafEndpoints.holds_literalKPair {S : Fol.Structure Foundation.LNF} {n : ℕ} (hExt : SemanticCore.Extensional S) (v : SemanticCore.Var → S.carrier) (xs : DVec S.carrier n) (z w t : SemanticCore.Var) (iz iw it : Fin n) (hz : v z = SemanticCore.Lowering.lookup xs iz) (hw : v w = SemanticCore.Lowering.lookup xs iw) (ht : v t = SemanticCore.Lowering.lookup xs it) : SemanticCore.Wff.Holds S v (SemanticCore.Wff.classEq (SemanticCore.Class.cv z) (CompactSourceSyntax.synCopk (SemanticCore.Class.cv w) (SemanticCore.Class.cv t))) ↔ SemanticCore.Lowering.FormulaHolds S xs (Foundation.ExactLiteralTrial.literalKPair iz iw it)

theorem NFChoice.Compiler.NFCompactLeafEndpoints.holds_literalPairMem {S : Fol.Structure Foundation.LNF} {n : ℕ} (hExt : SemanticCore.Extensional S) (v : SemanticCore.Var → S.carrier) (xs : DVec S.carrier n) (a b r : SemanticCore.Var) (ia ib ir : Fin n) (ha : v a = SemanticCore.Lowering.lookup xs ia) (hb : v b = SemanticCore.Lowering.lookup xs ib) (hr : v r = SemanticCore.Lowering.lookup xs ir) : SemanticCore.Wff.Holds S v (SemanticCore.Wff.classMem (CompactSourceSyntax.synCopk (SemanticCore.Class.cv a) (SemanticCore.Class.cv b)) (SemanticCore.Class.cv r)) ↔ SemanticCore.Lowering.FormulaHolds S xs (Foundation.ExactLiteralTrial.literalPairMem ia ib ir)

theorem NFChoice.Compiler.NFCompactLeafEndpoints.holds_literalSingletonPairMem {S : Fol.Structure Foundation.LNF} {n : ℕ} (hExt : SemanticCore.Extensional S) (v : SemanticCore.Var → S.carrier) (xs : DVec S.carrier n) (a b r : SemanticCore.Var) (ia ib ir : Fin n) (ha : v a = SemanticCore.Lowering.lookup xs ia) (hb : v b = SemanticCore.Lowering.lookup xs ib) (hr : v r = SemanticCore.Lowering.lookup xs ir) : SemanticCore.Wff.Holds S v (SemanticCore.Wff.classMem (CompactSourceSyntax.synCopk (CompactSourceSyntax.synCsn (SemanticCore.Class.cv a)) (CompactSourceSyntax.synCsn (SemanticCore.Class.cv b))) (SemanticCore.Class.cv r)) ↔ SemanticCore.Lowering.FormulaHolds S xs (Foundation.ExactLiteralTrial.literalSingletonPairMem ia ib ir)

theorem NFChoice.Compiler.NFCompactLeafEndpoints.holds_literalInsertedPairMem {S : Fol.Structure Foundation.LNF} {n : ℕ} (hExt : SemanticCore.Extensional S) (v : SemanticCore.Var → S.carrier) (xs : DVec S.carrier n) (z w t r : SemanticCore.Var) (iz iw it ir : Fin n) (hz : v z = SemanticCore.Lowering.lookup xs iz) (hw : v w = SemanticCore.Lowering.lookup xs iw) (ht : v t = SemanticCore.Lowering.lookup xs it) (hr : v r = SemanticCore.Lowering.lookup xs ir) : SemanticCore.Wff.Holds S v (SemanticCore.Wff.classMem (CompactSourceSyntax.synCopk (CompactSourceSyntax.synCsn (CompactSourceSyntax.synCsn (SemanticCore.Class.cv z))) (CompactSourceSyntax.synCopk (SemanticCore.Class.cv w) (SemanticCore.Class.cv t))) (SemanticCore.Class.cv r)) ↔ SemanticCore.Lowering.FormulaHolds S xs (Foundation.ExactLiteralTrial.literalInsertedPairMem iz iw it ir)

theorem NFChoice.Compiler.NFCompactLeafEndpoints.holds_literalPairSingletonSecondMem {S : Fol.Structure Foundation.LNF} {n : ℕ} (hExt : SemanticCore.Extensional S) (v : SemanticCore.Var → S.carrier) (xs : DVec S.carrier n) (a z r : SemanticCore.Var) (ia iz ir : Fin n) (ha : v a = SemanticCore.Lowering.lookup xs ia) (hz : v z = SemanticCore.Lowering.lookup xs iz) (hr : v r = SemanticCore.Lowering.lookup xs ir) : SemanticCore.Wff.Holds S v (SemanticCore.Wff.classMem (CompactSourceSyntax.synCopk (SemanticCore.Class.cv a) (CompactSourceSyntax.synCsn (SemanticCore.Class.cv z))) (SemanticCore.Class.cv r)) ↔ SemanticCore.Lowering.FormulaHolds S xs (Foundation.ExactLiteralTrial.literalPairSingletonSecondMem ia iz ir)