[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,

Lemma dependency for Specification RG-I-n-Theory

A lemma (entry) may depend on lemmas (entries) below its position, but never on lemmas above its position. This means the list is a topological order of the dependency graph. An entry 'all subs proved' means that all used lemmas are (transitively) proved.

Name:	Status:	Subs proved?	Used:
CSPAWN-sat-rely-guar	proved	all subs proved	CSPAWN-sat-rely-guar-ind,
CSPAWN-sat-rely-guar-ind	proved	all subs proved	CRelytosucc-CRelyto, CRelytosucc-CRely, CInittosucc-Cinittp, RG-restr-ok, CInitto-Idle, CSEQ-sat-rely-guar,
fair-never-violates-right-rely	proved	all subs proved	CRelytosucc-CRelyto, CRelytosucc-CRely, RG-restr-ok,
fair-never-violates-left-rely	proved	all subs proved	CRelytosucc-CRelyto, CRelytosucc-CRely, RG-restr-ok,
fair-always-right-relyinv	proved	all subs proved	CRelytosucc-CRelyto, CRelytosucc-CRely, RG-restr-ok,
fair-always-right-rely	proved	all subs proved	CRelytosucc-CRelyto, CRelytosucc-CRely, RG-restr-ok,
fair-always-left-relyinv	proved	all subs proved	CRelytosucc-CRelyto, CRelytosucc-CRely, RG-restr-ok,
fair-always-left-rely	proved	all subs proved	CRelytosucc-CRelyto, CRelytosucc-CRely, RG-restr-ok,
CSEQ-sat-rely-guar	proved	all subs proved	CRely-refl, COP-sat-rely-guar,
RG-restr-ok	proved	all subs proved	CRely-refl,
CRely-refl	proved	all subs proved	g-r,
CInitto-Idle	proved	all subs proved
CInittosucc-Cinittp	proved	all subs proved
CRelytosucc-CRely	proved	all subs proved
CRelytosucc-CRelyto	proved	all subs proved
COP-sat-rely-guar	proved	all subs proved
g-r	proved	all subs proved