Nominal proof certificates grouped in dependency order.

Certificates from NominalWPPReplayChunk010Compact001Part039.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gUnopab (ph ps : SemanticCore.Wff) (x y : SemanticCore.Var) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCopab x y ph) (Compiler.CompactSourceSyntax.synCopab x y ps)) (Compiler.CompactSourceSyntax.synCopab x y (Compiler.CompactSourceSyntax.synWo ph ps)))

Checked nominal proof certificate identified upstream as g_unopab.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gBreq (A B R S : SemanticCore.Class) : Nominal.NPrf ((SemanticCore.Wff.classEq R S).imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWbr A R B) (Compiler.CompactSourceSyntax.synWbr A S B)))

Checked nominal proof certificate identified upstream as g_breq.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gBreq1 (A B C R : SemanticCore.Class) : Nominal.NPrf ((SemanticCore.Wff.classEq A B).imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWbr A R C) (Compiler.CompactSourceSyntax.synWbr B R C)))

Checked nominal proof certificate identified upstream as g_breq1.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gBreq2 (A B C R : SemanticCore.Class) : Nominal.NPrf ((SemanticCore.Wff.classEq A B).imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWbr C R A) (Compiler.CompactSourceSyntax.synWbr C R B)))

Checked nominal proof certificate identified upstream as g_breq2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gBreq12 (A B C D R : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classEq A B) (SemanticCore.Wff.classEq C D)).imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWbr A R C) (Compiler.CompactSourceSyntax.synWbr B R D)))

Checked nominal proof certificate identified upstream as g_breq12.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gBreqi (A B R S : SemanticCore.Class) (hyp_breqi_1 : Nominal.NPrf (SemanticCore.Wff.classEq R S)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWbr A R B) (Compiler.CompactSourceSyntax.synWbr A S B))

Checked nominal proof certificate identified upstream as g_breqi.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gBreqi A B R S hyp_breqi_1 = NFChoice.DirectNominalPrf.Nominal.mp hyp_breqi_1 (NFChoice.DirectNominalPrf.WPPReplay.gBreq A B R S)

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gBreq1i (A B C R : SemanticCore.Class) (hyp_breq1i_1 : Nominal.NPrf (SemanticCore.Wff.classEq A B)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWbr A R C) (Compiler.CompactSourceSyntax.synWbr B R C))

Checked nominal proof certificate identified upstream as g_breq1i.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gBreq1i A B C R hyp_breq1i_1 = NFChoice.DirectNominalPrf.Nominal.mp hyp_breq1i_1 (NFChoice.DirectNominalPrf.WPPReplay.gBreq1 A B C R)

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gBreq2i (A B C R : SemanticCore.Class) (hyp_breq1i_1 : Nominal.NPrf (SemanticCore.Wff.classEq A B)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWbr C R A) (Compiler.CompactSourceSyntax.synWbr C R B))

Checked nominal proof certificate identified upstream as g_breq2i.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gBreq2i A B C R hyp_breq1i_1 = NFChoice.DirectNominalPrf.Nominal.mp hyp_breq1i_1 (NFChoice.DirectNominalPrf.WPPReplay.gBreq2 A B C R)

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gBreq12i (A B C D R : SemanticCore.Class) (hyp_breq1i_1 : Nominal.NPrf (SemanticCore.Wff.classEq A B)) (hyp_breq12i_2 : Nominal.NPrf (SemanticCore.Wff.classEq C D)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWbr A R C) (Compiler.CompactSourceSyntax.synWbr B R D))

Checked nominal proof certificate identified upstream as g_breq12i.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gBreq1d (ph : SemanticCore.Wff) (A B C R : SemanticCore.Class) (hyp_breq1d_1 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq A B))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWbr A R C) (Compiler.CompactSourceSyntax.synWbr B R C)))

Checked nominal proof certificate identified upstream as g_breq1d.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gBreqd (ph : SemanticCore.Wff) (A B C D : SemanticCore.Class) (hyp_breq1d_1 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq A B))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWbr C A D) (Compiler.CompactSourceSyntax.synWbr C B D)))

Checked nominal proof certificate identified upstream as g_breqd.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gBreq2d (ph : SemanticCore.Wff) (A B C R : SemanticCore.Class) (hyp_breq1d_1 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq A B))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWbr C R A) (Compiler.CompactSourceSyntax.synWbr C R B)))

