[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 split-prefix-append-to
⊦ # σ0 = ∞ → ((σ0 to n) + σ1 = σ0 ↔ σ1 = σ0 from n)
Type: A user defined theorem
Validity: The proof is valid.
Features: simp, localsimp,
Comment:
Used by:
emptystream-cancel
,
Used by units in proved state:
Proof exists?: Yes
View
the proof
Infos about the proof
Proved?: Yes
Interactions: 6
Proof steps: 11
Used lemmas:
Used spec theorems:
stream
/buffer-inf/
extensionality
stream
/buffer-inf/
get-from
stream
/buffer-inf/
get-append-ls
stream
/buffer-inf/
fin-size-from
Used simplifier rules:
stream
/buffer-inf/
to-plus-from-simp
stream
/buffer-inf/
size-append
nat-inf
/
add-inf-02
nat-inf
/
inf-less
nat-inf
/
add-comm
nat-inf
/
add-assoc
nat-basic2
/
l-02
nat-inf
/
ls-natinf-to-nat-2-1
nat-inf
/
add-fin
stream
/buffer-inf/
append-assoc
nat-basic2
/
c
nat-basic2
/
a
nat
/
eq-01
nat-inf-basic
/
sel
stream
/buffer-inf/
size-to
stream
/buffer-inf/
get-append-notls
nat-inf
/
less-inf1
nat-inf-basic
/
disj
stream-basic
/buffer-inf/
stream-fin-forward
nat-inf
/
less-inf2
stream
/buffer-inf/
size-fin
stream
/buffer-inf/
notfin-sizeinf
stream-basic
/buffer-inf/
stream-inf-forward
stream
/buffer-inf/
sel-inf
stream
/buffer-inf/
from-inf
stream
/buffer-inf/
size-inf