Proofgold Address

Param and : ο → ο → ο
Definition inj := λ x0 x1 . λ x2 : ι → ι . and (∀ x3 . prim1 x3 x0 ⟶ prim1 (x2 x3) x1) (∀ x3 . prim1 x3 x0 ⟶ ∀ x4 . prim1 x4 x0 ⟶ x2 x3 = x2 x4 ⟶ x3 = x4)
Definition surj := λ x0 x1 . λ x2 : ι → ι . and (∀ x3 . prim1 x3 x0 ⟶ prim1 (x2 x3) x1) (∀ x3 . prim1 x3 x1 ⟶ ∀ x4 : ο . (∀ x5 . and (prim1 x5 x0) (x2 x5 = x3) ⟶ x4) ⟶ x4)
Param 48ef8.. : ι
Param c2e41.. : ι → ι → ο
Definition 6eae3.. := λ x0 . ∀ x1 : ο . (∀ x2 . and (prim1 x2 48ef8..) (c2e41.. x0 x2) ⟶ x1) ⟶ x1
Definition False := ∀ x0 : ο . x0
Definition not := λ x0 : ο . x0 ⟶ False
Definition c036a.. := λ x0 . not (6eae3.. x0)
Param 14149.. : ι → ι → ι
Definition 0a59d.. := λ x0 x1 . and (and (prim1 x0 48ef8..) (prim1 x1 48ef8..)) (∀ x2 : ο . (∀ x3 . and (prim1 x3 48ef8..) (14149.. x0 x3 = x1) ⟶ x2) ⟶ x2)
Param 4ae4a.. : ι → ι
Param 4a7ef.. : ι
Param or : ο → ο → ο
Definition 94fdb.. := λ x0 . and (and (prim1 x0 48ef8..) (prim1 (4ae4a.. 4a7ef..) x0)) (∀ x1 . prim1 x1 48ef8.. ⟶ 0a59d.. x1 x0 ⟶ or (x1 = 4ae4a.. 4a7ef..) (x1 = x0))
Param 1ad11.. : ι → ι → ι
Definition 2a940.. := λ x0 x1 . and (and (prim1 x0 48ef8..) (prim1 x1 48ef8..)) (∀ x2 . prim1 x2 (1ad11.. 48ef8.. (4ae4a.. 4a7ef..)) ⟶ 0a59d.. x2 x0 ⟶ 0a59d.. x2 x1 ⟶ x2 = 4ae4a.. 4a7ef..)
Param 616bf.. : ι → ι → ι
Definition fc3b3.. := λ x0 x1 x2 . and (and (and (prim1 x0 48ef8..) (prim1 x1 48ef8..)) (prim1 x2 48ef8..)) (or (∀ x3 : ο . (∀ x4 . and (prim1 x4 48ef8..) (616bf.. x0 (14149.. x4 x2) = x1) ⟶ x3) ⟶ x3) (∀ x3 : ο . (∀ x4 . and (prim1 x4 48ef8..) (616bf.. x1 (14149.. x4 x2) = x0) ⟶ x3) ⟶ x3))
Param nat_primrec : ι → (ι → ι → ι) → ι → ι
Definition f6049.. := λ x0 . nat_primrec (4ae4a.. 4a7ef..) (λ x1 . 14149.. x0)
Definition 8d0f2.. := λ x0 . and (prim1 x0 48ef8..) (∀ x1 : ο . (∀ x2 . and (prim1 x2 48ef8..) (x0 = 14149.. (4ae4a.. (4ae4a.. 4a7ef..)) x2) ⟶ x1) ⟶ x1)
Definition b2df9.. := λ x0 . and (prim1 x0 48ef8..) (∀ x1 . prim1 x1 48ef8.. ⟶ x0 = 14149.. (4ae4a.. (4ae4a.. 4a7ef..)) x1 ⟶ ∀ x2 : ο . x2)
Definition 2f282.. := nat_primrec (4ae4a.. 4a7ef..) (λ x0 . 14149.. (4ae4a.. x0))
Param f482f.. : ι → ι → ι
Param 0fc90.. : ι → (ι → ι) → ι
Param If_i : ο → ι → ι → ι
Definition 455bd.. := λ x0 . f482f.. (nat_primrec (0fc90.. 48ef8.. (λ x1 . If_i (x1 = 4a7ef..) (4ae4a.. 4a7ef..) 4a7ef..)) (λ x1 x2 . 0fc90.. 48ef8.. (λ x3 . If_i (x3 = 4a7ef..) (4ae4a.. 4a7ef..) (616bf.. (f482f.. x2 (prim3 x3)) (f482f.. x2 x3)))) x0)
Param 1216a.. : ι → (ι → ο) → ι
Definition d091d.. := λ x0 . prim0 (λ x1 . and (prim1 x1 48ef8..) (c2e41.. x1 (1216a.. (4ae4a.. x0) (λ x2 . and (prim1 4a7ef.. x2) (2a940.. x2 x0)))))
Param 569d0.. : ι → ι → ι
Param e6316.. : ι → ι → ι
Param bc82c.. : ι → ι → ι
Param f4dc0.. : ι → ι
Definition 5c14e.. := λ x0 x1 . 569d0.. (2f282.. x0) (e6316.. (2f282.. (bc82c.. x0 (f4dc0.. x1))) (2f282.. x1))
Param a470d.. : ι
Definition 36be8.. := λ x0 x1 . and (and (prim1 x0 a470d..) (prim1 x1 a470d..)) (∀ x2 : ο . (∀ x3 . and (prim1 x3 a470d..) (e6316.. x0 x3 = x1) ⟶ x2) ⟶ x2)
Definition ff71c.. := λ x0 x1 x2 . and (and (and (prim1 x0 a470d..) (prim1 x1 a470d..)) (prim1 x2 (1ad11.. 48ef8.. (4ae4a.. 4a7ef..)))) (36be8.. (bc82c.. x0 (f4dc0.. x1)) x2)
Definition 51e8c.. := λ x0 x1 . and (and (prim1 x0 a470d..) (prim1 x1 a470d..)) (∀ x2 . prim1 x2 (1ad11.. 48ef8.. (4ae4a.. 4a7ef..)) ⟶ 36be8.. x2 x0 ⟶ 36be8.. x2 x1 ⟶ x2 = 4ae4a.. 4a7ef..)
Definition 62b6b.. := λ x0 . nat_primrec (4ae4a.. 4a7ef..) (λ x1 . e6316.. x0)
Param explicit_Nats : ι → ι → (ι → ι) → ο
Param explicit_Nats_primrec : ι → ι → (ι → ι) → ι → (ι → ι → ι) → ι → ι
Param explicit_Nats_one_plus : ι → ι → (ι → ι) → ι → ι → ι
Param explicit_Nats_one_plus : ι → ι → (ι → ι) → ι → ι → ι
Definition explicit_Nats_one_mult_alt := λ x0 x1 . λ x2 : ι → ι . λ x3 . explicit_Nats_primrec x0 x1 x2 x3 (λ x4 . explicit_Nats_one_plus x0 x1 x2 x3)
Definition explicit_Nats_lt := λ x0 x1 . λ x2 : ι → ι . λ x3 x4 . and (and (prim1 x3 x0) (prim1 x4 x0)) (∀ x5 : ο . (∀ x6 . and (prim1 x6 x0) (explicit_Nats_one_plus x0 x1 x2 x6 x3 = x4) ⟶ x5) ⟶ x5)
Definition 3db9b.. := λ x0 x1 . λ x2 : ι → ι . λ x3 . and (prim1 x3 x0) (∀ x4 . prim1 x4 x0 ⟶ explicit_Nats_lt x0 x1 x2 x4 x3 ⟶ or (x4 = x1) (x4 = x3))
Definition 340be.. := λ x0 x1 . λ x2 : ι → ι . λ x3 x4 . and (and (prim1 x3 x0) (prim1 x4 x0)) (∀ x5 . prim1 x5 x0 ⟶ explicit_Nats_lt x0 x1 x2 x5 x3 ⟶ explicit_Nats_lt x0 x1 x2 x5 x4 ⟶ x5 = 4ae4a.. 4a7ef..)
Definition 12b21.. := λ x0 x1 . λ x2 : ι → ι . λ x3 x4 x5 . and (and (and (prim1 x3 x0) (prim1 x4 x0)) (prim1 x5 x0)) (or (or (x3 = x4) (∀ x6 : ο . (∀ x7 . and (prim1 x7 x0) (explicit_Nats_one_plus x0 x1 x2 x3 (explicit_Nats_one_plus x0 x1 x2 x7 x5) = x4) ⟶ x6) ⟶ x6)) (∀ x6 : ο . (∀ x7 . and (prim1 x7 x0) (explicit_Nats_one_plus x0 x1 x2 x4 (explicit_Nats_one_plus x0 x1 x2 x7 x5) = x3) ⟶ x6) ⟶ x6))
Definition explicit_Nats_one_lt := λ x0 x1 . λ x2 : ι → ι . λ x3 x4 . and (and (prim1 x3 x0) (prim1 x4 x0)) (∀ x5 : ο . (∀ x6 . and (prim1 x6 x0) (explicit_Nats_one_plus x0 x1 x2 x3 x6 = x4) ⟶ x5) ⟶ x5)
Definition explicit_Nats_one_le := λ x0 x1 . λ x2 : ι → ι . λ x3 x4 . and (and (prim1 x3 x0) (prim1 x4 x0)) (or (x3 = x4) (∀ x5 : ο . (∀ x6 . and (prim1 x6 x0) (explicit_Nats_one_plus x0 x1 x2 x3 x6 = x4) ⟶ x5) ⟶ x5))
Definition 09583.. := λ x0 x1 . λ x2 : ι → ι . λ x3 . and (prim1 x3 x0) (∀ x4 : ο . (∀ x5 . and (prim1 x5 x0) (x3 = explicit_Nats_one_plus x0 x1 x2 (x2 x1) x5) ⟶ x4) ⟶ x4)
Definition bf748.. := λ x0 x1 . λ x2 : ι → ι . λ x3 . and (prim1 x3 x0) (∀ x4 . prim1 x4 x0 ⟶ x3 = explicit_Nats_one_plus x0 x1 x2 (x2 x1) x4 ⟶ ∀ x5 : ο . x5)
Definition 900a2.. := λ x0 x1 . λ x2 : ι → ι . explicit_Nats_primrec x0 x1 x2 x1 (λ x3 x4 . If_i (and (x3 = x1 ⟶ ∀ x5 : ο . x5) (340be.. x0 x1 x2 x3 x3)) (x2 x4) x4)