Nominal proof certificates grouped in dependency order.

Certificates from NominalWPPReplayChunk014Compact001Part056.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gLtfinsucle (A B : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCnnc) (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCnnc)).imp ((SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCopk B (Compiler.CompactSourceSyntax.synCplc A Compiler.CompactSourceSyntax.synC1c)) Compiler.CompactSourceSyntax.synCltfin).imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCopk B A) Compiler.CompactSourceSyntax.synClefin)))

Checked nominal proof certificate identified upstream as g_ltfinsucle.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gLefinsucsplit (A B : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCnnc) (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCnnc)).imp (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCopk B (Compiler.CompactSourceSyntax.synCplc A Compiler.CompactSourceSyntax.synC1c)) Compiler.CompactSourceSyntax.synClefin) (Compiler.CompactSourceSyntax.synWo (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCopk B A) Compiler.CompactSourceSyntax.synClefin) (SemanticCore.Wff.classEq B (Compiler.CompactSourceSyntax.synCplc A Compiler.CompactSourceSyntax.synC1c)))))

Checked nominal proof certificate identified upstream as g_lefinsucsplit.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gLefinzeroeq (B : SemanticCore.Class) : Nominal.NPrf ((SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCnnc).imp (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCopk B Compiler.CompactSourceSyntax.synC0c) Compiler.CompactSourceSyntax.synClefin) (SemanticCore.Wff.classEq B Compiler.CompactSourceSyntax.synC0c)))

Checked nominal proof certificate identified upstream as g_lefinzeroeq.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gKqfinsucsplit (A B : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCnnc) (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCnnc)).imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWbr B (Compiler.CompactSourceSyntax.synCkqrel Compiler.CompactSourceSyntax.synClefin) (Compiler.CompactSourceSyntax.synCplc A Compiler.CompactSourceSyntax.synC1c)) (Compiler.CompactSourceSyntax.synWo (Compiler.CompactSourceSyntax.synWbr B (Compiler.CompactSourceSyntax.synCkqrel Compiler.CompactSourceSyntax.synClefin) A) (SemanticCore.Wff.classEq B (Compiler.CompactSourceSyntax.synCplc A Compiler.CompactSourceSyntax.synC1c)))))

Checked nominal proof certificate identified upstream as g_kqfinsucsplit.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gKqfinzeroeq (B : SemanticCore.Class) : Nominal.NPrf ((SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCnnc).imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWbr B (Compiler.CompactSourceSyntax.synCkqrel Compiler.CompactSourceSyntax.synClefin) Compiler.CompactSourceSyntax.synC0c) (SemanticCore.Wff.classEq B Compiler.CompactSourceSyntax.synC0c)))

Checked nominal proof certificate identified upstream as g_kqfinzeroeq.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gKqfin0min (B : SemanticCore.Class) : Nominal.NPrf ((SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCnnc).imp (Compiler.CompactSourceSyntax.synWbr Compiler.CompactSourceSyntax.synC0c (Compiler.CompactSourceSyntax.synCkqrel Compiler.CompactSourceSyntax.synClefin) B))

Checked nominal proof certificate identified upstream as g_kqfin0min.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFinleastbase (y z t : SemanticCore.Var) (X : SemanticCore.Class) (dv_X_t : t ∉ X.fv) (dv_X_y : y ∉ X.fv) (dv_X_z : z ∉ X.fv) (dv_t_y : t ≠ y) (dv_t_z : t ≠ z) (dv_y_z : y ≠ z) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWss X Compiler.CompactSourceSyntax.synCnnc).imp ((Compiler.CompactSourceSyntax.synWrex t X (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv t) (Compiler.CompactSourceSyntax.synCkqrel Compiler.CompactSourceSyntax.synClefin) Compiler.CompactSourceSyntax.synC0c)).imp (Compiler.CompactSourceSyntax.synWrex z X (Compiler.CompactSourceSyntax.synWral y X (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv z) (Compiler.CompactSourceSyntax.synCkqrel Compiler.CompactSourceSyntax.synClefin) (SemanticCore.Class.cv y))))))

Checked nominal proof certificate identified upstream as g_finleastbase.

Equations

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

