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: |
|---|
| RG2-Strong-Total-Corr | proved | all subs proved
| inv-runs,
proc2-rg-totalcorr,
proc1-rg-totalcorr,
RG2-Sound+DF+Term,
|
| RG2-Sound+DF+Term | proved | all subs proved
| init-pre-inv,
rg2-lem2-term-strnger,
rg2-lem1-term-strnger,
rg2-not-pre2-term-strnger,
rg2-not-pre1-term-strnger,
inv-runs,
RG2-Sound+DF,
|
| RG2-Sound+DF | proved | all subs proved
| init-pre-inv,
rg2-sound-main,
rg2-not-pre2,
rg2-not-pre1,
inv-runs,
|
| rg2-lem1-term-strnger | proved | all subs proved
| po2-g-r-stable,
rg-blocked2-not-r2-term,
rg-blocked1-not-r1-term,
r2-refl,
post2-runs1,
r1-refl,
post1-runs2,
inv-runs,
|
| rg2-lem2-term-strnger | proved | all subs proved
| rg-blocked2-not-r2-term,
po1-g-r-stable,
rg-blocked1-not-r1-term,
r2-refl,
post2-runs1,
r1-refl,
post1-runs2,
inv-runs,
|
| rg2-sound-main | proved | all subs proved
| po2-g-r-stable,
rg-blocked2-not-r2,
po1-g-r-stable,
rg-blocked1-not-r1,
post2-runs1,
post1-runs2,
r2-refl,
r1-refl,
inv-runs,
|
| rg-blocked1-not-r1 | proved | all subs proved
| r1-trans,
r1-g2-r1,
r2-refl,
inv-runs,
|
| rg-blocked2-not-r2 | proved | all subs proved
| r2-trans,
r2-g1-r2,
r1-refl,
inv-runs,
|
| rg-blocked1-not-r1-term | proved | all subs proved
| r1-trans,
r1-g2-r1,
r2-refl,
inv-runs,
|
| rg-blocked2-not-r2-term | proved | all subs proved
| r2-trans,
r2-g1-r2,
r1-refl,
inv-runs,
|
| rg2-not-pre1-term-strnger | proved | all subs proved
| pre1-g-r-stable,
r2-refl,
inv-runs,
|
| rg2-not-pre2-term-strnger | proved | all subs proved
| pre2-g-r-stable,
r1-refl,
inv-runs,
|
| rg2-not-pre1 | proved | all subs proved
| pre1-g-r-stable,
r2-refl,
inv-runs,
|
| rg2-not-pre2 | proved | all subs proved
| pre2-g-r-stable,
r1-refl,
inv-runs,
|
| pre2-g-r-stable | proved | all subs proved
| g1-r2,
r2-trans,
pre2-stable-r2,
|
| pre1-g-r-stable | proved | all subs proved
| g2-r1,
r1-trans,
pre1-stable-r1,
|
| po1-g-r-stable | proved | all subs proved
| g2-r1,
r1-trans,
post1-stable-r1,
|
| po2-g-r-stable | proved | all subs proved
| g1-r2,
r2-trans,
post2-stable-r2,
|
| r2-g1-r2 | proved | all subs proved
| g1-r2,
r2-trans,
|
| r1-g2-r1 | proved | all subs proved
| g2-r1,
r1-trans,
|
| post1-runs2 | axiom | | |
| post2-runs1 | axiom | | |
| r1-refl | axiom | | |
| r2-refl | axiom | | |
| pre2-stable-r2 | axiom | | |
| pre1-stable-r1 | axiom | | |
| post2-stable-r2 | axiom | | |
| r2-trans | axiom | | |
| g1-r2 | axiom | | |
| post1-stable-r1 | axiom | | |
| r1-trans | axiom | | |
| g2-r1 | axiom | | |
| proc1-rg-totalcorr | axiom | | |
| proc2-rg-totalcorr | axiom | | |
| inv-runs | axiom | | |
| init-pre-inv | axiom | | |