Nominal proof certificates grouped in dependency order.

Certificates from NominalWPPReplayChunk013Compact001Part024.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFrd (ph : SemanticCore.Wff) (y z : SemanticCore.Var) (A R V X : SemanticCore.Class) (dv_R_y : y ∉ R.fv) (dv_R_z : z ∉ R.fv) (dv_X_y : y ∉ X.fv) (dv_X_z : z ∉ X.fv) (dv_y_z : y ≠ z) (hyp_frd_1 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCfound A))) (hyp_frd_2 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classMem X V))) (hyp_frd_3 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWss X A))) (hyp_frd_4 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWne X Compiler.CompactSourceSyntax.synC0))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWrex y X (Compiler.CompactSourceSyntax.synWral z X ((Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv z) R (SemanticCore.Class.cv y)).imp (SemanticCore.Wff.objEq z y)))))

Checked nominal proof certificate identified upstream as g_frd.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSymd (ph : SemanticCore.Wff) (A R X Y : SemanticCore.Class) (hyp_symd_1 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCsym A))) (hyp_symd_2 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classMem X A))) (hyp_symd_3 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classMem Y A))) (hyp_symd_4 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWbr X R Y))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWbr Y R X))

Checked nominal proof certificate identified upstream as g_symd.

Equations

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

Certificates from NominalWPPReplayChunk013Compact001Part025.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gTrrd (ph : SemanticCore.Wff) (x y z : SemanticCore.Var) (A R V W : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_A_y : y ∉ A.fv) (dv_A_z : z ∉ A.fv) (dv_R_x : x ∉ R.fv) (dv_R_y : y ∉ R.fv) (dv_R_z : z ∉ R.fv) (dv_ph_x : x ∉ ph.fv) (dv_ph_y : y ∉ ph.fv) (dv_ph_z : z ∉ ph.fv) (dv_x_y : x ≠ y) (dv_x_z : x ≠ z) (dv_y_z : y ≠ z) (hyp_trrd_1 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classMem R V))) (hyp_trrd_2 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classMem A W))) (hyp_trrd_3 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synW3a ph (Compiler.CompactSourceSyntax.synW3a (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) A) (SemanticCore.Wff.classMem (SemanticCore.Class.cv y) A) (SemanticCore.Wff.classMem (SemanticCore.Class.cv z) A)) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv x) R (SemanticCore.Class.cv y)) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv y) R (SemanticCore.Class.cv z)))).imp (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv x) R (SemanticCore.Class.cv z)))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCtrans A))

Checked nominal proof certificate identified upstream as g_trrd.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gRefrd (ph : SemanticCore.Wff) (x : SemanticCore.Var) (A R V W : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_R_x : x ∉ R.fv) (dv_ph_x : x ∉ ph.fv) (hyp_refrd_1 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classMem R V))) (hyp_refrd_2 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classMem A W))) (hyp_refrd_3 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa ph (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) A)).imp (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv x) R (SemanticCore.Class.cv x)))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCref A))

Checked nominal proof certificate identified upstream as g_refrd.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gRefd (ph : SemanticCore.Wff) (A R X : SemanticCore.Class) (hyp_refd_1 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCref A))) (hyp_refd_2 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classMem X A))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWbr X R X))

Checked nominal proof certificate identified upstream as g_refd.

Equations

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

Certificates from NominalWPPReplayChunk013Compact001Part026.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gAntird (ph : SemanticCore.Wff) (x y : SemanticCore.Var) (A R V W : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_A_y : y ∉ A.fv) (dv_R_x : x ∉ R.fv) (dv_R_y : y ∉ R.fv) (dv_ph_x : x ∉ ph.fv) (dv_ph_y : y ∉ ph.fv) (dv_x_y : x ≠ y) (hyp_antird_1 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classMem R V))) (hyp_antird_2 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classMem A W))) (hyp_antird_3 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synW3a ph (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) A) (SemanticCore.Wff.classMem (SemanticCore.Class.cv y) A)) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv x) R (SemanticCore.Class.cv y)) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv y) R (SemanticCore.Class.cv x)))).imp (SemanticCore.Wff.objEq x y))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCantisym A))

