Proofgold Address

Definition and^and := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x1 ⟶ x2) ⟶ x2
Param omega^omega : ι
Param setminus^setminus : ι → ι → ι
Param ordsucc^ordsucc : ι → ι
Definition or^or := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x2) ⟶ (x1 ⟶ x2) ⟶ x2
Param add_nat^add_nat : ι → ι → ι
Param mul_nat^mul_nat : ι → ι → ι
Definition equiv_nat_mod := λ x0 x1 x2 . and (and (and (x0 ∈ omega) (x1 ∈ omega)) (x2 ∈ setminus omega 1)) (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 int_alt1^int : ι
Param mul_SNo^mul_SNo : ι → ι → ι
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)
Param add_SNo^add_SNo : ι → ι → ι
Param minus_SNo^minus_SNo : ι → ι
Definition 6ccc6.. := λ x0 x1 x2 . and (and (and (x0 ∈ int_alt1) (x1 ∈ int_alt1)) (x2 ∈ setminus omega 1)) (divides_int_alt1 x2 (add_SNo x0 (minus_SNo x1)))
Param SNo^SNo : ι → ο
Known and4I^and4I : ∀ x0 x1 x2 x3 : ο . x0 ⟶ x1 ⟶ x2 ⟶ x3 ⟶ and (and (and x0 x1) x2) x3
Definition Subq^Subq := λ x0 x1 . ∀ x2 . x2 ∈ x0 ⟶ x2 ∈ x1
Known c3d99..^{Subq_omega_int} : omega ⊆ int_alt1
Known and3I^and3I : ∀ x0 x1 x2 : ο . x0 ⟶ x1 ⟶ x2 ⟶ and (and x0 x1) x2
Known a0aa5..^int_add_SNo : ∀ x0 . x0 ∈ int_alt1 ⟶ ∀ x1 . x1 ∈ int_alt1 ⟶ add_SNo x0 x1 ∈ int_alt1
Known daaad..^{int_minus_SNo} : ∀ x0 . x0 ∈ int_alt1 ⟶ minus_SNo x0 ∈ int_alt1
Known mul_nat_mul_SNo^{mul_nat_mul_SNo} : ∀ x0 . x0 ∈ omega ⟶ ∀ x1 . x1 ∈ omega ⟶ mul_nat x0 x1 = mul_SNo x0 x1
Known add_nat_add_SNo^{add_nat_add_SNo} : ∀ x0 . x0 ∈ omega ⟶ ∀ x1 . x1 ∈ omega ⟶ add_nat x0 x1 = add_SNo x0 x1
Known mul_SNo_In_omega^{mul_SNo_In_omega} : ∀ x0 . x0 ∈ omega ⟶ ∀ x1 . x1 ∈ omega ⟶ mul_SNo x0 x1 ∈ omega
Known andI^andI : ∀ x0 x1 : ο . x0 ⟶ x1 ⟶ and x0 x1
Known 1b4d5..^{int_minus_SNo_omega} : ∀ x0 . x0 ∈ omega ⟶ minus_SNo x0 ∈ int_alt1
Known mul_SNo_minus_distrR^{mul_minus_SNo_distrR} : ∀ x0 x1 . SNo x0 ⟶ SNo x1 ⟶ mul_SNo x0 (minus_SNo x1) = minus_SNo (mul_SNo x0 x1)
Known mul_SNo_com^mul_SNo_com : ∀ x0 x1 . SNo x0 ⟶ SNo x1 ⟶ mul_SNo x0 x1 = mul_SNo x1 x0
Known add_SNo_cancel_R^{add_SNo_cancel_R} : ∀ x0 x1 x2 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ add_SNo x0 x1 = add_SNo x2 x1 ⟶ x0 = x2
Known SNo_minus_SNo^{SNo_minus_SNo} : ∀ x0 . SNo x0 ⟶ SNo (minus_SNo x0)
Known SNo_add_SNo^SNo_add_SNo : ∀ x0 x1 . SNo x0 ⟶ SNo x1 ⟶ SNo (add_SNo x0 x1)
Known add_SNo_minus_R2'^{add_SNo_minus_R2} : ∀ x0 x1 . SNo x0 ⟶ SNo x1 ⟶ add_SNo (add_SNo x0 (minus_SNo x1)) x1 = x0
Known add_SNo_com^add_SNo_com : ∀ x0 x1 . SNo x0 ⟶ SNo x1 ⟶ add_SNo x0 x1 = add_SNo x1 x0
Known add_SNo_minus_R2^{add_SNo_minus_R2} : ∀ x0 x1 . SNo x0 ⟶ SNo x1 ⟶ add_SNo (add_SNo x0 x1) (minus_SNo x1) = x0
Known SNo_mul_SNo^SNo_mul_SNo : ∀ x0 x1 . SNo x0 ⟶ SNo x1 ⟶ SNo (mul_SNo x0 x1)
Known omega_SNo^omega_SNo : ∀ x0 . x0 ∈ omega ⟶ SNo x0
Known setminusE1^setminusE1 : ∀ x0 x1 x2 . x2 ∈ setminus x0 x1 ⟶ x2 ∈ x0
Theorem aa221.. : ∀ x0 x1 x2 . equiv_nat_mod x0 x1 x2 ⟶ 6ccc6.. x0 x1 x2 (proof)
Known a3283..^{int_SNo_cases} : ∀ x0 : ι → ο . (∀ x1 . x1 ∈ omega ⟶ x0 x1) ⟶ (∀ x1 . x1 ∈ omega ⟶ x0 (minus_SNo x1)) ⟶ ∀ x1 . x1 ∈ int_alt1 ⟶ x0 x1
Known orIL^orIL : ∀ x0 x1 : ο . x0 ⟶ or x0 x1
Known minus_SNo_invol^{minus_SNo_invol} : ∀ x0 . SNo x0 ⟶ minus_SNo (minus_SNo x0) = x0
Known mul_SNo_minus_distrL^{mul_SNo_minus_distrL} : ∀ x0 x1 . SNo x0 ⟶ SNo x1 ⟶ mul_SNo (minus_SNo x0) x1 = minus_SNo (mul_SNo x0 x1)
Known minus_add_SNo_distr^{minus_add_SNo_distr} : ∀ x0 x1 . SNo x0 ⟶ SNo x1 ⟶ minus_SNo (add_SNo x0 x1) = add_SNo (minus_SNo x0) (minus_SNo x1)
Known add_SNo_minus_SNo_prop2^{add_SNo_minus_SNo_prop2} : ∀ x0 x1 . SNo x0 ⟶ SNo x1 ⟶ add_SNo x0 (add_SNo (minus_SNo x0) x1) = x1
Known orIR^orIR : ∀ x0 x1 : ο . x1 ⟶ or x0 x1
Known 0c7a0.. : ∀ x0 . x0 ∈ int_alt1 ⟶ SNo x0
Theorem 6db0d.. : ∀ x0 . x0 ∈ omega ⟶ ∀ x1 . x1 ∈ omega ⟶ ∀ x2 . 6ccc6.. x0 x1 x2 ⟶ equiv_nat_mod x0 x1 x2 (proof)