Proofgold Address

Param SNo^SNo : ι → ο
Param SNoLt^SNoLt : ι → ι → ο
Param add_SNo^add_SNo : ι → ι → ι
Param SNoLe^SNoLe : ι → ι → ο
Param minus_SNo^minus_SNo : ι → ι
Definition False^False := ∀ x0 : ο . x0
Known idl_negcycle_6^{idl_negcycle_6} : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNo x3 ⟶ SNo x4 ⟶ SNo x5 ⟶ SNo x6 ⟶ SNo x7 ⟶ SNo x8 ⟶ SNo x9 ⟶ SNo x10 ⟶ SNo x11 ⟶ SNoLt (add_SNo x6 (add_SNo x7 (add_SNo x8 (add_SNo x9 (add_SNo x10 x11))))) 0 ⟶ SNoLe (add_SNo x1 (minus_SNo x0)) x6 ⟶ SNoLe (add_SNo x2 (minus_SNo x1)) x7 ⟶ SNoLe (add_SNo x3 (minus_SNo x2)) x8 ⟶ SNoLe (add_SNo x4 (minus_SNo x3)) x9 ⟶ SNoLe (add_SNo x5 (minus_SNo x4)) x10 ⟶ SNoLe (add_SNo x0 (minus_SNo x5)) x11 ⟶ False
Known minus_SNo_Lt_contra3^{minus_SNo_Lt_contra3} : ∀ x0 x1 . SNo x0 ⟶ SNo x1 ⟶ SNoLt (minus_SNo x0) (minus_SNo x1) ⟶ SNoLt x1 x0
Known SNo_0^SNo_0 : SNo 0
Known SNo_add_SNo_6^{SNo_add_SNo_6} : ∀ x0 x1 x2 x3 x4 x5 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNo x3 ⟶ SNo x4 ⟶ SNo x5 ⟶ SNo (add_SNo x0 (add_SNo x1 (add_SNo x2 (add_SNo x3 (add_SNo x4 x5)))))
Known minus_SNo_0^minus_SNo_0 : minus_SNo 0 = 0
Known minus_add_SNo_distr_m_5^{minus_add_SNo_distr_m_5} : ∀ x0 x1 x2 x3 x4 x5 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNo x3 ⟶ SNo x4 ⟶ SNo x5 ⟶ minus_SNo (add_SNo (minus_SNo x0) (add_SNo (minus_SNo x1) (add_SNo (minus_SNo x2) (add_SNo (minus_SNo x3) (add_SNo (minus_SNo x4) x5))))) = add_SNo x0 (add_SNo x1 (add_SNo x2 (add_SNo x3 (add_SNo x4 (minus_SNo x5)))))
Known minus_SNo_invol^{minus_SNo_invol} : ∀ x0 . SNo x0 ⟶ minus_SNo (minus_SNo x0) = x0
Known 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)
Known SNo_minus_SNo^{SNo_minus_SNo} : ∀ x0 . SNo x0 ⟶ SNo (minus_SNo x0)
Theorem a64b2.. : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNo x3 ⟶ SNo x4 ⟶ SNo x5 ⟶ SNo x6 ⟶ SNo x7 ⟶ SNo x8 ⟶ SNo x9 ⟶ SNo x10 ⟶ SNo x11 ⟶ SNoLt 0 (add_SNo x6 (add_SNo x7 (add_SNo x8 (add_SNo x9 (add_SNo x10 x11))))) ⟶ SNoLe x6 (add_SNo x0 (minus_SNo x1)) ⟶ SNoLe x7 (add_SNo x1 (minus_SNo x2)) ⟶ SNoLe x8 (add_SNo x2 (minus_SNo x3)) ⟶ SNoLe x9 (add_SNo x3 (minus_SNo x4)) ⟶ SNoLe x10 (add_SNo x4 (minus_SNo x5)) ⟶ SNoLe x11 (add_SNo x5 (minus_SNo x0)) ⟶ False (proof)
Known idl_negcycle_7^{idl_negcycle_7} : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNo x3 ⟶ SNo x4 ⟶ SNo x5 ⟶ SNo x6 ⟶ SNo x7 ⟶ SNo x8 ⟶ SNo x9 ⟶ SNo x10 ⟶ SNo x11 ⟶ SNo x12 ⟶ SNo x13 ⟶ SNoLt (add_SNo x7 (add_SNo x8 (add_SNo x9 (add_SNo x10 (add_SNo x11 (add_SNo x12 x13)))))) 0 ⟶ SNoLe (add_SNo x1 (minus_SNo x0)) x7 ⟶ SNoLe (add_SNo x2 (minus_SNo x1)) x8 ⟶ SNoLe (add_SNo x3 (minus_SNo x2)) x9 ⟶ SNoLe (add_SNo x4 (minus_SNo x3)) x10 ⟶ SNoLe (add_SNo x5 (minus_SNo x4)) x11 ⟶ SNoLe (add_SNo x6 (minus_SNo x5)) x12 ⟶ SNoLe (add_SNo x0 (minus_SNo x6)) x13 ⟶ False
Known SNo_add_SNo_7^{SNo_add_SNo_7} : ∀ x0 x1 x2 x3 x4 x5 x6 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNo x3 ⟶ SNo x4 ⟶ SNo x5 ⟶ SNo x6 ⟶ SNo (add_SNo x0 (add_SNo x1 (add_SNo x2 (add_SNo x3 (add_SNo x4 (add_SNo x5 x6))))))
Known minus_add_SNo_distr_m_6^{minus_add_SNo_distr_m_6} : ∀ x0 x1 x2 x3 x4 x5 x6 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNo x3 ⟶ SNo x4 ⟶ SNo x5 ⟶ SNo x6 ⟶ minus_SNo (add_SNo (minus_SNo x0) (add_SNo (minus_SNo x1) (add_SNo (minus_SNo x2) (add_SNo (minus_SNo x3) (add_SNo (minus_SNo x4) (add_SNo (minus_SNo x5) x6)))))) = add_SNo x0 (add_SNo x1 (add_SNo x2 (add_SNo x3 (add_SNo x4 (add_SNo x5 (minus_SNo x6))))))
Theorem 77fa4.. : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNo x3 ⟶ SNo x4 ⟶ SNo x5 ⟶ SNo x6 ⟶ SNo x7 ⟶ SNo x8 ⟶ SNo x9 ⟶ SNo x10 ⟶ SNo x11 ⟶ SNo x12 ⟶ SNo x13 ⟶ SNoLt 0 (add_SNo x7 (add_SNo x8 (add_SNo x9 (add_SNo x10 (add_SNo x11 (add_SNo x12 x13)))))) ⟶ SNoLe x7 (add_SNo x0 (minus_SNo x1)) ⟶ SNoLe x8 (add_SNo x1 (minus_SNo x2)) ⟶ SNoLe x9 (add_SNo x2 (minus_SNo x3)) ⟶ SNoLe x10 (add_SNo x3 (minus_SNo x4)) ⟶ SNoLe x11 (add_SNo x4 (minus_SNo x5)) ⟶ SNoLe x12 (add_SNo x5 (minus_SNo x6)) ⟶ SNoLe x13 (add_SNo x6 (minus_SNo x0)) ⟶ False (proof)
Known idl_negcycle_8^{idl_negcycle_8} : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNo x3 ⟶ SNo x4 ⟶ SNo x5 ⟶ SNo x6 ⟶ SNo x7 ⟶ SNo x8 ⟶ SNo x9 ⟶ SNo x10 ⟶ SNo x11 ⟶ SNo x12 ⟶ SNo x13 ⟶ SNo x14 ⟶ SNo x15 ⟶ SNoLt (add_SNo x8 (add_SNo x9 (add_SNo x10 (add_SNo x11 (add_SNo x12 (add_SNo x13 (add_SNo x14 x15))))))) 0 ⟶ SNoLe (add_SNo x1 (minus_SNo x0)) x8 ⟶ SNoLe (add_SNo x2 (minus_SNo x1)) x9 ⟶ SNoLe (add_SNo x3 (minus_SNo x2)) x10 ⟶ SNoLe (add_SNo x4 (minus_SNo x3)) x11 ⟶ SNoLe (add_SNo x5 (minus_SNo x4)) x12 ⟶ SNoLe (add_SNo x6 (minus_SNo x5)) x13 ⟶ SNoLe (add_SNo x7 (minus_SNo x6)) x14 ⟶ SNoLe (add_SNo x0 (minus_SNo x7)) x15 ⟶ False
Known SNo_add_SNo_8^{SNo_add_SNo_8} : ∀ x0 x1 x2 x3 x4 x5 x6 x7 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNo x3 ⟶ SNo x4 ⟶ SNo x5 ⟶ SNo x6 ⟶ SNo x7 ⟶ SNo (add_SNo x0 (add_SNo x1 (add_SNo x2 (add_SNo x3 (add_SNo x4 (add_SNo x5 (add_SNo x6 x7)))))))
Known minus_add_SNo_distr_m_7^{minus_add_SNo_distr_m_7} : ∀ x0 x1 x2 x3 x4 x5 x6 x7 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNo x3 ⟶ SNo x4 ⟶ SNo x5 ⟶ SNo x6 ⟶ SNo x7 ⟶ minus_SNo (add_SNo (minus_SNo x0) (add_SNo (minus_SNo x1) (add_SNo (minus_SNo x2) (add_SNo (minus_SNo x3) (add_SNo (minus_SNo x4) (add_SNo (minus_SNo x5) (add_SNo (minus_SNo x6) x7))))))) = add_SNo x0 (add_SNo x1 (add_SNo x2 (add_SNo x3 (add_SNo x4 (add_SNo x5 (add_SNo x6 (minus_SNo x7)))))))
Theorem 904ea.. : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNo x3 ⟶ SNo x4 ⟶ SNo x5 ⟶ SNo x6 ⟶ SNo x7 ⟶ SNo x8 ⟶ SNo x9 ⟶ SNo x10 ⟶ SNo x11 ⟶ SNo x12 ⟶ SNo x13 ⟶ SNo x14 ⟶ SNo x15 ⟶ SNoLt 0 (add_SNo x8 (add_SNo x9 (add_SNo x10 (add_SNo x11 (add_SNo x12 (add_SNo x13 (add_SNo x14 x15))))))) ⟶ SNoLe x8 (add_SNo x0 (minus_SNo x1)) ⟶ SNoLe x9 (add_SNo x1 (minus_SNo x2)) ⟶ SNoLe x10 (add_SNo x2 (minus_SNo x3)) ⟶ SNoLe x11 (add_SNo x3 (minus_SNo x4)) ⟶ SNoLe x12 (add_SNo x4 (minus_SNo x5)) ⟶ SNoLe x13 (add_SNo x5 (minus_SNo x6)) ⟶ SNoLe x14 (add_SNo x6 (minus_SNo x7)) ⟶ SNoLe x15 (add_SNo x7 (minus_SNo x0)) ⟶ False (proof)
Known idl_negcycle_9^{idl_negcycle_9} : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNo x3 ⟶ SNo x4 ⟶ SNo x5 ⟶ SNo x6 ⟶ SNo x7 ⟶ SNo x8 ⟶ SNo x9 ⟶ SNo x10 ⟶ SNo x11 ⟶ SNo x12 ⟶ SNo x13 ⟶ SNo x14 ⟶ SNo x15 ⟶ SNo x16 ⟶ SNo x17 ⟶ SNoLt (add_SNo x9 (add_SNo x10 (add_SNo x11 (add_SNo x12 (add_SNo x13 (add_SNo x14 (add_SNo x15 (add_SNo x16 x17)))))))) 0 ⟶ SNoLe (add_SNo x1 (minus_SNo x0)) x9 ⟶ SNoLe (add_SNo x2 (minus_SNo x1)) x10 ⟶ SNoLe (add_SNo x3 (minus_SNo x2)) x11 ⟶ SNoLe (add_SNo x4 (minus_SNo x3)) x12 ⟶ SNoLe (add_SNo x5 (minus_SNo x4)) x13 ⟶ SNoLe (add_SNo x6 (minus_SNo x5)) x14 ⟶ SNoLe (add_SNo x7 (minus_SNo x6)) x15 ⟶ SNoLe (add_SNo x8 (minus_SNo x7)) x16 ⟶ SNoLe (add_SNo x0 (minus_SNo x8)) x17 ⟶ False
Known SNo_add_SNo_9^{SNo_add_SNo_9} : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNo x3 ⟶ SNo x4 ⟶ SNo x5 ⟶ SNo x6 ⟶ SNo x7 ⟶ SNo x8 ⟶ SNo (add_SNo x0 (add_SNo x1 (add_SNo x2 (add_SNo x3 (add_SNo x4 (add_SNo x5 (add_SNo x6 (add_SNo x7 x8))))))))
Known minus_add_SNo_distr_m_8^{minus_add_SNo_distr_m_8} : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNo x3 ⟶ SNo x4 ⟶ SNo x5 ⟶ SNo x6 ⟶ SNo x7 ⟶ SNo x8 ⟶ minus_SNo (add_SNo (minus_SNo x0) (add_SNo (minus_SNo x1) (add_SNo (minus_SNo x2) (add_SNo (minus_SNo x3) (add_SNo (minus_SNo x4) (add_SNo (minus_SNo x5) (add_SNo (minus_SNo x6) (add_SNo (minus_SNo x7) x8)))))))) = add_SNo x0 (add_SNo x1 (add_SNo x2 (add_SNo x3 (add_SNo x4 (add_SNo x5 (add_SNo x6 (add_SNo x7 (minus_SNo x8))))))))
Theorem e8183.. : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNo x3 ⟶ SNo x4 ⟶ SNo x5 ⟶ SNo x6 ⟶ SNo x7 ⟶ SNo x8 ⟶ SNo x9 ⟶ SNo x10 ⟶ SNo x11 ⟶ SNo x12 ⟶ SNo x13 ⟶ SNo x14 ⟶ SNo x15 ⟶ SNo x16 ⟶ SNo x17 ⟶ SNoLt 0 (add_SNo x9 (add_SNo x10 (add_SNo x11 (add_SNo x12 (add_SNo x13 (add_SNo x14 (add_SNo x15 (add_SNo x16 x17)))))))) ⟶ SNoLe x9 (add_SNo x0 (minus_SNo x1)) ⟶ SNoLe x10 (add_SNo x1 (minus_SNo x2)) ⟶ SNoLe x11 (add_SNo x2 (minus_SNo x3)) ⟶ SNoLe x12 (add_SNo x3 (minus_SNo x4)) ⟶ SNoLe x13 (add_SNo x4 (minus_SNo x5)) ⟶ SNoLe x14 (add_SNo x5 (minus_SNo x6)) ⟶ SNoLe x15 (add_SNo x6 (minus_SNo x7)) ⟶ SNoLe x16 (add_SNo x7 (minus_SNo x8)) ⟶ SNoLe x17 (add_SNo x8 (minus_SNo x0)) ⟶ False (proof)
Known idl_negcycle_10^{idl_negcycle_10} : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNo x3 ⟶ SNo x4 ⟶ SNo x5 ⟶ SNo x6 ⟶ SNo x7 ⟶ SNo x8 ⟶ SNo x9 ⟶ SNo x10 ⟶ SNo x11 ⟶ SNo x12 ⟶ SNo x13 ⟶ SNo x14 ⟶ SNo x15 ⟶ SNo x16 ⟶ SNo x17 ⟶ SNo x18 ⟶ SNo x19 ⟶ SNoLt (add_SNo x10 (add_SNo x11 (add_SNo x12 (add_SNo x13 (add_SNo x14 (add_SNo x15 (add_SNo x16 (add_SNo x17 (add_SNo x18 x19))))))))) 0 ⟶ SNoLe (add_SNo x1 (minus_SNo x0)) x10 ⟶ SNoLe (add_SNo x2 (minus_SNo x1)) x11 ⟶ SNoLe (add_SNo x3 (minus_SNo x2)) x12 ⟶ SNoLe (add_SNo x4 (minus_SNo x3)) x13 ⟶ SNoLe (add_SNo x5 (minus_SNo x4)) x14 ⟶ SNoLe (add_SNo x6 (minus_SNo x5)) x15 ⟶ SNoLe (add_SNo x7 (minus_SNo x6)) x16 ⟶ SNoLe (add_SNo x8 (minus_SNo x7)) x17 ⟶ SNoLe (add_SNo x9 (minus_SNo x8)) x18 ⟶ SNoLe (add_SNo x0 (minus_SNo x9)) x19 ⟶ False
Known SNo_add_SNo_10^{SNo_add_SNo_10} : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNo x3 ⟶ SNo x4 ⟶ SNo x5 ⟶ SNo x6 ⟶ SNo x7 ⟶ SNo x8 ⟶ SNo x9 ⟶ SNo (add_SNo x0 (add_SNo x1 (add_SNo x2 (add_SNo x3 (add_SNo x4 (add_SNo x5 (add_SNo x6 (add_SNo x7 (add_SNo x8 x9)))))))))
Known minus_add_SNo_distr_m_9^{minus_add_SNo_distr_m_9} : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNo x3 ⟶ SNo x4 ⟶ SNo x5 ⟶ SNo x6 ⟶ SNo x7 ⟶ SNo x8 ⟶ SNo x9 ⟶ minus_SNo (add_SNo (minus_SNo x0) (add_SNo (minus_SNo x1) (add_SNo (minus_SNo x2) (add_SNo (minus_SNo x3) (add_SNo (minus_SNo x4) (add_SNo (minus_SNo x5) (add_SNo (minus_SNo x6) (add_SNo (minus_SNo x7) (add_SNo (minus_SNo x8) x9))))))))) = add_SNo x0 (add_SNo x1 (add_SNo x2 (add_SNo x3 (add_SNo x4 (add_SNo x5 (add_SNo x6 (add_SNo x7 (add_SNo x8 (minus_SNo x9)))))))))
Theorem 42999.. : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNo x3 ⟶ SNo x4 ⟶ SNo x5 ⟶ SNo x6 ⟶ SNo x7 ⟶ SNo x8 ⟶ SNo x9 ⟶ SNo x10 ⟶ SNo x11 ⟶ SNo x12 ⟶ SNo x13 ⟶ SNo x14 ⟶ SNo x15 ⟶ SNo x16 ⟶ SNo x17 ⟶ SNo x18 ⟶ SNo x19 ⟶ SNoLt 0 (add_SNo x10 (add_SNo x11 (add_SNo x12 (add_SNo x13 (add_SNo x14 (add_SNo x15 (add_SNo x16 (add_SNo x17 (add_SNo x18 x19))))))))) ⟶ SNoLe x10 (add_SNo x0 (minus_SNo x1)) ⟶ SNoLe x11 (add_SNo x1 (minus_SNo x2)) ⟶ SNoLe x12 (add_SNo x2 (minus_SNo x3)) ⟶ SNoLe x13 (add_SNo x3 (minus_SNo x4)) ⟶ SNoLe x14 (add_SNo x4 (minus_SNo x5)) ⟶ SNoLe x15 (add_SNo x5 (minus_SNo x6)) ⟶ SNoLe x16 (add_SNo x6 (minus_SNo x7)) ⟶ SNoLe x17 (add_SNo x7 (minus_SNo x8)) ⟶ SNoLe x18 (add_SNo x8 (minus_SNo x9)) ⟶ SNoLe x19 (add_SNo x9 (minus_SNo x0)) ⟶ False (proof)
Known idl_negcycle_11^{idl_negcycle_11} : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNo x3 ⟶ SNo x4 ⟶ SNo x5 ⟶ SNo x6 ⟶ SNo x7 ⟶ SNo x8 ⟶ SNo x9 ⟶ SNo x10 ⟶ SNo x11 ⟶ SNo x12 ⟶ SNo x13 ⟶ SNo x14 ⟶ SNo x15 ⟶ SNo x16 ⟶ SNo x17 ⟶ SNo x18 ⟶ SNo x19 ⟶ SNo x20 ⟶ SNo x21 ⟶ SNoLt (add_SNo x11 (add_SNo x12 (add_SNo x13 (add_SNo x14 (add_SNo x15 (add_SNo x16 (add_SNo x17 (add_SNo x18 (add_SNo x19 (add_SNo x20 x21)))))))))) 0 ⟶ SNoLe (add_SNo x1 (minus_SNo x0)) x11 ⟶ SNoLe (add_SNo x2 (minus_SNo x1)) x12 ⟶ SNoLe (add_SNo x3 (minus_SNo x2)) x13 ⟶ SNoLe (add_SNo x4 (minus_SNo x3)) x14 ⟶ SNoLe (add_SNo x5 (minus_SNo x4)) x15 ⟶ SNoLe (add_SNo x6 (minus_SNo x5)) x16 ⟶ SNoLe (add_SNo x7 (minus_SNo x6)) x17 ⟶ SNoLe (add_SNo x8 (minus_SNo x7)) x18 ⟶ SNoLe (add_SNo x9 (minus_SNo x8)) x19 ⟶ SNoLe (add_SNo x10 (minus_SNo x9)) x20 ⟶ SNoLe (add_SNo x0 (minus_SNo x10)) x21 ⟶ False
Known SNo_add_SNo_11^{SNo_add_SNo_11} : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNo x3 ⟶ SNo x4 ⟶ SNo x5 ⟶ SNo x6 ⟶ SNo x7 ⟶ SNo x8 ⟶ SNo x9 ⟶ SNo x10 ⟶ SNo (add_SNo x0 (add_SNo x1 (add_SNo x2 (add_SNo x3 (add_SNo x4 (add_SNo x5 (add_SNo x6 (add_SNo x7 (add_SNo x8 (add_SNo x9 x10))))))))))
Known minus_add_SNo_distr_m_10^{minus_add_SNo_distr_m_10} : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNo x3 ⟶ SNo x4 ⟶ SNo x5 ⟶ SNo x6 ⟶ SNo x7 ⟶ SNo x8 ⟶ SNo x9 ⟶ SNo x10 ⟶ minus_SNo (add_SNo (minus_SNo x0) (add_SNo (minus_SNo x1) (add_SNo (minus_SNo x2) (add_SNo (minus_SNo x3) (add_SNo (minus_SNo x4) (add_SNo (minus_SNo x5) (add_SNo (minus_SNo x6) (add_SNo (minus_SNo x7) (add_SNo (minus_SNo x8) (add_SNo (minus_SNo x9) x10)))))))))) = add_SNo x0 (add_SNo x1 (add_SNo x2 (add_SNo x3 (add_SNo x4 (add_SNo x5 (add_SNo x6 (add_SNo x7 (add_SNo x8 (add_SNo x9 (minus_SNo x10))))))))))
Theorem 8365f.. : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNo x3 ⟶ SNo x4 ⟶ SNo x5 ⟶ SNo x6 ⟶ SNo x7 ⟶ SNo x8 ⟶ SNo x9 ⟶ SNo x10 ⟶ SNo x11 ⟶ SNo x12 ⟶ SNo x13 ⟶ SNo x14 ⟶ SNo x15 ⟶ SNo x16 ⟶ SNo x17 ⟶ SNo x18 ⟶ SNo x19 ⟶ SNo x20 ⟶ SNo x21 ⟶ SNoLt 0 (add_SNo x11 (add_SNo x12 (add_SNo x13 (add_SNo x14 (add_SNo x15 (add_SNo x16 (add_SNo x17 (add_SNo x18 (add_SNo x19 (add_SNo x20 x21)))))))))) ⟶ SNoLe x11 (add_SNo x0 (minus_SNo x1)) ⟶ SNoLe x12 (add_SNo x1 (minus_SNo x2)) ⟶ SNoLe x13 (add_SNo x2 (minus_SNo x3)) ⟶ SNoLe x14 (add_SNo x3 (minus_SNo x4)) ⟶ SNoLe x15 (add_SNo x4 (minus_SNo x5)) ⟶ SNoLe x16 (add_SNo x5 (minus_SNo x6)) ⟶ SNoLe x17 (add_SNo x6 (minus_SNo x7)) ⟶ SNoLe x18 (add_SNo x7 (minus_SNo x8)) ⟶ SNoLe x19 (add_SNo x8 (minus_SNo x9)) ⟶ SNoLe x20 (add_SNo x9 (minus_SNo x10)) ⟶ SNoLe x21 (add_SNo x10 (minus_SNo x0)) ⟶ False (proof)
Known idl_negcycle_12^{idl_negcycle_12} : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNo x3 ⟶ SNo x4 ⟶ SNo x5 ⟶ SNo x6 ⟶ SNo x7 ⟶ SNo x8 ⟶ SNo x9 ⟶ SNo x10 ⟶ SNo x11 ⟶ SNo x12 ⟶ SNo x13 ⟶ SNo x14 ⟶ SNo x15 ⟶ SNo x16 ⟶ SNo x17 ⟶ SNo x18 ⟶ SNo x19 ⟶ SNo x20 ⟶ SNo x21 ⟶ SNo x22 ⟶ SNo x23 ⟶ SNoLt (add_SNo x12 (add_SNo x13 (add_SNo x14 (add_SNo x15 (add_SNo x16 (add_SNo x17 (add_SNo x18 (add_SNo x19 (add_SNo x20 (add_SNo x21 (add_SNo x22 x23))))))))))) 0 ⟶ SNoLe (add_SNo x1 (minus_SNo x0)) x12 ⟶ SNoLe (add_SNo x2 (minus_SNo x1)) x13 ⟶ SNoLe (add_SNo x3 (minus_SNo x2)) x14 ⟶ SNoLe (add_SNo x4 (minus_SNo x3)) x15 ⟶ SNoLe (add_SNo x5 (minus_SNo x4)) x16 ⟶ SNoLe (add_SNo x6 (minus_SNo x5)) x17 ⟶ SNoLe (add_SNo x7 (minus_SNo x6)) x18 ⟶ SNoLe (add_SNo x8 (minus_SNo x7)) x19 ⟶ SNoLe (add_SNo x9 (minus_SNo x8)) x20 ⟶ SNoLe (add_SNo x10 (minus_SNo x9)) x21 ⟶ SNoLe (add_SNo x11 (minus_SNo x10)) x22 ⟶ SNoLe (add_SNo x0 (minus_SNo x11)) x23 ⟶ False
Known SNo_add_SNo_12^{SNo_add_SNo_12} : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNo x3 ⟶ SNo x4 ⟶ SNo x5 ⟶ SNo x6 ⟶ SNo x7 ⟶ SNo x8 ⟶ SNo x9 ⟶ SNo x10 ⟶ SNo x11 ⟶ SNo (add_SNo x0 (add_SNo x1 (add_SNo x2 (add_SNo x3 (add_SNo x4 (add_SNo x5 (add_SNo x6 (add_SNo x7 (add_SNo x8 (add_SNo x9 (add_SNo x10 x11)))))))))))
Known minus_add_SNo_distr_m_11^{minus_add_SNo_distr_m_11} : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNo x3 ⟶ SNo x4 ⟶ SNo x5 ⟶ SNo x6 ⟶ SNo x7 ⟶ SNo x8 ⟶ SNo x9 ⟶ SNo x10 ⟶ SNo x11 ⟶ minus_SNo (add_SNo (minus_SNo x0) (add_SNo (minus_SNo x1) (add_SNo (minus_SNo x2) (add_SNo (minus_SNo x3) (add_SNo (minus_SNo x4) (add_SNo (minus_SNo x5) (add_SNo (minus_SNo x6) (add_SNo (minus_SNo x7) (add_SNo (minus_SNo x8) (add_SNo (minus_SNo x9) (add_SNo (minus_SNo x10) x11))))))))))) = add_SNo x0 (add_SNo x1 (add_SNo x2 (add_SNo x3 (add_SNo x4 (add_SNo x5 (add_SNo x6 (add_SNo x7 (add_SNo x8 (add_SNo x9 (add_SNo x10 (minus_SNo x11)))))))))))
Theorem 136a9.. : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNo x3 ⟶ SNo x4 ⟶ SNo x5 ⟶ SNo x6 ⟶ SNo x7 ⟶ SNo x8 ⟶ SNo x9 ⟶ SNo x10 ⟶ SNo x11 ⟶ SNo x12 ⟶ SNo x13 ⟶ SNo x14 ⟶ SNo x15 ⟶ SNo x16 ⟶ SNo x17 ⟶ SNo x18 ⟶ SNo x19 ⟶ SNo x20 ⟶ SNo x21 ⟶ SNo x22 ⟶ SNo x23 ⟶ SNoLt 0 (add_SNo x12 (add_SNo x13 (add_SNo x14 (add_SNo x15 (add_SNo x16 (add_SNo x17 (add_SNo x18 (add_SNo x19 (add_SNo x20 (add_SNo x21 (add_SNo x22 x23))))))))))) ⟶ SNoLe x12 (add_SNo x0 (minus_SNo x1)) ⟶ SNoLe x13 (add_SNo x1 (minus_SNo x2)) ⟶ SNoLe x14 (add_SNo x2 (minus_SNo x3)) ⟶ SNoLe x15 (add_SNo x3 (minus_SNo x4)) ⟶ SNoLe x16 (add_SNo x4 (minus_SNo x5)) ⟶ SNoLe x17 (add_SNo x5 (minus_SNo x6)) ⟶ SNoLe x18 (add_SNo x6 (minus_SNo x7)) ⟶ SNoLe x19 (add_SNo x7 (minus_SNo x8)) ⟶ SNoLe x20 (add_SNo x8 (minus_SNo x9)) ⟶ SNoLe x21 (add_SNo x9 (minus_SNo x10)) ⟶ SNoLe x22 (add_SNo x10 (minus_SNo x11)) ⟶ SNoLe x23 (add_SNo x11 (minus_SNo x0)) ⟶ False (proof)
Known idl_negcycle_13^{idl_negcycle_13} : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNo x3 ⟶ SNo x4 ⟶ SNo x5 ⟶ SNo x6 ⟶ SNo x7 ⟶ SNo x8 ⟶ SNo x9 ⟶ SNo x10 ⟶ SNo x11 ⟶ SNo x12 ⟶ SNo x13 ⟶ SNo x14 ⟶ SNo x15 ⟶ SNo x16 ⟶ SNo x17 ⟶ SNo x18 ⟶ SNo x19 ⟶ SNo x20 ⟶ SNo x21 ⟶ SNo x22 ⟶ SNo x23 ⟶ SNo x24 ⟶ SNo x25 ⟶ SNoLt (add_SNo x13 (add_SNo x14 (add_SNo x15 (add_SNo x16 (add_SNo x17 (add_SNo x18 (add_SNo x19 (add_SNo x20 (add_SNo x21 (add_SNo x22 (add_SNo x23 (add_SNo x24 x25)))))))))))) 0 ⟶ SNoLe (add_SNo x1 (minus_SNo x0)) x13 ⟶ SNoLe (add_SNo x2 (minus_SNo x1)) x14 ⟶ SNoLe (add_SNo x3 (minus_SNo x2)) x15 ⟶ SNoLe (add_SNo x4 (minus_SNo x3)) x16 ⟶ SNoLe (add_SNo x5 (minus_SNo x4)) x17 ⟶ SNoLe (add_SNo x6 (minus_SNo x5)) x18 ⟶ SNoLe (add_SNo x7 (minus_SNo x6)) x19 ⟶ SNoLe (add_SNo x8 (minus_SNo x7)) x20 ⟶ SNoLe (add_SNo x9 (minus_SNo x8)) x21 ⟶ SNoLe (add_SNo x10 (minus_SNo x9)) x22 ⟶ SNoLe (add_SNo x11 (minus_SNo x10)) x23 ⟶ SNoLe (add_SNo x12 (minus_SNo x11)) x24 ⟶ SNoLe (add_SNo x0 (minus_SNo x12)) x25 ⟶ False
Known SNo_add_SNo_13^{SNo_add_SNo_13} : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNo x3 ⟶ SNo x4 ⟶ SNo x5 ⟶ SNo x6 ⟶ SNo x7 ⟶ SNo x8 ⟶ SNo x9 ⟶ SNo x10 ⟶ SNo x11 ⟶ SNo x12 ⟶ SNo (add_SNo x0 (add_SNo x1 (add_SNo x2 (add_SNo x3 (add_SNo x4 (add_SNo x5 (add_SNo x6 (add_SNo x7 (add_SNo x8 (add_SNo x9 (add_SNo x10 (add_SNo x11 x12))))))))))))
Known minus_add_SNo_distr_m_12^{minus_add_SNo_distr_m_12} : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNo x3 ⟶ SNo x4 ⟶ SNo x5 ⟶ SNo x6 ⟶ SNo x7 ⟶ SNo x8 ⟶ SNo x9 ⟶ SNo x10 ⟶ SNo x11 ⟶ SNo x12 ⟶ minus_SNo (add_SNo (minus_SNo x0) (add_SNo (minus_SNo x1) (add_SNo (minus_SNo x2) (add_SNo (minus_SNo x3) (add_SNo (minus_SNo x4) (add_SNo (minus_SNo x5) (add_SNo (minus_SNo x6) (add_SNo (minus_SNo x7) (add_SNo (minus_SNo x8) (add_SNo (minus_SNo x9) (add_SNo (minus_SNo x10) (add_SNo (minus_SNo x11) x12)))))))))))) = add_SNo x0 (add_SNo x1 (add_SNo x2 (add_SNo x3 (add_SNo x4 (add_SNo x5 (add_SNo x6 (add_SNo x7 (add_SNo x8 (add_SNo x9 (add_SNo x10 (add_SNo x11 (minus_SNo x12))))))))))))
Theorem 07117.. : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNo x3 ⟶ SNo x4 ⟶ SNo x5 ⟶ SNo x6 ⟶ SNo x7 ⟶ SNo x8 ⟶ SNo x9 ⟶ SNo x10 ⟶ SNo x11 ⟶ SNo x12 ⟶ SNo x13 ⟶ SNo x14 ⟶ SNo x15 ⟶ SNo x16 ⟶ SNo x17 ⟶ SNo x18 ⟶ SNo x19 ⟶ SNo x20 ⟶ SNo x21 ⟶ SNo x22 ⟶ SNo x23 ⟶ SNo x24 ⟶ SNo x25 ⟶ SNoLt 0 (add_SNo x13 (add_SNo x14 (add_SNo x15 (add_SNo x16 (add_SNo x17 (add_SNo x18 (add_SNo x19 (add_SNo x20 (add_SNo x21 (add_SNo x22 (add_SNo x23 (add_SNo x24 x25)))))))))))) ⟶ SNoLe x13 (add_SNo x0 (minus_SNo x1)) ⟶ SNoLe x14 (add_SNo x1 (minus_SNo x2)) ⟶ SNoLe x15 (add_SNo x2 (minus_SNo x3)) ⟶ SNoLe x16 (add_SNo x3 (minus_SNo x4)) ⟶ SNoLe x17 (add_SNo x4 (minus_SNo x5)) ⟶ SNoLe x18 (add_SNo x5 (minus_SNo x6)) ⟶ SNoLe x19 (add_SNo x6 (minus_SNo x7)) ⟶ SNoLe x20 (add_SNo x7 (minus_SNo x8)) ⟶ SNoLe x21 (add_SNo x8 (minus_SNo x9)) ⟶ SNoLe x22 (add_SNo x9 (minus_SNo x10)) ⟶ SNoLe x23 (add_SNo x10 (minus_SNo x11)) ⟶ SNoLe x24 (add_SNo x11 (minus_SNo x12)) ⟶ SNoLe x25 (add_SNo x12 (minus_SNo x0)) ⟶ False (proof)
Known idl_negcycle_14^{idl_negcycle_14} : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 x26 x27 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNo x3 ⟶ SNo x4 ⟶ SNo x5 ⟶ SNo x6 ⟶ SNo x7 ⟶ SNo x8 ⟶ SNo x9 ⟶ SNo x10 ⟶ SNo x11 ⟶ SNo x12 ⟶ SNo x13 ⟶ SNo x14 ⟶ SNo x15 ⟶ SNo x16 ⟶ SNo x17 ⟶ SNo x18 ⟶ SNo x19 ⟶ SNo x20 ⟶ SNo x21 ⟶ SNo x22 ⟶ SNo x23 ⟶ SNo x24 ⟶ SNo x25 ⟶ SNo x26 ⟶ SNo x27 ⟶ SNoLt (add_SNo x14 (add_SNo x15 (add_SNo x16 (add_SNo x17 (add_SNo x18 (add_SNo x19 (add_SNo x20 (add_SNo x21 (add_SNo x22 (add_SNo x23 (add_SNo x24 (add_SNo x25 (add_SNo x26 x27))))))))))))) 0 ⟶ SNoLe (add_SNo x1 (minus_SNo x0)) x14 ⟶ SNoLe (add_SNo x2 (minus_SNo x1)) x15 ⟶ SNoLe (add_SNo x3 (minus_SNo x2)) x16 ⟶ SNoLe (add_SNo x4 (minus_SNo x3)) x17 ⟶ SNoLe (add_SNo x5 (minus_SNo x4)) x18 ⟶ SNoLe (add_SNo x6 (minus_SNo x5)) x19 ⟶ SNoLe (add_SNo x7 (minus_SNo x6)) x20 ⟶ SNoLe (add_SNo x8 (minus_SNo x7)) x21 ⟶ SNoLe (add_SNo x9 (minus_SNo x8)) x22 ⟶ SNoLe (add_SNo x10 (minus_SNo x9)) x23 ⟶ SNoLe (add_SNo x11 (minus_SNo x10)) x24 ⟶ SNoLe (add_SNo x12 (minus_SNo x11)) x25 ⟶ SNoLe (add_SNo x13 (minus_SNo x12)) x26 ⟶ SNoLe (add_SNo x0 (minus_SNo x13)) x27 ⟶ False
Known SNo_add_SNo_14^{SNo_add_SNo_14} : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNo x3 ⟶ SNo x4 ⟶ SNo x5 ⟶ SNo x6 ⟶ SNo x7 ⟶ SNo x8 ⟶ SNo x9 ⟶ SNo x10 ⟶ SNo x11 ⟶ SNo x12 ⟶ SNo x13 ⟶ SNo (add_SNo x0 (add_SNo x1 (add_SNo x2 (add_SNo x3 (add_SNo x4 (add_SNo x5 (add_SNo x6 (add_SNo x7 (add_SNo x8 (add_SNo x9 (add_SNo x10 (add_SNo x11 (add_SNo x12 x13)))))))))))))
Known minus_add_SNo_distr_m_13^{minus_add_SNo_distr_m_13} : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNo x3 ⟶ SNo x4 ⟶ SNo x5 ⟶ SNo x6 ⟶ SNo x7 ⟶ SNo x8 ⟶ SNo x9 ⟶ SNo x10 ⟶ SNo x11 ⟶ SNo x12 ⟶ SNo x13 ⟶ minus_SNo (add_SNo (minus_SNo x0) (add_SNo (minus_SNo x1) (add_SNo (minus_SNo x2) (add_SNo (minus_SNo x3) (add_SNo (minus_SNo x4) (add_SNo (minus_SNo x5) (add_SNo (minus_SNo x6) (add_SNo (minus_SNo x7) (add_SNo (minus_SNo x8) (add_SNo (minus_SNo x9) (add_SNo (minus_SNo x10) (add_SNo (minus_SNo x11) (add_SNo (minus_SNo x12) x13))))))))))))) = add_SNo x0 (add_SNo x1 (add_SNo x2 (add_SNo x3 (add_SNo x4 (add_SNo x5 (add_SNo x6 (add_SNo x7 (add_SNo x8 (add_SNo x9 (add_SNo x10 (add_SNo x11 (add_SNo x12 (minus_SNo x13)))))))))))))
Theorem 2cba7.. : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 x26 x27 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNo x3 ⟶ SNo x4 ⟶ SNo x5 ⟶ SNo x6 ⟶ SNo x7 ⟶ SNo x8 ⟶ SNo x9 ⟶ SNo x10 ⟶ SNo x11 ⟶ SNo x12 ⟶ SNo x13 ⟶ SNo x14 ⟶ SNo x15 ⟶ SNo x16 ⟶ SNo x17 ⟶ SNo x18 ⟶ SNo x19 ⟶ SNo x20 ⟶ SNo x21 ⟶ SNo x22 ⟶ SNo x23 ⟶ SNo x24 ⟶ SNo x25 ⟶ SNo x26 ⟶ SNo x27 ⟶ SNoLt 0 (add_SNo x14 (add_SNo x15 (add_SNo x16 (add_SNo x17 (add_SNo x18 (add_SNo x19 (add_SNo x20 (add_SNo x21 (add_SNo x22 (add_SNo x23 (add_SNo x24 (add_SNo x25 (add_SNo x26 x27))))))))))))) ⟶ SNoLe x14 (add_SNo x0 (minus_SNo x1)) ⟶ SNoLe x15 (add_SNo x1 (minus_SNo x2)) ⟶ SNoLe x16 (add_SNo x2 (minus_SNo x3)) ⟶ SNoLe x17 (add_SNo x3 (minus_SNo x4)) ⟶ SNoLe x18 (add_SNo x4 (minus_SNo x5)) ⟶ SNoLe x19 (add_SNo x5 (minus_SNo x6)) ⟶ SNoLe x20 (add_SNo x6 (minus_SNo x7)) ⟶ SNoLe x21 (add_SNo x7 (minus_SNo x8)) ⟶ SNoLe x22 (add_SNo x8 (minus_SNo x9)) ⟶ SNoLe x23 (add_SNo x9 (minus_SNo x10)) ⟶ SNoLe x24 (add_SNo x10 (minus_SNo x11)) ⟶ SNoLe x25 (add_SNo x11 (minus_SNo x12)) ⟶ SNoLe x26 (add_SNo x12 (minus_SNo x13)) ⟶ SNoLe x27 (add_SNo x13 (minus_SNo x0)) ⟶ False (proof)
Known idl_negcycle_15^{idl_negcycle_15} : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNo x3 ⟶ SNo x4 ⟶ SNo x5 ⟶ SNo x6 ⟶ SNo x7 ⟶ SNo x8 ⟶ SNo x9 ⟶ SNo x10 ⟶ SNo x11 ⟶ SNo x12 ⟶ SNo x13 ⟶ SNo x14 ⟶ SNo x15 ⟶ SNo x16 ⟶ SNo x17 ⟶ SNo x18 ⟶ SNo x19 ⟶ SNo x20 ⟶ SNo x21 ⟶ SNo x22 ⟶ SNo x23 ⟶ SNo x24 ⟶ SNo x25 ⟶ SNo x26 ⟶ SNo x27 ⟶ SNo x28 ⟶ SNo x29 ⟶ SNoLt (add_SNo x15 (add_SNo x16 (add_SNo x17 (add_SNo x18 (add_SNo x19 (add_SNo x20 (add_SNo x21 (add_SNo x22 (add_SNo x23 (add_SNo x24 (add_SNo x25 (add_SNo x26 (add_SNo x27 (add_SNo x28 x29)))))))))))))) 0 ⟶ SNoLe (add_SNo x1 (minus_SNo x0)) x15 ⟶ SNoLe (add_SNo x2 (minus_SNo x1)) x16 ⟶ SNoLe (add_SNo x3 (minus_SNo x2)) x17 ⟶ SNoLe (add_SNo x4 (minus_SNo x3)) x18 ⟶ SNoLe (add_SNo x5 (minus_SNo x4)) x19 ⟶ SNoLe (add_SNo x6 (minus_SNo x5)) x20 ⟶ SNoLe (add_SNo x7 (minus_SNo x6)) x21 ⟶ SNoLe (add_SNo x8 (minus_SNo x7)) x22 ⟶ SNoLe (add_SNo x9 (minus_SNo x8)) x23 ⟶ SNoLe (add_SNo x10 (minus_SNo x9)) x24 ⟶ SNoLe (add_SNo x11 (minus_SNo x10)) x25 ⟶ SNoLe (add_SNo x12 (minus_SNo x11)) x26 ⟶ SNoLe (add_SNo x13 (minus_SNo x12)) x27 ⟶ SNoLe (add_SNo x14 (minus_SNo x13)) x28 ⟶ SNoLe (add_SNo x0 (minus_SNo x14)) x29 ⟶ False
Known SNo_add_SNo_15^{SNo_add_SNo_15} : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNo x3 ⟶ SNo x4 ⟶ SNo x5 ⟶ SNo x6 ⟶ SNo x7 ⟶ SNo x8 ⟶ SNo x9 ⟶ SNo x10 ⟶ SNo x11 ⟶ SNo x12 ⟶ SNo x13 ⟶ SNo x14 ⟶ SNo (add_SNo x0 (add_SNo x1 (add_SNo x2 (add_SNo x3 (add_SNo x4 (add_SNo x5 (add_SNo x6 (add_SNo x7 (add_SNo x8 (add_SNo x9 (add_SNo x10 (add_SNo x11 (add_SNo x12 (add_SNo x13 x14))))))))))))))
Known minus_add_SNo_distr_m_14^{minus_add_SNo_distr_m_14} : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNo x3 ⟶ SNo x4 ⟶ SNo x5 ⟶ SNo x6 ⟶ SNo x7 ⟶ SNo x8 ⟶ SNo x9 ⟶ SNo x10 ⟶ SNo x11 ⟶ SNo x12 ⟶ SNo x13 ⟶ SNo x14 ⟶ minus_SNo (add_SNo (minus_SNo x0) (add_SNo (minus_SNo x1) (add_SNo (minus_SNo x2) (add_SNo (minus_SNo x3) (add_SNo (minus_SNo x4) (add_SNo (minus_SNo x5) (add_SNo (minus_SNo x6) (add_SNo (minus_SNo x7) (add_SNo (minus_SNo x8) (add_SNo (minus_SNo x9) (add_SNo (minus_SNo x10) (add_SNo (minus_SNo x11) (add_SNo (minus_SNo x12) (add_SNo (minus_SNo x13) x14)))))))))))))) = add_SNo x0 (add_SNo x1 (add_SNo x2 (add_SNo x3 (add_SNo x4 (add_SNo x5 (add_SNo x6 (add_SNo x7 (add_SNo x8 (add_SNo x9 (add_SNo x10 (add_SNo x11 (add_SNo x12 (add_SNo x13 (minus_SNo x14))))))))))))))
Theorem 8aac7.. : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNo x3 ⟶ SNo x4 ⟶ SNo x5 ⟶ SNo x6 ⟶ SNo x7 ⟶ SNo x8 ⟶ SNo x9 ⟶ SNo x10 ⟶ SNo x11 ⟶ SNo x12 ⟶ SNo x13 ⟶ SNo x14 ⟶ SNo x15 ⟶ SNo x16 ⟶ SNo x17 ⟶ SNo x18 ⟶ SNo x19 ⟶ SNo x20 ⟶ SNo x21 ⟶ SNo x22 ⟶ SNo x23 ⟶ SNo x24 ⟶ SNo x25 ⟶ SNo x26 ⟶ SNo x27 ⟶ SNo x28 ⟶ SNo x29 ⟶ SNoLt 0 (add_SNo x15 (add_SNo x16 (add_SNo x17 (add_SNo x18 (add_SNo x19 (add_SNo x20 (add_SNo x21 (add_SNo x22 (add_SNo x23 (add_SNo x24 (add_SNo x25 (add_SNo x26 (add_SNo x27 (add_SNo x28 x29)))))))))))))) ⟶ SNoLe x15 (add_SNo x0 (minus_SNo x1)) ⟶ SNoLe x16 (add_SNo x1 (minus_SNo x2)) ⟶ SNoLe x17 (add_SNo x2 (minus_SNo x3)) ⟶ SNoLe x18 (add_SNo x3 (minus_SNo x4)) ⟶ SNoLe x19 (add_SNo x4 (minus_SNo x5)) ⟶ SNoLe x20 (add_SNo x5 (minus_SNo x6)) ⟶ SNoLe x21 (add_SNo x6 (minus_SNo x7)) ⟶ SNoLe x22 (add_SNo x7 (minus_SNo x8)) ⟶ SNoLe x23 (add_SNo x8 (minus_SNo x9)) ⟶ SNoLe x24 (add_SNo x9 (minus_SNo x10)) ⟶ SNoLe x25 (add_SNo x10 (minus_SNo x11)) ⟶ SNoLe x26 (add_SNo x11 (minus_SNo x12)) ⟶ SNoLe x27 (add_SNo x12 (minus_SNo x13)) ⟶ SNoLe x28 (add_SNo x13 (minus_SNo x14)) ⟶ SNoLe x29 (add_SNo x14 (minus_SNo x0)) ⟶ False (proof)
Known idl_negcycle_16^{idl_negcycle_16} : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNo x3 ⟶ SNo x4 ⟶ SNo x5 ⟶ SNo x6 ⟶ SNo x7 ⟶ SNo x8 ⟶ SNo x9 ⟶ SNo x10 ⟶ SNo x11 ⟶ SNo x12 ⟶ SNo x13 ⟶ SNo x14 ⟶ SNo x15 ⟶ SNo x16 ⟶ SNo x17 ⟶ SNo x18 ⟶ SNo x19 ⟶ SNo x20 ⟶ SNo x21 ⟶ SNo x22 ⟶ SNo x23 ⟶ SNo x24 ⟶ SNo x25 ⟶ SNo x26 ⟶ SNo x27 ⟶ SNo x28 ⟶ SNo x29 ⟶ SNo x30 ⟶ SNo x31 ⟶ SNoLt (add_SNo x16 (add_SNo x17 (add_SNo x18 (add_SNo x19 (add_SNo x20 (add_SNo x21 (add_SNo x22 (add_SNo x23 (add_SNo x24 (add_SNo x25 (add_SNo x26 (add_SNo x27 (add_SNo x28 (add_SNo x29 (add_SNo x30 x31))))))))))))))) 0 ⟶ SNoLe (add_SNo x1 (minus_SNo x0)) x16 ⟶ SNoLe (add_SNo x2 (minus_SNo x1)) x17 ⟶ SNoLe (add_SNo x3 (minus_SNo x2)) x18 ⟶ SNoLe (add_SNo x4 (minus_SNo x3)) x19 ⟶ SNoLe (add_SNo x5 (minus_SNo x4)) x20 ⟶ SNoLe (add_SNo x6 (minus_SNo x5)) x21 ⟶ SNoLe (add_SNo x7 (minus_SNo x6)) x22 ⟶ SNoLe (add_SNo x8 (minus_SNo x7)) x23 ⟶ SNoLe (add_SNo x9 (minus_SNo x8)) x24 ⟶ SNoLe (add_SNo x10 (minus_SNo x9)) x25 ⟶ SNoLe (add_SNo x11 (minus_SNo x10)) x26 ⟶ SNoLe (add_SNo x12 (minus_SNo x11)) x27 ⟶ SNoLe (add_SNo x13 (minus_SNo x12)) x28 ⟶ SNoLe (add_SNo x14 (minus_SNo x13)) x29 ⟶ SNoLe (add_SNo x15 (minus_SNo x14)) x30 ⟶ SNoLe (add_SNo x0 (minus_SNo x15)) x31 ⟶ False
Known SNo_add_SNo_16^{SNo_add_SNo_16} : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNo x3 ⟶ SNo x4 ⟶ SNo x5 ⟶ SNo x6 ⟶ SNo x7 ⟶ SNo x8 ⟶ SNo x9 ⟶ SNo x10 ⟶ SNo x11 ⟶ SNo x12 ⟶ SNo x13 ⟶ SNo x14 ⟶ SNo x15 ⟶ SNo (add_SNo x0 (add_SNo x1 (add_SNo x2 (add_SNo x3 (add_SNo x4 (add_SNo x5 (add_SNo x6 (add_SNo x7 (add_SNo x8 (add_SNo x9 (add_SNo x10 (add_SNo x11 (add_SNo x12 (add_SNo x13 (add_SNo x14 x15)))))))))))))))
Known minus_add_SNo_distr_m_15^{minus_add_SNo_distr_m_15} : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNo x3 ⟶ SNo x4 ⟶ SNo x5 ⟶ SNo x6 ⟶ SNo x7 ⟶ SNo x8 ⟶ SNo x9 ⟶ SNo x10 ⟶ SNo x11 ⟶ SNo x12 ⟶ SNo x13 ⟶ SNo x14 ⟶ SNo x15 ⟶ minus_SNo (add_SNo (minus_SNo x0) (add_SNo (minus_SNo x1) (add_SNo (minus_SNo x2) (add_SNo (minus_SNo x3) (add_SNo (minus_SNo x4) (add_SNo (minus_SNo x5) (add_SNo (minus_SNo x6) (add_SNo (minus_SNo x7) (add_SNo (minus_SNo x8) (add_SNo (minus_SNo x9) (add_SNo (minus_SNo x10) (add_SNo (minus_SNo x11) (add_SNo (minus_SNo x12) (add_SNo (minus_SNo x13) (add_SNo (minus_SNo x14) x15))))))))))))))) = add_SNo x0 (add_SNo x1 (add_SNo x2 (add_SNo x3 (add_SNo x4 (add_SNo x5 (add_SNo x6 (add_SNo x7 (add_SNo x8 (add_SNo x9 (add_SNo x10 (add_SNo x11 (add_SNo x12 (add_SNo x13 (add_SNo x14 (minus_SNo x15)))))))))))))))
Theorem cd63f.. : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNo x3 ⟶ SNo x4 ⟶ SNo x5 ⟶ SNo x6 ⟶ SNo x7 ⟶ SNo x8 ⟶ SNo x9 ⟶ SNo x10 ⟶ SNo x11 ⟶ SNo x12 ⟶ SNo x13 ⟶ SNo x14 ⟶ SNo x15 ⟶ SNo x16 ⟶ SNo x17 ⟶ SNo x18 ⟶ SNo x19 ⟶ SNo x20 ⟶ SNo x21 ⟶ SNo x22 ⟶ SNo x23 ⟶ SNo x24 ⟶ SNo x25 ⟶ SNo x26 ⟶ SNo x27 ⟶ SNo x28 ⟶ SNo x29 ⟶ SNo x30 ⟶ SNo x31 ⟶ SNoLt 0 (add_SNo x16 (add_SNo x17 (add_SNo x18 (add_SNo x19 (add_SNo x20 (add_SNo x21 (add_SNo x22 (add_SNo x23 (add_SNo x24 (add_SNo x25 (add_SNo x26 (add_SNo x27 (add_SNo x28 (add_SNo x29 (add_SNo x30 x31))))))))))))))) ⟶ SNoLe x16 (add_SNo x0 (minus_SNo x1)) ⟶ SNoLe x17 (add_SNo x1 (minus_SNo x2)) ⟶ SNoLe x18 (add_SNo x2 (minus_SNo x3)) ⟶ SNoLe x19 (add_SNo x3 (minus_SNo x4)) ⟶ SNoLe x20 (add_SNo x4 (minus_SNo x5)) ⟶ SNoLe x21 (add_SNo x5 (minus_SNo x6)) ⟶ SNoLe x22 (add_SNo x6 (minus_SNo x7)) ⟶ SNoLe x23 (add_SNo x7 (minus_SNo x8)) ⟶ SNoLe x24 (add_SNo x8 (minus_SNo x9)) ⟶ SNoLe x25 (add_SNo x9 (minus_SNo x10)) ⟶ SNoLe x26 (add_SNo x10 (minus_SNo x11)) ⟶ SNoLe x27 (add_SNo x11 (minus_SNo x12)) ⟶ SNoLe x28 (add_SNo x12 (minus_SNo x13)) ⟶ SNoLe x29 (add_SNo x13 (minus_SNo x14)) ⟶ SNoLe x30 (add_SNo x14 (minus_SNo x15)) ⟶ SNoLe x31 (add_SNo x15 (minus_SNo x0)) ⟶ False (proof)