Certificates from NominalWPPReplayChunk014Compact001Part057.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFinleaststep (y z u t : SemanticCore.Var) (A X : SemanticCore.Class) (dv_A_t : t ∉ A.fv) (dv_A_u : u ∉ A.fv) (dv_A_y : y ∉ A.fv) (dv_A_z : z ∉ A.fv) (dv_X_t : t ∉ X.fv) (dv_X_u : u ∉ X.fv) (dv_X_y : y ∉ X.fv) (dv_X_z : z ∉ X.fv) (dv_t_u : t ≠ u) (dv_t_y : t ≠ y) (dv_t_z : t ≠ z) (dv_u_y : u ≠ y) (_dv_u_z : u ≠ z) (dv_y_z : y ≠ z) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synWss X Compiler.CompactSourceSyntax.synCnnc)).imp ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWrex u X (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synCkqrel Compiler.CompactSourceSyntax.synClefin) A)).neg (Compiler.CompactSourceSyntax.synWrex t X (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv t) (Compiler.CompactSourceSyntax.synCkqrel Compiler.CompactSourceSyntax.synClefin) (Compiler.CompactSourceSyntax.synCplc A Compiler.CompactSourceSyntax.synC1c)))).imp (Compiler.CompactSourceSyntax.synWrex z X (Compiler.CompactSourceSyntax.synWral y X (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv z) (Compiler.CompactSourceSyntax.synCkqrel Compiler.CompactSourceSyntax.synClefin) (SemanticCore.Class.cv y))))))

Checked nominal proof certificate identified upstream as g_finleaststep.

Equations

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

Certificates from NominalWPPReplayChunk014Compact001Part058.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFinleastnn (y z : SemanticCore.Var) (V X : SemanticCore.Class) (_dv_V_y : y ∉ V.fv) (_dv_V_z : z ∉ V.fv) (dv_X_y : y ∉ X.fv) (dv_X_z : z ∉ X.fv) (dv_y_z : y ≠ z) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synW3a (SemanticCore.Wff.classMem X V) (Compiler.CompactSourceSyntax.synWss X Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synWne X Compiler.CompactSourceSyntax.synC0)).imp (Compiler.CompactSourceSyntax.synWrex z X (Compiler.CompactSourceSyntax.synWral y X (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv z) (Compiler.CompactSourceSyntax.synCkqrel Compiler.CompactSourceSyntax.synClefin) (SemanticCore.Class.cv y)))))

Checked nominal proof certificate identified upstream as g_finleastnn.

Equations

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

Certificates from NominalWPPReplayChunk014Compact001Part059.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFinlefr : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCkqrel Compiler.CompactSourceSyntax.synClefin) Compiler.CompactSourceSyntax.synCfound Compiler.CompactSourceSyntax.synCnnc)

Checked nominal proof certificate identified upstream as g_finlefr.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFinlewe : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCkqrel Compiler.CompactSourceSyntax.synClefin) Compiler.CompactSourceSyntax.synCwe Compiler.CompactSourceSyntax.synCnnc)

Checked nominal proof certificate identified upstream as g_finlewe.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWpporbit0 (F I : SemanticCore.Class) (_dv_F_I : Disjoint F.fv I.fv) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synW3a (SemanticCore.Wff.classMem F Compiler.CompactSourceSyntax.synCfuns) (SemanticCore.Wff.classMem I (Compiler.CompactSourceSyntax.synCdm F)) (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCrn F) (Compiler.CompactSourceSyntax.synCdm F))).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCfrec F I) Compiler.CompactSourceSyntax.synC0c) I))

Checked nominal proof certificate identified upstream as g_wpporbit0.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWpporbitsuc (F I N : SemanticCore.Class) (_dv_F_I : Disjoint F.fv I.fv) (_dv_F_N : Disjoint F.fv N.fv) (_dv_I_N : Disjoint I.fv N.fv) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synW3a (SemanticCore.Wff.classMem F Compiler.CompactSourceSyntax.synCfuns) (SemanticCore.Wff.classMem I (Compiler.CompactSourceSyntax.synCdm F)) (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCrn F) (Compiler.CompactSourceSyntax.synCdm F))) (SemanticCore.Wff.classMem N Compiler.CompactSourceSyntax.synCnnc)).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCfrec F I) (Compiler.CompactSourceSyntax.synCplc N Compiler.CompactSourceSyntax.synC1c)) (Compiler.CompactSourceSyntax.synCfv F (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCfrec F I) N))))

Checked nominal proof certificate identified upstream as g_wpporbitsuc.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gKqfinsucnle (A : SemanticCore.Class) : Nominal.NPrf ((SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCnnc).imp (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCplc A Compiler.CompactSourceSyntax.synC1c) (Compiler.CompactSourceSyntax.synCkqrel Compiler.CompactSourceSyntax.synClefin) A).neg)

Checked nominal proof certificate identified upstream as g_kqfinsucnle.

Equations

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