Nominal proof certificates grouped in dependency order.

Certificates from NominalWPPReplayChunk013Compact001Part049.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSbthlem1 (A B C D R G X : SemanticCore.Class) (hyp_sbthlem1_1 : Nominal.NPrf (SemanticCore.Wff.classMem R Compiler.CompactSourceSyntax.synCvv)) (hyp_sbthlem1_2 : Nominal.NPrf (SemanticCore.Wff.classMem X Compiler.CompactSourceSyntax.synCvv)) (hyp_sbthlem1_3 : Nominal.NPrf (SemanticCore.Wff.classEq G (Compiler.CompactSourceSyntax.synCclos1 (Compiler.CompactSourceSyntax.synCdif X (Compiler.CompactSourceSyntax.synCrn R)) R))) (hyp_sbthlem1_4 : Nominal.NPrf (SemanticCore.Wff.classEq A (Compiler.CompactSourceSyntax.synCin X G))) (hyp_sbthlem1_5 : Nominal.NPrf (SemanticCore.Wff.classEq B (Compiler.CompactSourceSyntax.synCdif X G))) (hyp_sbthlem1_6 : Nominal.NPrf (SemanticCore.Wff.classEq C (Compiler.CompactSourceSyntax.synCin (Compiler.CompactSourceSyntax.synCrn R) G))) (hyp_sbthlem1_7 : Nominal.NPrf (SemanticCore.Wff.classEq D (Compiler.CompactSourceSyntax.synCdif (Compiler.CompactSourceSyntax.synCrn R) G))) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWfun R) (Compiler.CompactSourceSyntax.synWfun (Compiler.CompactSourceSyntax.synCcnv R))) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWss X (Compiler.CompactSourceSyntax.synCdm R)) (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCrn R) X))).imp (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCrn R) Compiler.CompactSourceSyntax.synCen X))

Checked nominal proof certificate identified upstream as g_sbthlem1.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSbthlem2 (B R V : SemanticCore.Class) (hyp_sbthlem2_1 : Nominal.NPrf (SemanticCore.Wff.classMem R Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWfun R) (Compiler.CompactSourceSyntax.synWfun (Compiler.CompactSourceSyntax.synCcnv R))) (Compiler.CompactSourceSyntax.synW3a (SemanticCore.Wff.classMem B V) (Compiler.CompactSourceSyntax.synWss B (Compiler.CompactSourceSyntax.synCdm R)) (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCrn R) B))).imp (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCrn R) Compiler.CompactSourceSyntax.synCen B))

Checked nominal proof certificate identified upstream as g_sbthlem2.

Equations

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

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

Checked nominal proof certificate identified upstream as g_sbthlem3.

Equations

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

Certificates from NominalWPPReplayChunk013Compact001Part050.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSbth (A B : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCncs) (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCncs)).imp ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr A Compiler.CompactSourceSyntax.synClec B) (Compiler.CompactSourceSyntax.synWbr B Compiler.CompactSourceSyntax.synClec A)).imp (SemanticCore.Wff.classEq A B)))

Checked nominal proof certificate identified upstream as g_sbth.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gLtlenlec (M N : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem M Compiler.CompactSourceSyntax.synCncs) (SemanticCore.Wff.classMem N Compiler.CompactSourceSyntax.synCncs)).imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWbr M Compiler.CompactSourceSyntax.synCltc N) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr M Compiler.CompactSourceSyntax.synClec N) (Compiler.CompactSourceSyntax.synWbr N Compiler.CompactSourceSyntax.synClec M).neg)))

Checked nominal proof certificate identified upstream as g_ltlenlec.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gAddlec (M N V W : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synW3a (SemanticCore.Wff.classMem M V) (SemanticCore.Wff.classMem N W) (Compiler.CompactSourceSyntax.synWne (Compiler.CompactSourceSyntax.synCplc M N) Compiler.CompactSourceSyntax.synC0)).imp (Compiler.CompactSourceSyntax.synWbr M Compiler.CompactSourceSyntax.synClec (Compiler.CompactSourceSyntax.synCplc M N)))

Checked nominal proof certificate identified upstream as g_addlec.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gAddlecncs (M N : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem M Compiler.CompactSourceSyntax.synCncs) (SemanticCore.Wff.classMem N Compiler.CompactSourceSyntax.synCncs)).imp (Compiler.CompactSourceSyntax.synWbr M Compiler.CompactSourceSyntax.synClec (Compiler.CompactSourceSyntax.synCplc M N)))

Checked nominal proof certificate identified upstream as g_addlecncs.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gDflec2 (M N : SemanticCore.Class) (p : SemanticCore.Var) (dv_M_p : p ∉ M.fv) (dv_N_p : p ∉ N.fv) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem M Compiler.CompactSourceSyntax.synCncs) (SemanticCore.Wff.classMem N Compiler.CompactSourceSyntax.synCncs)).imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWbr M Compiler.CompactSourceSyntax.synClec N) (Compiler.CompactSourceSyntax.synWrex p Compiler.CompactSourceSyntax.synCncs (SemanticCore.Wff.classEq N (Compiler.CompactSourceSyntax.synCplc M (SemanticCore.Class.cv p))))))

Checked nominal proof certificate identified upstream as g_dflec2.

Equations

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

Certificates from NominalWPPReplayChunk013Compact001Part051.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gLectr (A B C : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synW3a (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCncs) (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCncs) (SemanticCore.Wff.classMem C Compiler.CompactSourceSyntax.synCncs)).imp ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr A Compiler.CompactSourceSyntax.synClec B) (Compiler.CompactSourceSyntax.synWbr B Compiler.CompactSourceSyntax.synClec C)).imp (Compiler.CompactSourceSyntax.synWbr A Compiler.CompactSourceSyntax.synClec C)))

