Proofgold Address

Import Signature c718f..
Known 264f3..^eq_1_Sing0 : 1 = Sing 0
Known cad6f..^nat_trans : ∀ x0 . nat_p x0 ⟶ ∀ x1 . x1 ∈ x0 ⟶ x1 ⊆ x0
Param 1a64d..^nat_primrec : ι → (ι → ι → ι) → ι → ι
Known be11a..^{nat_primrec_0} : ∀ x0 . ∀ x1 : ι → ι → ι . nat_primrec x0 x1 0 = x0
Known fe4c8..^{nat_primrec_S} : ∀ x0 . ∀ x1 : ι → ι → ι . ∀ x2 . nat_p x2 ⟶ nat_primrec x0 x1 (ordsucc x2) = x1 x2 (nat_primrec x0 x1 x2)
Param 29768..^add_nat : ι → ι → ι
Known 23277..^add_nat_0R : ∀ x0 . add_nat x0 0 = x0
Known e61e1..^add_nat_SR : ∀ x0 x1 . nat_p x1 ⟶ add_nat x0 (ordsucc x1) = ordsucc (add_nat x0 x1)
Known 4c1d5..^add_nat_p : ∀ x0 . nat_p x0 ⟶ ∀ x1 . nat_p x1 ⟶ nat_p (add_nat x0 x1)
Known 84fbe..^add_nat_0L : ∀ x0 . nat_p x0 ⟶ add_nat 0 x0 = x0
Known e6efb..^add_nat_SL : ∀ x0 . nat_p x0 ⟶ ∀ x1 . nat_p x1 ⟶ add_nat (ordsucc x0) x1 = ordsucc (add_nat x0 x1)
Known 4ab17..^add_nat_com : ∀ x0 . nat_p x0 ⟶ ∀ x1 . nat_p x1 ⟶ add_nat x0 x1 = add_nat x1 x0
Param 80ccc..^mul_nat : ι → ι → ι
Known 1e5b2..^mul_nat_0R : ∀ x0 . mul_nat x0 0 = 0
Known 6dd6f..^mul_nat_SR : ∀ x0 x1 . nat_p x1 ⟶ mul_nat x0 (ordsucc x1) = add_nat x0 (mul_nat x0 x1)
Known a3051..^mul_nat_1R : ∀ x0 . mul_nat x0 1 = x0
Known e910c..^mul_nat_p : ∀ x0 . nat_p x0 ⟶ ∀ x1 . nat_p x1 ⟶ nat_p (mul_nat x0 x1)
Known 5d6ce..^mul_nat_com : ∀ x0 . nat_p x0 ⟶ ∀ x1 . nat_p x1 ⟶ mul_nat x0 x1 = mul_nat x1 x0
Param 53ee8..^ordinal : ι → ο
Known c9e70..^{ordinal_TransSet} : ∀ x0 . ordinal x0 ⟶ TransSet x0
Known 7d95d..^{ordinal_Empty} : ordinal 0
Known 43b0f..^{ordinal_Hered} : ∀ x0 . ordinal x0 ⟶ ∀ x1 . x1 ∈ x0 ⟶ ordinal x1
Known ab0f7..^{ordinal_ordsucc} : ∀ x0 . ordinal x0 ⟶ ordinal (ordsucc x0)
Known 47cd4..^{nat_p_ordinal} : ∀ x0 . nat_p x0 ⟶ ordinal x0
Known b0030..^{ordinal_ordsucc_In_Subq} : ∀ x0 . ordinal x0 ⟶ ∀ x1 . x1 ∈ x0 ⟶ ordsucc x1 ⊆ x0
Known 21f2d..^{ordinal_trichotomy_or} : ∀ x0 x1 . ordinal x0 ⟶ ordinal x1 ⟶ or (or (x0 ∈ x1) (x0 = x1)) (x1 ∈ x0)
Known bb6d2..^{ordinal_trichotomy_or_impred} : ∀ x0 x1 . ordinal x0 ⟶ ordinal x1 ⟶ ∀ x2 : ο . (x0 ∈ x1 ⟶ x2) ⟶ (x0 = x1 ⟶ x2) ⟶ (x1 ∈ x0 ⟶ x2) ⟶ x2
Known 7b99b..^{ordinal_In_Or_Subq} : ∀ x0 x1 . ordinal x0 ⟶ ordinal x1 ⟶ or (x0 ∈ x1) (x1 ⊆ x0)
Param ad9ad..^omega : ι
Known c2c61..^omega_nat_p : ∀ x0 . x0 ∈ omega ⟶ nat_p x0
Known d5080..^nat_p_omega : ∀ x0 . nat_p x0 ⟶ x0 ∈ omega
Known 17fb6..^{omega_ordsucc} : ∀ x0 . x0 ∈ omega ⟶ ordsucc x0 ∈ omega
Known c79e7..^{omega_TransSet} : TransSet omega
Known 17748..^{omega_ordinal} : ordinal omega
Known ecfad..^{ordsucc_omega_ordinal} : ordinal (ordsucc omega)
Def 44295..^inj : ι → ι → (ι → ι) → ο := λ x0 x1 . λ x2 : ι → ι . and (∀ x3 . x3 ∈ x0 ⟶ x2 x3 ∈ x1) (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ x2 x3 = x2 x4 ⟶ x3 = x4)
Def f022f..^surj : ι → ι → (ι → ι) → ο := λ x0 x1 . λ x2 : ι → ι . and (∀ x3 . x3 ∈ x0 ⟶ x2 x3 ∈ x1) (∀ x3 . x3 ∈ x1 ⟶ ∀ x4 : ο . (∀ x5 . and (x5 ∈ x0) (x2 x5 = x3) ⟶ x4) ⟶ x4)
Param f7d93..^bij : ι → ι → (ι → ι) → ο
Known 3229f..^bijI : ∀ x0 x1 . ∀ x2 : ι → ι . (∀ x3 . x3 ∈ x0 ⟶ x2 x3 ∈ x1) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ x2 x3 = x2 x4 ⟶ x3 = x4) ⟶ (∀ x3 . x3 ∈ x1 ⟶ ∀ x4 : ο . (∀ x5 . and (x5 ∈ x0) (x2 x5 = x3) ⟶ x4) ⟶ x4) ⟶ bij x0 x1 x2
Known cf075..^bijE : ∀ x0 x1 . ∀ x2 : ι → ι . bij x0 x1 x2 ⟶ ∀ x3 : ο . ((∀ x4 . x4 ∈ x0 ⟶ x2 x4 ∈ x1) ⟶ (∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ x2 x4 = x2 x5 ⟶ x4 = x5) ⟶ (∀ x4 . x4 ∈ x1 ⟶ ∀ x5 : ο . (∀ x6 . and (x6 ∈ x0) (x2 x6 = x4) ⟶ x5) ⟶ x5) ⟶ x3) ⟶ x3
Param f3a01..^inv : ι → (ι → ι) → ι → ι
Known 6489d..^surj_rinv : ∀ x0 x1 . ∀ x2 : ι → ι . (∀ x3 . x3 ∈ x1 ⟶ ∀ x4 : ο . (∀ x5 . and (x5 ∈ x0) (x2 x5 = x3) ⟶ x4) ⟶ x4) ⟶ ∀ x3 . x3 ∈ x1 ⟶ and (inv x0 x2 x3 ∈ x0) (x2 (inv x0 x2 x3) = x3)
Known d1655..^inj_linv : ∀ x0 . ∀ x1 : ι → ι . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 = x1 x3 ⟶ x2 = x3) ⟶ ∀ x2 . x2 ∈ x0 ⟶ inv x0 x1 (x1 x2) = x2
Known 69c53..^bij_inv : ∀ x0 x1 . ∀ x2 : ι → ι . bij x0 x1 x2 ⟶ bij x1 x0 (inv x0 x2)
Known 4c904..^bij_comp : ∀ x0 x1 x2 . ∀ x3 x4 : ι → ι . bij x0 x1 x3 ⟶ bij x1 x2 x4 ⟶ bij x0 x2 (λ x5 . x4 (x3 x5))
Known 707f3..^bij_id : ∀ x0 . bij x0 x0 (λ x1 . x1)
Known 00097..^bij_inj : ∀ x0 x1 . ∀ x2 : ι → ι . bij x0 x1 x2 ⟶ inj x0 x1 x2
Known 7fa9a..^bij_surj : ∀ x0 x1 . ∀ x2 : ι → ι . bij x0 x1 x2 ⟶ surj x0 x1 x2
Known de895..^inj_surj_bij : ∀ x0 x1 . ∀ x2 : ι → ι . inj x0 x1 x2 ⟶ surj x0 x1 x2 ⟶ bij x0 x1 x2
Known dde3b..^surj_inv_inj : ∀ x0 x1 . ∀ x2 : ι → ι . (∀ x3 . x3 ∈ x1 ⟶ ∀ x4 : ο . (∀ x5 . and (x5 ∈ x0) (x2 x5 = x3) ⟶ x4) ⟶ x4) ⟶ inj x1 x0 (inv x0 x2)
Param 13545..^atleastp : ι → ι → ο
Known e67b3.. : ∀ x0 . atleastp x0 x0
Known c412b..^atleastp_tra : ∀ x0 x1 x2 . atleastp x0 x1 ⟶ atleastp x1 x2 ⟶ atleastp x0 x2
Known 3a427..^{Subq_atleastp} : ∀ x0 x1 . x0 ⊆ x1 ⟶ atleastp x0 x1
Known 364bd.. : ∀ x0 . nat_p x0 ⟶ ∀ x1 . x1 ∈ x0 ⟶ atleastp x1 x0
Param 7f2bf..^equip : ι → ι → ο
Known 9a412..^{equip_atleastp} : ∀ x0 x1 . equip x0 x1 ⟶ atleastp x0 x1
Known c41fb..^equip_ref : ∀ x0 . equip x0 x0
Known 272f0..^equip_sym : ∀ x0 x1 . equip x0 x1 ⟶ equip x1 x0
Known d616c..^equip_tra : ∀ x0 x1 x2 . equip x0 x1 ⟶ equip x1 x2 ⟶ equip x0 x2
Known 03a2c..^{SchroederBernstein} : ∀ x0 x1 . ∀ x2 x3 : ι → ι . inj x0 x1 x2 ⟶ inj x1 x0 x3 ⟶ equip x0 x1
Known 2c48a..^{atleastp_antisym_equip} : ∀ x0 x1 . atleastp x0 x1 ⟶ atleastp x1 x0 ⟶ equip x0 x1