[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
Status:
Proved!
Axioms: 1, User Theorems: 43 (Proved: 43, Partially proved: 0, Unproved: 0, Invalid: 0, Siginvalid: 0)
Proof steps: 1059, Interactions: 594
RG-restr-def(0,0)
not-pre1-term-unfair(37,20)
pre2-r2(4,1)
rg-blocked1-not-r1-unfair(22,12)
rg2-lem1-term-strnger-term-unfair(108,59)
rg2-not-pre1-unfair(14,8)
rg2-sound-main-unfair(46,24)
RG2-Sound+DF(15,11)
not-pre2-term-unfair(29,16)
r-g-r(1,0)
rg-blocked2-not-r2(19,11)
rg2-lem2-term(51,29)
rg2-not-pre2(13,8)
runs(4,1)
RG2-Sound+DF+Term(50,33)
post1-r1(4,1)
r1-trans(4,1)
rg-blocked2-not-r2-term(15,8)
rg2-lem2-term-strnger(50,29)
rg2-not-pre2-term(24,13)
RG2-Sound+DF+Term-unfair(24,17)
post1-runs2(4,1)
r2-trans(4,1)
rg-blocked2-not-r2-term-unfair(31,17)
rg2-lem2-term-strnger-term-unfair(108,63)
rg2-not-pre2-term-strnger(24,13)
RG2-Sound+DF-unfair(21,14)
post2-r1(4,1)
rg-blocked1-not-r1(18,10)
rg-blocked2-not-r2-unfair(22,12)
rg2-not-pre1(12,7)
rg2-not-pre2-unfair(14,8)
g1-r2(4,1)
post2-runs1(4,1)
rg-blocked1-not-r1-term(19,10)
rg2-lem1-term(51,29)
rg2-not-pre1-term(23,12)
rg2-sound-main(41,24)
g2-r1(4,1)
pre1-r1(4,1)
rg-blocked1-not-r1-term-unfair(30,17)
rg2-lem1-term-strnger(51,29)
rg2-not-pre1-term-strnger(23,12)
rg2-sound-main-term-unfair(9,8)