Nominal proof certificates grouped in dependency order.

Certificates from NominalWPPReplayChunk009StructuralPart044.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gLtfintri (M N : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synW3a (SemanticCore.Wff.classMem M Compiler.CompactSourceSyntax.synCnnc) (SemanticCore.Wff.classMem N Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synWne M Compiler.CompactSourceSyntax.synC0)).imp (Compiler.CompactSourceSyntax.synW3o (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCopk M N) Compiler.CompactSourceSyntax.synCltfin) (SemanticCore.Wff.classEq M N) (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCopk N M) Compiler.CompactSourceSyntax.synCltfin)))

Checked nominal proof certificate identified upstream as g_ltfintri.

Equations

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

Certificates from NominalWPPReplayChunk009StructuralPart045.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gLefinrflx (A V : SemanticCore.Class) : Nominal.NPrf ((SemanticCore.Wff.classMem A V).imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCopk A A) Compiler.CompactSourceSyntax.synClefin))

Checked nominal proof certificate identified upstream as g_lefinrflx.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gLtlefin (A B V W : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem A V) (SemanticCore.Wff.classMem B W)).imp ((SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCopk A B) Compiler.CompactSourceSyntax.synCltfin).imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCopk A B) Compiler.CompactSourceSyntax.synClefin)))

Checked nominal proof certificate identified upstream as g_ltlefin.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gLenltfin (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 A B) Compiler.CompactSourceSyntax.synClefin) (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCopk B A) Compiler.CompactSourceSyntax.synCltfin).neg))

Checked nominal proof certificate identified upstream as g_lenltfin.

Equations

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

Certificates from NominalWPPReplayChunk009StructuralPart046.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSsfin (A B V : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synW3a (SemanticCore.Wff.classMem A V) (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCfin) (Compiler.CompactSourceSyntax.synWss A B)).imp (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCfin))

Checked nominal proof certificate identified upstream as g_ssfin.

Equations

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

Certificates from NominalWPPReplayChunk009StructuralPart047.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gVfinnc (x : SemanticCore.Var) (A V : SemanticCore.Class) (dv_A_x : x ∉ A.fv) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem A V) (SemanticCore.Wff.classMem Compiler.CompactSourceSyntax.synCvv Compiler.CompactSourceSyntax.synCfin)).imp (Compiler.CompactSourceSyntax.synWreu x Compiler.CompactSourceSyntax.synCnnc (SemanticCore.Wff.classMem A (SemanticCore.Class.cv x))))

Checked nominal proof certificate identified upstream as g_vfinnc.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNcfinex (A : SemanticCore.Class) : Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCncfin A) Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_ncfinex.

Equations

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

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

Checked nominal proof certificate identified upstream as g_ncfineq.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNcfinprop (A V : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem Compiler.CompactSourceSyntax.synCvv Compiler.CompactSourceSyntax.synCfin) (SemanticCore.Wff.classMem A V)).imp (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCncfin A) Compiler.CompactSourceSyntax.synCnnc) (SemanticCore.Wff.classMem A (Compiler.CompactSourceSyntax.synCncfin A))))

Checked nominal proof certificate identified upstream as g_ncfinprop.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNcfindi (A B V W : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synW3a (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem Compiler.CompactSourceSyntax.synCvv Compiler.CompactSourceSyntax.synCfin) (SemanticCore.Wff.classMem A V)) (SemanticCore.Wff.classMem B W) (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin A B) Compiler.CompactSourceSyntax.synC0)).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCncfin (Compiler.CompactSourceSyntax.synCun A B)) (Compiler.CompactSourceSyntax.synCplc (Compiler.CompactSourceSyntax.synCncfin A) (Compiler.CompactSourceSyntax.synCncfin B))))

Checked nominal proof certificate identified upstream as g_ncfindi.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNcfinsn (A V : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem Compiler.CompactSourceSyntax.synCvv Compiler.CompactSourceSyntax.synCfin) (SemanticCore.Wff.classMem A V)).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCncfin (Compiler.CompactSourceSyntax.synCsn A)) Compiler.CompactSourceSyntax.synC1c))

Checked nominal proof certificate identified upstream as g_ncfinsn.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEqpwrelk (A B : SemanticCore.Class) (hyp_eqpwrelk_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) (hyp_eqpwrelk_2 : Nominal.NPrf (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCopk (Compiler.CompactSourceSyntax.synCsn A) B) (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCimak (Compiler.CompactSourceSyntax.synCsymdif (Compiler.CompactSourceSyntax.synCins2k Compiler.CompactSourceSyntax.synCssetk) (Compiler.CompactSourceSyntax.synCins3k (Compiler.CompactSourceSyntax.synCsik Compiler.CompactSourceSyntax.synCssetk))) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 Compiler.CompactSourceSyntax.synC1c))))) (SemanticCore.Wff.classEq B (Compiler.CompactSourceSyntax.synCpw A)))

Checked nominal proof certificate identified upstream as g_eqpwrelk.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEqpw1relk (A B : SemanticCore.Class) (hyp_eqpw1relk_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) (hyp_eqpw1relk_2 : Nominal.NPrf (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCopk A (Compiler.CompactSourceSyntax.synCsn B)) (Compiler.CompactSourceSyntax.synCdif (Compiler.CompactSourceSyntax.synCxpk (Compiler.CompactSourceSyntax.synCpw Compiler.CompactSourceSyntax.synC1c) Compiler.CompactSourceSyntax.synCvv) (Compiler.CompactSourceSyntax.synCimak (Compiler.CompactSourceSyntax.synCsymdif (Compiler.CompactSourceSyntax.synCins3k Compiler.CompactSourceSyntax.synCssetk) (Compiler.CompactSourceSyntax.synCins2k (Compiler.CompactSourceSyntax.synCsik Compiler.CompactSourceSyntax.synCssetk))) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 Compiler.CompactSourceSyntax.synC1c)))))) (SemanticCore.Wff.classEq A (Compiler.CompactSourceSyntax.synCpw1 B)))

Checked nominal proof certificate identified upstream as g_eqpw1relk.

Equations

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