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

¬ ( ¬ 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, 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))), r ∈ firstn(i→n(countrefs(i0 ' + ints1)) * i→n(i1), refs1)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Proof step 20:
⊦ 0 ≤ i2 → i→n(countrefs(i2 ' + i1 ' + ints1)) = i→n(countrefs(i1 ' + ints1)) * i→n(i2) + 1
Proof step 22:
# 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, 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))), r ∈ firstn(i→n(countrefs(i0 ' + ints1)) * i→n(i1), refs1), posints((n→i(# acc) + i1 + 1) ' + i0 ' + ints1)

Rule argument

[emptyarg]

Additional information

[[CONCRETESIMPRULES : ([CSIMPSEQ : ⊦ ¬ n→i(n) + 1 < 0], [CSIMPSEQ : ⊦ i + j < j ↔ i < 0], [CSIMPSEQ : ⊦ (i ' + ints) .first = i], [CSIMPSEQ : ⊦ i + j + i0 = (i + j) + i0], [CSIMPSEQ : ⊦ ((* j)) = i0 + ((* j0)) ↔ j - j0 = i0], [CSIMPSEQ : ⊦ ¬ i ∈ ints → (i ∈ i0 ' + ints ↔ i = i0)], [CSIMPSEQ : ⊦ (ints + i ' + ints0) .butlast = ints + (i ' + ints0) .butlast], [CSIMPSEQ : ⊦ i ≤ j → (¬ ¬ j < i ↔ false)], [CSIMPSEQ : ⊦ ¬ i ≤ j ↔ j < i], [CSIMPSEQ : ⊦ i ' ≠ []], [CSIMPSEQ : ⊦ ¬ ints + ints0 ≠ [] ↔ ints = [] ∧ ints0 = []], [CSIMPSEQ : ⊦ m + n = m + n0 ↔ n = n0], [CSIMPSEQ : ⊦ (ints + ints0) + ints1 = ints + ints0 + ints1], [CSIMPSEQ : ⊦ (i ' + ints) .rest = ints], [CSIMPSEQ : ⊦ # firstn(n, refs) = n], [CSIMPSEQ : ⊦ # r ' = 0 +1], [CSIMPSEQ : ⊦ # (refs + refs0) = # refs + # refs0], [CSIMPSEQ : ⊦ (refs + refs0) + refs1 = refs + refs0 + refs1], [CSIMPSEQ : ⊦ r ≠ r0 → (r ∈ r0 ' + refs ↔ r ∈ refs)], [CSIMPSEQ : ⊦ m + n = n + m], [CSIMPSEQ : ⊦ (m + n0) + n1 = m + n0 + n1], [CSIMPSEQ : ⊦ m0 * m * n = (m0 * m) * n], [CSIMPSEQ : ⊦ m * n = n * m], [CSIMPSEQ : ⊦ i + j = j + i])]]