Nominal proof certificates grouped in dependency order.

Certificates from NominalWPPReplayChunk015Compact001Part021.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHncardmono (A D : SemanticCore.Class) (hyp_hncardmono_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss D A)) (hyp_hncardmono_2 : Nominal.NPrf (SemanticCore.Wff.classMem D Compiler.CompactSourceSyntax.synCvv)) (hyp_hncardmono_3 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synChncard D) Compiler.CompactSourceSyntax.synClec (Compiler.CompactSourceSyntax.synChncard A))

Checked nominal proof certificate identified upstream as g_hncardmono.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHnwcutcodecnndv (x : SemanticCore.Var) (D R : SemanticCore.Class) (hyp_hnwcutcodecnndv_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCwe D)) : Nominal.NPrf ((SemanticCore.Wff.classMem (SemanticCore.Class.cv x) D).imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synChnwcutcode R D (SemanticCore.Class.cv x)) (Compiler.CompactSourceSyntax.synChwcn D)))

Checked nominal proof certificate identified upstream as g_hnwcutcodecnndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHnwcutcodecnclndv (B D R : SemanticCore.Class) (hyp_hnwcutcodecnclndv_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCwe D)) : Nominal.NPrf ((SemanticCore.Wff.classMem B D).imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synChnwcutcode R D B) (Compiler.CompactSourceSyntax.synChwcn D)))

Checked nominal proof certificate identified upstream as g_hnwcutcodecnclndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHnwcutrelfndv (D R : SemanticCore.Class) (hyp_hnwcutrelfndv_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCwe D)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWf (Compiler.CompactSourceSyntax.synChnwcutrel R D) (Compiler.CompactSourceSyntax.synCpw1 D) (Compiler.CompactSourceSyntax.synChwcn D))

Checked nominal proof certificate identified upstream as g_hnwcutrelfndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHnwcutsirelvalndv (D R : SemanticCore.Class) (q : SemanticCore.Var) (hyp_hnwcutsirelvalndv_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCwe D)) : Nominal.NPrf ((SemanticCore.Wff.classMem (SemanticCore.Class.cv q) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 D))).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCsi (Compiler.CompactSourceSyntax.synChnwcutrel R D)) (SemanticCore.Class.cv q)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synChnwcutcode R D (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv q)))))))

Checked nominal proof certificate identified upstream as g_hnwcutsirelvalndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHnwcutclassltnendv (x y : SemanticCore.Var) (D R : SemanticCore.Class) (hyp_hnwcutclassltnendv_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCwe D)) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv y) D) (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv y)))))).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCec (Compiler.CompactSourceSyntax.synChnwcutcode R D (SemanticCore.Class.cv x)) (Compiler.CompactSourceSyntax.synChwniso D)) (Compiler.CompactSourceSyntax.synCec (Compiler.CompactSourceSyntax.synChnwcutcode R D (SemanticCore.Class.cv y)) (Compiler.CompactSourceSyntax.synChwniso D))).neg)

Checked nominal proof certificate identified upstream as g_hnwcutclassltnendv.

Equations

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

Certificates from NominalWPPReplayChunk015Compact001Part022.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHnwcutclassinjndv (x y : SemanticCore.Var) (D R : SemanticCore.Class) (hyp_hnwcutclassinjndv_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCwe D)) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) D) (SemanticCore.Wff.classMem (SemanticCore.Class.cv y) D)).imp ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCec (Compiler.CompactSourceSyntax.synChnwcutcode R D (SemanticCore.Class.cv x)) (Compiler.CompactSourceSyntax.synChwniso D)) (Compiler.CompactSourceSyntax.synCec (Compiler.CompactSourceSyntax.synChnwcutcode R D (SemanticCore.Class.cv y)) (Compiler.CompactSourceSyntax.synChwniso D))).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv x) (SemanticCore.Class.cv y))))

Checked nominal proof certificate identified upstream as g_hnwcutclassinjndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHnwcutclassinjclndv (B C D R : SemanticCore.Class) (hyp_hnwcutclassinjclndv_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCwe D)) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem B D) (SemanticCore.Wff.classMem C D)).imp ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCec (Compiler.CompactSourceSyntax.synChnwcutcode R D B) (Compiler.CompactSourceSyntax.synChwniso D)) (Compiler.CompactSourceSyntax.synCec (Compiler.CompactSourceSyntax.synChnwcutcode R D C) (Compiler.CompactSourceSyntax.synChwniso D))).imp (SemanticCore.Wff.classEq B C)))

