[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 21 from proof copy-comp (
previous step
)
i2 < i1, i + i4 * (i1 - i2) < i3, 0 ≤ i2, 0 ≤ i4, 0 ≤ j0, j0 ≤ i4, 0 ≤ i, ∀ j. 0 ≤ j ∧ j < i3 → st[r -- (i1 + j) '] = st[r -- (i2 + j) '] ⊦ st[r -- (i1 + i + j0 * (i1 - i2)) '] = st[r -- (i1 + i) ']
A spec-lemma