Nominal proof certificates grouped in dependency order.

Certificates from NominalWPPReplayChunk014Compact001Part001.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFrecexg (F G I V : SemanticCore.Class) (hyp_frecex_1 : Nominal.NPrf (SemanticCore.Wff.classEq F (Compiler.CompactSourceSyntax.synCfrec G I))) : Nominal.NPrf ((SemanticCore.Wff.classMem G V).imp (SemanticCore.Wff.classMem F Compiler.CompactSourceSyntax.synCvv))

Checked nominal proof certificate identified upstream as g_frecexg.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFrecex (F G I : SemanticCore.Class) (hyp_frecex_1 : Nominal.NPrf (SemanticCore.Wff.classEq F (Compiler.CompactSourceSyntax.synCfrec G I))) (hyp_frecex_2 : Nominal.NPrf (SemanticCore.Wff.classMem G Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (SemanticCore.Wff.classMem F Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_frecex.

Equations

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

Certificates from NominalWPPReplayChunk014Compact001Part002.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFrecxp (F G I : SemanticCore.Class) (hyp_frecxp_1 : Nominal.NPrf (SemanticCore.Wff.classEq F (Compiler.CompactSourceSyntax.synCfrec G I))) (hyp_frecxp_2 : Nominal.NPrf (SemanticCore.Wff.classMem G Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss F (Compiler.CompactSourceSyntax.synCxp Compiler.CompactSourceSyntax.synCnnc (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCrn G) (Compiler.CompactSourceSyntax.synCsn I))))

Checked nominal proof certificate identified upstream as g_frecxp.

Equations

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

Certificates from NominalWPPReplayChunk014Compact001Part003.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFrecxpg (F G I V : SemanticCore.Class) (hyp_frecxpg_1 : Nominal.NPrf (SemanticCore.Wff.classEq F (Compiler.CompactSourceSyntax.synCfrec G I))) : Nominal.NPrf ((SemanticCore.Wff.classMem G V).imp (Compiler.CompactSourceSyntax.synWss F (Compiler.CompactSourceSyntax.synCxp Compiler.CompactSourceSyntax.synCnnc (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCrn G) (Compiler.CompactSourceSyntax.synCsn I)))))

Checked nominal proof certificate identified upstream as g_frecxpg.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gDmfrec (ph : SemanticCore.Wff) (F G I V : SemanticCore.Class) (hyp_dmfrec_1 : Nominal.NPrf (SemanticCore.Wff.classEq F (Compiler.CompactSourceSyntax.synCfrec G I))) (hyp_dmfrec_2 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classMem G V))) (hyp_dmfrec_3 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classMem I (Compiler.CompactSourceSyntax.synCdm G)))) (hyp_dmfrec_4 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCrn G) (Compiler.CompactSourceSyntax.synCdm G)))) : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCdm F) Compiler.CompactSourceSyntax.synCnnc))

Checked nominal proof certificate identified upstream as g_dmfrec.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFnfreclem1 (y z w : SemanticCore.Var) (F V : SemanticCore.Class) (dv_F_w : w ∉ F.fv) (dv_F_y : y ∉ F.fv) (dv_F_z : z ∉ F.fv) (dv_w_y : w ≠ y) (dv_w_z : w ≠ z) (dv_y_z : y ≠ z) : Nominal.NPrf ((SemanticCore.Wff.classMem F V).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cab w (SemanticCore.Wff.all y (SemanticCore.Wff.all z ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv w) F (SemanticCore.Class.cv y)) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv w) F (SemanticCore.Class.cv z))).imp (SemanticCore.Wff.objEq y z))))) Compiler.CompactSourceSyntax.synCvv))

Checked nominal proof certificate identified upstream as g_fnfreclem1.

Equations

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

Certificates from NominalWPPReplayChunk014Compact001Part004.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFnfreclem2 (ph : SemanticCore.Wff) (F G I V X : SemanticCore.Class) (hyp_fnfreclem2_1 : Nominal.NPrf (SemanticCore.Wff.classEq F (Compiler.CompactSourceSyntax.synCfrec G I))) (hyp_fnfreclem2_2 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classMem G V))) (hyp_fnfreclem2_3 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classMem I (Compiler.CompactSourceSyntax.synCdm G)))) (_hyp_fnfreclem2_4 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCrn G) (Compiler.CompactSourceSyntax.synCdm G)))) : Nominal.NPrf (ph.imp ((Compiler.CompactSourceSyntax.synWbr Compiler.CompactSourceSyntax.synC0c F X).imp (SemanticCore.Wff.classEq X I)))

Checked nominal proof certificate identified upstream as g_fnfreclem2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFnfreclem3 (ph : SemanticCore.Wff) (z : SemanticCore.Var) (F G I V X Y : SemanticCore.Class) (dv_F_z : z ∉ F.fv) (dv_G_z : z ∉ G.fv) (_dv_I_z : z ∉ I.fv) (dv_X_z : z ∉ X.fv) (dv_Y_z : z ∉ Y.fv) (dv_ph_z : z ∉ ph.fv) (hyp_fnfreclem2_1 : Nominal.NPrf (SemanticCore.Wff.classEq F (Compiler.CompactSourceSyntax.synCfrec G I))) (hyp_fnfreclem2_2 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classMem G V))) (hyp_fnfreclem2_3 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classMem I (Compiler.CompactSourceSyntax.synCdm G)))) (hyp_fnfreclem2_4 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCrn G) (Compiler.CompactSourceSyntax.synCdm G)))) (hyp_fnfreclem3_5 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classMem X Compiler.CompactSourceSyntax.synCnnc))) (hyp_fnfreclem3_6 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCplc X Compiler.CompactSourceSyntax.synC1c) F Y))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWex z (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr X F (SemanticCore.Class.cv z)) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv z) G Y))))

Checked nominal proof certificate identified upstream as g_fnfreclem3.

Equations

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

Certificates from NominalWPPReplayChunk014Compact001Part005.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFnfrec (ph : SemanticCore.Wff) (F G I : SemanticCore.Class) (hyp_fnfrec_1 : Nominal.NPrf (SemanticCore.Wff.classEq F (Compiler.CompactSourceSyntax.synCfrec G I))) (hyp_fnfrec_2 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classMem G Compiler.CompactSourceSyntax.synCfuns))) (hyp_fnfrec_3 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classMem I (Compiler.CompactSourceSyntax.synCdm G)))) (hyp_fnfrec_4 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCrn G) (Compiler.CompactSourceSyntax.synCdm G)))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWfn F Compiler.CompactSourceSyntax.synCnnc))

Checked nominal proof certificate identified upstream as g_fnfrec.

Equations

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