Param add_SNo^add_SNo : ι → ι → ι
Param ordsucc^ordsucc : ι → ι
Param omega^omega : ι
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
Param nat_p^nat_p : ι → ο
Known nat_p_omega^nat_p_omega : ∀ x0 . nat_p x0 ⟶ x0 ∈ omega
Known nat_4^nat_4 : nat_p 4
Known nat_3^nat_3 : nat_p 3
Known add_nat_SR^add_nat_SR : ∀ x0 x1 . nat_p x1 ⟶ add_nat x0 (ordsucc x1) = ordsucc (add_nat x0 x1)
Known nat_2^nat_2 : nat_p 2
Known nat_1^nat_1 : nat_p 1
Known nat_0^nat_0 : nat_p 0
Known add_nat_0R^add_nat_0R : ∀ x0 . add_nat x0 0 = x0
Theorem add_SNo_4_3^add_SNo_4_3 : add_SNo 4 3 = 7 (proof)
Param ordinal^ordinal : ι → ο
Known add_SNo_ordinal_SR^{add_SNo_ordinal_SR} : ∀ x0 . ordinal x0 ⟶ ∀ x1 . ordinal x1 ⟶ add_SNo x0 (ordsucc x1) = ordsucc (add_SNo x0 x1)
Known nat_p_ordinal^{nat_p_ordinal} : ∀ x0 . nat_p x0 ⟶ ordinal x0
Theorem add_SNo_4_4^add_SNo_4_4 : add_SNo 4 4 = 8 (proof)
Param int^int : ι
Definition Subq^Subq := λ x0 x1 . ∀ x2 . x2 ∈ x0 ⟶ x2 ∈ x1
Known Subq_omega_int^{Subq_omega_int} : omega ⊆ int
Theorem nat_p_int^nat_p_int : ∀ x0 . nat_p x0 ⟶ x0 ∈ int (proof)
Param minus_SNo^minus_SNo : ι → ι
Known int_minus_SNo_omega^{int_minus_SNo_omega} : ∀ x0 . x0 ∈ omega ⟶ minus_SNo x0 ∈ int
Theorem nat_p_int_minus_SNo^{nat_p_int_minus_SNo} : ∀ x0 . nat_p x0 ⟶ minus_SNo x0 ∈ int (proof)
Param SNo^SNo : ι → ο
Definition or^or := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x2) ⟶ (x1 ⟶ x2) ⟶ x2
Param PNoLt^PNoLt : ι → (ι → ο) → ι → (ι → ο) → ο
Param and^and : ο → ο → ο
Param PNoEq_^PNoEq_ : ι → (ι → ο) → (ι → ο) → ο
Definition PNoLe^PNoLe := λ x0 . λ x1 : ι → ο . λ x2 . λ x3 : ι → ο . or (PNoLt x0 x1 x2 x3) (and (x0 = x2) (PNoEq_ x0 x1 x3))
Param SNoLev^SNoLev : ι → ι
Definition SNoLe^SNoLe := λ x0 x1 . PNoLe (SNoLev x0) (λ x2 . x2 ∈ x0) (SNoLev x1) (λ x2 . x2 ∈ x1)
Known minus_SNo_invol^{minus_SNo_invol} : ∀ x0 . SNo x0 ⟶ minus_SNo (minus_SNo x0) = x0
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 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 minus_SNo_Le_contra^{minus_SNo_Le_contra} : ∀ x0 x1 . SNo x0 ⟶ SNo x1 ⟶ SNoLe x0 x1 ⟶ SNoLe (minus_SNo x1) (minus_SNo x0)
Known add_SNo_com^add_SNo_com : ∀ x0 x1 . SNo x0 ⟶ SNo x1 ⟶ add_SNo x0 x1 = add_SNo x1 x0
Theorem minus_SNo_Le_swap^{minus_SNo_Le_swap} : ∀ x0 x1 x2 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNoLe x0 (add_SNo x1 (minus_SNo x2)) ⟶ SNoLe (add_SNo x2 (minus_SNo x1)) (minus_SNo x0) (proof)
Theorem minus_SNo_Le_swap2^{minus_SNo_Le_swap2} : ∀ x0 x1 x2 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNoLe (minus_SNo x0) (add_SNo x1 (minus_SNo x2)) ⟶ SNoLe (add_SNo x2 (minus_SNo x1)) x0 (proof)
Param nat_primrec^nat_primrec : ι → (ι → ι → ι) → ι → ι
Definition finite_add_SNo^{finite_add_SNo} := λ x0 . λ x1 : ι → ι . nat_primrec 0 (λ x2 x3 . add_SNo x3 (x1 x2)) x0
Known nat_primrec_0^{nat_primrec_0} : ∀ x0 . ∀ x1 : ι → ι → ι . nat_primrec x0 x1 0 = x0
Theorem 7d69d.. : ∀ x0 : ι → ι . finite_add_SNo 0 x0 = 0 (proof)
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 73a8e.. : ∀ x0 : ι → ι . ∀ x1 . nat_p x1 ⟶ finite_add_SNo (ordsucc x1) x0 = add_SNo (finite_add_SNo x1 x0) (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_0^SNo_0 : SNo 0
Known ordsuccI2^ordsuccI2 : ∀ x0 . x0 ∈ ordsucc x0
Known ordsuccI1^ordsuccI1 : ∀ x0 . x0 ⊆ ordsucc x0
Theorem dc840.. : ∀ x0 . nat_p x0 ⟶ ∀ x1 : ι → ι . (∀ x2 . x2 ∈ x0 ⟶ SNo (x1 x2)) ⟶ SNo (finite_add_SNo x0 x1) (proof)
Theorem 055f8.. : ∀ x0 . nat_p x0 ⟶ ∀ x1 x2 : ι → ι . (∀ x3 . x3 ∈ x0 ⟶ x1 x3 = x2 x3) ⟶ finite_add_SNo x0 x1 = finite_add_SNo x0 x2 (proof)
Known add_SNo_0L^add_SNo_0L : ∀ x0 . SNo x0 ⟶ add_SNo 0 x0 = x0
Known In_0_1^In_0_1 : 0 ∈ 1
Known add_SNo_minus_SNo_rinv^{add_SNo_minus_SNo_rinv} : ∀ x0 . SNo x0 ⟶ add_SNo x0 (minus_SNo x0) = 0
Known nat_ordsucc^nat_ordsucc : ∀ x0 . nat_p x0 ⟶ nat_p (ordsucc x0)
Param If_i^If_i : ο → ι → ι → ι
Known add_SNo_assoc^{add_SNo_assoc} : ∀ x0 x1 x2 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ add_SNo x0 (add_SNo x1 x2) = add_SNo (add_SNo x0 x1) x2
Known ordsuccE^ordsuccE : ∀ x0 x1 . x1 ∈ ordsucc x0 ⟶ or (x1 ∈ x0) (x1 = x0)
Known ordinal_ordsucc_In^{ordinal_ordsucc_In} : ∀ x0 . ordinal x0 ⟶ ∀ x1 . x1 ∈ x0 ⟶ ordsucc x1 ∈ ordsucc x0
Known add_SNo_Le3^add_SNo_Le3 : ∀ x0 x1 x2 x3 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNo x3 ⟶ SNoLe x0 x2 ⟶ SNoLe x1 x3 ⟶ SNoLe (add_SNo x0 x1) (add_SNo x2 x3)
Known add_SNo_com_4_inner_mid^{add_SNo_com_4_inner_mid} : ∀ x0 x1 x2 x3 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNo x3 ⟶ add_SNo (add_SNo x0 x1) (add_SNo x2 x3) = add_SNo (add_SNo x0 x2) (add_SNo x1 x3)
Known add_SNo_0R^add_SNo_0R : ∀ x0 . SNo x0 ⟶ add_SNo x0 0 = x0
Definition False^False := ∀ x0 : ο . x0
Definition not^not := λ x0 : ο . x0 ⟶ False
Known If_i_0^If_i_0 : ∀ x0 : ο . ∀ x1 x2 . not x0 ⟶ If_i x0 x1 x2 = x2
Definition nIn^nIn := λ x0 x1 . not (x0 ∈ x1)
Known In_irref^In_irref : ∀ x0 . nIn x0 x0
Known If_i_1^If_i_1 : ∀ x0 : ο . ∀ x1 x2 . x0 ⟶ If_i x0 x1 x2 = x1
Known nat_0_in_ordsucc^{nat_0_in_ordsucc} : ∀ x0 . nat_p x0 ⟶ 0 ∈ ordsucc x0
Theorem SNo_idl_cycle_nonneg^{SNo_idl_cycle_nonneg} : ∀ x0 . nat_p x0 ⟶ ∀ x1 x2 : ι → ι . (∀ x3 . x3 ∈ ordsucc x0 ⟶ SNo (x1 x3)) ⟶ (∀ x3 . x3 ∈ ordsucc x0 ⟶ SNo (x2 x3)) ⟶ x1 (ordsucc x0) = x1 0 ⟶ (∀ x3 . x3 ∈ ordsucc x0 ⟶ SNoLe (add_SNo (x1 (ordsucc x3)) (minus_SNo (x1 x3))) (x2 x3)) ⟶ SNoLe 0 (finite_add_SNo (ordsucc x0) x2) (proof)
Param SNoLt^SNoLt : ι → ι → ο
Known SNoLt_irref^SNoLt_irref : ∀ x0 . not (SNoLt x0 x0)
Known SNoLeLt_tra^SNoLeLt_tra : ∀ x0 x1 x2 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNoLe x0 x1 ⟶ SNoLt x1 x2 ⟶ SNoLt x0 x2
Known SNo_add_SNo_4^{SNo_add_SNo_4} : ∀ x0 x1 x2 x3 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNo x3 ⟶ SNo (add_SNo x0 (add_SNo x1 (add_SNo x2 x3)))
Param ap^ap : ι → ι → ι
Param lam^Sigma : ι → (ι → ι) → ι
Known cases_4^cases_4 : ∀ x0 . x0 ∈ 4 ⟶ ∀ x1 : ι → ο . x1 0 ⟶ x1 1 ⟶ x1 2 ⟶ x1 3 ⟶ x1 x0
Known tuple_5_0_eq^tuple_5_0_eq : ∀ x0 x1 x2 x3 x4 . ap (lam 5 (λ x6 . If_i (x6 = 0) x0 (If_i (x6 = 1) x1 (If_i (x6 = 2) x2 (If_i (x6 = 3) x3 x4))))) 0 = x0
Known tuple_5_1_eq^tuple_5_1_eq : ∀ x0 x1 x2 x3 x4 . ap (lam 5 (λ x6 . If_i (x6 = 0) x0 (If_i (x6 = 1) x1 (If_i (x6 = 2) x2 (If_i (x6 = 3) x3 x4))))) 1 = x1
Known tuple_5_2_eq^tuple_5_2_eq : ∀ x0 x1 x2 x3 x4 . ap (lam 5 (λ x6 . If_i (x6 = 0) x0 (If_i (x6 = 1) x1 (If_i (x6 = 2) x2 (If_i (x6 = 3) x3 x4))))) 2 = x2
Known tuple_5_3_eq^tuple_5_3_eq : ∀ x0 x1 x2 x3 x4 . ap (lam 5 (λ x6 . If_i (x6 = 0) x0 (If_i (x6 = 1) x1 (If_i (x6 = 2) x2 (If_i (x6 = 3) x3 x4))))) 3 = x3
Known tuple_4_0_eq^tuple_4_0_eq : ∀ x0 x1 x2 x3 . ap (lam 4 (λ x5 . If_i (x5 = 0) x0 (If_i (x5 = 1) x1 (If_i (x5 = 2) x2 x3)))) 0 = x0
Known tuple_4_1_eq^tuple_4_1_eq : ∀ x0 x1 x2 x3 . ap (lam 4 (λ x5 . If_i (x5 = 0) x0 (If_i (x5 = 1) x1 (If_i (x5 = 2) x2 x3)))) 1 = x1
Known tuple_4_2_eq^tuple_4_2_eq : ∀ x0 x1 x2 x3 . ap (lam 4 (λ x5 . If_i (x5 = 0) x0 (If_i (x5 = 1) x1 (If_i (x5 = 2) x2 x3)))) 2 = x2
Known tuple_4_3_eq^tuple_4_3_eq : ∀ x0 x1 x2 x3 . ap (lam 4 (λ x5 . If_i (x5 = 0) x0 (If_i (x5 = 1) x1 (If_i (x5 = 2) x2 x3)))) 3 = x3
Known tuple_5_4_eq^tuple_5_4_eq : ∀ x0 x1 x2 x3 x4 . ap (lam 5 (λ x6 . If_i (x6 = 0) x0 (If_i (x6 = 1) x1 (If_i (x6 = 2) x2 (If_i (x6 = 3) x3 x4))))) 4 = x4
Known add_SNo_assoc_4^{add_SNo_assoc_4} : ∀ x0 x1 x2 x3 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNo x3 ⟶ add_SNo x0 (add_SNo x1 (add_SNo x2 x3)) = add_SNo (add_SNo x0 (add_SNo x1 x2)) x3
Theorem idl_negcycle_4^{idl_negcycle_4} : ∀ x0 x1 x2 x3 x4 x5 x6 x7 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNo x3 ⟶ SNo x4 ⟶ SNo x5 ⟶ SNo x6 ⟶ SNo x7 ⟶ SNoLt (add_SNo x4 (add_SNo x5 (add_SNo x6 x7))) 0 ⟶ SNoLe (add_SNo x1 (minus_SNo x0)) x4 ⟶ SNoLe (add_SNo x2 (minus_SNo x1)) x5 ⟶ SNoLe (add_SNo x3 (minus_SNo x2)) x6 ⟶ SNoLe (add_SNo x0 (minus_SNo x3)) x7 ⟶ False (proof)

Proofgold Address