Checked nominal proof certificate identified upstream as g_antird.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gAntid (ph : SemanticCore.Wff) (A R X Y : SemanticCore.Class) (hyp_antid_1 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCantisym A))) (hyp_antid_2 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classMem X A))) (hyp_antid_3 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classMem Y A))) (hyp_antid_4 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWbr X R Y))) (hyp_antid_5 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWbr Y R X))) : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq X Y))

Checked nominal proof certificate identified upstream as g_antid.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gConnexrd (ph : SemanticCore.Wff) (x y : SemanticCore.Var) (A R V W : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_A_y : y ∉ A.fv) (dv_R_x : x ∉ R.fv) (dv_R_y : y ∉ R.fv) (dv_ph_x : x ∉ ph.fv) (dv_ph_y : y ∉ ph.fv) (dv_x_y : x ≠ y) (hyp_connexrd_1 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classMem R V))) (hyp_connexrd_2 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classMem A W))) (hyp_connexrd_3 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synW3a ph (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) A) (SemanticCore.Wff.classMem (SemanticCore.Class.cv y) A)).imp (Compiler.CompactSourceSyntax.synWo (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv x) R (SemanticCore.Class.cv y)) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv y) R (SemanticCore.Class.cv x))))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCconnex A))

Checked nominal proof certificate identified upstream as g_connexrd.

Equations

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

Certificates from NominalWPPReplayChunk013Compact001Part027.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gConnexd (ph : SemanticCore.Wff) (A R X Y : SemanticCore.Class) (hyp_connexd_1 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCconnex A))) (hyp_connexd_2 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classMem X A))) (hyp_connexd_3 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classMem Y A))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWo (Compiler.CompactSourceSyntax.synWbr X R Y) (Compiler.CompactSourceSyntax.synWbr Y R X)))

Checked nominal proof certificate identified upstream as g_connexd.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gErsymtr (A R : SemanticCore.Class) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCer A) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCsym A) (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCtrans A)))

Checked nominal proof certificate identified upstream as g_ersymtr.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gPorta (A R : SemanticCore.Class) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCpartial A) (Compiler.CompactSourceSyntax.synW3a (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCref A) (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCtrans A) (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCantisym A)))

Checked nominal proof certificate identified upstream as g_porta.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSopc (A R : SemanticCore.Class) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCstrict A) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCpartial A) (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCconnex A)))

Checked nominal proof certificate identified upstream as g_sopc.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFrds (ph ps ch th : SemanticCore.Wff) (x y z : SemanticCore.Var) (A R : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_A_y : y ∉ A.fv) (dv_A_z : z ∉ A.fv) (dv_R_y : y ∉ R.fv) (dv_R_z : z ∉ R.fv) (dv_ch_x : x ∉ ch.fv) (dv_ps_y : y ∉ ps.fv) (dv_ps_z : z ∉ ps.fv) (dv_th_x : x ∉ th.fv) (dv_x_y : x ≠ y) (dv_x_z : x ≠ z) (dv_y_z : y ≠ z) (hyp_frds_1 : Nominal.NPrf (SemanticCore.Wff.classMem (SemanticCore.Class.cab x ps) Compiler.CompactSourceSyntax.synCvv)) (hyp_frds_2 : Nominal.NPrf ((SemanticCore.Wff.objEq x y).imp (Compiler.CompactSourceSyntax.synWb ps ch))) (hyp_frds_3 : Nominal.NPrf ((SemanticCore.Wff.objEq x z).imp (Compiler.CompactSourceSyntax.synWb ps th))) (hyp_frds_4 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCfound A))) (hyp_frds_5 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWrex x A ps))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWrex y A (Compiler.CompactSourceSyntax.synWa ch (Compiler.CompactSourceSyntax.synWral z A ((Compiler.CompactSourceSyntax.synWa th (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv z) R (SemanticCore.Class.cv y))).imp (SemanticCore.Wff.objEq z y))))))

