Nominal proof certificates grouped in dependency order.

Certificates from NominalWPPReplayChunk014Compact001Part029.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFdcolcodemapf12 (A B R : SemanticCore.Class) (dv_A_B : Disjoint A.fv B.fv) (dv_A_R : Disjoint A.fv R.fv) (dv_B_R : Disjoint B.fv R.fv) (hyp_fdcolcodemapf12_1 : Nominal.NPrf (SemanticCore.Wff.classMem R Compiler.CompactSourceSyntax.synCvv)) (hyp_fdcolcodemapf12_2 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) (hyp_fdcolcodemapf12_3 : Nominal.NPrf (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCwe A) (Compiler.CompactSourceSyntax.synWss A (Compiler.CompactSourceSyntax.synCpw B))).imp (Compiler.CompactSourceSyntax.synWf1 (Compiler.CompactSourceSyntax.synCfdcolcodemap R A B) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 A)) (Compiler.CompactSourceSyntax.synCpw (Compiler.CompactSourceSyntax.synCpw (Compiler.CompactSourceSyntax.synCfdif R A B)))))

Checked nominal proof certificate identified upstream as g_fdcolcodemapf12.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFdcolcodecardle2 (A B R : SemanticCore.Class) (dv_A_B : Disjoint A.fv B.fv) (dv_A_R : Disjoint A.fv R.fv) (dv_B_R : Disjoint B.fv R.fv) (hyp_fdcolcodecardle2_1 : Nominal.NPrf (SemanticCore.Wff.classMem R Compiler.CompactSourceSyntax.synCvv)) (hyp_fdcolcodecardle2_2 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) (hyp_fdcolcodecardle2_3 : Nominal.NPrf (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCwe A) (Compiler.CompactSourceSyntax.synWss A (Compiler.CompactSourceSyntax.synCpw B))).imp (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCnc (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 A))) Compiler.CompactSourceSyntax.synClec (Compiler.CompactSourceSyntax.synCnc (Compiler.CompactSourceSyntax.synCpw (Compiler.CompactSourceSyntax.synCpw (Compiler.CompactSourceSyntax.synCfdif R A B))))))

Checked nominal proof certificate identified upstream as g_fdcolcodecardle2.

Equations

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

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

Checked nominal proof certificate identified upstream as g_fdcolcodetc2nc.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFdcolcodetc2le2 (A B R : SemanticCore.Class) (dv_A_B : Disjoint A.fv B.fv) (dv_A_R : Disjoint A.fv R.fv) (dv_B_R : Disjoint B.fv R.fv) (hyp_fdcolcodetc2le2_1 : Nominal.NPrf (SemanticCore.Wff.classMem R Compiler.CompactSourceSyntax.synCvv)) (hyp_fdcolcodetc2le2_2 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) (hyp_fdcolcodetc2le2_3 : Nominal.NPrf (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCwe A) (Compiler.CompactSourceSyntax.synWss A (Compiler.CompactSourceSyntax.synCpw B))).imp (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCnc A))) Compiler.CompactSourceSyntax.synClec (Compiler.CompactSourceSyntax.synCnc (Compiler.CompactSourceSyntax.synCpw (Compiler.CompactSourceSyntax.synCpw (Compiler.CompactSourceSyntax.synCfdif R A B))))))

Checked nominal proof certificate identified upstream as g_fdcolcodetc2le2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHwcodesex (A : SemanticCore.Class) (hyp_hwcodesex_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synChwcodes A) Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_hwcodesex.

Equations

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

Certificates from NominalWPPReplayChunk014Compact001Part030.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHwcodesexg (A V : SemanticCore.Class) : Nominal.NPrf ((SemanticCore.Wff.classMem A V).imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synChwcodes A) Compiler.CompactSourceSyntax.synCvv))

Checked nominal proof certificate identified upstream as g_hwcodesexg.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gElhwcodes (A D R : SemanticCore.Class) (_dv_A_R : Disjoint A.fv R.fv) (hyp_elhwcodes_1 : Nominal.NPrf (SemanticCore.Wff.classMem R Compiler.CompactSourceSyntax.synCvv)) (hyp_elhwcodes_2 : Nominal.NPrf (SemanticCore.Wff.classMem D Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCop R D) (Compiler.CompactSourceSyntax.synChwcodes A)) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCwe D) (Compiler.CompactSourceSyntax.synWss D A)))

