[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 44 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, ∀ 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)))) ⊦ (~1) = n→i(# acc) + i1, (~1) = i1, 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))), r ≠ r0 ∧ ¬ r ∈ refs1

User applied rule apply induction

And obtained the following new goals

Proof step 11:
# 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, ∀ 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)))) ⊦ # (r0 ' + firstn(i→n(countrefs(i0 ' + ints1)) * i→n(i1), refs1)) < # (r0 + refs1), (~1) = n→i(# acc) + i1, (~1) = i1, 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))), r ≠ r0 ∧ ¬ r ∈ refs1
Proof step 43:
r ∈ r0 ' + firstn(i→n(countrefs(i0 ' + ints1)) * i→n(i1), refs1) ∧ n→i(# (r1 ' + acc)) + i1 = ((n→i(# acc) + i1 + 1) ' + i0 ' + ints1) .first ∧ # (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 → 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))), # 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, ∀ 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)))) ⊦ (~1) = n→i(# acc) + i1, (~1) = i1, 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))), r ≠ r0 ∧ ¬ r ∈ refs1

Rule argument

[substlist-arg: [st, ty, ints, i, acc, r, refs0] → [addmultiarrays (r1 ' + refs, i0, [], ty, i0 ' + ints1, st), ty, (n→i(# acc) + i1 + 1) ' + i0 ' + ints1, i1, r1 ' + acc, r, r0 ' + firstn (i→n(countrefs(i0 ' + ints1)) * i→n(i1), refs1)] ]

Additional information

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