Nominal proof certificates grouped in dependency order.

Certificates from NominalWPPReplayChunk013Compact001Part029.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gErth (ph : SemanticCore.Wff) (A B R V X : SemanticCore.Class) (hyp_erth_1 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCer Compiler.CompactSourceSyntax.synCvv))) (hyp_erth_2 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCdm R) X))) (hyp_erth_3 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classMem A X))) (hyp_erth_4 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classMem B V))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWbr A R B) (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCec A R) (Compiler.CompactSourceSyntax.synCec B R))))

Checked nominal proof certificate identified upstream as g_erth.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gErth2 (ph : SemanticCore.Wff) (A B R V X : SemanticCore.Class) (hyp_erth2_1 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCer Compiler.CompactSourceSyntax.synCvv))) (hyp_erth2_2 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCdm R) X))) (hyp_erth2_3 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classMem A V))) (hyp_erth2_4 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classMem B X))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWbr A R B) (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCec A R) (Compiler.CompactSourceSyntax.synCec B R))))

Checked nominal proof certificate identified upstream as g_erth2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gErthi (ph : SemanticCore.Wff) (A B R : SemanticCore.Class) (hyp_erthi_1 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCer Compiler.CompactSourceSyntax.synCvv))) (hyp_erthi_4 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWbr A R B))) : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCec A R) (Compiler.CompactSourceSyntax.synCec B R)))

Checked nominal proof certificate identified upstream as g_erthi.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gErdisj (A B R : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCer Compiler.CompactSourceSyntax.synCvv).imp (Compiler.CompactSourceSyntax.synWo (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCec A R) (Compiler.CompactSourceSyntax.synCec B R)) (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (Compiler.CompactSourceSyntax.synCec A R) (Compiler.CompactSourceSyntax.synCec B R)) Compiler.CompactSourceSyntax.synC0)))

Checked nominal proof certificate identified upstream as g_erdisj.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gQseq1 (A B C : SemanticCore.Class) : Nominal.NPrf ((SemanticCore.Wff.classEq A B).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCqs A C) (Compiler.CompactSourceSyntax.synCqs B C)))

Checked nominal proof certificate identified upstream as g_qseq1.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gQseq2 (A B C : SemanticCore.Class) : Nominal.NPrf ((SemanticCore.Wff.classEq A B).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCqs C A) (Compiler.CompactSourceSyntax.synCqs C B)))

Checked nominal proof certificate identified upstream as g_qseq2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gElqsg (x : SemanticCore.Var) (A B R V : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_B_x : x ∉ B.fv) (dv_R_x : x ∉ R.fv) : Nominal.NPrf ((SemanticCore.Wff.classMem B V).imp (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem B (Compiler.CompactSourceSyntax.synCqs A R)) (Compiler.CompactSourceSyntax.synWrex x A (SemanticCore.Wff.classEq B (Compiler.CompactSourceSyntax.synCec (SemanticCore.Class.cv x) R)))))

Checked nominal proof certificate identified upstream as g_elqsg.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gElqs (x : SemanticCore.Var) (A B R : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_B_x : x ∉ B.fv) (dv_R_x : x ∉ R.fv) (hyp_elqs_1 : Nominal.NPrf (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem B (Compiler.CompactSourceSyntax.synCqs A R)) (Compiler.CompactSourceSyntax.synWrex x A (SemanticCore.Wff.classEq B (Compiler.CompactSourceSyntax.synCec (SemanticCore.Class.cv x) R))))

Checked nominal proof certificate identified upstream as g_elqs.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gElqsi (x : SemanticCore.Var) (A B R : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_B_x : x ∉ B.fv) (dv_R_x : x ∉ R.fv) : Nominal.NPrf ((SemanticCore.Wff.classMem B (Compiler.CompactSourceSyntax.synCqs A R)).imp (Compiler.CompactSourceSyntax.synWrex x A (SemanticCore.Wff.classEq B (Compiler.CompactSourceSyntax.synCec (SemanticCore.Class.cv x) R))))

Checked nominal proof certificate identified upstream as g_elqsi.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEcelqsg (A B R V : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem R V) (SemanticCore.Wff.classMem B A)).imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCec B R) (Compiler.CompactSourceSyntax.synCqs A R)))

Checked nominal proof certificate identified upstream as g_ecelqsg.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEcelqsi (A B R : SemanticCore.Class) (hyp_ecelqsi_1 : Nominal.NPrf (SemanticCore.Wff.classMem R Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf ((SemanticCore.Wff.classMem B A).imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCec B R) (Compiler.CompactSourceSyntax.synCqs A R)))

Checked nominal proof certificate identified upstream as g_ecelqsi.

Equations

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

Certificates from NominalWPPReplayChunk013Compact001Part030.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gQsexg (A R V W : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem R V) (SemanticCore.Wff.classMem A W)).imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCqs A R) Compiler.CompactSourceSyntax.synCvv))

