[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 RG2+DF-Theory-Ext
Status:
Proved!
Axioms: 17, User Theorems: 20 (Proved: 20, Partially proved: 0, Unproved: 0, Invalid: 0, Siginvalid: 0)
Proof steps: 380, Interactions: 218
RG2-Sound+DF(19,13)
init-pre-inv(0,0)
post2-runs1(0,0)
proc1-rg-totalcorr(0,0)
r2-refl(0,0)
rg2-lem1-term-strnger(42,23)
rg2-sound-main(31,18)
RG2-Sound+DF+Term(49,32)
inv-runs(0,0)
post2-stable-r2(0,0)
proc2-rg-totalcorr(0,0)
r2-trans(0,0)
rg2-lem2-term-strnger(42,23)
RG2-Strong-Total-Corr(33,20)
po1-g-r-stable(3,2)
pre1-g-r-stable(3,2)
r1-g2-r1(2,1)
rg-blocked1-not-r1(20,11)
rg2-not-pre1(13,7)
g1-r2(0,0)
po2-g-r-stable(3,2)
pre1-stable-r1(0,0)
r1-refl(0,0)
rg-blocked1-not-r1-term(16,8)
rg2-not-pre1-term-strnger(24,12)
g2-r1(0,0)
post1-runs2(0,0)
pre2-g-r-stable(3,2)
r1-trans(0,0)
rg-blocked2-not-r2(19,11)
rg2-not-pre2(14,8)
init-ex(0,0)
post1-stable-r1(0,0)
pre2-stable-r2(0,0)
r2-g1-r2(2,1)
rg-blocked2-not-r2-term(17,9)
rg2-not-pre2-term-strnger(25,13)