Proofgold Address

Param ordsucc^ordsucc : ι → ι
Definition u1 := 1
Definition u2 := ordsucc u1
Definition u3 := ordsucc u2
Definition u4 := ordsucc u3
Definition u5 := ordsucc u4
Definition u6 := ordsucc u5
Definition u7 := ordsucc u6
Definition u8 := ordsucc u7
Definition u9 := ordsucc u8
Definition u10 := ordsucc u9
Definition u11 := ordsucc u10
Definition u12 := ordsucc u11
Definition u13 := ordsucc u12
Definition u14 := ordsucc u13
Definition u15 := ordsucc u14
Definition u16 := ordsucc u15
Definition u17 := ordsucc u16
Definition u18 := ordsucc u17
Definition u19 := ordsucc u18
Known neq_ordsucc_0^{neq_ordsucc_0} : ∀ x0 . ordsucc x0 = 0 ⟶ ∀ x1 : ο . x1
Theorem fd18a.. : u19 = 0 ⟶ ∀ x0 : ο . x0 (proof)
Known ordsucc_inj_contra^{ordsucc_inj_contra} : ∀ x0 x1 . (x0 = x1 ⟶ ∀ x2 : ο . x2) ⟶ ordsucc x0 = ordsucc x1 ⟶ ∀ x2 : ο . x2
Known 99743.. : u18 = 0 ⟶ ∀ x0 : ο . x0
Theorem 70279.. : u19 = u1 ⟶ ∀ x0 : ο . x0 (proof)
Known 9ccac.. : u18 = u1 ⟶ ∀ x0 : ο . x0
Theorem 81672.. : u19 = u2 ⟶ ∀ x0 : ο . x0 (proof)
Known ad866.. : u18 = u2 ⟶ ∀ x0 : ο . x0
Theorem 2e7b7.. : u19 = u3 ⟶ ∀ x0 : ο . x0 (proof)
Known 1f012.. : u18 = u3 ⟶ ∀ x0 : ο . x0
Theorem 26e28.. : u19 = u4 ⟶ ∀ x0 : ο . x0 (proof)
Known 60e5c.. : u18 = u4 ⟶ ∀ x0 : ο . x0
Theorem dcd9d.. : u19 = u5 ⟶ ∀ x0 : ο . x0 (proof)
Known ac512.. : u18 = u5 ⟶ ∀ x0 : ο . x0
Theorem b1809.. : u19 = u6 ⟶ ∀ x0 : ο . x0 (proof)
Known 8347f.. : u18 = u6 ⟶ ∀ x0 : ο . x0
Theorem 36989.. : u19 = u7 ⟶ ∀ x0 : ο . x0 (proof)
Known c9d3b.. : u18 = u7 ⟶ ∀ x0 : ο . x0
Theorem 9b462.. : u19 = u8 ⟶ ∀ x0 : ο . x0 (proof)
Known d47e8.. : u18 = u8 ⟶ ∀ x0 : ο . x0
Theorem 4545d.. : u19 = u9 ⟶ ∀ x0 : ο . x0 (proof)
Known d3922.. : u18 = u9 ⟶ ∀ x0 : ο . x0
Theorem 7d160.. : u19 = u10 ⟶ ∀ x0 : ο . x0 (proof)
Known a335e.. : u18 = u10 ⟶ ∀ x0 : ο . x0
Theorem 8109a.. : u19 = u11 ⟶ ∀ x0 : ο . x0 (proof)
Known 8da43.. : u18 = u11 ⟶ ∀ x0 : ο . x0
Theorem a5243.. : u19 = u12 ⟶ ∀ x0 : ο . x0 (proof)
Known c1bd9.. : u18 = u12 ⟶ ∀ x0 : ο . x0
Theorem 8c598.. : u19 = u13 ⟶ ∀ x0 : ο . x0 (proof)
Known 5cb8a.. : u18 = u13 ⟶ ∀ x0 : ο . x0
Theorem 35149.. : u19 = u14 ⟶ ∀ x0 : ο . x0 (proof)
Known d92fd.. : u18 = u14 ⟶ ∀ x0 : ο . x0
Theorem 38ccc.. : u19 = u15 ⟶ ∀ x0 : ο . x0 (proof)
Known dfba1.. : u18 = u15 ⟶ ∀ x0 : ο . x0
Theorem 0384c.. : u19 = u16 ⟶ ∀ x0 : ο . x0 (proof)
Known 0eaf4.. : u18 = u16 ⟶ ∀ x0 : ο . x0
Theorem 3c054.. : u19 = u17 ⟶ ∀ x0 : ο . x0 (proof)
Known 82c6a.. : u18 = u17 ⟶ ∀ x0 : ο . x0
Theorem 97eb4.. : u19 = u18 ⟶ ∀ x0 : ο . x0 (proof)
Definition u20 := ordsucc u19
Theorem 4552b.. : u20 = 0 ⟶ ∀ x0 : ο . x0 (proof)
Theorem d8b53.. : u20 = u1 ⟶ ∀ x0 : ο . x0 (proof)
Theorem c9329.. : u20 = u2 ⟶ ∀ x0 : ο . x0 (proof)
Theorem 0af1b.. : u20 = u3 ⟶ ∀ x0 : ο . x0 (proof)
Theorem f2a22.. : u20 = u4 ⟶ ∀ x0 : ο . x0 (proof)
Theorem 98620.. : u20 = u5 ⟶ ∀ x0 : ο . x0 (proof)
Theorem fd91d.. : u20 = u6 ⟶ ∀ x0 : ο . x0 (proof)
Theorem ae219.. : u20 = u7 ⟶ ∀ x0 : ο . x0 (proof)
Theorem 54bdc.. : u20 = u8 ⟶ ∀ x0 : ο . x0 (proof)
Theorem 6bb84.. : u20 = u9 ⟶ ∀ x0 : ο . x0 (proof)
Theorem 8b01c.. : u20 = u10 ⟶ ∀ x0 : ο . x0 (proof)
Theorem 66622.. : u20 = u11 ⟶ ∀ x0 : ο . x0 (proof)
Theorem 01bb6.. : u20 = u12 ⟶ ∀ x0 : ο . x0 (proof)
Theorem 551bd.. : u20 = u13 ⟶ ∀ x0 : ο . x0 (proof)
Theorem 28d21.. : u20 = u14 ⟶ ∀ x0 : ο . x0 (proof)
Theorem bf7ce.. : u20 = u15 ⟶ ∀ x0 : ο . x0 (proof)
Theorem 996e8.. : u20 = u16 ⟶ ∀ x0 : ο . x0 (proof)
Theorem 9ce5b.. : u20 = u17 ⟶ ∀ x0 : ο . x0 (proof)
Theorem 75fad.. : u20 = u18 ⟶ ∀ x0 : ο . x0 (proof)
Theorem 2615b.. : u20 = u19 ⟶ ∀ x0 : ο . x0 (proof)
Definition u21 := ordsucc u20
Theorem 1158c.. : u21 = 0 ⟶ ∀ x0 : ο . x0 (proof)
Theorem db0cd.. : u21 = u1 ⟶ ∀ x0 : ο . x0 (proof)
Theorem ebee4.. : u21 = u2 ⟶ ∀ x0 : ο . x0 (proof)
Theorem 272ed.. : u21 = u3 ⟶ ∀ x0 : ο . x0 (proof)
Theorem ac7ac.. : u21 = u4 ⟶ ∀ x0 : ο . x0 (proof)
Theorem 18fbb.. : u21 = u5 ⟶ ∀ x0 : ο . x0 (proof)
Theorem 2ec13.. : u21 = u6 ⟶ ∀ x0 : ο . x0 (proof)
Theorem 471c9.. : u21 = u7 ⟶ ∀ x0 : ο . x0 (proof)
Theorem ada11.. : u21 = u8 ⟶ ∀ x0 : ο . x0 (proof)
Theorem f159f.. : u21 = u9 ⟶ ∀ x0 : ο . x0 (proof)
Theorem b1234.. : u21 = u10 ⟶ ∀ x0 : ο . x0 (proof)
Theorem 4c4e0.. : u21 = u11 ⟶ ∀ x0 : ο . x0 (proof)
Theorem 6371d.. : u21 = u12 ⟶ ∀ x0 : ο . x0 (proof)
Theorem 87a9a.. : u21 = u13 ⟶ ∀ x0 : ο . x0 (proof)
Theorem 25d09.. : u21 = u14 ⟶ ∀ x0 : ο . x0 (proof)
Theorem 17bc6.. : u21 = u15 ⟶ ∀ x0 : ο . x0 (proof)
Theorem 39009.. : u21 = u16 ⟶ ∀ x0 : ο . x0 (proof)
Theorem b821e.. : u21 = u17 ⟶ ∀ x0 : ο . x0 (proof)
Theorem 80a82.. : u21 = u18 ⟶ ∀ x0 : ο . x0 (proof)
Theorem 44711.. : u21 = u19 ⟶ ∀ x0 : ο . x0 (proof)
Theorem 32e25.. : u21 = u20 ⟶ ∀ x0 : ο . x0 (proof)
Definition u22 := ordsucc u21
Theorem e8714.. : u22 = 0 ⟶ ∀ x0 : ο . x0 (proof)
Theorem 9e7b1.. : u22 = u1 ⟶ ∀ x0 : ο . x0 (proof)
Theorem af720.. : u22 = u2 ⟶ ∀ x0 : ο . x0 (proof)
Theorem 17aea.. : u22 = u3 ⟶ ∀ x0 : ο . x0 (proof)
Theorem 7f2f2.. : u22 = u4 ⟶ ∀ x0 : ο . x0 (proof)
Theorem 9a712.. : u22 = u5 ⟶ ∀ x0 : ο . x0 (proof)
Theorem f4b67.. : u22 = u6 ⟶ ∀ x0 : ο . x0 (proof)
Theorem 362ec.. : u22 = u7 ⟶ ∀ x0 : ο . x0 (proof)
Theorem 9d557.. : u22 = u8 ⟶ ∀ x0 : ο . x0 (proof)
Theorem ac02b.. : u22 = u9 ⟶ ∀ x0 : ο . x0 (proof)
Theorem 4d4dd.. : u22 = u10 ⟶ ∀ x0 : ο . x0 (proof)
Theorem 2051a.. : u22 = u11 ⟶ ∀ x0 : ο . x0 (proof)
Theorem db21d.. : u22 = u12 ⟶ ∀ x0 : ο . x0 (proof)
Theorem 6a662.. : u22 = u13 ⟶ ∀ x0 : ο . x0 (proof)
Theorem bd746.. : u22 = u14 ⟶ ∀ x0 : ο . x0 (proof)
Theorem ac3f7.. : u22 = u15 ⟶ ∀ x0 : ο . x0 (proof)
Theorem e7d80.. : u22 = u16 ⟶ ∀ x0 : ο . x0 (proof)
Theorem d3e26.. : u22 = u17 ⟶ ∀ x0 : ο . x0 (proof)
Theorem 7957c.. : u22 = u18 ⟶ ∀ x0 : ο . x0 (proof)
Theorem b0147.. : u22 = u19 ⟶ ∀ x0 : ο . x0 (proof)
Theorem c8ac0.. : u22 = u20 ⟶ ∀ x0 : ο . x0 (proof)
Theorem 41315.. : u22 = u21 ⟶ ∀ x0 : ο . x0 (proof)
Definition u23 := ordsucc u22
Theorem c432c.. : u23 = 0 ⟶ ∀ x0 : ο . x0 (proof)
Theorem 13d86.. : u23 = u1 ⟶ ∀ x0 : ο . x0 (proof)
Theorem 60a3a.. : u23 = u2 ⟶ ∀ x0 : ο . x0 (proof)
Theorem 3d5c1.. : u23 = u3 ⟶ ∀ x0 : ο . x0 (proof)
Theorem 7d70a.. : u23 = u4 ⟶ ∀ x0 : ο . x0 (proof)
Theorem b1d7f.. : u23 = u5 ⟶ ∀ x0 : ο . x0 (proof)
Theorem 51d86.. : u23 = u6 ⟶ ∀ x0 : ο . x0 (proof)
Theorem 49af3.. : u23 = u7 ⟶ ∀ x0 : ο . x0 (proof)
Theorem b0bcb.. : u23 = u8 ⟶ ∀ x0 : ο . x0 (proof)
Theorem b0849.. : u23 = u9 ⟶ ∀ x0 : ο . x0 (proof)
Theorem b7dd9.. : u23 = u10 ⟶ ∀ x0 : ο . x0 (proof)
Theorem 258a9.. : u23 = u11 ⟶ ∀ x0 : ο . x0 (proof)
Theorem 3982c.. : u23 = u12 ⟶ ∀ x0 : ο . x0 (proof)
Theorem 4e72c.. : u23 = u13 ⟶ ∀ x0 : ο . x0 (proof)
Theorem ef472.. : u23 = u14 ⟶ ∀ x0 : ο . x0 (proof)
Theorem eff68.. : u23 = u15 ⟶ ∀ x0 : ο . x0 (proof)
Theorem c26ad.. : u23 = u16 ⟶ ∀ x0 : ο . x0 (proof)
Theorem e9a91.. : u23 = u17 ⟶ ∀ x0 : ο . x0 (proof)
Theorem 3bccb.. : u23 = u18 ⟶ ∀ x0 : ο . x0 (proof)
Theorem ad532.. : u23 = u19 ⟶ ∀ x0 : ο . x0 (proof)
Theorem 94779.. : u23 = u20 ⟶ ∀ x0 : ο . x0 (proof)
Theorem 1a616.. : u23 = u21 ⟶ ∀ x0 : ο . x0 (proof)
Theorem 3105f.. : u23 = u22 ⟶ ∀ x0 : ο . x0 (proof)