Checked nominal proof certificate identified upstream as g_qsexg.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gQsex (A R : SemanticCore.Class) (hyp_qsex_1 : Nominal.NPrf (SemanticCore.Wff.classMem R Compiler.CompactSourceSyntax.synCvv)) (hyp_qsex_2 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCqs A R) Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_qsex.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEctocld (ph ps ch : SemanticCore.Wff) (x : SemanticCore.Var) (A B R S : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_B_x : x ∉ B.fv) (dv_R_x : x ∉ R.fv) (dv_ch_x : x ∉ ch.fv) (dv_ps_x : x ∉ ps.fv) (hyp_ectocl_1 : Nominal.NPrf (SemanticCore.Wff.classEq S (Compiler.CompactSourceSyntax.synCqs B R))) (hyp_ectocl_2 : Nominal.NPrf ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCec (SemanticCore.Class.cv x) R) A).imp (Compiler.CompactSourceSyntax.synWb ph ps))) (hyp_ectocld_3 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa ch (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) B)).imp ph)) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa ch (SemanticCore.Wff.classMem A S)).imp ps)

Checked nominal proof certificate identified upstream as g_ectocld.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEctocl (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) (A B R S : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_B_x : x ∉ B.fv) (dv_R_x : x ∉ R.fv) (dv_ps_x : x ∉ ps.fv) (hyp_ectocl_1 : Nominal.NPrf (SemanticCore.Wff.classEq S (Compiler.CompactSourceSyntax.synCqs B R))) (hyp_ectocl_2 : Nominal.NPrf ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCec (SemanticCore.Class.cv x) R) A).imp (Compiler.CompactSourceSyntax.synWb ph ps))) (hyp_ectocl_3 : Nominal.NPrf ((SemanticCore.Wff.classMem (SemanticCore.Class.cv x) B).imp ph)) : Nominal.NPrf ((SemanticCore.Wff.classMem A S).imp ps)

Checked nominal proof certificate identified upstream as g_ectocl.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gElqsn0 (A B R : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCdm R) A) (SemanticCore.Wff.classMem B (Compiler.CompactSourceSyntax.synCqs A R))).imp (Compiler.CompactSourceSyntax.synWne B Compiler.CompactSourceSyntax.synC0))

Checked nominal proof certificate identified upstream as g_elqsn0.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gMapexi (A B : SemanticCore.Class) (f : SemanticCore.Var) (dv_A_f : f ∉ A.fv) (dv_B_f : f ∉ B.fv) (hyp_mapexi_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) (hyp_mapexi_2 : Nominal.NPrf (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (SemanticCore.Wff.classMem (SemanticCore.Class.cab f (Compiler.CompactSourceSyntax.synWf (SemanticCore.Class.cv f) A B)) Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_mapexi.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gMapex (A B C D : SemanticCore.Class) (f : SemanticCore.Var) (dv_A_f : f ∉ A.fv) (dv_B_f : f ∉ B.fv) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem A C) (SemanticCore.Wff.classMem B D)).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cab f (Compiler.CompactSourceSyntax.synWf (SemanticCore.Class.cv f) A B)) Compiler.CompactSourceSyntax.synCvv))

Checked nominal proof certificate identified upstream as g_mapex.

Equations

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

Certificates from NominalWPPReplayChunk013Compact001Part031.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gMapvalg (A B C D : SemanticCore.Class) (f : SemanticCore.Var) (dv_A_f : f ∉ A.fv) (dv_B_f : f ∉ B.fv) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem A C) (SemanticCore.Wff.classMem B D)).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCo A Compiler.CompactSourceSyntax.synCmap B) (SemanticCore.Class.cab f (Compiler.CompactSourceSyntax.synWf (SemanticCore.Class.cv f) B A))))

Checked nominal proof certificate identified upstream as g_mapvalg.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gElmapg (A B C V W X : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synW3a (SemanticCore.Wff.classMem A V) (SemanticCore.Wff.classMem B W) (SemanticCore.Wff.classMem C X)).imp (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem C (Compiler.CompactSourceSyntax.synCo A Compiler.CompactSourceSyntax.synCmap B)) (Compiler.CompactSourceSyntax.synWf C B A)))

Checked nominal proof certificate identified upstream as g_elmapg.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gElmapi (A B C : SemanticCore.Class) : Nominal.NPrf ((SemanticCore.Wff.classMem A (Compiler.CompactSourceSyntax.synCo B Compiler.CompactSourceSyntax.synCmap C)).imp (Compiler.CompactSourceSyntax.synWf A C B))

Checked nominal proof certificate identified upstream as g_elmapi.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gBren (A B : SemanticCore.Class) (f : SemanticCore.Var) (dv_A_f : f ∉ A.fv) (dv_B_f : f ∉ B.fv) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWbr A Compiler.CompactSourceSyntax.synCen B) (Compiler.CompactSourceSyntax.synWex f (Compiler.CompactSourceSyntax.synWf1o (SemanticCore.Class.cv f) A B)))

Checked nominal proof certificate identified upstream as g_bren.

Equations

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

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