Checked nominal proof certificate identified upstream as g_hnwcutclassinjclndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gLnkereq (R S : SemanticCore.Class) : Nominal.NPrf ((SemanticCore.Wff.classEq R S).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synClnker R) (Compiler.CompactSourceSyntax.synClnker S)))

Checked nominal proof certificate identified upstream as g_lnkereq.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gLnanbi12ni (ph ps ch th : SemanticCore.Wff) (hyp_lnanbi12ni_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ph ps)) (hyp_lnanbi12ni_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ch th)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWa ph ch.neg) (Compiler.CompactSourceSyntax.synWa ps th.neg))

Checked nominal proof certificate identified upstream as g_lnanbi12ni.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gLndifopvalg (A B V W : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem A V) (SemanticCore.Wff.classMem B W)).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCo A Compiler.CompactSourceSyntax.synClndifop B) (Compiler.CompactSourceSyntax.synCdif A B)))

Checked nominal proof certificate identified upstream as g_lndifopvalg.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFnlndifop : Nominal.NPrf (Compiler.CompactSourceSyntax.synWfn Compiler.CompactSourceSyntax.synClndifop Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_fnlndifop.

Equations

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

Certificates from NominalWPPReplayChunk015Compact001Part023.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gLndifopex : Nominal.NPrf (SemanticCore.Wff.classMem Compiler.CompactSourceSyntax.synClndifop Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_lndifopex.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gLn1stfn : Nominal.NPrf (Compiler.CompactSourceSyntax.synWfn Compiler.CompactSourceSyntax.synC1st Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_ln1stfn.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gLn2ndfn : Nominal.NPrf (Compiler.CompactSourceSyntax.synWfn Compiler.CompactSourceSyntax.synC2nd Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_ln2ndfn.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gLnpwasymfnfn : Nominal.NPrf (Compiler.CompactSourceSyntax.synWfn Compiler.CompactSourceSyntax.synClnpwasymfn Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_lnpwasymfnfn.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gLnpwasymfnex : Nominal.NPrf (SemanticCore.Wff.classMem Compiler.CompactSourceSyntax.synClnpwasymfn Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_lnpwasymfnex.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gLnpwasymfnval (D R : SemanticCore.Class) (hyp_lnpwasymfnval_1 : Nominal.NPrf (SemanticCore.Wff.classMem R Compiler.CompactSourceSyntax.synCvv)) (hyp_lnpwasymfnval_2 : Nominal.NPrf (SemanticCore.Wff.classMem D Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synClnpwasymfn (Compiler.CompactSourceSyntax.synCop R D)) (Compiler.CompactSourceSyntax.synCdif R (Compiler.CompactSourceSyntax.synCcnv R)))

Checked nominal proof certificate identified upstream as g_lnpwasymfnval.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gTc3lecan (M N : SemanticCore.Class) (hyp_tc3lecb_1 : Nominal.NPrf (SemanticCore.Wff.classMem M Compiler.CompactSourceSyntax.synCncs)) (hyp_tc3lecb_2 : Nominal.NPrf (SemanticCore.Wff.classMem N Compiler.CompactSourceSyntax.synCncs)) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc M))) Compiler.CompactSourceSyntax.synClec (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc N)))).imp (Compiler.CompactSourceSyntax.synWbr M Compiler.CompactSourceSyntax.synClec N))

Checked nominal proof certificate identified upstream as g_tc3lecan.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFdifssa (A B R : SemanticCore.Class) (dv_A_B : Disjoint A.fv B.fv) (dv_A_R : Disjoint A.fv R.fv) (dv_B_R : Disjoint B.fv R.fv) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCfdif R A B) A)

