[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 7 from proof at-write-at (
previous step
)
# ax0 = # ndx1, adr ∈ ax0, ∀ ndx0, adr1, fs0. # ndx1 = # ndx0 ∧ adr1 ∈ ax0 → fs0[ax0, ndx0][adr1] = ndx0[pos(adr1, ax0)] ⊦ fs[adr0, nd][ax0, ndx1][adr] = ndx1[pos(adr, ax0)], dups(ax0), adr0 ∈ ax0
Heuristic quantifier closing applied rule all left
And closed the goal!
Rule argument
pos: left 3 terms: ndx1, adr, fs[adr0, nd]
Additional information
Used terms: ndx1, adr, fs[adr0, nd]