Proofgold Address

Param odd_nat^odd_nat : ι → ο
Param equip^equip : ι → ι → ο
Definition and^and := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x1 ⟶ x2) ⟶ x2
Known d3cb5.. : ∀ x0 x1 . odd_nat x1 ⟶ equip x0 x1 ⟶ ∀ x2 : ι → ι . (∀ x3 . x3 ∈ x0 ⟶ x2 x3 ∈ x0) ⟶ (∀ x3 . x3 ∈ x0 ⟶ x2 (x2 x3) = x3) ⟶ ∀ x3 : ο . (∀ x4 . and (x4 ∈ x0) (x2 x4 = x4) ⟶ x3) ⟶ x3
Param nat_p^nat_p : ι → ο
Known 74e07.. : ∀ x0 . nat_p x0 ⟶ ∀ x1 . equip x0 x1 ⟶ ∀ x2 : ι → ι . (∀ x3 . x3 ∈ x1 ⟶ x2 x3 ∈ x1) ⟶ (∀ x3 . x3 ∈ x1 ⟶ x2 (x2 x3) = x3) ⟶ (∀ x3 : ο . (∀ x4 . and (x4 ∈ x1) (and (x2 x4 = x4) (∀ x5 . x5 ∈ x1 ⟶ x2 x5 = x5 ⟶ x4 = x5)) ⟶ x3) ⟶ x3) ⟶ odd_nat x0
Param SNo^SNo : ι → ο
Param mul_SNo^mul_SNo : ι → ι → ι
Param add_SNo^add_SNo : ι → ι → ι
Known 7bd74.. : ∀ x0 x1 x2 x3 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNo x3 ⟶ mul_SNo (add_SNo x0 (add_SNo x1 x2)) x3 = add_SNo (mul_SNo x0 x3) (add_SNo (mul_SNo x1 x3) (mul_SNo x2 x3))
Param ordsucc^ordsucc : ι → ι
Param minus_SNo^minus_SNo : ι → ι
Param omega^omega : ι
Param lam^Sigma : ι → (ι → ι) → ι
Param If_i^If_i : ο → ι → ι → ι
Param ap^ap : ι → ι → ι
Param SNoLt^SNoLt : ι → ι → ο
Known omega_nat_p^omega_nat_p : ∀ x0 . x0 ∈ omega ⟶ nat_p x0
Known equip_sym^equip_sym : ∀ x0 x1 . equip x0 x1 ⟶ equip x1 x0
Param ordinal^ordinal : ι → ο
Known ordinal_trichotomy_or_impred^{ordinal_trichotomy_or_impred} : ∀ x0 x1 . ordinal x0 ⟶ ordinal x1 ⟶ ∀ x2 : ο . (x0 ∈ x1 ⟶ x2) ⟶ (x0 = x1 ⟶ x2) ⟶ (x1 ∈ x0 ⟶ x2) ⟶ x2
Known nat_p_ordinal^{nat_p_ordinal} : ∀ x0 . nat_p x0 ⟶ ordinal x0
Known add_SNo_In_omega^{add_SNo_In_omega} : ∀ x0 . x0 ∈ omega ⟶ ∀ x1 . x1 ∈ omega ⟶ add_SNo x0 x1 ∈ omega
Known mul_SNo_In_omega^{mul_SNo_In_omega} : ∀ x0 . x0 ∈ omega ⟶ ∀ x1 . x1 ∈ omega ⟶ mul_SNo x0 x1 ∈ omega
Known nat_p_omega^nat_p_omega : ∀ x0 . nat_p x0 ⟶ x0 ∈ omega
Known nat_2^nat_2 : nat_p 2
Param int^int : ι
Param SNoLe^SNoLe : ι → ι → ο
Known aa7e8..^{nonneg_int_nat_p} : ∀ x0 . x0 ∈ int ⟶ SNoLe 0 x0 ⟶ nat_p x0
Known int_add_SNo^int_add_SNo : ∀ x0 . x0 ∈ int ⟶ ∀ x1 . x1 ∈ int ⟶ add_SNo x0 x1 ∈ int
Definition Subq^Subq := λ x0 x1 . ∀ x2 . x2 ∈ x0 ⟶ x2 ∈ x1
Known Subq_omega_int^{Subq_omega_int} : omega ⊆ int
Known int_minus_SNo^{int_minus_SNo} : ∀ x0 . x0 ∈ int ⟶ minus_SNo x0 ∈ int
Known 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))
Known omega_SNo^omega_SNo : ∀ x0 . x0 ∈ omega ⟶ SNo x0
Known SNo_add_SNo^SNo_add_SNo : ∀ x0 x1 . SNo x0 ⟶ SNo x1 ⟶ SNo (add_SNo x0 x1)
Known SNo_0^SNo_0 : SNo 0
Known add_SNo_0L^add_SNo_0L : ∀ x0 . SNo x0 ⟶ add_SNo 0 x0 = x0
Known SNoLtLe^SNoLtLe : ∀ x0 x1 . SNoLt x0 x1 ⟶ SNoLe x0 x1
Known ordinal_In_SNoLt^{ordinal_In_SNoLt} : ∀ x0 . ordinal x0 ⟶ ∀ x1 . x1 ∈ x0 ⟶ SNoLt x1 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 8b4bf.. : ∀ x0 x1 . SNo x0 ⟶ SNo x1 ⟶ mul_SNo (add_SNo x0 x1) (add_SNo x0 x1) = add_SNo (mul_SNo x0 x0) (add_SNo (mul_SNo 2 (mul_SNo x0 x1)) (mul_SNo x1 x1))
Known SNo_mul_SNo^SNo_mul_SNo : ∀ x0 x1 . SNo x0 ⟶ SNo x1 ⟶ SNo (mul_SNo x0 x1)
Known SNo_2^SNo_2 : SNo 2
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 mul_SNo_com_4_inner_mid^{mul_SNo_com_4_inner_mid} : ∀ x0 x1 x2 x3 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNo x3 ⟶ mul_SNo (mul_SNo x0 x1) (mul_SNo x2 x3) = mul_SNo (mul_SNo x0 x2) (mul_SNo x1 x3)
Known ecc46.. : mul_SNo 2 2 = 4
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
Known 48da5.. : SNo 4
Known add_SNo_rotate_3_1^{add_SNo_rotate_3_1} : ∀ x0 x1 x2 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ add_SNo x0 (add_SNo x1 x2) = add_SNo x2 (add_SNo x0 x1)
Known add_SNo_com^add_SNo_com : ∀ x0 x1 . SNo x0 ⟶ SNo x1 ⟶ add_SNo x0 x1 = add_SNo x1 x0
Known 55f68.. : ∀ x0 x1 x2 x3 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNo x3 ⟶ mul_SNo x3 (add_SNo x0 (add_SNo x1 x2)) = add_SNo (mul_SNo x3 x0) (add_SNo (mul_SNo x3 x1) (mul_SNo x3 x2))
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_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 SNo_minus_SNo^{SNo_minus_SNo} : ∀ x0 . SNo x0 ⟶ SNo (minus_SNo x0)
Definition False^False := ∀ x0 : ο . x0
Known FalseE^FalseE : False ⟶ ∀ x0 : ο . x0
Known add_SNo_minus_Lt2b3^{add_SNo_minus_Lt2b3} : ∀ x0 x1 x2 x3 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNo x3 ⟶ SNoLt (add_SNo x3 x2) (add_SNo x0 x1) ⟶ SNoLt x3 (add_SNo x0 (add_SNo x1 (minus_SNo x2)))
Known b5021.. : ∀ x0 x1 . SNo x0 ⟶ SNo x1 ⟶ mul_SNo (add_SNo x0 (minus_SNo x1)) (add_SNo x0 (minus_SNo x1)) = add_SNo (mul_SNo x0 x0) (add_SNo (minus_SNo (mul_SNo 2 (mul_SNo x0 x1))) (mul_SNo x1 x1))
Known SNo_add_SNo_3^{SNo_add_SNo_3} : ∀ x0 x1 x2 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNo (add_SNo x0 (add_SNo x1 x2))
Known add_SNo_rotate_5_1^{add_SNo_rotate_5_1} : ∀ x0 x1 x2 x3 x4 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNo x3 ⟶ SNo x4 ⟶ add_SNo x0 (add_SNo x1 (add_SNo x2 (add_SNo x3 x4))) = add_SNo x4 (add_SNo x0 (add_SNo x1 (add_SNo x2 x3)))
Known add_SNo_minus_SNo_linv^{add_SNo_minus_SNo_linv} : ∀ x0 . SNo x0 ⟶ add_SNo (minus_SNo x0) x0 = 0
Known add_SNo_0R^add_SNo_0R : ∀ x0 . SNo x0 ⟶ add_SNo x0 0 = x0
Known add_SNo_minus_L2^{add_SNo_minus_L2} : ∀ x0 x1 . SNo x0 ⟶ SNo x1 ⟶ add_SNo (minus_SNo x0) (add_SNo x0 x1) = x1
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 tuple_3_0_eq^tuple_3_0_eq : ∀ x0 x1 x2 . ap (lam 3 (λ x4 . If_i (x4 = 0) x0 (If_i (x4 = 1) x1 x2))) 0 = x0
Known tuple_3_1_eq^tuple_3_1_eq : ∀ x0 x1 x2 . ap (lam 3 (λ x4 . If_i (x4 = 0) x0 (If_i (x4 = 1) x1 x2))) 1 = x1
Known tuple_3_2_eq^tuple_3_2_eq : ∀ x0 x1 x2 . ap (lam 3 (λ x4 . If_i (x4 = 0) x0 (If_i (x4 = 1) x1 x2))) 2 = 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
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 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 d67ed.. : ∀ x0 . SNo x0 ⟶ mul_SNo 2 x0 = add_SNo x0 x0
Known minus_SNo_invol^{minus_SNo_invol} : ∀ x0 . SNo x0 ⟶ minus_SNo (minus_SNo x0) = x0
Known add_SNo_minus_SNo_rinv^{add_SNo_minus_SNo_rinv} : ∀ x0 . SNo x0 ⟶ add_SNo x0 (minus_SNo x0) = 0
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 andI^andI : ∀ x0 x1 : ο . x0 ⟶ x1 ⟶ and x0 x1
Known ordinal_SNoLt_In^{ordinal_SNoLt_In} : ∀ x0 x1 . ordinal x0 ⟶ ordinal x1 ⟶ SNoLt x0 x1 ⟶ x0 ∈ x1
Known add_SNo_Lt2^add_SNo_Lt2 : ∀ x0 x1 x2 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNoLt x1 x2 ⟶ SNoLt (add_SNo x0 x1) (add_SNo x0 x2)
Known add_SNo_Lt1^add_SNo_Lt1 : ∀ x0 x1 x2 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNoLt x0 x2 ⟶ SNoLt (add_SNo x0 x1) (add_SNo x2 x1)
Known minus_SNo_Lt_contra1^{minus_SNo_Lt_contra1} : ∀ x0 x1 . SNo x0 ⟶ SNo x1 ⟶ SNoLt (minus_SNo x0) x1 ⟶ SNoLt (minus_SNo x1) x0
Known minus_SNo_0^minus_SNo_0 : minus_SNo 0 = 0
Known int_mul_SNo^int_mul_SNo : ∀ x0 . x0 ∈ int ⟶ ∀ x1 . x1 ∈ int ⟶ mul_SNo x0 x1 ∈ int
Known nat_p_int^nat_p_int : ∀ x0 . nat_p x0 ⟶ x0 ∈ int
Theorem 91770.. : ∀ x0 x1 x2 : ι → ι → ι → ι . ∀ x3 x4 x5 : ι → ι → ι → ο . (∀ x6 x7 x8 . x3 x6 x7 x8 ⟶ x0 x6 x7 x8 = add_SNo x6 (mul_SNo 2 x8)) ⟶ (∀ x6 x7 x8 . x3 x6 x7 x8 ⟶ x1 x6 x7 x8 = x8) ⟶ (∀ x6 x7 x8 . x3 x6 x7 x8 ⟶ x2 x6 x7 x8 = add_SNo x7 (minus_SNo (add_SNo x6 x8))) ⟶ (∀ x6 x7 x8 . x4 x6 x7 x8 ⟶ x0 x6 x7 x8 = add_SNo (mul_SNo 2 x7) (minus_SNo x6)) ⟶ (∀ x6 x7 x8 . x4 x6 x7 x8 ⟶ x1 x6 x7 x8 = x7) ⟶ (∀ x6 x7 x8 . x4 x6 x7 x8 ⟶ x2 x6 x7 x8 = add_SNo x6 (add_SNo x8 (minus_SNo x7))) ⟶ (∀ x6 x7 x8 . x5 x6 x7 x8 ⟶ x0 x6 x7 x8 = add_SNo x6 (minus_SNo (mul_SNo 2 x7))) ⟶ (∀ x6 x7 x8 . x5 x6 x7 x8 ⟶ x1 x6 x7 x8 = add_SNo x6 (add_SNo x8 (minus_SNo x7))) ⟶ (∀ x6 x7 x8 . x5 x6 x7 x8 ⟶ x2 x6 x7 x8 = x7) ⟶ (∀ x6 x7 x8 . add_SNo x6 x8 ∈ x7 ⟶ x3 x6 x7 x8) ⟶ (∀ x6 x7 x8 . x3 x6 x7 x8 ⟶ add_SNo x6 x8 ∈ x7) ⟶ (∀ x6 x7 x8 . x7 ∈ add_SNo x6 x8 ⟶ x6 ∈ mul_SNo 2 x7 ⟶ x4 x6 x7 x8) ⟶ (∀ x6 x7 x8 . x4 x6 x7 x8 ⟶ x7 ∈ add_SNo x6 x8) ⟶ (∀ x6 x7 x8 . x4 x6 x7 x8 ⟶ x6 ∈ mul_SNo 2 x7) ⟶ (∀ x6 x7 x8 . x7 ∈ add_SNo x6 x8 ⟶ mul_SNo 2 x7 ∈ x6 ⟶ x5 x6 x7 x8) ⟶ (∀ x6 x7 x8 . x5 x6 x7 x8 ⟶ x7 ∈ add_SNo x6 x8) ⟶ (∀ x6 x7 x8 . x5 x6 x7 x8 ⟶ mul_SNo 2 x7 ∈ x6) ⟶ ∀ x6 . x6 ∈ omega ⟶ ∀ x7 . equip x7 x6 ⟶ (∀ x8 . x8 ∈ x7 ⟶ lam 3 (λ x10 . If_i (x10 = 0) (ap x8 0) (If_i (x10 = 1) (ap x8 1) (ap x8 2))) = x8) ⟶ (∀ x8 x9 x10 . lam 3 (λ x11 . If_i (x11 = 0) x8 (If_i (x11 = 1) x9 x10)) ∈ x7 ⟶ ∀ x11 : ο . (x8 ∈ omega ⟶ x9 ∈ omega ⟶ x10 ∈ omega ⟶ SNoLt 0 x8 ⟶ SNoLt 0 x9 ⟶ SNoLt 0 x10 ⟶ (add_SNo x8 x10 = x9 ⟶ ∀ x12 : ο . x12) ⟶ (x8 = mul_SNo 2 x9 ⟶ ∀ x12 : ο . x12) ⟶ lam 3 (λ x12 . If_i (x12 = 0) x8 (If_i (x12 = 1) x10 x9)) ∈ x7 ⟶ x11) ⟶ x11) ⟶ (∀ x8 x9 x10 x11 . x11 ∈ omega ⟶ ∀ x12 . x12 ∈ omega ⟶ ∀ x13 . x13 ∈ omega ⟶ lam 3 (λ x14 . If_i (x14 = 0) x8 (If_i (x14 = 1) x9 x10)) ∈ x7 ⟶ add_SNo (mul_SNo x11 x11) (mul_SNo 4 (mul_SNo x12 x13)) = add_SNo (mul_SNo x8 x8) (mul_SNo 4 (mul_SNo x9 x10)) ⟶ lam 3 (λ x14 . If_i (x14 = 0) x11 (If_i (x14 = 1) x12 x13)) ∈ x7) ⟶ ∀ x8 x9 x10 . lam 3 (λ x11 . If_i (x11 = 0) x8 (If_i (x11 = 1) x9 x10)) ∈ x7 ⟶ x0 x8 x9 x10 = x8 ⟶ x1 x8 x9 x10 = x9 ⟶ x2 x8 x9 x10 = x10 ⟶ (∀ x11 x12 x13 . lam 3 (λ x14 . If_i (x14 = 0) x11 (If_i (x14 = 1) x12 x13)) ∈ x7 ⟶ x0 x11 x12 x13 = x11 ⟶ x1 x11 x12 x13 = x12 ⟶ x2 x11 x12 x13 = x13 ⟶ and (and (x11 = x8) (x12 = x9)) (x13 = x10)) ⟶ ∀ x11 : ο . (∀ x12 . (∀ x13 : ο . (∀ x14 . lam 3 (λ x15 . If_i (x15 = 0) x12 (If_i (x15 = 1) x14 x14)) ∈ x7 ⟶ x13) ⟶ x13) ⟶ x11) ⟶ x11 (proof)