Param SNo^SNo : ι → ο
Param SNoLe^SNoLe : ι → ι → ο
Param add_SNo^add_SNo : ι → ι → ι
Param minus_SNo^minus_SNo : ι → ι
Definition or^or := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x2) ⟶ (x1 ⟶ x2) ⟶ x2
Param SNoLt^SNoLt : ι → ι → ο
Known SNoLeE^SNoLeE : ∀ x0 x1 . SNo x0 ⟶ SNo x1 ⟶ SNoLe x0 x1 ⟶ or (SNoLt x0 x1) (x0 = x1)
Known SNo_add_SNo^SNo_add_SNo : ∀ x0 x1 . SNo x0 ⟶ SNo x1 ⟶ SNo (add_SNo x0 x1)
Known SNo_minus_SNo^{SNo_minus_SNo} : ∀ x0 . SNo x0 ⟶ SNo (minus_SNo x0)
Known SNoLtLe^SNoLtLe : ∀ x0 x1 . SNoLt x0 x1 ⟶ SNoLe x0 x1
Known add_SNo_minus_Lt1^{add_SNo_minus_Lt1} : ∀ x0 x1 x2 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNoLt (add_SNo x0 (minus_SNo x1)) x2 ⟶ SNoLt x0 (add_SNo x2 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 SNoLe_ref^SNoLe_ref : ∀ x0 . SNoLe x0 x0
Theorem 05aff.. : ∀ x0 x1 x2 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNoLe (add_SNo x0 (minus_SNo x1)) x2 ⟶ SNoLe x0 (add_SNo x2 x1) (proof)
Known add_SNo_minus_Lt1b^{add_SNo_minus_Lt1b} : ∀ x0 x1 x2 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNoLt x0 (add_SNo x2 x1) ⟶ SNoLt (add_SNo x0 (minus_SNo x1)) x2
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
Theorem add_SNo_minus_Le1b^{add_SNo_minus_Le1b} : ∀ x0 x1 x2 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNoLe x0 (add_SNo x2 x1) ⟶ SNoLe (add_SNo x0 (minus_SNo x1)) x2 (proof)
Known add_SNo_minus_Lt2^{add_SNo_minus_Lt2} : ∀ x0 x1 x2 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNoLt x2 (add_SNo x0 (minus_SNo x1)) ⟶ SNoLt (add_SNo x2 x1) x0
Theorem add_SNo_minus_Le2^{add_SNo_minus_Le2} : ∀ x0 x1 x2 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNoLe x2 (add_SNo x0 (minus_SNo x1)) ⟶ SNoLe (add_SNo x2 x1) x0 (proof)
Known add_SNo_minus_Lt2b^{add_SNo_minus_Lt2b} : ∀ x0 x1 x2 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNoLt (add_SNo x2 x1) x0 ⟶ SNoLt x2 (add_SNo x0 (minus_SNo x1))
Theorem add_SNo_minus_Le2b^{add_SNo_minus_Le2b} : ∀ x0 x1 x2 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNoLe (add_SNo x2 x1) x0 ⟶ SNoLe x2 (add_SNo x0 (minus_SNo x1)) (proof)
Param nat_primrec^nat_primrec : ι → (ι → ι → ι) → ι → ι
Param ordsucc^ordsucc : ι → ι
Param mul_SNo^mul_SNo : ι → ι → ι
Definition exp_SNo_nat^exp_SNo_nat := λ x0 . nat_primrec 1 (λ x1 . mul_SNo x0)
Known nat_primrec_0^{nat_primrec_0} : ∀ x0 . ∀ x1 : ι → ι → ι . nat_primrec x0 x1 0 = x0
Theorem exp_SNo_nat_0^{exp_SNo_nat_0} : ∀ x0 . SNo x0 ⟶ exp_SNo_nat x0 0 = 1 (proof)
Param nat_p^nat_p : ι → ο
Known nat_primrec_S^{nat_primrec_S} : ∀ x0 . ∀ x1 : ι → ι → ι . ∀ x2 . nat_p x2 ⟶ nat_primrec x0 x1 (ordsucc x2) = x1 x2 (nat_primrec x0 x1 x2)
Theorem exp_SNo_nat_S^{exp_SNo_nat_S} : ∀ x0 . SNo x0 ⟶ ∀ x1 . nat_p x1 ⟶ exp_SNo_nat x0 (ordsucc x1) = mul_SNo x0 (exp_SNo_nat x0 x1) (proof)
Known nat_ind^nat_ind : ∀ x0 : ι → ο . x0 0 ⟶ (∀ x1 . nat_p x1 ⟶ x0 x1 ⟶ x0 (ordsucc x1)) ⟶ ∀ x1 . nat_p x1 ⟶ x0 x1
Known SNo_1^SNo_1 : SNo 1
Known SNo_mul_SNo^SNo_mul_SNo : ∀ x0 x1 . SNo x0 ⟶ SNo x1 ⟶ SNo (mul_SNo x0 x1)
Theorem SNo_exp_SNo_nat^{SNo_exp_SNo_nat} : ∀ x0 . SNo x0 ⟶ ∀ x1 . nat_p x1 ⟶ SNo (exp_SNo_nat x0 x1) (proof)
Known nat_p_SNo^nat_p_SNo : ∀ x0 . nat_p x0 ⟶ SNo x0
Known nat_1^nat_1 : nat_p 1
Param omega^omega : ι
Param mul_nat^mul_nat : ι → ι → ι
Known mul_nat_mul_SNo^{mul_nat_mul_SNo} : ∀ x0 . x0 ∈ omega ⟶ ∀ x1 . x1 ∈ omega ⟶ mul_nat x0 x1 = mul_SNo x0 x1
Known nat_p_omega^nat_p_omega : ∀ x0 . nat_p x0 ⟶ x0 ∈ omega
Known mul_nat_p^mul_nat_p : ∀ x0 . nat_p x0 ⟶ ∀ x1 . nat_p x1 ⟶ nat_p (mul_nat x0 x1)
Theorem nat_exp_SNo_nat^{nat_exp_SNo_nat} : ∀ x0 . nat_p x0 ⟶ ∀ x1 . nat_p x1 ⟶ nat_p (exp_SNo_nat x0 x1) (proof)
Param eps_^eps_ : ι → ι
Known eps_0_1^eps_0_1 : eps_ 0 = 1
Known SNo_2^SNo_2 : SNo 2
Known mul_SNo_oneR^mul_SNo_oneR : ∀ x0 . SNo x0 ⟶ mul_SNo x0 1 = x0
Known mul_SNo_assoc^{mul_SNo_assoc} : ∀ x0 x1 x2 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ mul_SNo x0 (mul_SNo x1 x2) = mul_SNo (mul_SNo x0 x1) x2
Known add_SNo_1_1_2^{add_SNo_1_1_2} : add_SNo 1 1 = 2
Known mul_SNo_distrL^{mul_SNo_distrL} : ∀ x0 x1 x2 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ mul_SNo x0 (add_SNo x1 x2) = add_SNo (mul_SNo x0 x1) (mul_SNo x0 x2)
Known eps_ordsucc_half_add^{eps_ordsucc_half_add} : ∀ x0 . nat_p x0 ⟶ add_SNo (eps_ (ordsucc x0)) (eps_ (ordsucc x0)) = eps_ x0
Known SNo_eps_^SNo_eps_ : ∀ x0 . x0 ∈ omega ⟶ SNo (eps_ x0)
Known nat_ordsucc^nat_ordsucc : ∀ x0 . nat_p x0 ⟶ nat_p (ordsucc x0)
Theorem mul_SNo_eps_power_2^{mul_SNo_eps_power_2} : ∀ x0 . nat_p x0 ⟶ mul_SNo (eps_ x0) (exp_SNo_nat 2 x0) = 1 (proof)
Known mul_SNo_com^mul_SNo_com : ∀ x0 x1 . SNo x0 ⟶ SNo x1 ⟶ mul_SNo x0 x1 = mul_SNo x1 x0
Theorem mul_SNo_eps_power_2'^{mul_SNo_eps_power_2} : ∀ x0 . nat_p x0 ⟶ mul_SNo (exp_SNo_nat 2 x0) (eps_ x0) = 1 (proof)
Known add_SNo_0R^add_SNo_0R : ∀ x0 . SNo x0 ⟶ add_SNo x0 0 = x0
Param add_nat^add_nat : ι → ι → ι
Known add_nat_add_SNo^{add_nat_add_SNo} : ∀ x0 . x0 ∈ omega ⟶ ∀ x1 . x1 ∈ omega ⟶ add_nat x0 x1 = add_SNo x0 x1
Known omega_ordsucc^{omega_ordsucc} : ∀ x0 . x0 ∈ omega ⟶ ordsucc x0 ∈ omega
Known add_nat_SR^add_nat_SR : ∀ x0 x1 . nat_p x1 ⟶ add_nat x0 (ordsucc x1) = ordsucc (add_nat x0 x1)
Known add_nat_p^add_nat_p : ∀ x0 . nat_p x0 ⟶ ∀ x1 . nat_p x1 ⟶ nat_p (add_nat x0 x1)
Theorem exp_SNo_nat_mul_add^{exp_SNo_nat_mul_add} : ∀ x0 . SNo x0 ⟶ ∀ x1 . nat_p x1 ⟶ ∀ x2 . nat_p x2 ⟶ mul_SNo (exp_SNo_nat x0 x1) (exp_SNo_nat x0 x2) = exp_SNo_nat x0 (add_SNo x1 x2) (proof)
Known omega_nat_p^omega_nat_p : ∀ x0 . x0 ∈ omega ⟶ nat_p x0
Theorem exp_SNo_nat_mul_add'^{exp_SNo_nat_mul_add} : ∀ x0 . SNo x0 ⟶ ∀ x1 . x1 ∈ omega ⟶ ∀ x2 . x2 ∈ omega ⟶ mul_SNo (exp_SNo_nat x0 x1) (exp_SNo_nat x0 x2) = exp_SNo_nat x0 (add_SNo x1 x2) (proof)
Known SNoLt_0_1^SNoLt_0_1 : SNoLt 0 1
Known mul_SNo_zeroR^{mul_SNo_zeroR} : ∀ x0 . SNo x0 ⟶ mul_SNo x0 0 = 0
Known pos_mul_SNo_Lt^{pos_mul_SNo_Lt} : ∀ x0 x1 x2 . SNo x0 ⟶ SNoLt 0 x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNoLt x1 x2 ⟶ SNoLt (mul_SNo x0 x1) (mul_SNo x0 x2)
Known SNo_0^SNo_0 : SNo 0
Theorem exp_SNo_nat_pos^{exp_SNo_nat_pos} : ∀ x0 . SNo x0 ⟶ SNoLt 0 x0 ⟶ ∀ x1 . nat_p x1 ⟶ SNoLt 0 (exp_SNo_nat x0 x1) (proof)
Known SNoLt_trichotomy_or_impred^{SNoLt_trichotomy_or_impred} : ∀ x0 x1 . SNo x0 ⟶ SNo x1 ⟶ ∀ x2 : ο . (SNoLt x0 x1 ⟶ x2) ⟶ (x0 = x1 ⟶ x2) ⟶ (SNoLt x1 x0 ⟶ x2) ⟶ x2
Definition False^False := ∀ x0 : ο . x0
Known FalseE^FalseE : False ⟶ ∀ x0 : ο . x0
Definition not^not := λ x0 : ο . x0 ⟶ False
Known SNoLt_irref^SNoLt_irref : ∀ x0 . not (SNoLt x0 x0)
Known neg_mul_SNo_Lt^{neg_mul_SNo_Lt} : ∀ x0 x1 x2 . SNo x0 ⟶ SNoLt x0 0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNoLt x2 x1 ⟶ SNoLt (mul_SNo x0 x1) (mul_SNo x0 x2)
Theorem mul_SNo_nonzero_cancel^{mul_SNo_nonzero_cancel_L} : ∀ x0 x1 x2 . SNo x0 ⟶ (x0 = 0 ⟶ ∀ x3 : ο . x3) ⟶ SNo x1 ⟶ SNo x2 ⟶ mul_SNo x0 x1 = mul_SNo x0 x2 ⟶ x1 = x2 (proof)
Known SNoLt_0_2^SNoLt_0_2 : SNoLt 0 2
Known add_SNo_In_omega^{add_SNo_In_omega} : ∀ x0 . x0 ∈ omega ⟶ ∀ x1 . x1 ∈ omega ⟶ add_SNo x0 x1 ∈ omega
Known mul_SNo_oneL^mul_SNo_oneL : ∀ x0 . SNo x0 ⟶ mul_SNo 1 x0 = x0
Theorem mul_SNo_eps_eps_add_SNo^{mul_SNo_eps_eps_add_SNo} : ∀ x0 . x0 ∈ omega ⟶ ∀ x1 . x1 ∈ omega ⟶ mul_SNo (eps_ x0) (eps_ x1) = eps_ (add_SNo x0 x1) (proof)

Proofgold Address