[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 33 from proof keys-shift-left (
previous step
)
n0 + 1 < # zbrar, n0 < n, n < # zbrar, nused < # zbrar, n0 < # zbrar, n0 < nused, sorted(zbrar, 0, nused + 1), n ≤ nused ⊦ zbrar[n0].key = zbrar[n].key, ∃ n1. n1 < nused ∧ (n1 < n ⊃ zbrar[n1];zbrar[n1 + 1]).key = zbrar[n0].key
User applied rule exists right
And closed the goal!
Rule argument
pos: right 2 terms: n0 abort: F discard: F computed: T
Additional information
Used terms: n0