[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 two-mon-size
mon(⌜σf⌝ ), mon(⌜σg⌝ ), ∀ n. # σf(n) = # σg(n) + ⌜m⌝ ⊦ # lim(⌜σf⌝ ) = # lim(⌜σg⌝ ) + ⌜m⌝
Type: A user defined theorem
Validity: The proof is valid.
Features:
Comment:
Used by:
Used by units in proved state:
Proof exists?: Yes
View
the proof
Infos about the proof
Proved?: Yes
Interactions: 43
Proof steps: 75
Used lemmas:
lim-def
,
Used spec theorems:
stream
/
prefix-def
stream
/
extensionality
nat-inf
/
lele-refl
stream
/
size-to
nat-inf
/
add-assoc
Used simplifier rules:
stream
/
sel-inf
nat-inf
/
less-inf2
stream
/
size-inf
stream
/
fun-nonempty
nat-inf
/
addeqinf-cancel
nat-inf
/
add-assoc
nat-inf
/
add-comm
nat-inf
/
less-inf1
stream
/
size-succ
nat-basic
/
c
nat-basic
/
a
nat-inf
/
add-fin
nat
/
elim-sub
nat-inf
/
ls-natinf-to-nat-2-1
nat-inf
/
add-ls-cancel-01
nat
/
lep
nat-inf
/
add-cancel-01
nat-inf
/
less-succ-leq
stream
/
append-assoc
stream
/
size-to
stream
/
size-to-02
stream
/
size-append
nat-inf
/
inf-inseq-reduce
nat-inf
/
add-all-inf
nat-inf
/
disj-rqui-infty
stream
/
size-fin
nat-inf
/
add-cancel-03
nat-inf
/
sum-zero-fin
nat-basic
/
f
nat-inf
/
ls-lsadd
nat
/
le-def
nat-basic
/
refl-nat
nat-inf
/
less-fin
stream
/
finlen-tolen-02
nat-inf
/
add-inf2
stream
/
get-append2-fin
stream
/
append-inf
stream
/
append-empty
stream
/
empty
list
/
a
list
/
app
list
/
Nil
nat-basic
/
add-base
list-data
/
size-nil
nat-basic
/
lf-02
stream
/
sel-fin
stream
/
appfin-sel
list
/
len
nat-inf
/
eq-natinf-to-nat-2-1
list-data
/
l
nat-inf
/
inj-rqui
nat-basic
/
l-02
nat-inf
/
ls-le
nat-inf
/
ls-trans
nat-inf
/
inf-less
nat-inf
/
add-cancel-02
nat-inf
/
add-cancel-num-02