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: |
|---|
| abs-theorem | axiom | | abs-init,
step-absstep-idle-I1-invINSERT-same,
step-absstep-idle-I1-invINSERT-other,
step-absstep-I1-I2-tau-same,
step-absstep-I2-I3-tau-same,
step-absstep-I3-I4-tau-same,
step-absstep-I4-I5-tau-same,
step-absstep-I5-I6-tau-same,
step-absstep-I5-I21-tau-same,
step-absstep-I6-I7-doINSERT-same,
step-absstep-I6-I7-doINSERT-other,
step-absstep-I6-I7-tau-same,
step-absstep-I7-I8-tau-same,
step-absstep-I7-I10-tau-same,
step-absstep-I8-I9-tau-same,
step-absstep-I9-idle-retINSERT-same,
step-absstep-I9-idle-retINSERT-other,
step-absstep-I10-I11-tau-same,
step-absstep-I10-I12-tau-same,
step-absstep-I11-I17-tau-same,
step-absstep-I12-I13-doINSERT-same,
step-absstep-I12-I13-doINSERT-other,
step-absstep-I12-I13-tau-same,
step-absstep-I12-I13-tau-other,
step-absstep-I13-I14-tau-same,
step-absstep-I13-I16-tau-same,
step-absstep-I14-I15-tau-same,
step-absstep-I15-idle-retINSERT-same,
step-absstep-I15-idle-retINSERT-other,
step-absstep-I16-I17-tau-same,
step-absstep-I17-I18-tau-same,
step-absstep-I17-I20-tau-same,
step-absstep-I18-I19-doINSERT-same,
step-absstep-I18-I19-doINSERT-other,
step-absstep-I19-idle-retINSERT-same,
step-absstep-I19-idle-retINSERT-other,
step-absstep-I20-I5-tau-same,
step-absstep-I21-idle-retINSERT-same,
step-absstep-I21-idle-retINSERT-other,
step-absstep-idle-M1-invMEMBER-same,
step-absstep-idle-M1-invMEMBER-other,
step-absstep-M1-M2-tau-same,
step-absstep-M2-M3-tau-same,
step-absstep-M3-M4-tau-same,
step-absstep-M4-M5-tau-same,
step-absstep-M5-M6-tau-same,
step-absstep-M5-M18-tau-same,
step-absstep-M6-M7-doMEMBER-same,
step-absstep-M6-M7-doMEMBER-other,
step-absstep-M6-M7-tau-same,
step-absstep-M7-M8-tau-same,
step-absstep-M7-M10-tau-same,
step-absstep-M8-M9-tau-same,
step-absstep-M9-idle-retMEMBER-same,
step-absstep-M9-idle-retMEMBER-other,
step-absstep-M10-M11-tau-same,
step-absstep-M10-M13-tau-same,
step-absstep-M11-M12-tau-same,
step-absstep-M12-idle-retMEMBER-same,
step-absstep-M12-idle-retMEMBER-other,
step-absstep-M13-M14-tau-same,
step-absstep-M14-M15-tau-same,
step-absstep-M14-M17-tau-same,
step-absstep-M15-M16-tau-same,
step-absstep-M16-idle-retMEMBER-same,
step-absstep-M16-idle-retMEMBER-other,
step-absstep-M17-M5-tau-same,
step-absstep-M18-idle-retMEMBER-same,
step-absstep-M18-idle-retMEMBER-other,
|
| abs-init | proved | all subs proved
| labs-def,
gabs-def,
abs-def,
|
| step-absstep-M18-idle-retMEMBER-other | proved | all subs proved
| |
| step-absstep-M18-idle-retMEMBER-same | proved | all subs proved
| |
| step-absstep-M17-M5-tau-same | proved | all subs proved
| |
| step-absstep-M16-idle-retMEMBER-other | proved | all subs proved
| |
| step-absstep-M16-idle-retMEMBER-same | proved | all subs proved
| |
| step-absstep-M15-M16-tau-same | proved | all subs proved
| |
| step-absstep-M14-M17-tau-same | proved | all subs proved
| |
| step-absstep-M14-M15-tau-same | proved | all subs proved
| |
| step-absstep-M13-M14-tau-same | proved | all subs proved
| |
| step-absstep-M12-idle-retMEMBER-other | proved | all subs proved
| |
| step-absstep-M12-idle-retMEMBER-same | proved | all subs proved
| |
| step-absstep-M11-M12-tau-same | proved | all subs proved
| |
| step-absstep-M10-M13-tau-same | proved | all subs proved
| |
| step-absstep-M10-M11-tau-same | proved | all subs proved
| |
| step-absstep-M9-idle-retMEMBER-other | proved | all subs proved
| |
| step-absstep-M9-idle-retMEMBER-same | proved | all subs proved
| |
| step-absstep-M8-M9-tau-same | proved | all subs proved
| |
| step-absstep-M7-M10-tau-same | proved | all subs proved
| |
| step-absstep-M7-M8-tau-same | proved | all subs proved
| |
| step-absstep-M6-M7-tau-same | proved | all subs proved
| |
| step-absstep-M6-M7-doMEMBER-other | proved | all subs proved
| |
| step-absstep-M6-M7-doMEMBER-same | proved | all subs proved
| |
| step-absstep-M5-M18-tau-same | proved | all subs proved
| |
| step-absstep-M5-M6-tau-same | proved | all subs proved
| |
| step-absstep-M4-M5-tau-same | proved | all subs proved
| |
| step-absstep-M3-M4-tau-same | proved | all subs proved
| |
| step-absstep-M2-M3-tau-same | proved | all subs proved
| |
| step-absstep-M1-M2-tau-same | proved | all subs proved
| |
| step-absstep-idle-M1-invMEMBER-other | proved | all subs proved
| |
| step-absstep-idle-M1-invMEMBER-same | proved | all subs proved
| |
| step-absstep-I21-idle-retINSERT-other | proved | all subs proved
| |
| step-absstep-I21-idle-retINSERT-same | proved | all subs proved
| |
| step-absstep-I20-I5-tau-same | proved | all subs proved
| |
| step-absstep-I19-idle-retINSERT-other | proved | all subs proved
| |
| step-absstep-I19-idle-retINSERT-same | proved | all subs proved
| |
| step-absstep-I18-I19-doINSERT-other | proved | all subs proved
| |
| step-absstep-I18-I19-doINSERT-same | proved | all subs proved
| |
| step-absstep-I17-I20-tau-same | proved | all subs proved
| |
| step-absstep-I17-I18-tau-same | proved | all subs proved
| |
| step-absstep-I16-I17-tau-same | proved | all subs proved
| |
| step-absstep-I15-idle-retINSERT-other | proved | all subs proved
| |
| step-absstep-I15-idle-retINSERT-same | proved | all subs proved
| |
| step-absstep-I14-I15-tau-same | proved | all subs proved
| |
| step-absstep-I13-I16-tau-same | proved | all subs proved
| |
| step-absstep-I13-I14-tau-same | proved | all subs proved
| |
| step-absstep-I12-I13-tau-other | proved | all subs proved
| |
| step-absstep-I12-I13-tau-same | proved | all subs proved
| |
| step-absstep-I12-I13-doINSERT-other | proved | all subs proved
| |
| step-absstep-I12-I13-doINSERT-same | proved | all subs proved
| |
| step-absstep-I11-I17-tau-same | proved | all subs proved
| |
| step-absstep-I10-I12-tau-same | proved | all subs proved
| |
| step-absstep-I10-I11-tau-same | proved | all subs proved
| |
| step-absstep-I9-idle-retINSERT-other | proved | all subs proved
| |
| step-absstep-I9-idle-retINSERT-same | proved | all subs proved
| |
| step-absstep-I8-I9-tau-same | proved | all subs proved
| |
| step-absstep-I7-I10-tau-same | proved | all subs proved
| |
| step-absstep-I7-I8-tau-same | proved | all subs proved
| |
| step-absstep-I6-I7-tau-same | proved | all subs proved
| |
| step-absstep-I6-I7-doINSERT-other | proved | all subs proved
| |
| step-absstep-I6-I7-doINSERT-same | proved | all subs proved
| |
| step-absstep-I5-I21-tau-same | proved | all subs proved
| |
| step-absstep-I5-I6-tau-same | proved | all subs proved
| |
| step-absstep-I4-I5-tau-same | proved | all subs proved
| |
| step-absstep-I3-I4-tau-same | proved | all subs proved
| |
| step-absstep-I2-I3-tau-same | proved | all subs proved
| |
| step-absstep-I1-I2-tau-same | proved | all subs proved
| |
| step-absstep-idle-I1-invINSERT-other | proved | all subs proved
| |
| step-absstep-idle-I1-invINSERT-same | proved | all subs proved
| |
| abs-def | axiom | | |
| gabs-def | axiom | | |
| labs-def | axiom | | |