[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 RG-I-2-Theory
Status:
Proved!
Axioms: 1, User Theorems: 37 (Proved: 37, Partially proved: 0, Unproved: 0, Invalid: 0, Siginvalid: 0)
Proof steps: 793, Interactions: 431
RG-restr-def(0,0)
fair-always-left-rely(60,34)
g2-r1(2,0)
post2-r2(2,0)
r1-refl(2,0)
rg-blocked2-not-r2-term-unfair(3,1)
rg2-sound+term-unfair-main(11,8)
RG-restr-sym(6,0)
fair-always-right-rely(2,1)
i-r1-i(2,0)
pre1-i(2,0)
r1-trans(2,0)
rg-blocked2-not-r2-unfair(5,3)
rg2-sound-main-unfair(61,38)
RG2-Sound(3,2)
fair-never-violates-left-rely(14,7)
i-r2-i(2,0)
pre1-r1(2,0)
r2-refl(2,0)
rg2-lem1-term-unfair(211,120)
RG2-Sound+Term(3,2)
fair-never-violates-right-rely(3,1)
not-pre1-term-unfair(27,14)
pre2-i(2,0)
r2-trans(2,0)
rg2-lem2-term-unfair(184,104)
RG2-Sound+Term-unfair(21,15)
fair-sustains-implies-always(71,42)
not-pre2-term-unfair(3,1)
pre2-r2(2,0)
rg-blocked1-not-r1-term-unfair(23,12)
rg2-not-pre1-unfair(15,8)
RG2-Sound-unfair(7,7)
g1-r2(2,0)
post1-r1(2,0)
r-g-r(12,0)
rg-blocked1-not-r1-unfair(15,8)
rg2-not-pre2-unfair(5,3)