[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 100 from proof inv-gc-copy (
previous step
)
ndx1 = ndx ⊦ ⟪gjournal_split_nodes#(n; ndx, ndx0)⟫ (ndx1 = ndx0 + ndx ∧ ndx0.flashsize ≤ n ∧ (ndx = [] ∨ ndx0.flashsize + ndx.head.flashsize > n))
Lemma
prepost-split-nodes