Checked nominal proof certificate identified upstream as g_elhwcodes.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gBrhwiso (v u : SemanticCore.Var) (A : SemanticCore.Class) (h : SemanticCore.Var) (dv_A_h : h ∉ A.fv) (dv_A_u : u ∉ A.fv) (dv_A_v : v ∉ A.fv) (dv_h_u : h ≠ u) (dv_h_v : h ≠ v) (dv_u_v : u ≠ v) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwiso A) (SemanticCore.Class.cv v)) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwcodes A)) (SemanticCore.Wff.classMem (SemanticCore.Class.cv v) (Compiler.CompactSourceSyntax.synChwcodes A))) (Compiler.CompactSourceSyntax.synWex h (Compiler.CompactSourceSyntax.synWiso (SemanticCore.Class.cv h) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC1st (SemanticCore.Class.cv u)) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC1st (SemanticCore.Class.cv v)) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv v))))))

Checked nominal proof certificate identified upstream as g_brhwiso.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gBrhwisoany (v u : SemanticCore.Var) (A : SemanticCore.Class) (h : SemanticCore.Var) (dv_A_h : h ∉ A.fv) (dv_h_u : h ≠ u) (dv_h_v : h ≠ v) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwiso A) (SemanticCore.Class.cv v)) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwcodes A)) (SemanticCore.Wff.classMem (SemanticCore.Class.cv v) (Compiler.CompactSourceSyntax.synChwcodes A))) (Compiler.CompactSourceSyntax.synWex h (Compiler.CompactSourceSyntax.synWiso (SemanticCore.Class.cv h) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC1st (SemanticCore.Class.cv u)) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC1st (SemanticCore.Class.cv v)) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv v))))))

Checked nominal proof certificate identified upstream as g_brhwisoany.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHwisosymi (v u : SemanticCore.Var) (A : SemanticCore.Class) (dv_A_u : u ∉ A.fv) (dv_A_v : v ∉ A.fv) (dv_u_v : u ≠ v) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwiso A) (SemanticCore.Class.cv v)).imp (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv v) (Compiler.CompactSourceSyntax.synChwiso A) (SemanticCore.Class.cv u)))

Checked nominal proof certificate identified upstream as g_hwisosymi.

Equations

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

Certificates from NominalWPPReplayChunk014Compact001Part031.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHwisotri (w v u : SemanticCore.Var) (A : SemanticCore.Class) (dv_A_u : u ∉ A.fv) (dv_A_v : v ∉ A.fv) (dv_A_w : w ∉ A.fv) (dv_u_v : u ≠ v) (dv_u_w : u ≠ w) (dv_v_w : v ≠ w) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwiso A) (SemanticCore.Class.cv v)) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv v) (Compiler.CompactSourceSyntax.synChwiso A) (SemanticCore.Class.cv w))).imp (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwiso A) (SemanticCore.Class.cv w)))

Checked nominal proof certificate identified upstream as g_hwisotri.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHwisorefl (u : SemanticCore.Var) (A : SemanticCore.Class) (_dv_A_u : u ∉ A.fv) : Nominal.NPrf ((SemanticCore.Wff.classMem (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwcodes A)).imp (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwiso A) (SemanticCore.Class.cv u)))

Checked nominal proof certificate identified upstream as g_hwisorefl.

Equations

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

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

Checked nominal proof certificate identified upstream as g_hwrelsex.

Equations

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

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

Checked nominal proof certificate identified upstream as g_hwbijex.

Equations

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

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

Checked nominal proof certificate identified upstream as g_hwgenex.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHwcnex (A : SemanticCore.Class) (hyp_hwcnex_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synChwcn A) Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_hwcnex.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHwnisoex (A : SemanticCore.Class) (hyp_hwnisoex_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synChwniso A) Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_hwnisoex.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHnordex (A : SemanticCore.Class) (hyp_hnordex_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synChnord A) Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_hnordex.

Equations

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

Certificates from NominalWPPReplayChunk014Compact001Part032.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gElhwrrels (u : SemanticCore.Var) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (SemanticCore.Class.cv u) Compiler.CompactSourceSyntax.synChwrels) (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC1st (SemanticCore.Class.cv u)) (Compiler.CompactSourceSyntax.synCxp (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)))))

Checked nominal proof certificate identified upstream as g_elhwrrels.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gElhwcn (u : SemanticCore.Var) (A : SemanticCore.Class) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwcn A)) (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwcodes A)) (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC1st (SemanticCore.Class.cv u)) (Compiler.CompactSourceSyntax.synCxp (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u))))))