Checked nominal proof certificate identified upstream as g_fdifssa.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFdordwe2 (A B R : SemanticCore.Class) (dv_A_B : Disjoint A.fv B.fv) (dv_A_R : Disjoint A.fv R.fv) (dv_B_R : Disjoint B.fv R.fv) (hyp_fdordwe2_1 : Nominal.NPrf (SemanticCore.Wff.classMem R Compiler.CompactSourceSyntax.synCvv)) (hyp_fdordwe2_2 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) (hyp_fdordwe2_3 : Nominal.NPrf (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCwe A).imp (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCfdord R A B) Compiler.CompactSourceSyntax.synCwe (Compiler.CompactSourceSyntax.synCfdif R A B)))

Checked nominal proof certificate identified upstream as g_fdordwe2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNcpw1pw2 (A : SemanticCore.Class) (hyp_ncpw1pw2_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCnc (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw (Compiler.CompactSourceSyntax.synCpw A)))) (Compiler.CompactSourceSyntax.synCnc (Compiler.CompactSourceSyntax.synCpw (Compiler.CompactSourceSyntax.synCpw (Compiler.CompactSourceSyntax.synCpw1 A)))))

Checked nominal proof certificate identified upstream as g_ncpw1pw2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gTc3nc (A : SemanticCore.Class) (hyp_tc3nc_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCnc A)))) (Compiler.CompactSourceSyntax.synCnc (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 A)))))

Checked nominal proof certificate identified upstream as g_tc3nc.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gKqlefintcb (M N : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem M Compiler.CompactSourceSyntax.synCnnc) (SemanticCore.Wff.classMem N Compiler.CompactSourceSyntax.synCnnc)).imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWbr M (Compiler.CompactSourceSyntax.synCkqrel Compiler.CompactSourceSyntax.synClefin) N) (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCtc M) (Compiler.CompactSourceSyntax.synCkqrel Compiler.CompactSourceSyntax.synClefin) (Compiler.CompactSourceSyntax.synCtc N))))

Checked nominal proof certificate identified upstream as g_kqlefintcb.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gTcnnresfn : Nominal.NPrf (Compiler.CompactSourceSyntax.synWfn (Compiler.CompactSourceSyntax.synCres Compiler.CompactSourceSyntax.synCtcfn (Compiler.CompactSourceSyntax.synCpw1 Compiler.CompactSourceSyntax.synCnnc)) (Compiler.CompactSourceSyntax.synCpw1 Compiler.CompactSourceSyntax.synCnnc))

Checked nominal proof certificate identified upstream as g_tcnnresfn.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gTcnnex : Nominal.NPrf (SemanticCore.Wff.classMem Compiler.CompactSourceSyntax.synCtcnn Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_tcnnex.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEltcnn (A : SemanticCore.Class) (q : SemanticCore.Var) (dv_A_q : q ∉ A.fv) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCtcnn) (Compiler.CompactSourceSyntax.synWrex q (Compiler.CompactSourceSyntax.synCpw1 Compiler.CompactSourceSyntax.synCnnc) (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCres Compiler.CompactSourceSyntax.synCtcfn (Compiler.CompactSourceSyntax.synCpw1 Compiler.CompactSourceSyntax.synCnnc)) (SemanticCore.Class.cv q)) A)))

Checked nominal proof certificate identified upstream as g_eltcnn.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gTcfnfvcl (B : SemanticCore.Class) : Nominal.NPrf ((SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synCtcfn (Compiler.CompactSourceSyntax.synCsn B)) (Compiler.CompactSourceSyntax.synCtc B)))

Checked nominal proof certificate identified upstream as g_tcfnfvcl.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gTcnnssnn : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss Compiler.CompactSourceSyntax.synCtcnn Compiler.CompactSourceSyntax.synCnnc)

Checked nominal proof certificate identified upstream as g_tcnnssnn.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNntcsuc (N : SemanticCore.Class) : Nominal.NPrf ((SemanticCore.Wff.classMem N Compiler.CompactSourceSyntax.synCnnc).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCplc N Compiler.CompactSourceSyntax.synC1c)) (Compiler.CompactSourceSyntax.synCplc (Compiler.CompactSourceSyntax.synCtc N) Compiler.CompactSourceSyntax.synC1c)))

Checked nominal proof certificate identified upstream as g_nntcsuc.

Equations

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

Certificates from NominalWPPReplayChunk015Compact001Part024.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNntctcnn (N : SemanticCore.Class) : Nominal.NPrf ((SemanticCore.Wff.classMem N Compiler.CompactSourceSyntax.synCnnc).imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCtc N) Compiler.CompactSourceSyntax.synCtcnn))

