Nominal proof certificates grouped in dependency order.

Certificates from NominalWPPReplayChunk016Compact001Part021.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWecutisogenfixedfwd (x y : SemanticCore.Var) (D R S : SemanticCore.Class) (f : SemanticCore.Var) (E : SemanticCore.Class) (dv_D_f : f ∉ D.fv) (_dv_D_x : x ∉ D.fv) (dv_E_f : f ∉ E.fv) (_dv_E_y : y ∉ E.fv) (dv_R_f : f ∉ R.fv) (_dv_R_x : x ∉ R.fv) (dv_S_f : f ∉ S.fv) (_dv_S_y : y ∉ S.fv) (dv_f_x : f ≠ x) (dv_f_y : f ≠ y) (hyp_wecutisogenfixedfwd_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCwe D)) (hyp_wecutisogenfixedfwd_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr S Compiler.CompactSourceSyntax.synCwe E)) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) D) (SemanticCore.Wff.classMem (SemanticCore.Class.cv y) E)) (Compiler.CompactSourceSyntax.synWiso (SemanticCore.Class.cv f) (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 (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 x)))))) (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 (SemanticCore.Class.cv y)))) (Compiler.CompactSourceSyntax.synCin E (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif S Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv y)))))) (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv x)))) (Compiler.CompactSourceSyntax.synCin E (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif S Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv y)))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv f) (Compiler.CompactSourceSyntax.synCwecutisogen R D S E)))

Checked nominal proof certificate identified upstream as g_wecutisogenfixedfwd.

Equations

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

Certificates from NominalWPPReplayChunk016Compact001Part022.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWecutisossgen (D R S E : SemanticCore.Class) (hyp_wecutisossgen_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCwe D)) (hyp_wecutisossgen_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr S Compiler.CompactSourceSyntax.synCwe E)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCwecutiso R D S E) (Compiler.CompactSourceSyntax.synCwecutisogen R D S E))

Checked nominal proof certificate identified upstream as g_wecutisossgen.

Equations

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

Certificates from NominalWPPReplayChunk016Compact001Part023.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWecutisogensswecutiso (D R S E : SemanticCore.Class) (hyp_wecutisogensswecutiso_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCwe D)) (hyp_wecutisogensswecutiso_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr S Compiler.CompactSourceSyntax.synCwe E)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCwecutisogen R D S E) (Compiler.CompactSourceSyntax.synCwecutiso R D S E))

Checked nominal proof certificate identified upstream as g_wecutisogensswecutiso.

Equations

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

Certificates from NominalWPPReplayChunk016Compact001Part024.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWecutisogeneq (D R S E : SemanticCore.Class) (hyp_wecutisogeneq_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCwe D)) (hyp_wecutisogeneq_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr S Compiler.CompactSourceSyntax.synCwe E)) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCwecutiso R D S E) (Compiler.CompactSourceSyntax.synCwecutisogen R D S E))

Checked nominal proof certificate identified upstream as g_wecutisogeneq.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWecutisogenex (D R S E : SemanticCore.Class) (hyp_wecutisogenex_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCwe D)) (hyp_wecutisogenex_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr S Compiler.CompactSourceSyntax.synCwe E)) : Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCwecutisogen R D S E) Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_wecutisogenex.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWecutisoex (D R S E : SemanticCore.Class) (hyp_wecutisoex_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCwe D)) (hyp_wecutisoex_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr S Compiler.CompactSourceSyntax.synCwe E)) : Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCwecutiso R D S E) Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_wecutisoex.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWecutisouniex (D R S E : SemanticCore.Class) (hyp_wecutisouniex_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCwe D)) (hyp_wecutisouniex_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr S Compiler.CompactSourceSyntax.synCwe E)) : Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCwecutiso R D S E)) Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_wecutisouniex.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWecutcardfnfn (D R : SemanticCore.Class) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWfn (Compiler.CompactSourceSyntax.synCwecutcardfn R D) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 D)))

