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-Sound+DF+Term-unfair | proved | all subs proved
| RG-restr-def,
rg2-sound-main-term-unfair,
not-pre2-term-unfair,
not-pre1-term-unfair,
RG2-Sound+DF-unfair,
|
| RG2-Sound+DF+Term | proved | all subs proved
| RG-restr-def,
rg2-lem2-term,
rg2-lem1-term,
rg2-not-pre2-term,
rg2-not-pre1-term,
RG2-Sound+DF,
|
| RG2-Sound+DF-unfair | proved | all subs proved
| RG-restr-def,
rg2-sound-main-unfair,
rg2-not-pre2-unfair,
rg2-not-pre1-unfair,
|
| rg2-sound-main-term-unfair | proved | all subs proved
| rg2-lem2-term-strnger-term-unfair,
rg2-lem1-term-strnger-term-unfair,
|
| RG2-Sound+DF | proved | all subs proved
| RG-restr-def,
rg2-sound-main,
rg2-not-pre2,
rg2-not-pre1,
|
| rg2-lem1-term-strnger-term-unfair | proved | all subs proved
| post2-r1,
post2-runs1,
rg-blocked2-not-r2-term-unfair,
rg-blocked1-not-r1-term-unfair,
r2-trans,
g1-r2,
RG-restr-def,
post1-r1,
r1-trans,
g2-r1,
post1-runs2,
runs,
|
| rg2-lem2-term-strnger-term-unfair | proved | all subs proved
| rg-blocked2-not-r2-term-unfair,
rg-blocked1-not-r1-term-unfair,
r2-trans,
g1-r2,
r-g-r,
RG-restr-def,
post1-r1,
r1-trans,
g2-r1,
post1-runs2,
runs,
|
| rg2-sound-main-unfair | proved | all subs proved
| rg-blocked2-not-r2-unfair,
post2-r1,
post2-runs1,
r-g-r,
rg-blocked1-not-r1-unfair,
r2-trans,
g1-r2,
post1-r1,
r1-trans,
g2-r1,
post1-runs2,
runs,
RG-restr-def,
|
| rg2-lem1-term | proved | all subs proved
| post2-r1,
post2-runs1,
rg-blocked2-not-r2-term,
rg-blocked1-not-r1-term,
r2-trans,
g1-r2,
post1-r1,
r1-trans,
g2-r1,
post1-runs2,
runs,
|
| rg2-lem2-term | proved | all subs proved
| rg-blocked2-not-r2-term,
post2-r1,
post2-runs1,
r-g-r,
post1-r1,
r1-trans,
post1-runs2,
g2-r1,
runs,
rg-blocked1-not-r1-term,
r2-trans,
g1-r2,
|
| rg2-sound-main | proved | all subs proved
| rg-blocked2-not-r2,
post2-r1,
post2-runs1,
r-g-r,
rg-blocked1-not-r1,
r2-trans,
g1-r2,
post1-r1,
r1-trans,
g2-r1,
post1-runs2,
runs,
|
| rg2-lem2-term-strnger | proved | all subs proved
| rg-blocked2-not-r2-term,
post2-r1,
post2-runs1,
r-g-r,
post1-r1,
r1-trans,
post1-runs2,
g2-r1,
runs,
r2-trans,
g1-r2,
rg-blocked1-not-r1-term,
|
| rg2-lem1-term-strnger | proved | all subs proved
| post2-r1,
post2-runs1,
rg-blocked2-not-r2-term,
rg-blocked1-not-r1-term,
r2-trans,
g1-r2,
post1-r1,
r1-trans,
g2-r1,
post1-runs2,
runs,
|
| rg-blocked1-not-r1-unfair | proved | all subs proved
| r1-trans,
g2-r1,
r-g-r,
RG-restr-def,
|
| rg-blocked1-not-r1 | proved | all subs proved
| r1-trans,
g2-r1,
r-g-r,
|
| rg-blocked1-not-r1-term-unfair | proved | all subs proved
| r1-trans,
g2-r1,
r-g-r,
|
| rg-blocked1-not-r1-term | proved | all subs proved
| r1-trans,
g2-r1,
r-g-r,
|
| not-pre1-term-unfair | proved | all subs proved
| r-g-r,
pre1-r1,
r1-trans,
g2-r1,
|
| rg-blocked2-not-r2-unfair | proved | all subs proved
| r2-trans,
g1-r2,
RG-restr-def,
|
| rg-blocked2-not-r2 | proved | all subs proved
| r2-trans,
g1-r2,
|
| rg-blocked2-not-r2-term-unfair | proved | all subs proved
| r2-trans,
g1-r2,
|
| post1-r1 | proved | all subs proved
| RG-restr-def,
post1-runs2,
|
| rg-blocked2-not-r2-term | proved | all subs proved
| r2-trans,
g1-r2,
|
| post2-r1 | proved | all subs proved
| RG-restr-def,
post2-runs1,
|
| r-g-r | proved | all subs proved
| r1-trans,
g2-r1,
|
| rg2-not-pre1-unfair | proved | all subs proved
| pre1-r1,
r1-trans,
g2-r1,
|
| rg2-not-pre2-unfair | proved | all subs proved
| pre2-r2,
r2-trans,
g1-r2,
|
| not-pre2-term-unfair | proved | all subs proved
| pre2-r2,
r2-trans,
g1-r2,
|
| rg2-not-pre1-term | proved | all subs proved
| pre1-r1,
r1-trans,
g2-r1,
|
| rg2-not-pre2-term | proved | all subs proved
| pre2-r2,
r2-trans,
g1-r2,
|
| rg2-not-pre1 | proved | all subs proved
| pre1-r1,
r1-trans,
g2-r1,
|
| rg2-not-pre2 | proved | all subs proved
| pre2-r2,
r2-trans,
g1-r2,
|
| rg2-not-pre2-term-strnger | proved | all subs proved
| pre2-r2,
r2-trans,
g1-r2,
|
| rg2-not-pre1-term-strnger | proved | all subs proved
| pre1-r1,
r1-trans,
g2-r1,
|
| runs | proved | all subs proved
| RG-restr-def,
|
| post2-runs1 | proved | all subs proved
| RG-restr-def,
|
| post1-runs2 | proved | all subs proved
| RG-restr-def,
|
| g1-r2 | proved | all subs proved
| RG-restr-def,
|
| r2-trans | proved | all subs proved
| RG-restr-def,
|
| pre2-r2 | proved | all subs proved
| RG-restr-def,
|
| g2-r1 | proved | all subs proved
| RG-restr-def,
|
| r1-trans | proved | all subs proved
| RG-restr-def,
|
| pre1-r1 | proved | all subs proved
| RG-restr-def,
|
| RG-restr-def | axiom | | |