Documentation

LeanPool.NFWeakPartition.NFCompactLeafFinalGate

NF weak partition development: NFCompactLeafFinalGate.

theorem NFChoice.Compiler.NFCompactLeafFinalGate.holds_xp_rhs {S : Fol.Structure Foundation.LNF} (hExt : SemanticCore.Extensional S) (v : SemanticCore.Var → S.carrier) (x y z w t : SemanticCore.Var) (hxw : x ≠ w) (hxt : x ≠ t) (_hyw : y ≠ w) (_hyt : y ≠ t) (hzw : z ≠ w) (hzt : z ≠ t) (hwt : w ≠ t) :

SemanticCore.Wff.Holds S v (CompactSourceSyntax.synWex w (CompactSourceSyntax.synWex t (CompactSourceSyntax.synWa (SemanticCore.Wff.classEq (SemanticCore.Class.cv z) (CompactSourceSyntax.synCopk (SemanticCore.Class.cv w) (SemanticCore.Class.cv t))) (SemanticCore.Wff.objMem t x)))) ↔ SemanticCore.Lowering.FormulaHolds S (DVec.cons (v z) (DVec.cons (v y) (DVec.cons (v x) DVec.nil))) ((Foundation.ExactLiteralTrial.literalKPair 2 1 0).conj (Foundation.Formula.mem 0 4)).ex.ex

theorem NFChoice.Compiler.NFCompactLeafFinalGate.axXpCompact {S : Fol.Structure Foundation.LNF} (hNF : Fol.allRealizeSentence S Foundation.ExactLiteralTrial.LiteralHailperinNF) (x y z w t : SemanticCore.Var) (hxy : x ≠ y) (hxz : x ≠ z) (hxw : x ≠ w) (hxt : x ≠ t) (hyz : y ≠ z) (hyw : y ≠ w) (hyt : y ≠ t) (hzw : z ≠ w) (hzt : z ≠ t) (hwt : w ≠ t) :

SemanticCore.Wff.Valid S (CompactSourceSyntax.synWex y (SemanticCore.Wff.all z (CompactSourceSyntax.synWb (SemanticCore.Wff.objMem z y) (CompactSourceSyntax.synWex w (CompactSourceSyntax.synWex t (CompactSourceSyntax.synWa (SemanticCore.Wff.classEq (SemanticCore.Class.cv z) (CompactSourceSyntax.synCopk (SemanticCore.Class.cv w) (SemanticCore.Class.cv t))) (SemanticCore.Wff.objMem t x)))))))

theorem NFChoice.Compiler.NFCompactLeafFinalGate.axCnvCompact {S : Fol.Structure Foundation.LNF} (hNF : Fol.allRealizeSentence S Foundation.ExactLiteralTrial.LiteralHailperinNF) (x y z w : SemanticCore.Var) (hxy : x ≠ y) (hxz : x ≠ z) (hxw : x ≠ w) (hyz : y ≠ z) (hyw : y ≠ w) (hzw : z ≠ w) :

SemanticCore.Wff.Valid S (CompactSourceSyntax.synWex y (SemanticCore.Wff.all z (SemanticCore.Wff.all w (CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (CompactSourceSyntax.synCopk (SemanticCore.Class.cv z) (SemanticCore.Class.cv w)) (SemanticCore.Class.cv y)) (SemanticCore.Wff.classMem (CompactSourceSyntax.synCopk (SemanticCore.Class.cv w) (SemanticCore.Class.cv z)) (SemanticCore.Class.cv x))))))

theorem NFChoice.Compiler.NFCompactLeafFinalGate.holds_literalSubset {S : Fol.Structure Foundation.LNF} {n : ℕ} (v : SemanticCore.Var → S.carrier) (xs : DVec S.carrier n) (y z w : SemanticCore.Var) (iy iz : Fin n) (hy : v y = SemanticCore.Lowering.lookup xs iy) (hz : v z = SemanticCore.Lowering.lookup xs iz) (hyw : y ≠ w) (hzw : z ≠ w) :

SemanticCore.Wff.Holds S v (SemanticCore.Wff.all w ((SemanticCore.Wff.objMem w y).imp (SemanticCore.Wff.objMem w z))) ↔ SemanticCore.Lowering.FormulaHolds S xs (Foundation.Formula.subset iy iz)

theorem NFChoice.Compiler.NFCompactLeafFinalGate.axSsetCompact {S : Fol.Structure Foundation.LNF} (hNF : Fol.allRealizeSentence S Foundation.ExactLiteralTrial.LiteralHailperinNF) (x y z w : SemanticCore.Var) (hxy : x ≠ y) (hxz : x ≠ z) (_hxw : x ≠ w) (hyz : y ≠ z) (hyw : y ≠ w) (hzw : z ≠ w) :