Checked nominal proof certificate identified upstream as g_breq2d.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gBreq12d (ph : SemanticCore.Wff) (A B C D R : SemanticCore.Class) (hyp_breq1d_1 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq A B))) (hyp_breq12d_2 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq C D))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWbr A R C) (Compiler.CompactSourceSyntax.synWbr B R D)))

Checked nominal proof certificate identified upstream as g_breq12d.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gBreqan12d (ph ps : SemanticCore.Wff) (A B C D R : SemanticCore.Class) (hyp_breq1d_1 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq A B))) (hyp_breqan12i_2 : Nominal.NPrf (ps.imp (SemanticCore.Wff.classEq C D))) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa ph ps).imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWbr A R C) (Compiler.CompactSourceSyntax.synWbr B R D)))

Checked nominal proof certificate identified upstream as g_breqan12d.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEqbrtri (A B C R : SemanticCore.Class) (hyp_eqbrtr_1 : Nominal.NPrf (SemanticCore.Wff.classEq A B)) (hyp_eqbrtr_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr B R C)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr A R C)

Checked nominal proof certificate identified upstream as g_eqbrtri.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEqbrtrd (ph : SemanticCore.Wff) (A B C R : SemanticCore.Class) (hyp_eqbrtrd_1 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq A B))) (hyp_eqbrtrd_2 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWbr B R C))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWbr A R C))

Checked nominal proof certificate identified upstream as g_eqbrtrd.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEqbrtrri (A B C R : SemanticCore.Class) (hyp_eqbrtrr_1 : Nominal.NPrf (SemanticCore.Wff.classEq A B)) (hyp_eqbrtrr_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr A R C)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr B R C)

Checked nominal proof certificate identified upstream as g_eqbrtrri.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEqbrtrrd (ph : SemanticCore.Wff) (A B C R : SemanticCore.Class) (hyp_eqbrtrrd_1 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq A B))) (hyp_eqbrtrrd_2 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWbr A R C))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWbr B R C))

Checked nominal proof certificate identified upstream as g_eqbrtrrd.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gBreqtri (A B C R : SemanticCore.Class) (hyp_breqtr_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr A R B)) (hyp_breqtr_2 : Nominal.NPrf (SemanticCore.Wff.classEq B C)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr A R C)

Checked nominal proof certificate identified upstream as g_breqtri.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gBreqtrd (ph : SemanticCore.Wff) (A B C R : SemanticCore.Class) (hyp_breqtrd_1 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWbr A R B))) (hyp_breqtrd_2 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq B C))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWbr A R C))

Checked nominal proof certificate identified upstream as g_breqtrd.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gBreqtrri (A B C R : SemanticCore.Class) (hyp_breqtrr_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr A R B)) (hyp_breqtrr_2 : Nominal.NPrf (SemanticCore.Wff.classEq C B)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr A R C)

Checked nominal proof certificate identified upstream as g_breqtrri.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gBreqtrrd (ph : SemanticCore.Wff) (A B C R : SemanticCore.Class) (hyp_breqtrrd_1 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWbr A R B))) (hyp_breqtrrd_2 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq C B))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWbr A R C))

Checked nominal proof certificate identified upstream as g_breqtrrd.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gN3brtr3i (A B C D R : SemanticCore.Class) (hyp_n_3brtr3_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr A R B)) (hyp_n_3brtr3_2 : Nominal.NPrf (SemanticCore.Wff.classEq A C)) (hyp_n_3brtr3_3 : Nominal.NPrf (SemanticCore.Wff.classEq B D)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr C R D)

Checked nominal proof certificate identified upstream as g_n_3brtr3i.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gN3brtr4d (ph : SemanticCore.Wff) (A B C D R : SemanticCore.Class) (hyp_n_3brtr4d_1 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWbr A R B))) (hyp_n_3brtr4d_2 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq C A))) (hyp_n_3brtr4d_3 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq D B))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWbr C R D))

Checked nominal proof certificate identified upstream as g_n_3brtr4d.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gN3brtr3g (ph : SemanticCore.Wff) (A B C D R : SemanticCore.Class) (hyp_n_3brtr3g_1 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWbr A R B))) (hyp_n_3brtr3g_2 : Nominal.NPrf (SemanticCore.Wff.classEq A C)) (hyp_n_3brtr3g_3 : Nominal.NPrf (SemanticCore.Wff.classEq B D)) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWbr C R D))

