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

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

User applied rule insert rewrite lemma

And obtained the following new goals

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

Rule argument

[crewrite-arg: multi-at-other , F , [sk, r, st, ints, ty, acc, i, refs] → [_length, r, addmultiarrays(r1 ' + refs, i0, [], ty, i0 ' + ints1, st), (n→i(# acc) + i1 + 1) ' + i0 ' + ints1, ty, r1 ' + acc, i1, r0 ' + firstn(i→n(countrefs(i0 ' + ints1)) * i→n(i1), refs1)] ]

Additional information

[[CONCRETESIMPRULES : ()], [EXTRATERMS : (_length, r, addmultiarrays (r1 ' + refs, i0, [], ty, i0 ' + ints1, st), (n→i(# acc) + i1 + 1) ' + i0 ' + ints1, ty, r1 ' + acc, i1, r0 ' + firstn (i→n(countrefs(i0 ' + ints1)) * i→n(i1), refs1))]]