Checked nominal proof certificate identified upstream as g_elhwcn.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gElhwbij (f : SemanticCore.Var) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (SemanticCore.Class.cv f) Compiler.CompactSourceSyntax.synChwbij) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWfun (SemanticCore.Class.cv f)) (Compiler.CompactSourceSyntax.synWfun (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f)))))

Checked nominal proof certificate identified upstream as g_elhwbij.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gElhnord (x u : SemanticCore.Var) (A : SemanticCore.Class) (dv_A_u : u ∉ A.fv) (_dv_A_x : x ∉ A.fv) (dv_u_x : u ≠ x) (hyp_elhnord_1 : Nominal.NPrf (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) (Compiler.CompactSourceSyntax.synChnord A)) (Compiler.CompactSourceSyntax.synWrex u (Compiler.CompactSourceSyntax.synChwcn A) (SemanticCore.Wff.classEq (SemanticCore.Class.cv x) (Compiler.CompactSourceSyntax.synCec (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwniso A)))))

Checked nominal proof certificate identified upstream as g_elhnord.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHwnisoclasselhnord (u : SemanticCore.Var) (A : SemanticCore.Class) (_dv_A_u : u ∉ A.fv) (hyp_hwnisoclasselhnord_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf ((SemanticCore.Wff.classMem (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwcn A)).imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCec (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwniso A)) (Compiler.CompactSourceSyntax.synChnord A)))

Checked nominal proof certificate identified upstream as g_hwnisoclasselhnord.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gImageswapfn : Nominal.NPrf (Compiler.CompactSourceSyntax.synWfn (Compiler.CompactSourceSyntax.synCimage Compiler.CompactSourceSyntax.synCswap) Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_imageswapfn.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gImageswapval (f : SemanticCore.Var) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCimage Compiler.CompactSourceSyntax.synCswap) (SemanticCore.Class.cv f)) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f)))

Checked nominal proof certificate identified upstream as g_imageswapval.

Equations

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

Certificates from NominalWPPReplayChunk014Compact001Part033.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHwtrnfn : Nominal.NPrf (Compiler.CompactSourceSyntax.synWfn Compiler.CompactSourceSyntax.synChwtrn Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_hwtrnfn.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHwtrnval (R : SemanticCore.Class) (f : SemanticCore.Var) (hyp_hwtrnval_1 : Nominal.NPrf (SemanticCore.Wff.classMem R Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synChwtrn (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv f) R)) (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synCcom (SemanticCore.Class.cv f) R) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f))))

Checked nominal proof certificate identified upstream as g_hwtrnval.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gRanfnfn : Nominal.NPrf (Compiler.CompactSourceSyntax.synWfn Compiler.CompactSourceSyntax.synCranfn Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_ranfnfn.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHwgenfn : Nominal.NPrf (Compiler.CompactSourceSyntax.synWfn Compiler.CompactSourceSyntax.synChwgen Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_hwgenfn.

Equations

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

Certificates from NominalWPPReplayChunk014Compact001Part034.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHwgenval (R : SemanticCore.Class) (f : SemanticCore.Var) (hyp_hwgenval_1 : Nominal.NPrf (SemanticCore.Wff.classMem R Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synChwgen (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv f) R)) (Compiler.CompactSourceSyntax.synCop (Compiler.CompactSourceSyntax.synCop R (Compiler.CompactSourceSyntax.synCdm (SemanticCore.Class.cv f))) (Compiler.CompactSourceSyntax.synCop (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synCcom (SemanticCore.Class.cv f) R) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f))) (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv f)))))

Checked nominal proof certificate identified upstream as g_hwgenval.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gElhwnisogen (v u : SemanticCore.Var) (A : SemanticCore.Class) (f r : SemanticCore.Var) (_dv_A_f : f ∉ A.fv) (_dv_A_r : r ∉ A.fv) (dv_f_r : f ≠ r) (dv_f_u : f ≠ u) (dv_f_v : f ≠ v) (dv_r_u : r ≠ u) (dv_r_v : r ≠ v) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwniso A) (SemanticCore.Class.cv v)) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwcn A)) (SemanticCore.Wff.classMem (SemanticCore.Class.cv v) (Compiler.CompactSourceSyntax.synChwcn A))) (Compiler.CompactSourceSyntax.synWrex f Compiler.CompactSourceSyntax.synChwbij (Compiler.CompactSourceSyntax.synWrex r Compiler.CompactSourceSyntax.synCvv (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synChwgen (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv f) (SemanticCore.Class.cv r))) (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv u) (SemanticCore.Class.cv v)))))))

