Proofgold Address

Param binunion^binunion : ι → ι → ι
Param nIn^nIn : ι → ι → ο
Param nat_p^nat_p : ι → ο
Param equip^equip : ι → ι → ο
Param add_nat^add_nat : ι → ι → ι
Param atleastp^atleastp : ι → ι → ο
Known 2c48a..^{atleastp_antisym_equip} : ∀ x0 x1 . atleastp x0 x1 ⟶ atleastp x1 x0 ⟶ equip x0 x1
Definition or^or := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x2) ⟶ (x1 ⟶ x2) ⟶ x2
Param ordsucc^ordsucc : ι → ι
Known 48e0f.. : ∀ x0 . nat_p x0 ⟶ ∀ x1 . or (atleastp x1 x0) (atleastp (ordsucc x0) x1)
Definition False^False := ∀ x0 : ο . x0
Known FalseE^FalseE : False ⟶ ∀ x0 : ο . x0
Definition not^not := λ x0 : ο . x0 ⟶ False
Known 4fb58..^{Pigeonhole_not_atleastp_ordsucc} : ∀ x0 . nat_p x0 ⟶ not (atleastp (ordsucc x0) x0)
Known add_nat_p^add_nat_p : ∀ x0 . nat_p x0 ⟶ ∀ x1 . nat_p x1 ⟶ nat_p (add_nat x0 x1)
Known atleastp_tra^atleastp_tra : ∀ x0 x1 x2 . atleastp x0 x1 ⟶ atleastp x1 x2 ⟶ atleastp x0 x2
Param setsum^setsum : ι → ι → ι
Known add_nat_SR^add_nat_SR : ∀ x0 x1 . nat_p x1 ⟶ add_nat x0 (ordsucc x1) = ordsucc (add_nat x0 x1)
Known equip_atleastp^{equip_atleastp} : ∀ x0 x1 . equip x0 x1 ⟶ atleastp x0 x1
Known c88e0.. : ∀ x0 x1 x2 x3 . nat_p x0 ⟶ nat_p x1 ⟶ equip x0 x2 ⟶ equip x1 x3 ⟶ equip (add_nat x0 x1) (setsum x2 x3)
Known nat_ordsucc^nat_ordsucc : ∀ x0 . nat_p x0 ⟶ nat_p (ordsucc x0)
Known equip_ref^equip_ref : ∀ x0 . equip x0 x0
Known 1fe14.. : ∀ x0 x1 x2 x3 . atleastp x0 x2 ⟶ atleastp x1 x3 ⟶ (∀ x4 . x4 ∈ x2 ⟶ nIn x4 x3) ⟶ atleastp (setsum x0 x1) (binunion x2 x3)
Known equip_sym^equip_sym : ∀ x0 x1 . equip x0 x1 ⟶ equip x1 x0
Definition and^and := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x1 ⟶ x2) ⟶ x2
Known nat_inv^nat_inv : ∀ x0 . nat_p x0 ⟶ or (x0 = 0) (∀ x1 : ο . (∀ x2 . and (nat_p x2) (x0 = ordsucc x2) ⟶ x1) ⟶ x1)
Known 71267.. : ∀ x0 . atleastp 0 x0
Known c558f.. : ∀ x0 x1 x2 x3 . atleastp x0 x2 ⟶ atleastp x1 x3 ⟶ atleastp (binunion x0 x1) (setsum x2 x3)
Theorem 8bf56.. : ∀ x0 x1 x2 x3 x4 . binunion x0 x1 = x2 ⟶ (∀ x5 . x5 ∈ x0 ⟶ nIn x5 x1) ⟶ nat_p x3 ⟶ nat_p x4 ⟶ equip x0 x3 ⟶ equip x2 (add_nat x3 x4) ⟶ equip x1 x4 (proof)
Theorem 8bf56.. : ∀ x0 x1 x2 x3 x4 . binunion x0 x1 = x2 ⟶ (∀ x5 . x5 ∈ x0 ⟶ nIn x5 x1) ⟶ nat_p x3 ⟶ nat_p x4 ⟶ equip x0 x3 ⟶ equip x2 (add_nat x3 x4) ⟶ equip x1 x4 (proof)