Checked nominal proof certificate identified upstream as g_lectr.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNc0le1 (N : SemanticCore.Class) : Nominal.NPrf ((SemanticCore.Wff.classMem N Compiler.CompactSourceSyntax.synCncs).imp (Compiler.CompactSourceSyntax.synWo (SemanticCore.Wff.classEq N Compiler.CompactSourceSyntax.synC0c) (Compiler.CompactSourceSyntax.synWbr Compiler.CompactSourceSyntax.synC1c Compiler.CompactSourceSyntax.synClec N)))

Checked nominal proof certificate identified upstream as g_nc0le1.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNc0suc (m : SemanticCore.Var) (N : SemanticCore.Class) (dv_N_m : m ∉ N.fv) : Nominal.NPrf ((SemanticCore.Wff.classMem N Compiler.CompactSourceSyntax.synCncs).imp (Compiler.CompactSourceSyntax.synWo (SemanticCore.Wff.classEq N Compiler.CompactSourceSyntax.synC0c) (Compiler.CompactSourceSyntax.synWrex m Compiler.CompactSourceSyntax.synCncs (SemanticCore.Wff.classEq N (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv m) Compiler.CompactSourceSyntax.synC1c)))))

Checked nominal proof certificate identified upstream as g_nc0suc.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gAddceq0 (A B : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCncs) (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCncs)).imp (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCplc A B) Compiler.CompactSourceSyntax.synC0c) (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classEq A Compiler.CompactSourceSyntax.synC0c) (SemanticCore.Wff.classEq B Compiler.CompactSourceSyntax.synC0c))))

Checked nominal proof certificate identified upstream as g_addceq0.

Equations

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

Certificates from NominalWPPReplayChunk013Compact001Part052.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gDflec3 (f : SemanticCore.Var) (M N : SemanticCore.Class) (a b : SemanticCore.Var) (dv_M_a : a ∉ M.fv) (dv_N_a : a ∉ N.fv) (dv_N_b : b ∉ N.fv) (dv_a_b : a ≠ b) (dv_a_f : a ≠ f) (dv_b_f : b ≠ f) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem M Compiler.CompactSourceSyntax.synCncs) (SemanticCore.Wff.classMem N Compiler.CompactSourceSyntax.synCncs)).imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWbr M Compiler.CompactSourceSyntax.synClec N) (Compiler.CompactSourceSyntax.synWrex a M (Compiler.CompactSourceSyntax.synWrex b N (Compiler.CompactSourceSyntax.synWex f (Compiler.CompactSourceSyntax.synWf1 (SemanticCore.Class.cv f) (SemanticCore.Class.cv a) (SemanticCore.Class.cv b)))))))

Checked nominal proof certificate identified upstream as g_dflec3.

Equations

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

Certificates from NominalWPPReplayChunk013Compact001Part053.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNclenc (A B : SemanticCore.Class) (f : SemanticCore.Var) (dv_A_f : f ∉ A.fv) (dv_B_f : f ∉ B.fv) (hyp_nclenc_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) (hyp_nclenc_2 : Nominal.NPrf (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCnc A) Compiler.CompactSourceSyntax.synClec (Compiler.CompactSourceSyntax.synCnc B)) (Compiler.CompactSourceSyntax.synWex f (Compiler.CompactSourceSyntax.synWf1 (SemanticCore.Class.cv f) A B)))

Checked nominal proof certificate identified upstream as g_nclenc.

Equations

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

Certificates from NominalWPPReplayChunk013Compact001Part054.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gLenc (x : SemanticCore.Var) (A M : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_M_x : x ∉ M.fv) (hyp_lenc_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf ((SemanticCore.Wff.classMem M Compiler.CompactSourceSyntax.synCncs).imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWbr M Compiler.CompactSourceSyntax.synClec (Compiler.CompactSourceSyntax.synCnc A)) (Compiler.CompactSourceSyntax.synWrex x M (Compiler.CompactSourceSyntax.synWss (SemanticCore.Class.cv x) A))))

Checked nominal proof certificate identified upstream as g_lenc.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gTcncg (A V : SemanticCore.Class) : Nominal.NPrf ((SemanticCore.Wff.classMem A V).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCnc A)) (Compiler.CompactSourceSyntax.synCnc (Compiler.CompactSourceSyntax.synCpw1 A))))

Checked nominal proof certificate identified upstream as g_tcncg.

Equations

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

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

Checked nominal proof certificate identified upstream as g_tcnc.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gTcnc1c : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCnc Compiler.CompactSourceSyntax.synC1c)) (Compiler.CompactSourceSyntax.synCnc (Compiler.CompactSourceSyntax.synCpw1 Compiler.CompactSourceSyntax.synC1c)))

Checked nominal proof certificate identified upstream as g_tcnc1c.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gTcnc1c = NFChoice.DirectNominalPrf.WPPReplay.gTcnc NFChoice.Compiler.CompactSourceSyntax.synC1c NFChoice.DirectNominalPrf.WPPReplay.gN1cex

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gTc11 (M N : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem M Compiler.CompactSourceSyntax.synCncs) (SemanticCore.Wff.classMem N Compiler.CompactSourceSyntax.synCncs)).imp (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCtc M) (Compiler.CompactSourceSyntax.synCtc N)) (SemanticCore.Wff.classEq M N)))

Checked nominal proof certificate identified upstream as g_tc11.

Equations

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