SemanticCore.Wff.Valid S (CompactSourceSyntax.synWex x (SemanticCore.Wff.all y (SemanticCore.Wff.all z (CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (CompactSourceSyntax.synCopk (SemanticCore.Class.cv y) (SemanticCore.Class.cv z)) (SemanticCore.Class.cv x)) (SemanticCore.Wff.all w ((SemanticCore.Wff.objMem w y).imp (SemanticCore.Wff.objMem w z)))))))

theorem NFChoice.Compiler.NFCompactLeafFinalGate.axSiCompact {S : Fol.Structure Foundation.LNF} (hNF : Fol.allRealizeSentence S Foundation.ExactLiteralTrial.LiteralHailperinNF) (x y z w : SemanticCore.Var) (hxy : x ≠ y) (hxz : x ≠ z) (hxw : x ≠ w) (hyz : y ≠ z) (hyw : y ≠ w) (hzw : z ≠ w) :

SemanticCore.Wff.Valid S (CompactSourceSyntax.synWex y (SemanticCore.Wff.all z (SemanticCore.Wff.all w (CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (CompactSourceSyntax.synCopk (CompactSourceSyntax.synCsn (SemanticCore.Class.cv z)) (CompactSourceSyntax.synCsn (SemanticCore.Class.cv w))) (SemanticCore.Class.cv y)) (SemanticCore.Wff.classMem (CompactSourceSyntax.synCopk (SemanticCore.Class.cv z) (SemanticCore.Class.cv w)) (SemanticCore.Class.cv x))))))

theorem NFChoice.Compiler.NFCompactLeafFinalGate.axIns2Compact {S : Fol.Structure Foundation.LNF} (hNF : Fol.allRealizeSentence S Foundation.ExactLiteralTrial.LiteralHailperinNF) (x y z w t : SemanticCore.Var) (hxy : x ≠ y) (hxz : x ≠ z) (hxw : x ≠ w) (hxt : x ≠ t) (hyz : y ≠ z) (hyw : y ≠ w) (hyt : y ≠ t) (hzw : z ≠ w) (hzt : z ≠ t) (hwt : w ≠ t) :

theorem NFChoice.Compiler.NFCompactLeafFinalGate.axIns3Compact {S : Fol.Structure Foundation.LNF} (hNF : Fol.allRealizeSentence S Foundation.ExactLiteralTrial.LiteralHailperinNF) (x y z w t : SemanticCore.Var) (hxy : x ≠ y) (hxz : x ≠ z) (hxw : x ≠ w) (hxt : x ≠ t) (hyz : y ≠ z) (hyw : y ≠ w) (hyt : y ≠ t) (hzw : z ≠ w) (hzt : z ≠ t) (hwt : w ≠ t) :

theorem NFChoice.Compiler.NFCompactLeafFinalGate.holds_typlower_rhs {S : Fol.Structure Foundation.LNF} (hExt : SemanticCore.Extensional S) (v : SemanticCore.Var → S.carrier) (x y z w : SemanticCore.Var) (hxw : x ≠ w) (hzw : z ≠ w) :

SemanticCore.Wff.Holds S v (SemanticCore.Wff.all w (SemanticCore.Wff.classMem (CompactSourceSyntax.synCopk (SemanticCore.Class.cv w) (CompactSourceSyntax.synCsn (SemanticCore.Class.cv z))) (SemanticCore.Class.cv x))) ↔ SemanticCore.Lowering.FormulaHolds S (DVec.cons (v z) (DVec.cons (v y) (DVec.cons (v x) DVec.nil))) (Foundation.ExactLiteralTrial.literalPairSingletonSecondMem 0 1 3).all

theorem NFChoice.Compiler.NFCompactLeafFinalGate.axTypeLowerCompact {S : Fol.Structure Foundation.LNF} (hNF : Fol.allRealizeSentence S Foundation.ExactLiteralTrial.LiteralHailperinNF) (x y z w : SemanticCore.Var) (hxy : x ≠ y) (hxz : x ≠ z) (hxw : x ≠ w) (hyz : y ≠ z) (_hyw : y ≠ w) (hzw : z ≠ w) :

SemanticCore.Wff.Valid S (CompactSourceSyntax.synWex y (SemanticCore.Wff.all z (CompactSourceSyntax.synWb (SemanticCore.Wff.objMem z y) (SemanticCore.Wff.all w (SemanticCore.Wff.classMem (CompactSourceSyntax.synCopk (SemanticCore.Class.cv w) (CompactSourceSyntax.synCsn (SemanticCore.Class.cv z))) (SemanticCore.Class.cv x))))))