Nominal proof certificates grouped in dependency order.

Certificates from NominalWPPReplayChunk016Compact001Part004.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWecutisofamilychainndv (D R S : SemanticCore.Class) (f g : SemanticCore.Var) (E : SemanticCore.Class) (hyp_wecutisofamilychainndv_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCwe D)) (hyp_wecutisofamilychainndv_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr S Compiler.CompactSourceSyntax.synCwe E)) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv f) (Compiler.CompactSourceSyntax.synCwecutiso R D S E)) (SemanticCore.Wff.classMem (SemanticCore.Class.cv g) (Compiler.CompactSourceSyntax.synCwecutiso R D S E))).imp (Compiler.CompactSourceSyntax.synWo (Compiler.CompactSourceSyntax.synWss (SemanticCore.Class.cv f) (SemanticCore.Class.cv g)) (Compiler.CompactSourceSyntax.synWss (SemanticCore.Class.cv g) (SemanticCore.Class.cv f))))

Checked nominal proof certificate identified upstream as g_wecutisofamilychainndv.

Equations

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

Certificates from NominalWPPReplayChunk016Compact001Part005.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWecutisounionfun11ndv (D R S E : SemanticCore.Class) (hyp_wecutisounionfun11ndv_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCwe D)) (hyp_wecutisounionfun11ndv_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr S Compiler.CompactSourceSyntax.synCwe E)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWfun (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCwecutiso R D S E))) (Compiler.CompactSourceSyntax.synWfun (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCwecutiso R D S E)))))

Checked nominal proof certificate identified upstream as g_wecutisounionfun11ndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gElwecutisodmrn (x u : SemanticCore.Var) (D R S : SemanticCore.Class) (f : SemanticCore.Var) (E : SemanticCore.Class) (dv_D_u : u ∉ D.fv) (dv_D_x : x ∉ D.fv) (dv_E_u : u ∉ E.fv) (dv_E_x : x ∉ E.fv) (dv_R_u : u ∉ R.fv) (dv_R_x : x ∉ R.fv) (dv_S_u : u ∉ S.fv) (dv_S_x : x ∉ S.fv) (dv_f_u : f ≠ u) (dv_f_x : f ≠ x) (dv_u_x : u ≠ x) : Nominal.NPrf ((SemanticCore.Wff.classMem (SemanticCore.Class.cv f) (Compiler.CompactSourceSyntax.synCwecutiso R D S E)).imp (Compiler.CompactSourceSyntax.synWrex x D (Compiler.CompactSourceSyntax.synWrex u E (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCdm (SemanticCore.Class.cv f)) (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv x))))) (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv f)) (Compiler.CompactSourceSyntax.synCin E (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif S Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv u)))))))))

Checked nominal proof certificate identified upstream as g_elwecutisodmrn.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gElwecutisodmrnss (D R S : SemanticCore.Class) (f : SemanticCore.Var) (E : SemanticCore.Class) : Nominal.NPrf ((SemanticCore.Wff.classMem (SemanticCore.Class.cv f) (Compiler.CompactSourceSyntax.synCwecutiso R D S E)).imp (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCdm (SemanticCore.Class.cv f)) D) (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv f)) E)))

Checked nominal proof certificate identified upstream as g_elwecutisodmrnss.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWecutisouniondmrnss (D R S E : SemanticCore.Class) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCdm (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCwecutiso R D S E))) D) (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCrn (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCwecutiso R D S E))) E))

Checked nominal proof certificate identified upstream as g_wecutisouniondmrnss.

Equations

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

Certificates from NominalWPPReplayChunk016Compact001Part006.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWecutisouniondirectedndv (B C D R S : SemanticCore.Class) (h : SemanticCore.Var) (E : SemanticCore.Class) (dv_B_h : h ∉ B.fv) (dv_C_h : h ∉ C.fv) (dv_D_h : h ∉ D.fv) (dv_E_h : h ∉ E.fv) (dv_R_h : h ∉ R.fv) (dv_S_h : h ∉ S.fv) (hyp_wecutisouniondirectedndv_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCwe D)) (hyp_wecutisouniondirectedndv_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr S Compiler.CompactSourceSyntax.synCwe E)) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem C (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCwecutiso R D S E))) (SemanticCore.Wff.classMem B (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCwecutiso R D S E)))).imp (Compiler.CompactSourceSyntax.synWrex h (Compiler.CompactSourceSyntax.synCwecutiso R D S E) (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem C (SemanticCore.Class.cv h)) (SemanticCore.Wff.classMem B (SemanticCore.Class.cv h)))))

Checked nominal proof certificate identified upstream as g_wecutisouniondirectedndv.

Equations

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

Certificates from NominalWPPReplayChunk016Compact001Part007.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWecutisomemberrelndv (C D R S : SemanticCore.Class) (f : SemanticCore.Var) (E K L M : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv f) (Compiler.CompactSourceSyntax.synCwecutiso R D S E)) (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCop C L) (SemanticCore.Class.cv f)) (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCop K M) (SemanticCore.Class.cv f)))).imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWbr C R K) (Compiler.CompactSourceSyntax.synWbr L S M)))

Checked nominal proof certificate identified upstream as g_wecutisomemberrelndv.

Equations

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

Certificates from NominalWPPReplayChunk016Compact001Part008.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWecutisounionrelndv (C D R S E K L M : SemanticCore.Class) (hyp_wecutisounionrelndv_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCwe D)) (hyp_wecutisounionrelndv_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr S Compiler.CompactSourceSyntax.synCwe E)) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCop C L) (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCwecutiso R D S E))) (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCop K M) (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCwecutiso R D S E)))).imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWbr C R K) (Compiler.CompactSourceSyntax.synWbr L S M)))

Checked nominal proof certificate identified upstream as g_wecutisounionrelndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWecutisounionisondv (D R S E : SemanticCore.Class) (hyp_wecutisounionisondv_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCwe D)) (hyp_wecutisounionisondv_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr S Compiler.CompactSourceSyntax.synCwe E)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWiso (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCwecutiso R D S E)) R S (Compiler.CompactSourceSyntax.synCdm (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCwecutiso R D S E))) (Compiler.CompactSourceSyntax.synCrn (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCwecutiso R D S E))))

Checked nominal proof certificate identified upstream as g_wecutisounionisondv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWecutisomemberdmdownndv (y z : SemanticCore.Var) (D R S : SemanticCore.Class) (f : SemanticCore.Var) (E : SemanticCore.Class) (hyp_wecutisomemberdmdownndv_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCwe D)) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv f) (Compiler.CompactSourceSyntax.synCwecutiso R D S E)) (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv y) (Compiler.CompactSourceSyntax.synCdm (SemanticCore.Class.cv f))) (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv z) D) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv z) R (SemanticCore.Class.cv y))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv z) (Compiler.CompactSourceSyntax.synCdm (SemanticCore.Class.cv f))))

Checked nominal proof certificate identified upstream as g_wecutisomemberdmdownndv.

Equations

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