Checked nominal proof certificate identified upstream as g_frds.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gPod (ph : SemanticCore.Wff) (x y z : SemanticCore.Var) (A R V W : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_A_y : y ∉ A.fv) (dv_A_z : z ∉ A.fv) (dv_R_x : x ∉ R.fv) (dv_R_y : y ∉ R.fv) (dv_R_z : z ∉ R.fv) (dv_ph_x : x ∉ ph.fv) (dv_ph_y : y ∉ ph.fv) (dv_ph_z : z ∉ ph.fv) (dv_x_y : x ≠ y) (dv_x_z : x ≠ z) (dv_y_z : y ≠ z) (hyp_pod_1 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classMem R V))) (hyp_pod_2 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classMem A W))) (hyp_pod_3 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa ph (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) A)).imp (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv x) R (SemanticCore.Class.cv x)))) (hyp_pod_4 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synW3a ph (Compiler.CompactSourceSyntax.synW3a (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) A) (SemanticCore.Wff.classMem (SemanticCore.Class.cv y) A) (SemanticCore.Wff.classMem (SemanticCore.Class.cv z) A)) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv x) R (SemanticCore.Class.cv y)) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv y) R (SemanticCore.Class.cv z)))).imp (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv x) R (SemanticCore.Class.cv z)))) (hyp_pod_5 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synW3a ph (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) A) (SemanticCore.Wff.classMem (SemanticCore.Class.cv y) A)) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv x) R (SemanticCore.Class.cv y)) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv y) R (SemanticCore.Class.cv x)))).imp (SemanticCore.Wff.objEq x y))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCpartial A))

Checked nominal proof certificate identified upstream as g_pod.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSod (ph : SemanticCore.Wff) (x y z : SemanticCore.Var) (A R V W : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_A_y : y ∉ A.fv) (dv_A_z : z ∉ A.fv) (dv_R_x : x ∉ R.fv) (dv_R_y : y ∉ R.fv) (dv_R_z : z ∉ R.fv) (dv_ph_x : x ∉ ph.fv) (dv_ph_y : y ∉ ph.fv) (dv_ph_z : z ∉ ph.fv) (dv_x_y : x ≠ y) (dv_x_z : x ≠ z) (dv_y_z : y ≠ z) (hyp_sod_1 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classMem R V))) (hyp_sod_2 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classMem A W))) (hyp_sod_3 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa ph (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) A)).imp (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv x) R (SemanticCore.Class.cv x)))) (hyp_sod_4 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synW3a ph (Compiler.CompactSourceSyntax.synW3a (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) A) (SemanticCore.Wff.classMem (SemanticCore.Class.cv y) A) (SemanticCore.Wff.classMem (SemanticCore.Class.cv z) A)) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv x) R (SemanticCore.Class.cv y)) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv y) R (SemanticCore.Class.cv z)))).imp (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv x) R (SemanticCore.Class.cv z)))) (hyp_sod_5 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synW3a ph (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) A) (SemanticCore.Wff.classMem (SemanticCore.Class.cv y) A)) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv x) R (SemanticCore.Class.cv y)) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv y) R (SemanticCore.Class.cv x)))).imp (SemanticCore.Wff.objEq x y))) (hyp_sod_6 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synW3a ph (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) A) (SemanticCore.Wff.classMem (SemanticCore.Class.cv y) A)).imp (Compiler.CompactSourceSyntax.synWo (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv x) R (SemanticCore.Class.cv y)) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv y) R (SemanticCore.Class.cv x))))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCstrict A))

Checked nominal proof certificate identified upstream as g_sod.

Equations

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

