[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,
Used simplifier rules/spec theorems by specification
Used from specification RGI-Conds
- RGI-Conds/g-r
is used by
g-r,
RG-restr-ok,
- RGI-Conds/g-refl
is used by
CSEQ-sat-rely-guar,
CRely-refl,
- RGI-Conds/init-ex
is used by
fair-never-violates-right-rely,
fair-never-violates-left-rely,
fair-always-right-relyinv,
fair-always-right-rely,
fair-always-left-relyinv,
fair-always-left-rely,
- RGI-Conds/init-idle
is used by
fair-never-violates-right-rely,
fair-never-violates-left-rely,
fair-always-right-relyinv,
fair-always-right-rely,
fair-always-left-relyinv,
fair-always-left-rely,
CSPAWN-sat-rely-guar,
- RGI-Conds/r-trans
is used by
RG-restr-ok,
- RGI-Conds/COP-sat-rely-guar
is used by
COP-sat-rely-guar,
- RGI-Conds/g-refl
is used by
CSEQ-sat-rely-guar,
- RGI-Conds/init-inv
is used by
fair-never-violates-right-rely,
fair-never-violates-left-rely,
fair-always-right-relyinv,
fair-always-right-rely,
fair-always-left-relyinv,
fair-always-left-rely,
CSPAWN-sat-rely-guar,
Used from specification nat
- nat/add-01
is used by
CSPAWN-sat-rely-guar-ind,
- nat/eqle-one
is used by
CSPAWN-sat-rely-guar-ind,
- nat/fle
is used by
CSPAWN-sat-rely-guar-ind,
CRelytosucc-CRelyto,
CInittosucc-Cinittp,
- nat/fle-01
is used by
fair-never-violates-left-rely,
fair-always-right-relyinv,
fair-always-right-rely,
fair-always-left-relyinv,
fair-always-left-rely,
RG-restr-ok,
CSPAWN-sat-rely-guar-ind,
CSEQ-sat-rely-guar,
COP-sat-rely-guar,
- nat/le-add
is used by
RG-restr-ok,
CSEQ-sat-rely-guar,
- nat/lels
is used by
CSEQ-sat-rely-guar,
- nat/lels-01
is used by
CSPAWN-sat-rely-guar-ind,
CRelytosucc-CRelyto,
CInittosucc-Cinittp,
- nat/lels-03
is used by
CSPAWN-sat-rely-guar-ind,
- nat/lep-02
is used by
CSPAWN-sat-rely-guar-ind,
CRelytosucc-CRely,
- nat/ler
is used by
CSPAWN-sat-rely-guar,
CInitto-Idle,
- nat/lez
is used by
CSPAWN-sat-rely-guar-ind,
- nat/lez-01
is used by
CSPAWN-sat-rely-guar-ind,
- nat/succ-01
is used by
CSPAWN-sat-rely-guar-ind,
CInitto-Idle-less,
Used from specification nat-basic2
- nat-basic2/a
is used by
fair-never-violates-right-rely,
fair-never-violates-left-rely,
fair-always-right-relyinv,
fair-always-right-rely,
fair-always-left-relyinv,
fair-always-left-rely,
RG-restr-ok,
CSPAWN-sat-rely-guar-ind,
CSEQ-sat-rely-guar,
CRelytosucc-CRelyto,
CRelytosucc-CRely,
CRely-refl,
COP-sat-rely-guar,
CInittosucc-Cinittp,
CInitto-Idle-less,
- nat-basic2/add-base
is used by
CSPAWN-sat-rely-guar-ind,
- nat-basic2/c
is used by
fair-never-violates-right-rely,
fair-never-violates-left-rely,
fair-always-right-relyinv,
fair-always-right-rely,
fair-always-left-relyinv,
fair-always-left-rely,
RG-restr-ok,
CSPAWN-sat-rely-guar-ind,
CSEQ-sat-rely-guar,
CRelytosucc-CRelyto,
CRelytosucc-CRely,
CRely-refl,
COP-sat-rely-guar,
CInittosucc-Cinittp,
CInitto-Idle-less,
- nat-basic2/eq
is used by
CRely-refl,
- nat-basic2/l
is used by
CSEQ-sat-rely-guar,
- nat-basic2/l-02
is used by
CSPAWN-sat-rely-guar-ind,
CRelytosucc-CRelyto,
CInittosucc-Cinittp,
- nat-basic2/oz
is used by
CSPAWN-sat-rely-guar-ind,
- nat-basic2/s
is used by
CSEQ-sat-rely-guar,
COP-sat-rely-guar,
- nat-basic2/succ
is used by
fair-never-violates-right-rely,
fair-never-violates-left-rely,
fair-always-right-relyinv,
fair-always-right-rely,
fair-always-left-relyinv,
fair-always-left-rely,
CSPAWN-sat-rely-guar-ind,
CSEQ-sat-rely-guar,
CRely-refl,
COP-sat-rely-guar,
Used from specification nat-basic1
- nat-basic1/f
is used by
fair-never-violates-right-rely,
fair-never-violates-left-rely,
fair-always-right-relyinv,
fair-always-right-rely,
fair-always-left-relyinv,
fair-always-left-rely,
RG-restr-ok,
CSPAWN-sat-rely-guar-ind,
CSPAWN-sat-rely-guar,
CSEQ-sat-rely-guar,
CRelytosucc-CRelyto,
COP-sat-rely-guar,
CInittosucc-Cinittp,
CInitto-Idle-less,
- nat-basic1/lf
is used by
fair-never-violates-right-rely,
fair-never-violates-left-rely,
fair-always-right-relyinv,
fair-always-right-rely,
fair-always-left-relyinv,
fair-always-left-rely,
CSPAWN-sat-rely-guar-ind,
- nat-basic1/lf-01
is used by
CSEQ-sat-rely-guar,
- nat-basic1/lf-02
is used by
CSEQ-sat-rely-guar,
- nat-basic1/ls-02
is used by
CSEQ-sat-rely-guar,
- nat-basic1/ref-1
is used by
CSEQ-sat-rely-guar,
COP-sat-rely-guar,
- nat-basic1/trans-1
is used by
fair-never-violates-right-rely,
fair-never-violates-left-rely,
fair-always-right-relyinv,
fair-always-right-rely,
fair-always-left-relyinv,
fair-always-left-rely,
CSPAWN-sat-rely-guar-ind,
- CSPAWN+Preds/CGuar-def
is used by
g-r,
RG-restr-ok,
CSEQ-sat-rely-guar,
CRely-refl,
COP-sat-rely-guar,
- CSPAWN+Preds/CGuarto-def
is used by
RG-restr-ok,
CSPAWN-sat-rely-guar-ind,
- CSPAWN+Preds/CInit-def
is used by
fair-never-violates-right-rely,
fair-never-violates-left-rely,
fair-always-right-relyinv,
fair-always-right-rely,
fair-always-left-relyinv,
fair-always-left-rely,
RG-restr-ok,
CSPAWN-sat-rely-guar-ind,
CSPAWN-sat-rely-guar,
CInitto-Idle-less,
CInitto-Idle,
- CSPAWN+Preds/CInitto-def
is used by
fair-never-violates-left-rely,
fair-always-right-relyinv,
fair-always-right-rely,
fair-always-left-relyinv,
fair-always-left-rely,
RG-restr-ok,
CSPAWN-sat-rely-guar-ind,
CSPAWN-sat-rely-guar,
CInittosucc-Cinittp,
CInitto-Idle-less,
CInitto-Idle,
- CSPAWN+Preds/CInv-def
is used by
g-r,
fair-never-violates-right-rely,
fair-never-violates-left-rely,
fair-always-right-relyinv,
fair-always-right-rely,
fair-always-left-relyinv,
fair-always-left-rely,
RG-restr-ok,
CSPAWN-sat-rely-guar,
CSEQ-sat-rely-guar,
CRely-refl,
COP-sat-rely-guar,
- CSPAWN+Preds/CRely-def
is used by
g-r,
RG-restr-ok,
CSEQ-sat-rely-guar,
COP-sat-rely-guar,
- CSPAWN+Preds/CRrelyto-def
is used by
RG-restr-ok,
CSPAWN-sat-rely-guar-ind,
CRelytosucc-CRelyto,
CRelytosucc-CRely,