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+Term | proved | all subs proved
| RG2-Sound+Term-unfair,
pre2-i,
|
| RG2-Sound+Term-unfair | proved | all subs proved
| rg2-sound+term-unfair-main,
not-pre2-term-unfair,
not-pre1-term-unfair,
RG2-Sound-unfair,
pre2-i,
|
| RG2-Sound | proved | all subs proved
| RG2-Sound-unfair,
pre2-i,
|
| rg2-sound+term-unfair-main | proved | all subs proved
| rg2-lem2-term-unfair,
rg2-lem1-term-unfair,
pre2-i,
|
| RG2-Sound-unfair | proved | all subs proved
| pre2-i,
rg2-sound-main-unfair,
rg2-not-pre2-unfair,
rg2-not-pre1-unfair,
|
| fair-sustains-implies-always | proved | all subs proved
| fair-always-left-rely,
r2-refl,
r1-trans,
g2-r1,
i-r1-i,
i-r2-i,
r2-trans,
g1-r2,
pre2-i,
|
| fair-always-right-rely | proved | all subs proved
| pre2-i,
RG-restr-sym,
fair-always-left-rely,
|
| rg2-lem1-term-unfair | proved | all subs proved
| rg-blocked2-not-r2-term-unfair,
i-r1-i,
r1-trans,
g2-r1,
rg-blocked1-not-r1-term-unfair,
i-r2-i,
r2-trans,
g1-r2,
pre2-i,
|
| rg2-lem2-term-unfair | proved | all subs proved
| rg-blocked2-not-r2-term-unfair,
i-r1-i,
r1-trans,
g2-r1,
rg-blocked1-not-r1-term-unfair,
i-r2-i,
r2-trans,
g1-r2,
pre2-i,
|
| fair-always-left-rely | proved | all subs proved
| fair-never-violates-right-rely,
i-r1-i,
r1-trans,
fair-never-violates-left-rely,
i-r2-i,
r2-trans,
g1-r2,
g2-r1,
r1-refl,
pre2-i,
|
| rg2-sound-main-unfair | proved | all subs proved
| post2-r2,
r2-refl,
rg-blocked2-not-r2-unfair,
post1-r1,
r-g-r,
i-r1-i,
r1-trans,
rg-blocked1-not-r1-unfair,
i-r2-i,
r2-trans,
g1-r2,
g2-r1,
r1-refl,
pre2-i,
|
| rg-blocked2-not-r2-unfair | proved | all subs proved
| RG-restr-sym,
rg-blocked1-not-r1-unfair,
i-r2-i,
pre2-i,
|
| rg-blocked2-not-r2-term-unfair | proved | all subs proved
| RG-restr-sym,
rg-blocked1-not-r1-term-unfair,
i-r2-i,
pre1-i,
|
| fair-never-violates-right-rely | proved | all subs proved
| RG-restr-sym,
fair-never-violates-left-rely,
i-r2-i,
pre1-i,
|
| rg2-not-pre2-unfair | proved | all subs proved
| RG-restr-sym,
rg2-not-pre1-unfair,
pre1-i,
pre2-i,
|
| not-pre2-term-unfair | proved | all subs proved
| RG-restr-sym,
not-pre1-term-unfair,
pre1-i,
pre2-i,
|
| rg-blocked1-not-r1-unfair | proved | all subs proved
| i-r2-i,
r1-trans,
g2-r1,
r-g-r,
i-r1-i,
pre2-i,
|
| rg-blocked1-not-r1-term-unfair | proved | all subs proved
| i-r2-i,
r1-trans,
g2-r1,
r-g-r,
i-r1-i,
pre2-i,
|
| fair-never-violates-left-rely | proved | all subs proved
| i-r2-i,
r1-trans,
g2-r1,
r-g-r,
i-r1-i,
pre2-i,
|
| rg2-not-pre1-unfair | proved | all subs proved
| i-r2-i,
i-r1-i,
pre1-r1,
r1-trans,
g2-r1,
pre1-i,
pre2-i,
|
| not-pre1-term-unfair | proved | all subs proved
| r-g-r,
i-r2-i,
i-r1-i,
pre1-r1,
r1-trans,
g2-r1,
pre1-i,
pre2-i,
|
| post1-r1 | proved | all subs proved
| RG-restr-def,
|
| post2-r2 | proved | all subs proved
| RG-restr-def,
|
| pre1-r1 | proved | all subs proved
| RG-restr-def,
|
| r2-refl | proved | all subs proved
| RG-restr-def,
|
| pre1-i | proved | all subs proved
| RG-restr-def,
|
| r-g-r | proved | all subs proved
| RG-restr-def,
|
| RG-restr-sym | proved | all subs proved
| RG-restr-def,
|
| r1-refl | proved | all subs proved
| RG-restr-def,
|
| g2-r1 | 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,
|
| i-r2-i | proved | all subs proved
| RG-restr-def,
|
| r1-trans | proved | all subs proved
| RG-restr-def,
|
| i-r1-i | proved | all subs proved
| RG-restr-def,
|
| pre2-i | proved | all subs proved
| RG-restr-def,
|
| pre2-r2 | proved | all subs proved
| RG-restr-def,
|
| RG-restr-def | axiom | | |