Checked nominal proof certificate identified upstream as g_enex.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gF1oeng (A B C F : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem F C) (Compiler.CompactSourceSyntax.synWf1o F A B)).imp (Compiler.CompactSourceSyntax.synWbr A Compiler.CompactSourceSyntax.synCen B))

Checked nominal proof certificate identified upstream as g_f1oeng.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gF1oen (A B F : SemanticCore.Class) (hyp_f1oen_1 : Nominal.NPrf (SemanticCore.Wff.classMem F Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWf1o F A B).imp (Compiler.CompactSourceSyntax.synWbr A Compiler.CompactSourceSyntax.synCen B))

Checked nominal proof certificate identified upstream as g_f1oen.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEnrflxg (A V : SemanticCore.Class) : Nominal.NPrf ((SemanticCore.Wff.classMem A V).imp (Compiler.CompactSourceSyntax.synWbr A Compiler.CompactSourceSyntax.synCen A))

Checked nominal proof certificate identified upstream as g_enrflxg.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEnrflx (A : SemanticCore.Class) (hyp_enrflx_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr A Compiler.CompactSourceSyntax.synCen A)

Checked nominal proof certificate identified upstream as g_enrflx.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEnsymi (A B : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWbr A Compiler.CompactSourceSyntax.synCen B).imp (Compiler.CompactSourceSyntax.synWbr B Compiler.CompactSourceSyntax.synCen A))

Checked nominal proof certificate identified upstream as g_ensymi.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEnsym (A B : SemanticCore.Class) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWbr A Compiler.CompactSourceSyntax.synCen B) (Compiler.CompactSourceSyntax.synWbr B Compiler.CompactSourceSyntax.synCen A))

Checked nominal proof certificate identified upstream as g_ensym.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEntr (A B C : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr A Compiler.CompactSourceSyntax.synCen B) (Compiler.CompactSourceSyntax.synWbr B Compiler.CompactSourceSyntax.synCen C)).imp (Compiler.CompactSourceSyntax.synWbr A Compiler.CompactSourceSyntax.synCen C))

Checked nominal proof certificate identified upstream as g_entr.

Equations

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

Certificates from NominalWPPReplayChunk013Compact001Part032.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEner : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr Compiler.CompactSourceSyntax.synCen Compiler.CompactSourceSyntax.synCer Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_ener.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gIdssen : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss Compiler.CompactSourceSyntax.synCid Compiler.CompactSourceSyntax.synCen)

Checked nominal proof certificate identified upstream as g_idssen.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gDmen : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCdm Compiler.CompactSourceSyntax.synCen) Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_dmen.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEn0 (A : SemanticCore.Class) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWbr A Compiler.CompactSourceSyntax.synCen Compiler.CompactSourceSyntax.synC0) (SemanticCore.Wff.classEq A Compiler.CompactSourceSyntax.synC0))

Checked nominal proof certificate identified upstream as g_en0.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFundmen (F : SemanticCore.Class) (hyp_fundmen_1 : Nominal.NPrf (SemanticCore.Wff.classMem F Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWfun F).imp (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCdm F) Compiler.CompactSourceSyntax.synCen F))

Checked nominal proof certificate identified upstream as g_fundmen.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEn2sn (A B C D : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem A C) (SemanticCore.Wff.classMem B D)).imp (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCsn A) Compiler.CompactSourceSyntax.synCen (Compiler.CompactSourceSyntax.synCsn B)))

Checked nominal proof certificate identified upstream as g_en2sn.

Equations

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

Certificates from NominalWPPReplayChunk013Compact001Part033.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gUnen (A B C D : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr A Compiler.CompactSourceSyntax.synCen B) (Compiler.CompactSourceSyntax.synWbr C Compiler.CompactSourceSyntax.synCen D)) (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin A C) Compiler.CompactSourceSyntax.synC0) (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin B D) Compiler.CompactSourceSyntax.synC0))).imp (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCun A C) Compiler.CompactSourceSyntax.synCen (Compiler.CompactSourceSyntax.synCun B D)))

Checked nominal proof certificate identified upstream as g_unen.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gXpsnen (A B : SemanticCore.Class) (hyp_xpsnen_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) (hyp_xpsnen_2 : Nominal.NPrf (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCxp A (Compiler.CompactSourceSyntax.synCsn B)) Compiler.CompactSourceSyntax.synCen A)

Checked nominal proof certificate identified upstream as g_xpsnen.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gXpcomen (A B : SemanticCore.Class) (hyp_xpcomen_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) (hyp_xpcomen_2 : Nominal.NPrf (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCxp A B) Compiler.CompactSourceSyntax.synCen (Compiler.CompactSourceSyntax.synCxp B A))

Checked nominal proof certificate identified upstream as g_xpcomen.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gXpen (A B C D : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr A Compiler.CompactSourceSyntax.synCen B) (Compiler.CompactSourceSyntax.synWbr C Compiler.CompactSourceSyntax.synCen D)).imp (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCxp A C) Compiler.CompactSourceSyntax.synCen (Compiler.CompactSourceSyntax.synCxp B D)))

Checked nominal proof certificate identified upstream as g_xpen.

Equations

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