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

1 + # refs2 = n + i→n(countrefs(i1 ' + ints1)), lastn(i→n(countrefs(i1 ' + ints1)), r1 ' + refs2) = r0 ' + refs1, # refs2 = i→n(countrefs(i1 ' + ints1)) * i→n(i2) + i→n(countrefs(i1 ' + ints1)), (addmultiarrays(r0 ' + refs1, i1, [], ty, i1 ' + ints1, st)[r -- _length]) = intval(i3), 0 ≤ i3, r ∈ addmultiarrays(r0 ' + refs1, i1, [], ty, i1 ' + ints1, st), i→n(countrefs(i1 ' + ints1)) ≤ 1 + # refs2, 0 ≤ i2, i2 < i0, 0 < i0, 0 ≤ i1, posints(ints1), r -- _length ∈ addmultiarrays(r0 ' + refs1, i1, [], ty, i1 ' + ints1, st), r ∈ refs2, ∀ 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)) ⊦ r = r1, (~1) = i2, 0 = i0, r ∈ firstn(i→n(countrefs(i1 ' + ints1)) * i→n(i2), refs2), 0 ∈ (i1 ' + ints1) .butlast, r -- _length ∈ addmultiarrays (r1 ' + firstn(i→n(countrefs(i1 ' + ints1)) * 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(countrefs(i1 ' + ints1)) * 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(countrefs(i1 ' + ints1)) * i→n(i2), refs2), i2, r0 ' + acc, ty, i0 ' + i1 ' + ints1, addmultiarrays(r0 ' + refs1, i1, [], ty, i1 ' + ints1, st)) [r -- _length ] ) .intval < 0, r ≠ r0 ∧ ¬ r ∈ refs1 ∧ i→n(countrefs(i1 ' + ints1)) * i→n(i2) = n

User applied rule insert rewrite lemma

And obtained the following new goals

Proof step 24:
⊦ rk ∈ st ∧ # refs = i→n(countrefs(i ' + ints .rest)) ∧ ints ≠ [] ∧ 0 ≤ i ∧ posints(ints) ∧ ¬ 0 ∈ ints .butlast ∧ i ≤ ints .first → rk ∈ addmultiarrays(refs, i, acc, ty, ints, st)
Proof step 25:
⊦ 0 ≤ i2 → i→n(countrefs(i2 ' + i1 ' + ints1)) = i→n(countrefs(i1 ' + ints1)) * i→n(i2) + 1
Proof step 31:
r -- _length ∈ addmultiarrays(r0 ' + refs1, i1, [], ty, i1 ' + ints1, st) ∧ # (r1 ' + firstn(i→n(countrefs(i1 ' + ints1)) * i→n(i2), refs2)) = i→n(countrefs(i2 ' + (i0 ' + i1 ' + ints1) .rest)) ∧ i0 ' + i1 ' + ints1 ≠ [] ∧ 0 ≤ i2 ∧ posints(i0 ' + i1 ' + ints1) ∧ ¬ 0 ∈ (i0 ' + i1 ' + ints1) .butlast ∧ i2 ≤ (i0 ' + i1 ' + ints1) .first, 1 + # refs2 = n + i→n(countrefs(i1 ' + ints1)), lastn(i→n(countrefs(i1 ' + ints1)), r1 ' + refs2) = r0 ' + refs1, # refs2 = i→n(countrefs(i1 ' + ints1)) * i→n(i2) + i→n(countrefs(i1 ' + ints1)), (addmultiarrays(r0 ' + refs1, i1, [], ty, i1 ' + ints1, st)[r -- _length]) = intval(i3), 0 ≤ i3, r ∈ addmultiarrays(r0 ' + refs1, i1, [], ty, i1 ' + ints1, st), i→n(countrefs(i1 ' + ints1)) ≤ 1 + # refs2, 0 ≤ i2, i2 < i0, 0 < i0, 0 ≤ i1, posints(ints1), r -- _length ∈ addmultiarrays(r0 ' + refs1, i1, [], ty, i1 ' + ints1, st), r ∈ refs2, ∀ 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)) ⊦ r = r1, (~1) = i2, 0 = i0, r ∈ firstn(i→n(countrefs(i1 ' + ints1)) * i→n(i2), refs2), 0 ∈ (i1 ' + ints1) .butlast, true ∧ is_integervalue (addmultiarrays (r1 ' + firstn(i→n(countrefs(i1 ' + ints1)) * 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(countrefs(i1 ' + ints1)) * i→n(i2), refs2), i2, r0 ' + acc, ty, i0 ' + i1 ' + ints1, addmultiarrays(r0 ' + refs1, i1, [], ty, i1 ' + ints1, st)) [r -- _length ] ) .intval < 0, r ≠ r0 ∧ ¬ r ∈ refs1 ∧ i→n(countrefs(i1 ' + ints1)) * i→n(i2) = n

Rule argument

[crewrite-arg: multi-refin , F , [st, ints, ty, acc, i, refs, rk] → [addmultiarrays(r0 ' + refs1, i1, [], ty, i1 ' + ints1, st), i0 ' + i1 ' + ints1, ty, r0 ' + acc, i2, r1 ' + firstn(i→n(countrefs(i1 ' + ints1)) * i→n(i2), refs2), r -- _length] ]

Additional information

[[CONCRETESIMPRULES : ([CSIMPSEQ : ⊦ m * n = n * m], [CSIMPSEQ : ⊦ m0 * m * n = (m0 * m) * n], [CSIMPSEQ : ⊦ (m + n0) + n1 = m + n0 + n1], [CSIMPSEQ : ⊦ m + n = n + m], [CSIMPSEQ : ⊦ # (refs + refs0) = # refs + # refs0], [CSIMPSEQ : ⊦ # r ' = 0 +1], [CSIMPSEQ : ⊦ # firstn(n, refs) = n], [CSIMPSEQ : ⊦ (refs + refs0) + refs1 = refs + refs0 + refs1], [CSIMPSEQ : ⊦ (i ' + ints) .rest = ints], [CSIMPSEQ : ⊦ (ints + ints0) + ints1 = ints + ints0 + ints1], [CSIMPSEQ : ⊦ m + n = m + n0 ↔ n = n0], [CSIMPSEQ : ⊦ ¬ ints + ints0 ≠ [] ↔ ints = [] ∧ ints0 = []], [CSIMPSEQ : ⊦ i ' ≠ []], [CSIMPSEQ : ⊦ ¬ i ≤ j ↔ j < i], [CSIMPSEQ : ⊦ i ≤ j → (¬ ¬ j < i ↔ false)], [CSIMPSEQ : ⊦ 0 < i → ( posints(i ' + ints) ↔ posints(ints))], [CSIMPSEQ : ⊦ posints(i ' + ints) ↔ 0 ≤ i ∧ posints(ints)], [CSIMPSEQ : ⊦ (ints + i ' + ints0) .butlast = ints + (i ' + ints0) .butlast], [CSIMPSEQ : ⊦ i ≠ i0 → (i ∈ i0 ' + ints ↔ i ∈ ints)], [CSIMPSEQ : ⊦ (i ' + ints) .first = i], [CSIMPSEQ : ⊦ i < j → ¬ j < i])], [EXTRATERMS : (addmultiarrays (r0 ' + refs1, i1, [], ty, i1 ' + ints1, st), i0 ' + i1 ' + ints1, ty, r0 ' + acc, i2, r1 ' + firstn (i→n(countrefs(i1 ' + ints1)) * i→n(i2), refs2), r -- _length)]]