Proofgold Address

Param and^and : ο → ο → ο
Definition inj^inj := λ x0 x1 . λ x2 : ι → ι . and (∀ x3 . x3 ∈ x0 ⟶ x2 x3 ∈ x1) (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ x2 x3 = x2 x4 ⟶ x3 = x4)
Definition surj^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 omega^omega : ι
Param ccad8.. : ι → ι → ο
Definition e93bf.. := λ x0 . ∀ x1 : ο . (∀ x2 . and (x2 ∈ omega) (ccad8.. x0 x2) ⟶ x1) ⟶ x1
Definition False^False := ∀ x0 : ο . x0
Definition not^not := λ x0 : ο . x0 ⟶ False
Definition f9373.. := λ x0 . not (e93bf.. x0)
Param mul_nat^mul_nat : ι → ι → ι
Definition divides_nat^divides_nat := λ x0 x1 . and (and (x0 ∈ omega) (x1 ∈ omega)) (∀ x2 : ο . (∀ x3 . and (x3 ∈ omega) (mul_nat x0 x3 = x1) ⟶ x2) ⟶ x2)
Param ordsucc^ordsucc : ι → ι
Param or^or : ο → ο → ο
Definition prime_nat^prime_nat := λ x0 . and (and (x0 ∈ omega) (1 ∈ x0)) (∀ x1 . x1 ∈ omega ⟶ divides_nat x1 x0 ⟶ or (x1 = 1) (x1 = x0))
Param setminus^setminus : ι → ι → ι
Definition coprime_nat^coprime_nat := λ x0 x1 . and (and (x0 ∈ omega) (x1 ∈ omega)) (∀ x2 . x2 ∈ setminus omega 1 ⟶ divides_nat x2 x0 ⟶ divides_nat x2 x1 ⟶ x2 = 1)
Param add_nat^add_nat : ι → ι → ι
Definition b3e62..^{equiv_nat_mod} := λ x0 x1 x2 . and (and (and (x0 ∈ omega) (x1 ∈ omega)) (x2 ∈ omega)) (or (∀ x3 : ο . (∀ x4 . and (x4 ∈ omega) (add_nat x0 (mul_nat x4 x2) = x1) ⟶ x3) ⟶ x3) (∀ x3 : ο . (∀ x4 . and (x4 ∈ omega) (add_nat x1 (mul_nat x4 x2) = x0) ⟶ x3) ⟶ x3))
Param nat_primrec^nat_primrec : ι → (ι → ι → ι) → ι → ι
Definition exp_nat^exp_nat := λ x0 . nat_primrec 1 (λ x1 . mul_nat x0)
Definition even_nat^even_nat := λ x0 . and (x0 ∈ omega) (∀ x1 : ο . (∀ x2 . and (x2 ∈ omega) (x0 = mul_nat 2 x2) ⟶ x1) ⟶ x1)
Definition odd_nat^odd_nat := λ x0 . and (x0 ∈ omega) (∀ x1 . x1 ∈ omega ⟶ x0 = mul_nat 2 x1 ⟶ ∀ x2 : ο . x2)
Definition nat_factorial^{nat_factorial} := nat_primrec 1 (λ x0 . mul_nat (ordsucc x0))
Param ap^ap : ι → ι → ι
Param lam^Sigma : ι → (ι → ι) → ι
Param If_i^If_i : ο → ι → ι → ι
Definition aa403.. := λ x0 . ap (nat_primrec (lam omega (λ x1 . If_i (x1 = 0) 1 0)) (λ x1 x2 . lam omega (λ x3 . If_i (x3 = 0) 1 (add_nat (ap x2 (prim3 x3)) (ap x2 x3)))) x0)
Param Sep^Sep : ι → (ι → ο) → ι
Definition 9ae2c.. := λ x0 . prim0 (λ x1 . and (x1 ∈ omega) (ccad8.. x1 {x2 ∈ ordsucc x0|and (0 ∈ x2) (coprime_nat x2 x0)}))
Param div_SNo^div_SNo : ι → ι → ι
Param mul_SNo^mul_SNo : ι → ι → ι
Param add_SNo^add_SNo : ι → ι → ι
Param minus_SNo^minus_SNo : ι → ι
Definition 4f8b9.. := λ x0 x1 . div_SNo (nat_factorial x0) (mul_SNo (nat_factorial (add_SNo x0 (minus_SNo x1))) (nat_factorial x1))
Param int_alt1^int : ι
Definition divides_int_alt1^divides_int := λ x0 x1 . and (and (x0 ∈ int_alt1) (x1 ∈ int_alt1)) (∀ x2 : ο . (∀ x3 . and (x3 ∈ int_alt1) (mul_SNo x0 x3 = x1) ⟶ x2) ⟶ x2)
Definition a0bc4..^{equiv_int_mod} := λ x0 x1 x2 . and (and (and (x0 ∈ int_alt1) (x1 ∈ int_alt1)) (x2 ∈ setminus omega 1)) (divides_int_alt1 (add_SNo x0 (minus_SNo x1)) x2)
Definition 76fc5..^coprime_int := λ x0 x1 . and (and (x0 ∈ int_alt1) (x1 ∈ int_alt1)) (∀ x2 . x2 ∈ setminus omega 1 ⟶ divides_int_alt1 x2 x0 ⟶ divides_int_alt1 x2 x1 ⟶ x2 = 1)
Definition exp_SNo_nat^exp_SNo_nat := λ x0 . nat_primrec 1 (λ x1 . mul_SNo x0)
Param explicit_Nats^{explicit_Nats} : ι → ι → (ι → ι) → ο
Param explicit_Nats_primrec^{explicit_Nats_primrec} : ι → ι → (ι → ι) → ι → (ι → ι → ι) → ι → ι
Param explicit_Nats_one_plus^{explicit_Nats_one_plus} : ι → ι → (ι → ι) → ι → ι → ι
Param explicit_Nats_one_plus^{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 (x3 ∈ x0) (x4 ∈ x0)) (∀ x5 : ο . (∀ x6 . and (x6 ∈ x0) (explicit_Nats_one_plus x0 x1 x2 x6 x3 = x4) ⟶ x5) ⟶ x5)
Definition 75de2.. := λ x0 x1 . λ x2 : ι → ι . λ x3 . and (x3 ∈ x0) (∀ x4 . x4 ∈ x0 ⟶ explicit_Nats_lt x0 x1 x2 x4 x3 ⟶ or (x4 = x1) (x4 = x3))
Definition explicit_Nats_max_is_one := λ x0 x1 . λ x2 : ι → ι . λ x3 x4 . and (and (x3 ∈ x0) (x4 ∈ x0)) (∀ x5 . x5 ∈ x0 ⟶ explicit_Nats_lt x0 x1 x2 x5 x3 ⟶ explicit_Nats_lt x0 x1 x2 x5 x4 ⟶ x5 = 1)
Definition a1fba.. := λ x0 x1 . λ x2 : ι → ι . λ x3 x4 x5 . and (and (and (x3 ∈ x0) (x4 ∈ x0)) (x5 ∈ x0)) (or (or (x3 = x4) (∀ x6 : ο . (∀ x7 . and (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 (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^{explicit_Nats_one_lt} := λ x0 x1 . λ x2 : ι → ι . λ x3 x4 . and (and (x3 ∈ x0) (x4 ∈ x0)) (∀ x5 : ο . (∀ x6 . and (x6 ∈ x0) (explicit_Nats_one_plus x0 x1 x2 x3 x6 = x4) ⟶ x5) ⟶ x5)
Definition explicit_Nats_one_le^{explicit_Nats_one_le} := λ x0 x1 . λ x2 : ι → ι . λ x3 x4 . and (and (x3 ∈ x0) (x4 ∈ x0)) (or (x3 = x4) (∀ x5 : ο . (∀ x6 . and (x6 ∈ x0) (explicit_Nats_one_plus x0 x1 x2 x3 x6 = x4) ⟶ x5) ⟶ x5))
Definition e6fc1.. := λ x0 x1 . λ x2 : ι → ι . λ x3 . and (x3 ∈ x0) (∀ x4 : ο . (∀ x5 . and (x5 ∈ x0) (x3 = explicit_Nats_one_plus x0 x1 x2 (x2 x1) x5) ⟶ x4) ⟶ x4)
Definition e7d21.. := λ x0 x1 . λ x2 : ι → ι . λ x3 . and (x3 ∈ x0) (∀ x4 . x4 ∈ x0 ⟶ x3 = explicit_Nats_one_plus x0 x1 x2 (x2 x1) x4 ⟶ ∀ x5 : ο . x5)
Definition 9ff99.. := λ x0 x1 . λ x2 : ι → ι . explicit_Nats_primrec x0 x1 x2 x1 (λ x3 x4 . If_i (and (x3 = x1 ⟶ ∀ x5 : ο . x5) (explicit_Nats_max_is_one x0 x1 x2 x3 x3)) (x2 x4) x4)