Checked nominal proof certificate identified upstream as g_nntctcnn.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gTcnnsuc (A : SemanticCore.Class) : Nominal.NPrf ((SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCtcnn).imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCplc A Compiler.CompactSourceSyntax.synC1c) Compiler.CompactSourceSyntax.synCtcnn))

Checked nominal proof certificate identified upstream as g_tcnnsuc.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNntcnn (N : SemanticCore.Class) : Nominal.NPrf ((SemanticCore.Wff.classMem N Compiler.CompactSourceSyntax.synCnnc).imp (SemanticCore.Wff.classMem N Compiler.CompactSourceSyntax.synCtcnn))

Checked nominal proof certificate identified upstream as g_nntcnn.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gTcnnfo : Nominal.NPrf (Compiler.CompactSourceSyntax.synWfo (Compiler.CompactSourceSyntax.synCres Compiler.CompactSourceSyntax.synCtcfn (Compiler.CompactSourceSyntax.synCpw1 Compiler.CompactSourceSyntax.synCnnc)) (Compiler.CompactSourceSyntax.synCpw1 Compiler.CompactSourceSyntax.synCnnc) Compiler.CompactSourceSyntax.synCnnc)

Checked nominal proof certificate identified upstream as g_tcnnfo.

Equations

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

Certificates from NominalWPPReplayChunk015Compact001Part025.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gTcnnf1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWf1 (Compiler.CompactSourceSyntax.synCres Compiler.CompactSourceSyntax.synCtcfn (Compiler.CompactSourceSyntax.synCpw1 Compiler.CompactSourceSyntax.synCnnc)) (Compiler.CompactSourceSyntax.synCpw1 Compiler.CompactSourceSyntax.synCnnc) Compiler.CompactSourceSyntax.synCnnc)

Checked nominal proof certificate identified upstream as g_tcnnf1.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gTcnnf1o : Nominal.NPrf (Compiler.CompactSourceSyntax.synWf1o (Compiler.CompactSourceSyntax.synCres Compiler.CompactSourceSyntax.synCtcfn (Compiler.CompactSourceSyntax.synCpw1 Compiler.CompactSourceSyntax.synCnnc)) (Compiler.CompactSourceSyntax.synCpw1 Compiler.CompactSourceSyntax.synCnnc) Compiler.CompactSourceSyntax.synCnnc)

Checked nominal proof certificate identified upstream as g_tcnnf1o.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNntcpreim (x : SemanticCore.Var) (P : SemanticCore.Class) (dv_P_x : x ∉ P.fv) : Nominal.NPrf ((SemanticCore.Wff.classMem P Compiler.CompactSourceSyntax.synCnnc).imp (Compiler.CompactSourceSyntax.synWrex x Compiler.CompactSourceSyntax.synCnnc (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCtc (SemanticCore.Class.cv x)) P)))

Checked nominal proof certificate identified upstream as g_nntcpreim.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gPwpullex (R F : SemanticCore.Class) (hyp_pwpullex_1 : Nominal.NPrf (SemanticCore.Wff.classMem F Compiler.CompactSourceSyntax.synCvv)) (hyp_pwpullex_2 : Nominal.NPrf (SemanticCore.Wff.classMem R Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCpwpull F R) Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_pwpullex.

Equations

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

Certificates from NominalWPPReplayChunk015Compact001Part026.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEllntpcndv (A D R : SemanticCore.Class) (_dv_A_R : Disjoint A.fv R.fv) (_dv_D_R : Disjoint D.fv R.fv) (hyp_ellntpcndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) (hyp_ellntpcndv_2 : Nominal.NPrf (SemanticCore.Wff.classMem R Compiler.CompactSourceSyntax.synCvv)) (hyp_ellntpcndv_3 : Nominal.NPrf (SemanticCore.Wff.classMem D Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCop R D) (Compiler.CompactSourceSyntax.synClntpc A)) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCref D) (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCtrans D)) (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCconnex D)) (Compiler.CompactSourceSyntax.synWss R (Compiler.CompactSourceSyntax.synCxp D D))) (SemanticCore.Wff.classEq D A)))

