Proofgold Signed Transaction

Param SNo^SNo : ι → ο
Param SNoLe^SNoLe : ι → ι → ο
Param ordsucc^ordsucc : ι → ι
Param add_SNo^add_SNo : ι → ι → ι
Param minus_SNo^minus_SNo : ι → ι
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_1^SNo_1 : SNo 1
Theorem minus_SNo_Le_swap_1^{minus_SNo_Le_swap_1} : ∀ x0 x1 . SNo x0 ⟶ SNo x1 ⟶ SNoLe 1 (add_SNo x0 (minus_SNo x1)) ⟶ SNoLe (add_SNo x1 (minus_SNo x0)) (minus_SNo 1) (proof)
Param SNoLt^SNoLt : ι → ι → ο
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 SNo_0^SNo_0 : SNo 0
Known minus_SNo_0^minus_SNo_0 : minus_SNo 0 = 0
Known SNoLt_0_1^SNoLt_0_1 : SNoLt 0 1
Theorem SNoLt_minus_1_0^{SNoLt_minus_1_0} : SNoLt (minus_SNo 1) 0 (proof)
Param nat_p^nat_p : ι → ο
Param ordinal^ordinal : ι → ο
Known ordinal_ordsucc_SNo_eq^{ordinal_ordsucc_SNo_eq} : ∀ x0 . ordinal x0 ⟶ ordsucc x0 = add_SNo 1 x0
Known nat_p_ordinal^{nat_p_ordinal} : ∀ x0 . nat_p x0 ⟶ ordinal 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 nat_p_SNo^nat_p_SNo : ∀ x0 . nat_p x0 ⟶ SNo x0
Theorem add_minus_1_ordsucc^{add_minus_1_ordsucc} : ∀ x0 . nat_p x0 ⟶ add_SNo (minus_SNo 1) (ordsucc x0) = x0 (proof)
Definition False^False := ∀ x0 : ο . x0
Definition not^not := λ x0 : ο . x0 ⟶ False
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^SNo_add_SNo : ∀ x0 x1 . SNo x0 ⟶ SNo x1 ⟶ SNo (add_SNo x0 x1)
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 SNo_minus_SNo^{SNo_minus_SNo} : ∀ x0 . SNo x0 ⟶ SNo (minus_SNo 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_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_minus_SNo_rinv^{add_SNo_minus_SNo_rinv} : ∀ x0 . SNo x0 ⟶ add_SNo x0 (minus_SNo x0) = 0
Known add_SNo_minus_SNo_linv^{add_SNo_minus_SNo_linv} : ∀ x0 . SNo x0 ⟶ add_SNo (minus_SNo x0) x0 = 0
Known add_SNo_0L^add_SNo_0L : ∀ x0 . SNo x0 ⟶ add_SNo 0 x0 = x0
Theorem idl_negcycle_2^{idl_negcycle_2} : ∀ x0 x1 x2 x3 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNo x3 ⟶ SNoLt (add_SNo x2 x3) 0 ⟶ SNoLe (add_SNo x1 (minus_SNo x0)) x2 ⟶ SNoLe (add_SNo x0 (minus_SNo x1)) x3 ⟶ False (proof)
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_Le2^add_SNo_Le2 : ∀ x0 x1 x2 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNoLe x1 x2 ⟶ SNoLe (add_SNo x0 x1) (add_SNo x0 x2)
Known add_SNo_Le1^add_SNo_Le1 : ∀ x0 x1 x2 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNoLe x0 x2 ⟶ SNoLe (add_SNo x0 x1) (add_SNo x2 x1)
Known add_SNo_com_3b_1_2^{add_SNo_com_3b_1_2} : ∀ x0 x1 x2 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ add_SNo (add_SNo x0 x1) x2 = add_SNo (add_SNo x0 x2) 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)
Theorem idl_negcycle_3^{idl_negcycle_3} : ∀ x0 x1 x2 x3 x4 x5 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNo x3 ⟶ SNo x4 ⟶ SNo x5 ⟶ SNoLt (add_SNo x3 (add_SNo x4 x5)) 0 ⟶ SNoLe (add_SNo x1 (minus_SNo x0)) x3 ⟶ SNoLe (add_SNo x2 (minus_SNo x1)) x4 ⟶ SNoLe (add_SNo x0 (minus_SNo x2)) x5 ⟶ False (proof)
Known 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
Theorem idl_negcycle_5^{idl_negcycle_5} : ∀ 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 ⟶ SNoLt (add_SNo x5 (add_SNo x6 (add_SNo x7 (add_SNo x8 x9)))) 0 ⟶ SNoLe (add_SNo x1 (minus_SNo x0)) x5 ⟶ SNoLe (add_SNo x2 (minus_SNo x1)) x6 ⟶ SNoLe (add_SNo x3 (minus_SNo x2)) x7 ⟶ SNoLe (add_SNo x4 (minus_SNo x3)) x8 ⟶ SNoLe (add_SNo x0 (minus_SNo x4)) x9 ⟶ False (proof)
Theorem 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 (proof)
Theorem 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 (proof)
Theorem 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 (proof)
Theorem 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 (proof)
Theorem 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 (proof)
Theorem 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 (proof)
Theorem 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 (proof)
Theorem 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 (proof)
Theorem 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 (proof)
Theorem 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 (proof)
Theorem 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 (proof)