[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 19 from proof multi-lengthin (previous step)

# refs2 = 1 + # refs1 + i→n(i2) * # refs1 + i→n(i2), lastn(1 + # refs1, refs2) = r0 ' + refs1, 1 + # refs1 = i→n(countrefs(i1 ' + ints1)), posints(ints1), 0 ≤ i1, 0 < i0, i2 < i0, 0 ≤ i2, # refs1 < # refs2, r ∈ firstn(i→n(i2) * # refs1 + i→n(i2), refs2) ∨ r = r1 → r -- _length ∈ addmultiarrays (r1 ' + firstn(i→n(i2) * # refs1 + i→n(i2), refs2), i2, r0 ' + acc, ty, i0 ' + i1 ' + ints1, addmultiarrays(r0 ' + refs1, i1, [], ty, i1 ' + ints1, st)) ∧ is_integervalue (addmultiarrays (r1 ' + firstn(i→n(i2) * # refs1 + i→n(i2), refs2), i2, r0 ' + acc, ty, i0 ' + i1 ' + ints1, addmultiarrays(r0 ' + refs1, i1, [], ty, i1 ' + ints1, st)) [r -- _length ]) ∧ 0 ≤ (addmultiarrays (r1 ' + firstn(i→n(i2) * # refs1 + i→n(i2), refs2), i2, r0 ' + acc, ty, i0 ' + i1 ' + ints1, addmultiarrays(r0 ' + refs1, i1, [], ty, i1 ' + ints1, st)) [r -- _length ] ) .intval, ∀ st, ty, acc, ints, i, r, refs0. # refs0 < # (r1 + refs2) → ( true → ( r ∈ refs0 ∧ # refs0 = i→n(countrefs(i ' + ints .rest)) ∧ ints ≠ [] ∧ 0 ≤ i ∧ posints(ints) ∧ ¬ 0 ∈ ints .butlast ∧ i ≤ ints .first → r -- _length ∈ addmultiarrays(refs0, i, acc, ty, ints, st) ∧ is_integervalue(addmultiarrays(refs0, i, acc, ty, ints, st)[r -- _length]) ∧ 0 ≤ (addmultiarrays(refs0, i, acc, ty, ints, st)[r -- _length]) .intval)) ⊦ refs2 = [], 0 = i0, (~1) = i2, r = r0, 0 ∈ (i1 ' + ints1) .butlast, r ∈ refs1, r -- _length ∈ addmultiarrays (r1 ' + firstn(i→n(i2) * # refs1 + i→n(i2), refs2), i2, r0 ' + acc, ty, i0 ' + i1 ' + ints1, addmultiarrays(r0 ' + refs1, i1, [], ty, i1 ' + ints1, st)) ∧ is_integervalue (addmultiarrays (r1 ' + firstn(i→n(i2) * # refs1 + i→n(i2), refs2), i2, r0 ' + acc, ty, i0 ' + i1 ' + ints1, addmultiarrays(r0 ' + refs1, i1, [], ty, i1 ' + ints1, st)) [r -- _length ]) ∧ ¬ (addmultiarrays (r1 ' + firstn(i→n(i2) * # refs1 + i→n(i2), refs2), i2, r0 ' + acc, ty, i0 ' + i1 ' + ints1, addmultiarrays(r0 ' + refs1, i1, [], ty, i1 ' + ints1, st)) [r -- _length ] ) .intval < 0, r ≠ r1 ∧ ¬ r ∈ refs2

User applied rule insert rewrite lemma

And obtained the following new goals

Proof step 16:
⊦ lastn(n, refs) = refs0 ∧ ¬ r ∈ refs0 ∧ r ∈ refs ∧ n ≤ # refs ∧ m = # refs - n → r ∈ firstn(m, refs)
Proof step 18:
¬ ( lastn(1 + # refs1, refs2) = r0 ' + refs1 ∧ ¬ r ∈ r0 ' + refs1 ∧ r ∈ refs2 ∧ 1 + # refs1 ≤ # refs2 ∧ i→n(i2) * # refs1 + i→n(i2) = # refs2 - 1 + # refs1), # refs2 = 1 + # refs1 + i→n(i2) * # refs1 + i→n(i2), lastn(1 + # refs1, refs2) = r0 ' + refs1, 1 + # refs1 = i→n(countrefs(i1 ' + ints1)), posints(ints1), 0 ≤ i1, 0 < i0, i2 < i0, 0 ≤ i2, # refs1 < # refs2, r ∈ firstn(i→n(i2) * # refs1 + i→n(i2), refs2) ∨ r = r1 → r -- _length ∈ addmultiarrays (r1 ' + firstn(i→n(i2) * # refs1 + i→n(i2), refs2), i2, r0 ' + acc, ty, i0 ' + i1 ' + ints1, addmultiarrays(r0 ' + refs1, i1, [], ty, i1 ' + ints1, st)) ∧ is_integervalue (addmultiarrays (r1 ' + firstn(i→n(i2) * # refs1 + i→n(i2), refs2), i2, r0 ' + acc, ty, i0 ' + i1 ' + ints1, addmultiarrays(r0 ' + refs1, i1, [], ty, i1 ' + ints1, st)) [r -- _length ]) ∧ 0 ≤ (addmultiarrays (r1 ' + firstn(i→n(i2) * # refs1 + i→n(i2), refs2), i2, r0 ' + acc, ty, i0 ' + i1 ' + ints1, addmultiarrays(r0 ' + refs1, i1, [], ty, i1 ' + ints1, st)) [r -- _length ] ) .intval, ∀ st, ty, acc, ints, i, r, refs0. # refs0 < # (r1 + refs2) → ( true → ( r ∈ refs0 ∧ # refs0 = i→n(countrefs(i ' + ints .rest)) ∧ ints ≠ [] ∧ 0 ≤ i ∧ posints(ints) ∧ ¬ 0 ∈ ints .butlast ∧ i ≤ ints .first → r -- _length ∈ addmultiarrays(refs0, i, acc, ty, ints, st) ∧ is_integervalue(addmultiarrays(refs0, i, acc, ty, ints, st)[r -- _length]) ∧ 0 ≤ (addmultiarrays(refs0, i, acc, ty, ints, st)[r -- _length]) .intval)) ⊦ refs2 = [], 0 = i0, (~1) = i2, r = r0, 0 ∈ (i1 ' + ints1) .butlast, r ∈ refs1, r -- _length ∈ addmultiarrays (r1 ' + firstn(i→n(i2) * # refs1 + i→n(i2), refs2), i2, r0 ' + acc, ty, i0 ' + i1 ' + ints1, addmultiarrays(r0 ' + refs1, i1, [], ty, i1 ' + ints1, st)) ∧ is_integervalue (addmultiarrays (r1 ' + firstn(i→n(i2) * # refs1 + i→n(i2), refs2), i2, r0 ' + acc, ty, i0 ' + i1 ' + ints1, addmultiarrays(r0 ' + refs1, i1, [], ty, i1 ' + ints1, st)) [r -- _length ]) ∧ ¬ (addmultiarrays (r1 ' + firstn(i→n(i2) * # refs1 + i→n(i2), refs2), i2, r0 ' + acc, ty, i0 ' + i1 ' + ints1, addmultiarrays(r0 ' + refs1, i1, [], ty, i1 ' + ints1, st)) [r -- _length ] ) .intval < 0, r ≠ r1 ∧ ¬ r ∈ refs2

Rule argument

[speclemmaarg: , lastn(n, refs) = refs0 ∧ ¬ r ∈ refs0 ∧ r ∈ refs ∧ n ≤ # refs ∧ m = # refs - n → r ∈ firstn(m, refs) ,[n, refs, refs0, r, m] → [1 + # refs1, refs2, r0 ' + refs1, r, i→n(i2) * # refs1 + i→n(i2)] ,F ,list-del ,references ,lastn-firstn-in-01 ]

Additional information

[[CONCRETESIMPRULES : ([CSIMPSEQ : ⊦ m * n = n * m], [CSIMPSEQ : ⊦ m + n = n + m], [CSIMPSEQ : ⊦ (ints + ints0) + ints1 = ints + ints0 + ints1], [CSIMPSEQ : ⊦ m + 1 ≤ n ↔ m < n], [CSIMPSEQ : ⊦ (m + n0) + n1 = m + n0 + n1], [CSIMPSEQ : ⊦ r ≠ r0 → (r ∈ r0 ' + refs ↔ r ∈ refs)], [CSIMPSEQ : ⊦ (refs + refs0) + refs1 = refs + refs0 + refs1], [CSIMPSEQ : ⊦ i ≤ j → (¬ ¬ j < i ↔ false)])], [EXTRATERMS : (1 + # refs1, refs2, r0 ' + refs1, r, i→n(i2) * # refs1 + i→n(i2))]]