Checked nominal proof certificate identified upstream as g_elhwnisogen.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gElhwnisogenval (v u : SemanticCore.Var) (A : SemanticCore.Class) (f r : SemanticCore.Var) (dv_A_f : f ∉ A.fv) (dv_A_r : r ∉ A.fv) (dv_f_r : f ≠ r) (dv_f_u : f ≠ u) (dv_f_v : f ≠ v) (dv_r_u : r ≠ u) (dv_r_v : r ≠ v) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwniso A) (SemanticCore.Class.cv v)) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwcn A)) (SemanticCore.Wff.classMem (SemanticCore.Class.cv v) (Compiler.CompactSourceSyntax.synChwcn A))) (Compiler.CompactSourceSyntax.synWrex f Compiler.CompactSourceSyntax.synChwbij (Compiler.CompactSourceSyntax.synWrex r Compiler.CompactSourceSyntax.synCvv (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv r) (Compiler.CompactSourceSyntax.synCdm (SemanticCore.Class.cv f))) (SemanticCore.Class.cv u)) (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCop (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synCcom (SemanticCore.Class.cv f) (SemanticCore.Class.cv r)) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f))) (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv f))) (SemanticCore.Class.cv v)))))))

Checked nominal proof certificate identified upstream as g_elhwnisogenval.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gElhwnisogenfun (v u : SemanticCore.Var) (A : SemanticCore.Class) (f r : SemanticCore.Var) (dv_A_f : f ∉ A.fv) (dv_A_r : r ∉ A.fv) (dv_f_r : f ≠ r) (dv_f_u : f ≠ u) (dv_f_v : f ≠ v) (dv_r_u : r ≠ u) (dv_r_v : r ≠ v) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwniso A) (SemanticCore.Class.cv v)) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwcn A)) (SemanticCore.Wff.classMem (SemanticCore.Class.cv v) (Compiler.CompactSourceSyntax.synChwcn A))) (Compiler.CompactSourceSyntax.synWex f (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWfun (SemanticCore.Class.cv f)) (Compiler.CompactSourceSyntax.synWfun (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f)))) (Compiler.CompactSourceSyntax.synWrex r Compiler.CompactSourceSyntax.synCvv (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv r) (Compiler.CompactSourceSyntax.synCdm (SemanticCore.Class.cv f))) (SemanticCore.Class.cv u)) (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCop (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synCcom (SemanticCore.Class.cv f) (SemanticCore.Class.cv r)) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f))) (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv f))) (SemanticCore.Class.cv v))))))))

Checked nominal proof certificate identified upstream as g_elhwnisogenfun.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHwbijf1o (f : SemanticCore.Var) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (SemanticCore.Class.cv f) Compiler.CompactSourceSyntax.synChwbij) (Compiler.CompactSourceSyntax.synWf1o (SemanticCore.Class.cv f) (Compiler.CompactSourceSyntax.synCdm (SemanticCore.Class.cv f)) (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv f))))

Checked nominal proof certificate identified upstream as g_hwbijf1o.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gElhwnisogenf1o (v u : SemanticCore.Var) (A : SemanticCore.Class) (f r : SemanticCore.Var) (dv_A_f : f ∉ A.fv) (dv_A_r : r ∉ A.fv) (dv_f_r : f ≠ r) (dv_f_u : f ≠ u) (dv_f_v : f ≠ v) (dv_r_u : r ≠ u) (dv_r_v : r ≠ v) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwniso A) (SemanticCore.Class.cv v)) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwcn A)) (SemanticCore.Wff.classMem (SemanticCore.Class.cv v) (Compiler.CompactSourceSyntax.synChwcn A))) (Compiler.CompactSourceSyntax.synWex f (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWf1o (SemanticCore.Class.cv f) (Compiler.CompactSourceSyntax.synCdm (SemanticCore.Class.cv f)) (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv f))) (Compiler.CompactSourceSyntax.synWrex r Compiler.CompactSourceSyntax.synCvv (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv r) (Compiler.CompactSourceSyntax.synCdm (SemanticCore.Class.cv f))) (SemanticCore.Class.cv u)) (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCop (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synCcom (SemanticCore.Class.cv f) (SemanticCore.Class.cv r)) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f))) (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv f))) (SemanticCore.Class.cv v))))))))

Checked nominal proof certificate identified upstream as g_elhwnisogenf1o.

Equations

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