[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
- RG-I-2-Theory/fair-never-violates-left-rely
is used by
progress-left-aux,
progress-left,
no-progress-left-aux,
no-progress-left,
- RG-I-2-Theory/fair-never-violates-right-rely
is used by
progress-left-aux,
progress-left,
no-progress-left-aux0,
no-progress-left-aux,
no-progress-left,
- RG-I-2-Theory/RG-restr-sym
is used by
progress-right-aux,
progress-right,
no-progress-right-aux,
no-progress-right,
no-init-violation-right,
- RG-I-2-Theory/g1-r2
is used by
progress-left-aux,
progress-left,
no-progress-left-aux,
no-progress-left,
- RG-I-2-Theory/g2-r1
is used by
progress-left-aux,
progress-left,
no-progress-left-aux0,
no-progress-left-aux,
no-progress-left,
no-init-violation-left,
- RG-I-2-Theory/r1-refl
is used by
progress-left,
- RG-I-2-Theory/r1-trans
is used by
progress-left-aux,
progress-left,
no-progress-left-aux0,
no-progress-left-aux,
no-progress-left,
no-init-violation-left,
- RG-I-2-Theory/r2-refl
is used by
progress-left,
no-progress-left-aux,
- RG-I-2-Theory/r2-trans
is used by
progress-left-aux,
progress-left,
no-progress-left-aux,
no-progress-left,
Used from specification nat-basic2
- nat-basic2/a
is used by
progress-left-aux,
progress-left,
no-progress-left-aux0,
no-progress-left-aux,
no-progress-left,
no-init-violation-left,
- nat-basic2/c
is used by
progress-left-aux,
progress-left,
no-progress-left-aux0,
no-progress-left-aux,
no-progress-left,
no-init-violation-left,
- nat-basic2/s
is used by
progress-left-aux,
progress-left,
no-progress-left-aux0,
no-progress-left-aux,
no-progress-left,
no-init-violation-left,
- nat-basic2/succ
is used by
progress-left-aux,
progress-left,
no-progress-left-aux0,
no-progress-left-aux,
no-progress-left,
no-init-violation-left,
Used from specification nat-basic1