Certificates from NominalWPPReplayChunk013Compact001Part028.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWeds (ph ps ch th : SemanticCore.Wff) (x y z : SemanticCore.Var) (A R : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_A_y : y ∉ A.fv) (dv_A_z : z ∉ A.fv) (dv_R_y : y ∉ R.fv) (dv_R_z : z ∉ R.fv) (dv_ch_x : x ∉ ch.fv) (dv_ph_y : y ∉ ph.fv) (dv_ph_z : z ∉ ph.fv) (dv_ps_y : y ∉ ps.fv) (dv_ps_z : z ∉ ps.fv) (dv_th_x : x ∉ th.fv) (dv_x_y : x ≠ y) (dv_x_z : x ≠ z) (dv_y_z : y ≠ z) (hyp_weds_1 : Nominal.NPrf (SemanticCore.Wff.classMem (SemanticCore.Class.cab x ps) Compiler.CompactSourceSyntax.synCvv)) (hyp_weds_2 : Nominal.NPrf ((SemanticCore.Wff.objEq x y).imp (Compiler.CompactSourceSyntax.synWb ps ch))) (hyp_weds_3 : Nominal.NPrf ((SemanticCore.Wff.objEq x z).imp (Compiler.CompactSourceSyntax.synWb ps th))) (hyp_weds_4 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCwe A))) (hyp_weds_5 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWrex x A ps))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWrex y A (Compiler.CompactSourceSyntax.synWa ch (Compiler.CompactSourceSyntax.synWral z A (th.imp (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv y) R (SemanticCore.Class.cv z)))))))

Checked nominal proof certificate identified upstream as g_weds.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gIserd (ph : SemanticCore.Wff) (x y z : SemanticCore.Var) (A R V W : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_A_y : y ∉ A.fv) (dv_A_z : z ∉ A.fv) (dv_R_x : x ∉ R.fv) (dv_R_y : y ∉ R.fv) (dv_R_z : z ∉ R.fv) (dv_ph_x : x ∉ ph.fv) (dv_ph_y : y ∉ ph.fv) (dv_ph_z : z ∉ ph.fv) (dv_x_y : x ≠ y) (dv_x_z : x ≠ z) (dv_y_z : y ≠ z) (hyp_iserd_1 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classMem R V))) (hyp_iserd_2 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classMem A W))) (hyp_iserd_3 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synW3a ph (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) A) (SemanticCore.Wff.classMem (SemanticCore.Class.cv y) A)) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv x) R (SemanticCore.Class.cv y))).imp (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv y) R (SemanticCore.Class.cv x)))) (hyp_iserd_4 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synW3a ph (Compiler.CompactSourceSyntax.synW3a (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) A) (SemanticCore.Wff.classMem (SemanticCore.Class.cv y) A) (SemanticCore.Wff.classMem (SemanticCore.Class.cv z) A)) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv x) R (SemanticCore.Class.cv y)) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv y) R (SemanticCore.Class.cv z)))).imp (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv x) R (SemanticCore.Class.cv z)))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCer A))

Checked nominal proof certificate identified upstream as g_iserd.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gDfec2 (y : SemanticCore.Var) (A R : SemanticCore.Class) (dv_A_y : y ∉ A.fv) (dv_R_y : y ∉ R.fv) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCec A R) (SemanticCore.Class.cab y (Compiler.CompactSourceSyntax.synWbr A R (SemanticCore.Class.cv y))))

Checked nominal proof certificate identified upstream as g_dfec2.

Equations

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

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

Checked nominal proof certificate identified upstream as g_ecexg.

Equations

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

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

Checked nominal proof certificate identified upstream as g_ecexr.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gErsym (ph : SemanticCore.Wff) (A R X Y : SemanticCore.Class) (hyp_ersym_1 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCer A))) (hyp_ersym_2 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classMem X A))) (hyp_ersym_3 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classMem Y A))) (hyp_ersym_4 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWbr X R Y))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWbr Y R X))

Checked nominal proof certificate identified upstream as g_ersym.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gErsymb (ph : SemanticCore.Wff) (A R X Y : SemanticCore.Class) (hyp_ersymb_1 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCer A))) (hyp_ersymb_2 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classMem X A))) (hyp_ersymb_3 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classMem Y A))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWbr X R Y) (Compiler.CompactSourceSyntax.synWbr Y R X)))