Checked nominal proof certificate identified upstream as g_n_3brtr3g.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSyl5eqbrr (ph : SemanticCore.Wff) (A B C R : SemanticCore.Class) (hyp_syl5eqbrr_1 : Nominal.NPrf (SemanticCore.Wff.classEq B A)) (hyp_syl5eqbrr_2 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWbr B R C))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWbr A R C))

Checked nominal proof certificate identified upstream as g_syl5eqbrr.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSyl5breq (ph : SemanticCore.Wff) (A B C R : SemanticCore.Class) (hyp_syl5breq_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr A R B)) (hyp_syl5breq_2 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq B C))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWbr A R C))

Checked nominal proof certificate identified upstream as g_syl5breq.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSyl6eqbr (ph : SemanticCore.Wff) (A B C R : SemanticCore.Class) (hyp_syl6eqbr_1 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq A B))) (hyp_syl6eqbr_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr B R C)) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWbr A R C))

Checked nominal proof certificate identified upstream as g_syl6eqbr.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSsbrd (ph : SemanticCore.Wff) (A B C D : SemanticCore.Class) (hyp_ssbrd_1 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWss A B))) : Nominal.NPrf (ph.imp ((Compiler.CompactSourceSyntax.synWbr C A D).imp (Compiler.CompactSourceSyntax.synWbr C B D)))

Checked nominal proof certificate identified upstream as g_ssbrd.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSsbri (A B C D : SemanticCore.Class) (hyp_ssbri_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss A B)) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWbr C A D).imp (Compiler.CompactSourceSyntax.synWbr C B D))

Checked nominal proof certificate identified upstream as g_ssbri.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNfbrd (ph : SemanticCore.Wff) (x : SemanticCore.Var) (A B R : SemanticCore.Class) (hyp_nfbrd_2 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWnfc x A))) (hyp_nfbrd_3 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWnfc x R))) (hyp_nfbrd_4 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWnfc x B))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWnf x (Compiler.CompactSourceSyntax.synWbr A R B)))

Checked nominal proof certificate identified upstream as g_nfbrd.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNfbr (x : SemanticCore.Var) (A B R : SemanticCore.Class) (hyp_nfbr_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnfc x A)) (hyp_nfbr_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnfc x R)) (hyp_nfbr_3 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnfc x B)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf x (Compiler.CompactSourceSyntax.synWbr A R B))

Checked nominal proof certificate identified upstream as g_nfbr.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gBrex (A B R : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWbr A R B).imp (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv) (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv)))

Checked nominal proof certificate identified upstream as g_brex.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gBrreldmex (A B R : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWbr A R B).imp (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv))

Checked nominal proof certificate identified upstream as g_brreldmex.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gBrrelrnex (A B R : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWbr A R B).imp (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv))

Checked nominal proof certificate identified upstream as g_brrelrnex.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gBrun (A B R S : SemanticCore.Class) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWbr A (Compiler.CompactSourceSyntax.synCun R S) B) (Compiler.CompactSourceSyntax.synWo (Compiler.CompactSourceSyntax.synWbr A R B) (Compiler.CompactSourceSyntax.synWbr A S B)))

Checked nominal proof certificate identified upstream as g_brun.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gBrin (A B R S : SemanticCore.Class) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWbr A (Compiler.CompactSourceSyntax.synCin R S) B) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr A R B) (Compiler.CompactSourceSyntax.synWbr A S B)))

Checked nominal proof certificate identified upstream as g_brin.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gBrdif (A B R S : SemanticCore.Class) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWbr A (Compiler.CompactSourceSyntax.synCdif R S) B) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr A R B) (Compiler.CompactSourceSyntax.synWbr A S B).neg))

Checked nominal proof certificate identified upstream as g_brdif.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gOpabid (ph : SemanticCore.Wff) (x y : SemanticCore.Var) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)) (Compiler.CompactSourceSyntax.synCopab x y ph)) ph)

Checked nominal proof certificate identified upstream as g_opabid.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gElopab (ph : SemanticCore.Wff) (x y : SemanticCore.Var) (A : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_A_y : y ∉ A.fv) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem A (Compiler.CompactSourceSyntax.synCopab x y ph)) (Compiler.CompactSourceSyntax.synWex x (Compiler.CompactSourceSyntax.synWex y (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classEq A (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv x) (SemanticCore.Class.cv y))) ph))))

Checked nominal proof certificate identified upstream as g_elopab.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gOpelopabsb (ph : SemanticCore.Wff) (x y : SemanticCore.Var) (A B : SemanticCore.Class) (dv_B_x : x ∉ B.fv) (dv_x_y : x ≠ y) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCop A B) (Compiler.CompactSourceSyntax.synCopab x y ph)) (Compiler.CompactSourceSyntax.synWsbc A x (Compiler.CompactSourceSyntax.synWsbc B y ph)))

