[Imprint]
[Data Privacy Statement]
[E-Mail]
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 base summary for Specification product-refine
Status:
Proved!
Axioms: 16, User Theorems: 32 (Proved: 32, Partially proved: 0, Unproved: 0, Invalid: 0, Siginvalid: 0)
Proof steps: 1141, Interactions: 620
finfrag-repl-frag(135,67)
lift-get(11,1)
nounsharedextR-notcodren(2,0)
repl-frag(119,74)
repla-rec-addS(0,0)
repls-infrec-addS(18,10)
replstate-fin-def(0,0)
finfrag-repla-sametrace(44,23)
lift-rec(0,0)
nounsharedextR-notcodren-internal(4,2)
repl-size(81,52)
repla-rec-addboth(0,0)
repls-infrec-addboth(42,22)
replstate-inf(9,7)
finfrag-repla-sametrace-1(14,6)
lift-size(4,0)
nounsharedextR-notcodren-project(2,1)
repla-base(0,0)
repla-rec-skip(0,0)
repls-infrec-skip(15,9)
replstate-inf-def(0,0)
finfrag-repls-head(29,12)
mon-repla(4,2)
product-ok-refine-cext-imp-aext(36,22)
repla-infrec-addS(18,10)
replaction-fin-def(0,0)
repls-mon(107,53)
same-concrete-abstract(3,2)
frag-repla-sametrace(105,68)
mon-repla-1(23,13)
refines-product(33,18)
repla-infrec-addboth(42,22)
replaction-inf(3,1)
repls-rec-addS(0,0)
sameshared-def(0,0)
frag-repls-head(73,38)
mon-repls(5,2)
repl-exec(22,11)
repla-infrec-skip(15,9)
replaction-inf-def(0,0)
repls-rec-addboth(0,0)
sameshared-notcodc-notcoda(3,2)
lift-base(0,0)
nounsharedextR-def(0,0)
repl-fin-size(48,23)
repla-mon(72,38)
repls-base(0,0)
repls-rec-skip(0,0)