Checked nominal proof certificate identified upstream as g_ersymb.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gErtr (ph : SemanticCore.Wff) (A R X Y Z : SemanticCore.Class) (hyp_ertr_1 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCer A))) (hyp_ertr_2 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classMem X A))) (hyp_ertr_3 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classMem Y A))) (hyp_ertr_4 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classMem Z A))) : Nominal.NPrf (ph.imp ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr X R Y) (Compiler.CompactSourceSyntax.synWbr Y R Z)).imp (Compiler.CompactSourceSyntax.synWbr X R Z)))

Checked nominal proof certificate identified upstream as g_ertr.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gErtrd (ph : SemanticCore.Wff) (A R X Y Z : SemanticCore.Class) (hyp_ertr_1 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCer A))) (hyp_ertr_2 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classMem X A))) (hyp_ertr_3 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classMem Y A))) (hyp_ertr_4 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classMem Z A))) (hyp_ertrd_5 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWbr X R Y))) (hyp_ertrd_6 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWbr Y R Z))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWbr X R Z))

Checked nominal proof certificate identified upstream as g_ertrd.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gErtr3d (ph : SemanticCore.Wff) (A R X Y Z : SemanticCore.Class) (hyp_ertr_1 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCer A))) (hyp_ertr_2 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classMem X A))) (hyp_ertr_3 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classMem Y A))) (hyp_ertr_4 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classMem Z A))) (hyp_ertr3d_5 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWbr Y R X))) (hyp_ertr3d_6 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWbr Y R Z))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWbr X R Z))

Checked nominal proof certificate identified upstream as g_ertr3d.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gErtr4d (ph : SemanticCore.Wff) (A R X Y Z : SemanticCore.Class) (hyp_ertr_1 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCer A))) (hyp_ertr_2 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classMem X A))) (hyp_ertr_3 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classMem Y A))) (hyp_ertr_4 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classMem Z A))) (hyp_ertr4d_5 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWbr X R Y))) (hyp_ertr4d_6 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWbr Z R Y))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWbr X R Z))

Checked nominal proof certificate identified upstream as g_ertr4d.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gErref (ph : SemanticCore.Wff) (A R X : SemanticCore.Class) (hyp_erref_1 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCer Compiler.CompactSourceSyntax.synCvv))) (hyp_erref_2 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCdm R) A))) (hyp_erref_3 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classMem X A))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWbr X R X))

Checked nominal proof certificate identified upstream as g_erref.

Equations

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

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

Checked nominal proof certificate identified upstream as g_eceq1.

Equations

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

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

Checked nominal proof certificate identified upstream as g_eceq2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gElec (A B R : SemanticCore.Class) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem A (Compiler.CompactSourceSyntax.synCec B R)) (Compiler.CompactSourceSyntax.synWbr B R A))

Checked nominal proof certificate identified upstream as g_elec.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gErdmrn (R : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCer Compiler.CompactSourceSyntax.synCvv).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCdm R) (Compiler.CompactSourceSyntax.synCrn R)))

Checked nominal proof certificate identified upstream as g_erdmrn.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEcss (ph : SemanticCore.Wff) (A R X : SemanticCore.Class) (hyp_ecss_1 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCer Compiler.CompactSourceSyntax.synCvv))) (hyp_ecss_2 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCdm R) X))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCec A R) X))

Checked nominal proof certificate identified upstream as g_ecss.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEcdmn0 (A R : SemanticCore.Class) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem A (Compiler.CompactSourceSyntax.synCdm R)) (Compiler.CompactSourceSyntax.synWne (Compiler.CompactSourceSyntax.synCec A R) Compiler.CompactSourceSyntax.synC0))

Checked nominal proof certificate identified upstream as g_ecdmn0.

Equations

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