Checked nominal proof certificate identified upstream as g_opelopabsb.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gOpelopabga (ph ps : SemanticCore.Wff) (x y : SemanticCore.Var) (A B V W : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_A_y : y ∉ A.fv) (dv_B_x : x ∉ B.fv) (dv_B_y : y ∉ B.fv) (dv_ps_x : x ∉ ps.fv) (dv_ps_y : y ∉ ps.fv) (dv_x_y : x ≠ y) (hyp_opelopabga_1 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classEq (SemanticCore.Class.cv x) A) (SemanticCore.Wff.classEq (SemanticCore.Class.cv y) B)).imp (Compiler.CompactSourceSyntax.synWb ph ps))) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem A V) (SemanticCore.Wff.classMem B W)).imp (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCop A B) (Compiler.CompactSourceSyntax.synCopab x y ph)) ps))

Checked nominal proof certificate identified upstream as g_opelopabga.

Equations

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

Certificates from NominalWPPReplayChunk010Compact001Part040.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gBrabga (ph ps : SemanticCore.Wff) (x y : SemanticCore.Var) (A B R V W : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_A_y : y ∉ A.fv) (dv_B_x : x ∉ B.fv) (dv_B_y : y ∉ B.fv) (dv_ps_x : x ∉ ps.fv) (dv_ps_y : y ∉ ps.fv) (dv_x_y : x ≠ y) (hyp_opelopabga_1 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classEq (SemanticCore.Class.cv x) A) (SemanticCore.Wff.classEq (SemanticCore.Class.cv y) B)).imp (Compiler.CompactSourceSyntax.synWb ph ps))) (hyp_brabga_2 : Nominal.NPrf (SemanticCore.Wff.classEq R (Compiler.CompactSourceSyntax.synCopab x y ph))) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem A V) (SemanticCore.Wff.classMem B W)).imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWbr A R B) ps))

Checked nominal proof certificate identified upstream as g_brabga.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gOpelopaba (ph ps : SemanticCore.Wff) (x y : SemanticCore.Var) (A B : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_A_y : y ∉ A.fv) (dv_B_x : x ∉ B.fv) (dv_B_y : y ∉ B.fv) (dv_ps_x : x ∉ ps.fv) (dv_ps_y : y ∉ ps.fv) (dv_x_y : x ≠ y) (hyp_opelopaba_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) (hyp_opelopaba_2 : Nominal.NPrf (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv)) (hyp_opelopaba_3 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classEq (SemanticCore.Class.cv x) A) (SemanticCore.Wff.classEq (SemanticCore.Class.cv y) B)).imp (Compiler.CompactSourceSyntax.synWb ph ps))) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCop A B) (Compiler.CompactSourceSyntax.synCopab x y ph)) ps)

Checked nominal proof certificate identified upstream as g_opelopaba.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gBraba (ph ps : SemanticCore.Wff) (x y : SemanticCore.Var) (A B R : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_A_y : y ∉ A.fv) (dv_B_x : x ∉ B.fv) (dv_B_y : y ∉ B.fv) (dv_ps_x : x ∉ ps.fv) (dv_ps_y : y ∉ ps.fv) (dv_x_y : x ≠ y) (hyp_opelopaba_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) (hyp_opelopaba_2 : Nominal.NPrf (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv)) (hyp_opelopaba_3 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classEq (SemanticCore.Class.cv x) A) (SemanticCore.Wff.classEq (SemanticCore.Class.cv y) B)).imp (Compiler.CompactSourceSyntax.synWb ph ps))) (hyp_braba_4 : Nominal.NPrf (SemanticCore.Wff.classEq R (Compiler.CompactSourceSyntax.synCopab x y ph))) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWbr A R B) ps)

Checked nominal proof certificate identified upstream as g_braba.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gOpelopabg (ph ps ch : SemanticCore.Wff) (x y : SemanticCore.Var) (A B V W : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_A_y : y ∉ A.fv) (dv_B_x : x ∉ B.fv) (dv_B_y : y ∉ B.fv) (dv_ch_x : x ∉ ch.fv) (dv_ch_y : y ∉ ch.fv) (dv_x_y : x ≠ y) (hyp_opelopabg_1 : Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv x) A).imp (Compiler.CompactSourceSyntax.synWb ph ps))) (hyp_opelopabg_2 : Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv y) B).imp (Compiler.CompactSourceSyntax.synWb ps ch))) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem A V) (SemanticCore.Wff.classMem B W)).imp (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCop A B) (Compiler.CompactSourceSyntax.synCopab x y ph)) ch))

