Documentation

LeanPool.NFWeakPartition.Certificates.NominalWPPReplayChunk017Compact001Block017

Nominal proof certificates grouped in dependency order.

Certificates from NominalWPPReplayChunk017Compact001Part071.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHnwcutcodecmpbrndv (x y u : SemanticCore.Var) (A : SemanticCore.Class) (dv_A_u : u ∉ A.fv) (dv_u_x : u ≠ x) (dv_u_y : u ≠ y) :

Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv) (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwcn A)) (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u))) (SemanticCore.Wff.classMem (SemanticCore.Class.cv y) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)))))).imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synChnwcutcode (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC1st (SemanticCore.Class.cv u)) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)) (SemanticCore.Class.cv x)) (Compiler.CompactSourceSyntax.synChncodecmpset A) (Compiler.CompactSourceSyntax.synChnwcutcode (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC1st (SemanticCore.Class.cv u)) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)) (SemanticCore.Class.cv y))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv x) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC1st (SemanticCore.Class.cv u)) (SemanticCore.Class.cv y))))

Checked nominal proof certificate identified upstream as g_hnwcutcodecmpbrndv.

Equations

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

Instances For

Certificates from NominalWPPReplayChunk017Compact001Part072.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHnwcutcodecmpbrclndv (u : SemanticCore.Var) (A B C : SemanticCore.Class) (dv_A_u : u ∉ A.fv) :

Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv) (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwcn A)) (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem B (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u))) (SemanticCore.Wff.classMem C (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)))))).imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synChnwcutcode (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC1st (SemanticCore.Class.cv u)) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)) B) (Compiler.CompactSourceSyntax.synChncodecmpset A) (Compiler.CompactSourceSyntax.synChnwcutcode (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC1st (SemanticCore.Class.cv u)) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)) C)) (Compiler.CompactSourceSyntax.synWbr B (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC1st (SemanticCore.Class.cv u)) C)))

Checked nominal proof certificate identified upstream as g_hnwcutcodecmpbrclndv.

Equations

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

Instances For

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gPw12si2brndv (D R : SemanticCore.Class) (q p : SemanticCore.Var) (dv_R_p : p ∉ R.fv) :

Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv p) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 D))) (SemanticCore.Wff.classMem (SemanticCore.Class.cv q) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 D)))).imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv p) (Compiler.CompactSourceSyntax.synCsi (Compiler.CompactSourceSyntax.synCsi R)) (SemanticCore.Class.cv q)) (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv p))) R (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv q))))))

Checked nominal proof certificate identified upstream as g_pw12si2brndv.

Equations

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

Instances For

Certificates from NominalWPPReplayChunk017Compact001Part073.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gIsostrictsegresclndv (B D R S E H : SemanticCore.Class) :

Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWiso H R S D E) (SemanticCore.Wff.classMem B D)).imp (Compiler.CompactSourceSyntax.synWiso (Compiler.CompactSourceSyntax.synCres H (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn B)))) (Compiler.CompactSourceSyntax.synCin R (Compiler.CompactSourceSyntax.synCxp (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn B))) (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn B))))) (Compiler.CompactSourceSyntax.synCin S (Compiler.CompactSourceSyntax.synCxp (Compiler.CompactSourceSyntax.synCin E (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif S Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCfv H B)))) (Compiler.CompactSourceSyntax.synCin E (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif S Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCfv H B)))))) (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn B))) (Compiler.CompactSourceSyntax.synCin E (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif S Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCfv H B))))))

Checked nominal proof certificate identified upstream as g_isostrictsegresclndv.

Equations

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

Instances For

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHnsiquomappreexclndv (x : SemanticCore.Var) (A B : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_B_x : x ∉ B.fv) (hyp_hnsiquomappreexclndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) :

Nominal.NPrf ((SemanticCore.Wff.classMem B (Compiler.CompactSourceSyntax.synChnord (Compiler.CompactSourceSyntax.synCpw1 A))).imp (Compiler.CompactSourceSyntax.synWrex x (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synChnord A)) (SemanticCore.Wff.classEq B (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChnsiquomap A) (SemanticCore.Class.cv x)))))

Checked nominal proof certificate identified upstream as g_hnsiquomappreexclndv.

Equations

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

Instances For

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHnsiquomaprepvalcl2ndv (A C : SemanticCore.Class) (q : SemanticCore.Var) (dv_A_q : q ∉ A.fv) (hyp_hnsiquomaprepvalcl2ndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) :

Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv q) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synChnord A))) (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem C (Compiler.CompactSourceSyntax.synChwcn A)) (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv q)) (Compiler.CompactSourceSyntax.synCec C (Compiler.CompactSourceSyntax.synChwniso A))))).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChnsiquomap A) (SemanticCore.Class.cv q)) (Compiler.CompactSourceSyntax.synCec (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChnsicodemap A) (Compiler.CompactSourceSyntax.synCsn C)) (Compiler.CompactSourceSyntax.synChwniso (Compiler.CompactSourceSyntax.synCpw1 A)))))

Checked nominal proof certificate identified upstream as g_hnsiquomaprepvalcl2ndv.

Equations

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

Instances For