Checked nominal proof certificate identified upstream as g_ellntpcndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEllnpwcndv (A D R : SemanticCore.Class) (_dv_A_R : Disjoint A.fv R.fv) (_dv_D_R : Disjoint D.fv R.fv) (hyp_ellnpwcndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem R Compiler.CompactSourceSyntax.synCvv)) (hyp_ellnpwcndv_2 : Nominal.NPrf (SemanticCore.Wff.classMem D Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCop R D) (Compiler.CompactSourceSyntax.synClnpwc A)) (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCop R D) (Compiler.CompactSourceSyntax.synClntpc A)) (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCdif R (Compiler.CompactSourceSyntax.synCcnv R)) Compiler.CompactSourceSyntax.synCfound D)))

Checked nominal proof certificate identified upstream as g_ellnpwcndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gLnpwkerfnfn : Nominal.NPrf (Compiler.CompactSourceSyntax.synWfn Compiler.CompactSourceSyntax.synClnpwkerfn Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_lnpwkerfnfn.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gLnpwkerfnex : Nominal.NPrf (SemanticCore.Wff.classMem Compiler.CompactSourceSyntax.synClnpwkerfn Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_lnpwkerfnex.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gLnpwkerfnval (D R : SemanticCore.Class) (hyp_lnpwkerfnval_1 : Nominal.NPrf (SemanticCore.Wff.classMem R Compiler.CompactSourceSyntax.synCvv)) (hyp_lnpwkerfnval_2 : Nominal.NPrf (SemanticCore.Wff.classMem D Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synClnpwkerfn (Compiler.CompactSourceSyntax.synCop R D)) (Compiler.CompactSourceSyntax.synClnker R))

Checked nominal proof certificate identified upstream as g_lnpwkerfnval.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gLninteropfn : Nominal.NPrf (Compiler.CompactSourceSyntax.synWfn Compiler.CompactSourceSyntax.synClninterop Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_lninteropfn.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gLninteropex : Nominal.NPrf (SemanticCore.Wff.classMem Compiler.CompactSourceSyntax.synClninterop Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_lninteropex.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gLninteropval (A B : SemanticCore.Class) (hyp_lninteropval_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) (hyp_lninteropval_2 : Nominal.NPrf (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synClninterop (Compiler.CompactSourceSyntax.synCop A B)) (Compiler.CompactSourceSyntax.synCin A B))

Checked nominal proof certificate identified upstream as g_lninteropval.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gLnimagecrossfnval (B R : SemanticCore.Class) (hyp_lnimagecrossfnval_1 : Nominal.NPrf (SemanticCore.Wff.classMem R Compiler.CompactSourceSyntax.synCvv)) (hyp_lnimagecrossfnval_2 : Nominal.NPrf (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synClnimagecrossfn (Compiler.CompactSourceSyntax.synCop R B)) (Compiler.CompactSourceSyntax.synCxp B Compiler.CompactSourceSyntax.synCvv))

Checked nominal proof certificate identified upstream as g_lnimagecrossfnval.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gLnimageresfnfn : Nominal.NPrf (Compiler.CompactSourceSyntax.synWfn Compiler.CompactSourceSyntax.synClnimageresfn Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_lnimageresfnfn.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gLnimageresfnex : Nominal.NPrf (SemanticCore.Wff.classMem Compiler.CompactSourceSyntax.synClnimageresfn Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_lnimageresfnex.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gLnimageresfnval (B R : SemanticCore.Class) (hyp_lnimageresfnval_1 : Nominal.NPrf (SemanticCore.Wff.classMem R Compiler.CompactSourceSyntax.synCvv)) (hyp_lnimageresfnval_2 : Nominal.NPrf (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synClnimageresfn (Compiler.CompactSourceSyntax.synCop R B)) (Compiler.CompactSourceSyntax.synCres R B))

Checked nominal proof certificate identified upstream as g_lnimageresfnval.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gLnimageopfn : Nominal.NPrf (Compiler.CompactSourceSyntax.synWfn Compiler.CompactSourceSyntax.synClnimageop Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_lnimageopfn.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gLnimageopex : Nominal.NPrf (SemanticCore.Wff.classMem Compiler.CompactSourceSyntax.synClnimageop Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_lnimageopex.

Equations

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