[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
,
Theorem addarray-base
⊦ i ≤ 0 → addarray(r, val, i, st) = st
Type: An axiom
Validity: The proof is valid.
Features: localsimp,
Comment:
Used by:
1dim
,
add-at-05
,
add-put-switch
,
at-1dim-other-index-01
,
in-1dim-02
,
in-1dim-07
,
in-1dim-10
,
in-1dim-13
,
in-1dim-other-index-01
,
lookup-1dim-01
,
newref-1dim-02
,
shift-1dim-01
,
switch-addarray-addclass-01
,
switch-addarray-addobj-01
,
Used by units in proved state:
Proof exists?: No