Documentation

LeanPool.NFWeakPartition.NominalWPPReplayChunk010Compact001Part046

NF weak partition development: NominalWPPReplayChunk010Compact001Part046.

source
noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSetconslem6 (x y z : SemanticCore.Var) (A : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_A_y : y ∉ A.fv) (dv_A_z : z ∉ A.fv) (dv_x_y : x ≠ y) (dv_x_z : x ≠ z) (dv_y_z : y ≠ z) :
Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCimak (Compiler.CompactSourceSyntax.synCin (Compiler.CompactSourceSyntax.synCxpk Compiler.CompactSourceSyntax.synCvv (Compiler.CompactSourceSyntax.synCxpk Compiler.CompactSourceSyntax.synCvv Compiler.CompactSourceSyntax.synCvv)) (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCimak (Compiler.CompactSourceSyntax.synCsymdif (Compiler.CompactSourceSyntax.synCins3k (Compiler.CompactSourceSyntax.synCsik (Compiler.CompactSourceSyntax.synCsik Compiler.CompactSourceSyntax.synCssetk))) (Compiler.CompactSourceSyntax.synCins2k (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCins3k (Compiler.CompactSourceSyntax.synCcomk Compiler.CompactSourceSyntax.synCssetk (Compiler.CompactSourceSyntax.synCsik (Compiler.CompactSourceSyntax.synCcnvk (Compiler.CompactSourceSyntax.synCimagek (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCin (Compiler.CompactSourceSyntax.synCimagek (Compiler.CompactSourceSyntax.synCimak (Compiler.CompactSourceSyntax.synCdif (Compiler.CompactSourceSyntax.synCins3k (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCimak (Compiler.CompactSourceSyntax.synCin (Compiler.CompactSourceSyntax.synCins3k Compiler.CompactSourceSyntax.synCssetk) (Compiler.CompactSourceSyntax.synCins2k Compiler.CompactSourceSyntax.synCssetk)) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 Compiler.CompactSourceSyntax.synC1c))))) (Compiler.CompactSourceSyntax.synCimak (Compiler.CompactSourceSyntax.synCsymdif (Compiler.CompactSourceSyntax.synCins2k (Compiler.CompactSourceSyntax.synCins2k Compiler.CompactSourceSyntax.synCssetk)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCins2k (Compiler.CompactSourceSyntax.synCins3k Compiler.CompactSourceSyntax.synCssetk)) (Compiler.CompactSourceSyntax.synCins3k (Compiler.CompactSourceSyntax.synCsik (Compiler.CompactSourceSyntax.synCsik Compiler.CompactSourceSyntax.synCssetk))))) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 Compiler.CompactSourceSyntax.synC1c)))))) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 Compiler.CompactSourceSyntax.synC1c)))) (Compiler.CompactSourceSyntax.synCxpk Compiler.CompactSourceSyntax.synCnnc Compiler.CompactSourceSyntax.synCvv)) (Compiler.CompactSourceSyntax.synCin Compiler.CompactSourceSyntax.synCidk (Compiler.CompactSourceSyntax.synCxpk (Compiler.CompactSourceSyntax.synCcompl Compiler.CompactSourceSyntax.synCnnc) Compiler.CompactSourceSyntax.synCvv)))))))) (Compiler.CompactSourceSyntax.synCins2k (Compiler.CompactSourceSyntax.synCimak (Compiler.CompactSourceSyntax.synCin (Compiler.CompactSourceSyntax.synCins2k Compiler.CompactSourceSyntax.synCssetk) (Compiler.CompactSourceSyntax.synCins3k (Compiler.CompactSourceSyntax.synCsik (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCimak (Compiler.CompactSourceSyntax.synCsymdif (Compiler.CompactSourceSyntax.synCins2k Compiler.CompactSourceSyntax.synCssetk) (Compiler.CompactSourceSyntax.synCins3k (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCcomk (Compiler.CompactSourceSyntax.synCcnvk (Compiler.CompactSourceSyntax.synCimagek (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCin (Compiler.CompactSourceSyntax.synCimagek (Compiler.CompactSourceSyntax.synCimak (Compiler.CompactSourceSyntax.synCdif (Compiler.CompactSourceSyntax.synCins3k (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCimak (Compiler.CompactSourceSyntax.synCin (Compiler.CompactSourceSyntax.synCins3k Compiler.CompactSourceSyntax.synCssetk) (Compiler.CompactSourceSyntax.synCins2k Compiler.CompactSourceSyntax.synCssetk)) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 Compiler.CompactSourceSyntax.synC1c))))) (Compiler.CompactSourceSyntax.synCimak (Compiler.CompactSourceSyntax.synCsymdif (Compiler.CompactSourceSyntax.synCins2k (Compiler.CompactSourceSyntax.synCins2k Compiler.CompactSourceSyntax.synCssetk)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCins2k (Compiler.CompactSourceSyntax.synCins3k Compiler.CompactSourceSyntax.synCssetk)) (Compiler.CompactSourceSyntax.synCins3k (Compiler.CompactSourceSyntax.synCsik (Compiler.CompactSourceSyntax.synCsik Compiler.CompactSourceSyntax.synCssetk))))) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 Compiler.CompactSourceSyntax.synC1c)))))) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 Compiler.CompactSourceSyntax.synC1c)))) (Compiler.CompactSourceSyntax.synCxpk Compiler.CompactSourceSyntax.synCnnc Compiler.CompactSourceSyntax.synCvv)) (Compiler.CompactSourceSyntax.synCin Compiler.CompactSourceSyntax.synCidk (Compiler.CompactSourceSyntax.synCxpk (Compiler.CompactSourceSyntax.synCcompl Compiler.CompactSourceSyntax.synCnnc) Compiler.CompactSourceSyntax.synCvv))))) Compiler.CompactSourceSyntax.synCssetk) (Compiler.CompactSourceSyntax.synCxpk (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)) Compiler.CompactSourceSyntax.synCvv)))) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 Compiler.CompactSourceSyntax.synC1c))))))) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 Compiler.CompactSourceSyntax.synC1c))))))) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 Compiler.CompactSourceSyntax.synC1c))))))) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 A))) (SemanticCore.Class.cab z (Compiler.CompactSourceSyntax.synWex x (Compiler.CompactSourceSyntax.synWex y (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classEq (SemanticCore.Class.cv z) (Compiler.CompactSourceSyntax.synCopk (SemanticCore.Class.cv x) (SemanticCore.Class.cv y))) (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)) A))))))

Checked nominal proof certificate identified upstream as g_setconslem6.

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