[Imprint][Data Privacy Statement][E-Mail]



View long theorem info. View the proof. Back to main index. View the specification. View theorem base summary, View theorem base listing, the used properties by spec, the dependency list, the symbol table,

Proof step 74 from proof long-automatic (previous step)

0 ≤ j ∨ j % 18446744073709551616 < ~9223372036854775808, 0 ≤ j ∨ ~9223372036854775808 ≤ j % 18446744073709551616, j < 0 ∨ j % 18446744073709551616 ≤ 9223372036854775807, j < 0 ∨ 9223372036854775807 < j % 18446744073709551616, (0 ≤ j ∧ j % 18446744073709551616 ≤ 9223372036854775807 ⊃ j % 18446744073709551616 ;(0 ≤ j ∧ 9223372036854775807 < j % 18446744073709551616 ⊃ j % 18446744073709551616 - 18446744073709551616 ;(j < 0 ∧ j % 18446744073709551616 < ~9223372036854775808 ⊃ 18446744073709551616 + j % 18446744073709551616 ;(j < 0 ∧ ~9223372036854775808 ≤ j % 18446744073709551616 ⊃ j % 18446744073709551616;j) ) ) ) < 0 ∨ 9223372036854775807 < (0 ≤ j ∧ j % 18446744073709551616 ≤ 9223372036854775807 ⊃ j % 18446744073709551616 ;(0 ≤ j ∧ 9223372036854775807 < j % 18446744073709551616 ⊃ j % 18446744073709551616 - 18446744073709551616 ;(j < 0 ∧ j % 18446744073709551616 < ~9223372036854775808 ⊃ 18446744073709551616 + j % 18446744073709551616 ;(j < 0 ∧ ~9223372036854775808 ≤ j % 18446744073709551616 ⊃ j % 18446744073709551616;j) ) ) ) % 18446744073709551616, (0 ≤ j ∧ j % 18446744073709551616 ≤ 9223372036854775807 ⊃ j % 18446744073709551616 ;(0 ≤ j ∧ 9223372036854775807 < j % 18446744073709551616 ⊃ j % 18446744073709551616 - 18446744073709551616 ;(j < 0 ∧ j % 18446744073709551616 < ~9223372036854775808 ⊃ 18446744073709551616 + j % 18446744073709551616 ;(j < 0 ∧ ~9223372036854775808 ≤ j % 18446744073709551616 ⊃ j % 18446744073709551616;j) ) ) ) < 0 ∨ (0 ≤ j ∧ j % 18446744073709551616 ≤ 9223372036854775807 ⊃ j % 18446744073709551616 ;(0 ≤ j ∧ 9223372036854775807 < j % 18446744073709551616 ⊃ j % 18446744073709551616 - 18446744073709551616 ;(j < 0 ∧ j % 18446744073709551616 < ~9223372036854775808 ⊃ 18446744073709551616 + j % 18446744073709551616 ;(j < 0 ∧ ~9223372036854775808 ≤ j % 18446744073709551616 ⊃ j % 18446744073709551616;j) ) ) ) % 18446744073709551616 ≤ 9223372036854775807, 0 ≤ (0 ≤ j ∧ j % 18446744073709551616 ≤ 9223372036854775807 ⊃ j % 18446744073709551616 ;(0 ≤ j ∧ 9223372036854775807 < j % 18446744073709551616 ⊃ j % 18446744073709551616 - 18446744073709551616 ;(j < 0 ∧ j % 18446744073709551616 < ~9223372036854775808 ⊃ 18446744073709551616 + j % 18446744073709551616 ;(j < 0 ∧ ~9223372036854775808 ≤ j % 18446744073709551616 ⊃ j % 18446744073709551616;j) ) ) ) ∨ ~9223372036854775808 ≤ (0 ≤ j ∧ j % 18446744073709551616 ≤ 9223372036854775807 ⊃ j % 18446744073709551616 ;(0 ≤ j ∧ 9223372036854775807 < j % 18446744073709551616 ⊃ j % 18446744073709551616 - 18446744073709551616 ;(j < 0 ∧ j % 18446744073709551616 < ~9223372036854775808 ⊃ 18446744073709551616 + j % 18446744073709551616 ;(j < 0 ∧ ~9223372036854775808 ≤ j % 18446744073709551616 ⊃ j % 18446744073709551616;j) ) ) ) % 18446744073709551616, 0 ≤ (0 ≤ j ∧ j % 18446744073709551616 ≤ 9223372036854775807 ⊃ j % 18446744073709551616 ;(0 ≤ j ∧ 9223372036854775807 < j % 18446744073709551616 ⊃ j % 18446744073709551616 - 18446744073709551616 ;(j < 0 ∧ j % 18446744073709551616 < ~9223372036854775808 ⊃ 18446744073709551616 + j % 18446744073709551616 ;(j < 0 ∧ ~9223372036854775808 ≤ j % 18446744073709551616 ⊃ j % 18446744073709551616;j) ) ) ) ∨ (0 ≤ j ∧ j % 18446744073709551616 ≤ 9223372036854775807 ⊃ j % 18446744073709551616 ;(0 ≤ j ∧ 9223372036854775807 < j % 18446744073709551616 ⊃ j % 18446744073709551616 - 18446744073709551616 ;(j < 0 ∧ j % 18446744073709551616 < ~9223372036854775808 ⊃ 18446744073709551616 + j % 18446744073709551616 ;(j < 0 ∧ ~9223372036854775808 ≤ j % 18446744073709551616 ⊃ j % 18446744073709551616;j) ) ) ) % 18446744073709551616 < ~9223372036854775808 ⊦ (¬ j < 0 ∧ ¬ 9223372036854775807 < j % 18446744073709551616 ⊃ j % 18446744073709551616 ;(¬ j < 0 ∧ ¬ j % 18446744073709551616 ≤ 9223372036854775807 ⊃ j % 18446744073709551616 - 18446744073709551616 ;(¬ 0 ≤ j ∧ ¬ ~9223372036854775808 ≤ j % 18446744073709551616 ⊃ 18446744073709551616 + j % 18446744073709551616 ;(¬ 0 ≤ j ∧ ¬ j % 18446744073709551616 < ~9223372036854775808 ⊃ j % 18446744073709551616;j) ) ) ) = j

Heuristic if-then-else split applied rule case distinction

And closed the goal!

Rule argument

pos: left 5

Additional information

Used simplifier rules: ⊦ i < j ∧ ¬ i0 < j → ¬ i0 < i;% ⊦ i < 0 ∧ 0 ≤ j → i < j;% ⊦ i < j → (¬ ¬ j ≤ i ↔ false);% ⊦ j < i ∧ i ≤ 0 → j < 0; (forward)% ⊦ i < (* j) ∧ j < 0 → i < 0; (forward)% ⊦ i < 0 ∧ 0 ≤ j → i ≤ j;%0 < j ⊦ i % (* j) < 0 ↔ i < 0 ∧ i % j ≠ 0;% ⊦ 0 < j → ¬ j + i % j < 0;% ⊦ i + j + i0 = (i + j) + i0;% ⊦ i + j = j + i;% ⊦ i ≤ j → (¬ ¬ j < i ↔ false);% ⊦ i ≤ 0 ∧ 0 ≤ j → i ≤ j;% ⊦ ¬ i < j ↔ j ≤ i;%j0 ≠ 0, j ≤ j0 ⊦ i ≤ (* j) → i ≤ (* j0);