Checked nominal proof certificate identified upstream as g_opelopabg.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gBrabg (ph ps ch : SemanticCore.Wff) (x y : SemanticCore.Var) (A B C D R : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_A_y : y ∉ A.fv) (dv_B_x : x ∉ B.fv) (dv_B_y : y ∉ B.fv) (dv_ch_x : x ∉ ch.fv) (dv_ch_y : y ∉ ch.fv) (dv_x_y : x ≠ y) (hyp_opelopabg_1 : Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv x) A).imp (Compiler.CompactSourceSyntax.synWb ph ps))) (hyp_opelopabg_2 : Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv y) B).imp (Compiler.CompactSourceSyntax.synWb ps ch))) (hyp_brabg_5 : Nominal.NPrf (SemanticCore.Wff.classEq R (Compiler.CompactSourceSyntax.synCopab x y ph))) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem A C) (SemanticCore.Wff.classMem B D)).imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWbr A R B) ch))

Checked nominal proof certificate identified upstream as g_brabg.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gOpelopab (ph ps ch : SemanticCore.Wff) (x y : SemanticCore.Var) (A B : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_A_y : y ∉ A.fv) (dv_B_x : x ∉ B.fv) (dv_B_y : y ∉ B.fv) (dv_ch_x : x ∉ ch.fv) (dv_ch_y : y ∉ ch.fv) (dv_x_y : x ≠ y) (hyp_opelopab_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) (hyp_opelopab_2 : Nominal.NPrf (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv)) (hyp_opelopab_3 : Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv x) A).imp (Compiler.CompactSourceSyntax.synWb ph ps))) (hyp_opelopab_4 : Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv y) B).imp (Compiler.CompactSourceSyntax.synWb ps ch))) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCop A B) (Compiler.CompactSourceSyntax.synCopab x y ph)) ch)

Checked nominal proof certificate identified upstream as g_opelopab.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gBrab (ph ps ch : SemanticCore.Wff) (x y : SemanticCore.Var) (A B R : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_A_y : y ∉ A.fv) (dv_B_x : x ∉ B.fv) (dv_B_y : y ∉ B.fv) (dv_ch_x : x ∉ ch.fv) (dv_ch_y : y ∉ ch.fv) (dv_x_y : x ≠ y) (hyp_opelopab_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) (hyp_opelopab_2 : Nominal.NPrf (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv)) (hyp_opelopab_3 : Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv x) A).imp (Compiler.CompactSourceSyntax.synWb ph ps))) (hyp_opelopab_4 : Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv y) B).imp (Compiler.CompactSourceSyntax.synWb ps ch))) (hyp_brab_5 : Nominal.NPrf (SemanticCore.Wff.classEq R (Compiler.CompactSourceSyntax.synCopab x y ph))) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWbr A R B) ch)

Checked nominal proof certificate identified upstream as g_brab.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSsopab2 (ph ps : SemanticCore.Wff) (x y : SemanticCore.Var) : Nominal.NPrf ((SemanticCore.Wff.all x (SemanticCore.Wff.all y (ph.imp ps))).imp (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCopab x y ph) (Compiler.CompactSourceSyntax.synCopab x y ps)))

Checked nominal proof certificate identified upstream as g_ssopab2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSsopab2dv (ph ps ch : SemanticCore.Wff) (x y : SemanticCore.Var) (dv_ph_x : x ∉ ph.fv) (dv_ph_y : y ∉ ph.fv) (hyp_ssopab2dv_1 : Nominal.NPrf (ph.imp (ps.imp ch))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCopab x y ps) (Compiler.CompactSourceSyntax.synCopab x y ch)))

Checked nominal proof certificate identified upstream as g_ssopab2dv.

Equations

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

Certificates from NominalWPPReplayChunk010Compact001Part041.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSetconslem1 (x : SemanticCore.Var) (A B : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_B_x : x ∉ B.fv) (hyp_setconslem1_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) (hyp_setconslem1_2 : Nominal.NPrf (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCopk (Compiler.CompactSourceSyntax.synCsn A) B) (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.synWrex x B (SemanticCore.Wff.classEq A (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv x)))))

Checked nominal proof certificate identified upstream as g_setconslem1.

Equations

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