Checked nominal proof certificate identified upstream as g_wecutcardfnfn.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWecutcardfactorex (D R : SemanticCore.Class) (hyp_wecutcardfactorex_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCwe D)) : Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCwecutcardfactor R D) Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_wecutcardfactorex.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWecutcardfactorfn (D R : SemanticCore.Class) (hyp_wecutcardfactorfn_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCwe D)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWfn (Compiler.CompactSourceSyntax.synCwecutcardfactor R D) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 D)))

Checked nominal proof certificate identified upstream as g_wecutcardfactorfn.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWecutcardhrelfn (D R : SemanticCore.Class) (hyp_wecutcardhrelfn_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCwe D)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWfn (Compiler.CompactSourceSyntax.synChnwcutrel R D) (Compiler.CompactSourceSyntax.synCpw1 D))

Checked nominal proof certificate identified upstream as g_wecutcardhrelfn.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWecutcardinnerf (D R : SemanticCore.Class) (hyp_wecutcardinnerf_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCwe D)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWf (Compiler.CompactSourceSyntax.synCcom Compiler.CompactSourceSyntax.synC2nd (Compiler.CompactSourceSyntax.synChnwcutrel R D)) (Compiler.CompactSourceSyntax.synCpw1 D) Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_wecutcardinnerf.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWecutcardsiliftfn (D R : SemanticCore.Class) (hyp_wecutcardsiliftfn_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCwe D)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWfn (Compiler.CompactSourceSyntax.synCsi (Compiler.CompactSourceSyntax.synCcom Compiler.CompactSourceSyntax.synC2nd (Compiler.CompactSourceSyntax.synChnwcutrel R D))) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 D)))

Checked nominal proof certificate identified upstream as g_wecutcardsiliftfn.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWecutcardfactorval (D R : SemanticCore.Class) (q : SemanticCore.Var) (_dv_D_q : q ∉ D.fv) (_dv_R_q : q ∉ R.fv) (hyp_wecutcardfactorval_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.synCwecutcardfactor R D) (SemanticCore.Class.cv q)) (Compiler.CompactSourceSyntax.synCnc (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv q)))))))))

Checked nominal proof certificate identified upstream as g_wecutcardfactorval.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWecutcardfnval (D R : SemanticCore.Class) (q : SemanticCore.Var) (_dv_D_q : q ∉ D.fv) (_dv_R_q : q ∉ R.fv) : 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.synCwecutcardfn R D) (SemanticCore.Class.cv q)) (Compiler.CompactSourceSyntax.synCnc (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv q)))))))))

Checked nominal proof certificate identified upstream as g_wecutcardfnval.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWecutcardfnfactor (D R : SemanticCore.Class) (hyp_wecutcardfnfactor_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCwe D)) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCwecutcardfn R D) (Compiler.CompactSourceSyntax.synCwecutcardfactor R D))

Checked nominal proof certificate identified upstream as g_wecutcardfnfactor.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWecutcardfnex (D R : SemanticCore.Class) (hyp_wecutcardfnex_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCwe D)) : Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCwecutcardfn R D) Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_wecutcardfnex.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWecutcardpreimandv (D R K : SemanticCore.Class) (q : SemanticCore.Var) (dv_D_q : q ∉ D.fv) (dv_R_q : q ∉ R.fv) : Nominal.NPrf ((SemanticCore.Wff.classMem (SemanticCore.Class.cv q) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 D))).imp (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (SemanticCore.Class.cv q) (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCwecutcardfn R D)) K)) (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCnc (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv q))))))) K)))

Checked nominal proof certificate identified upstream as g_wecutcardpreimandv.

Equations

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

Certificates from NominalWPPReplayChunk016Compact001Part025.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSiorndv (D R : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCwe D).imp (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCsi R) Compiler.CompactSourceSyntax.synCstrict (Compiler.CompactSourceSyntax.synCpw1 D)))

Checked nominal proof certificate identified upstream as g_siorndv.

Equations

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