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: |
|---|
| HashsetInv-thm | axiom | | init-state-inv,
step-idle-I1,
step-idle-M1,
step-I1-I2,
step-I2-I3,
step-I3-I4,
step-I4-I5,
step-I5-I6,
step-I5-I21,
step-I6-I7,
step-I7-I8,
step-I7-I10,
step-I8-I9,
step-I9-idle,
step-I10-I11,
step-I10-I12,
step-I11-I17,
step-I12-I13,
step-I13-I14,
step-I13-I16,
step-I14-I15,
step-I15-idle,
step-I16-I17,
step-I17-I18,
step-I17-I20,
step-I18-I19,
step-I19-idle,
step-I20-I5,
step-M1-M2,
step-M2-M3,
step-M3-M4,
step-M4-M5,
step-M5-M6,
step-M5-M18,
step-M6-M7,
step-M7-M8,
step-M7-M10,
step-M8-M9,
step-M9-idle,
step-M10-M11,
step-M10-M13,
step-M11-M12,
step-M12-idle,
step-M13-M14,
step-M14-M15,
step-M14-M17,
step-M15-M16,
step-M16-idle,
step-M17-M5,
rely-reflexive,
rely-I12-I13,
stable-I1,
stable-I10,
stable-I11,
stable-I12,
stable-I13,
stable-I14,
stable-I15,
stable-I16,
stable-I17,
stable-I18,
stable-I2,
stable-I20,
stable-I3,
stable-I4,
stable-I7,
stable-I8,
stable-I9,
stable-M10,
stable-M11,
stable-M13,
stable-M14,
stable-M15,
stable-M17,
stable-M4,
stable-M5,
stable-M7,
stable-M8,
stable-M9,
definedness-I11,
definedness-I12,
definedness-I16,
definedness-I6,
definedness-M13,
definedness-M6,
|
| step-HashsetLInv | axiom | | init-state-inv,
step-idle-I1,
step-idle-M1,
step-I1-I2,
step-I2-I3,
step-I3-I4,
step-I4-I5,
step-I5-I6,
step-I5-I21,
step-I6-I7,
step-I7-I8,
step-I7-I10,
step-I8-I9,
step-I9-idle,
step-I10-I11,
step-I10-I12,
step-I11-I17,
step-I12-I13,
step-I13-I14,
step-I13-I16,
step-I14-I15,
step-I15-idle,
step-I16-I17,
step-I17-I18,
step-I17-I20,
step-I18-I19,
step-I19-idle,
step-I20-I5,
step-M1-M2,
step-M2-M3,
step-M3-M4,
step-M4-M5,
step-M5-M6,
step-M5-M18,
step-M6-M7,
step-M7-M8,
step-M7-M10,
step-M8-M9,
step-M9-idle,
step-M10-M11,
step-M10-M13,
step-M11-M12,
step-M12-idle,
step-M13-M14,
step-M14-M15,
step-M14-M17,
step-M15-M16,
step-M16-idle,
step-M17-M5,
rely-reflexive,
rely-I12-I13,
stable-I1,
stable-I10,
stable-I11,
stable-I12,
stable-I13,
stable-I14,
stable-I15,
stable-I16,
stable-I17,
stable-I18,
stable-I2,
stable-I20,
stable-I3,
stable-I4,
stable-I7,
stable-I8,
stable-I9,
stable-M10,
stable-M11,
stable-M13,
stable-M14,
stable-M15,
stable-M17,
stable-M4,
stable-M5,
stable-M7,
stable-M8,
stable-M9,
definedness-I11,
definedness-I12,
definedness-I16,
definedness-I6,
definedness-M13,
definedness-M6,
|
| stable-HashsetLInv | axiom | | init-state-inv,
step-idle-I1,
step-idle-M1,
step-I1-I2,
step-I2-I3,
step-I3-I4,
step-I4-I5,
step-I5-I6,
step-I5-I21,
step-I6-I7,
step-I7-I8,
step-I7-I10,
step-I8-I9,
step-I9-idle,
step-I10-I11,
step-I10-I12,
step-I11-I17,
step-I12-I13,
step-I13-I14,
step-I13-I16,
step-I14-I15,
step-I15-idle,
step-I16-I17,
step-I17-I18,
step-I17-I20,
step-I18-I19,
step-I19-idle,
step-I20-I5,
step-M1-M2,
step-M2-M3,
step-M3-M4,
step-M4-M5,
step-M5-M6,
step-M5-M18,
step-M6-M7,
step-M7-M8,
step-M7-M10,
step-M8-M9,
step-M9-idle,
step-M10-M11,
step-M10-M13,
step-M11-M12,
step-M12-idle,
step-M13-M14,
step-M14-M15,
step-M14-M17,
step-M15-M16,
step-M16-idle,
step-M17-M5,
rely-reflexive,
rely-I12-I13,
stable-I1,
stable-I10,
stable-I11,
stable-I12,
stable-I13,
stable-I14,
stable-I15,
stable-I16,
stable-I17,
stable-I18,
stable-I2,
stable-I20,
stable-I3,
stable-I4,
stable-I7,
stable-I8,
stable-I9,
stable-M10,
stable-M11,
stable-M13,
stable-M14,
stable-M15,
stable-M17,
stable-M4,
stable-M5,
stable-M7,
stable-M8,
stable-M9,
definedness-I11,
definedness-I12,
definedness-I16,
definedness-I6,
definedness-M13,
definedness-M6,
|
| other-HashsetLInv | axiom | | init-state-inv,
step-idle-I1,
step-idle-M1,
step-I1-I2,
step-I2-I3,
step-I3-I4,
step-I4-I5,
step-I5-I6,
step-I5-I21,
step-I6-I7,
step-I7-I8,
step-I7-I10,
step-I8-I9,
step-I9-idle,
step-I10-I11,
step-I10-I12,
step-I11-I17,
step-I12-I13,
step-I13-I14,
step-I13-I16,
step-I14-I15,
step-I15-idle,
step-I16-I17,
step-I17-I18,
step-I17-I20,
step-I18-I19,
step-I19-idle,
step-I20-I5,
step-M1-M2,
step-M2-M3,
step-M3-M4,
step-M4-M5,
step-M5-M6,
step-M5-M18,
step-M6-M7,
step-M7-M8,
step-M7-M10,
step-M8-M9,
step-M9-idle,
step-M10-M11,
step-M10-M13,
step-M11-M12,
step-M12-idle,
step-M13-M14,
step-M14-M15,
step-M14-M17,
step-M15-M16,
step-M16-idle,
step-M17-M5,
rely-reflexive,
rely-I12-I13,
stable-I1,
stable-I10,
stable-I11,
stable-I12,
stable-I13,
stable-I14,
stable-I15,
stable-I16,
stable-I17,
stable-I18,
stable-I2,
stable-I20,
stable-I3,
stable-I4,
stable-I7,
stable-I8,
stable-I9,
stable-M10,
stable-M11,
stable-M13,
stable-M14,
stable-M15,
stable-M17,
stable-M4,
stable-M5,
stable-M7,
stable-M8,
stable-M9,
definedness-I11,
definedness-I12,
definedness-I16,
definedness-I6,
definedness-M13,
definedness-M6,
|
| rely-HashsetLInv | axiom | | init-state-inv,
step-idle-I1,
step-idle-M1,
step-I1-I2,
step-I2-I3,
step-I3-I4,
step-I4-I5,
step-I5-I6,
step-I5-I21,
step-I6-I7,
step-I7-I8,
step-I7-I10,
step-I8-I9,
step-I9-idle,
step-I10-I11,
step-I10-I12,
step-I11-I17,
step-I12-I13,
step-I13-I14,
step-I13-I16,
step-I14-I15,
step-I15-idle,
step-I16-I17,
step-I17-I18,
step-I17-I20,
step-I18-I19,
step-I19-idle,
step-I20-I5,
step-M1-M2,
step-M2-M3,
step-M3-M4,
step-M4-M5,
step-M5-M6,
step-M5-M18,
step-M6-M7,
step-M7-M8,
step-M7-M10,
step-M8-M9,
step-M9-idle,
step-M10-M11,
step-M10-M13,
step-M11-M12,
step-M12-idle,
step-M13-M14,
step-M14-M15,
step-M14-M17,
step-M15-M16,
step-M16-idle,
step-M17-M5,
rely-reflexive,
rely-I12-I13,
stable-I1,
stable-I10,
stable-I11,
stable-I12,
stable-I13,
stable-I14,
stable-I15,
stable-I16,
stable-I17,
stable-I18,
stable-I2,
stable-I20,
stable-I3,
stable-I4,
stable-I7,
stable-I8,
stable-I9,
stable-M10,
stable-M11,
stable-M13,
stable-M14,
stable-M15,
stable-M17,
stable-M4,
stable-M5,
stable-M7,
stable-M8,
stable-M9,
definedness-I11,
definedness-I12,
definedness-I16,
definedness-I6,
definedness-M13,
definedness-M6,
|
| definedness-M6 | proved | all subs proved
| |
| definedness-M13 | proved | all subs proved
| |
| definedness-I6 | proved | all subs proved
| |
| definedness-I16 | proved | all subs proved
| |
| definedness-I12 | proved | all subs proved
| |
| definedness-I11 | proved | all subs proved
| |
| stable-M9 | proved | all subs proved
| |
| stable-M8 | proved | all subs proved
| |
| stable-M7 | proved | all subs proved
| |
| stable-M5 | proved | all subs proved
| |
| stable-M4 | proved | all subs proved
| |
| stable-M17 | proved | all subs proved
| |
| stable-M15 | proved | all subs proved
| |
| stable-M14 | proved | all subs proved
| |
| stable-M13 | proved | all subs proved
| |
| stable-M11 | proved | all subs proved
| |
| stable-M10 | proved | all subs proved
| |
| stable-I9 | proved | all subs proved
| |
| stable-I8 | proved | all subs proved
| |
| stable-I7 | proved | all subs proved
| |
| stable-I4 | proved | all subs proved
| |
| stable-I3 | proved | all subs proved
| |
| stable-I20 | proved | all subs proved
| |
| stable-I2 | proved | all subs proved
| |
| stable-I18 | proved | all subs proved
| |
| stable-I17 | proved | all subs proved
| |
| stable-I16 | proved | all subs proved
| |
| stable-I15 | proved | all subs proved
| |
| stable-I14 | proved | all subs proved
| |
| stable-I13 | proved | all subs proved
| |
| stable-I12 | proved | all subs proved
| |
| stable-I11 | proved | all subs proved
| |
| stable-I10 | proved | all subs proved
| |
| stable-I1 | proved | all subs proved
| |
| rely-I12-I13 | proved | all subs proved
| |
| rely-reflexive | proved | all subs proved
| |
| step-M17-M5 | proved | all subs proved
| |
| step-M16-idle | proved | all subs proved
| |
| step-M15-M16 | proved | all subs proved
| |
| step-M14-M17 | proved | all subs proved
| |
| step-M14-M15 | proved | all subs proved
| |
| step-M13-M14 | proved | all subs proved
| |
| step-M12-idle | proved | all subs proved
| |
| step-M11-M12 | proved | all subs proved
| |
| step-M10-M13 | proved | all subs proved
| |
| step-M10-M11 | proved | all subs proved
| |
| step-M9-idle | proved | all subs proved
| |
| step-M8-M9 | proved | all subs proved
| |
| step-M7-M10 | proved | all subs proved
| |
| step-M7-M8 | proved | all subs proved
| |
| step-M6-M7 | proved | all subs proved
| |
| step-M5-M18 | proved | all subs proved
| |
| step-M5-M6 | proved | all subs proved
| |
| step-M4-M5 | proved | all subs proved
| |
| step-M3-M4 | proved | all subs proved
| |
| step-M2-M3 | proved | all subs proved
| |
| step-M1-M2 | proved | all subs proved
| |
| step-I20-I5 | proved | all subs proved
| |
| step-I19-idle | proved | all subs proved
| |
| step-I18-I19 | proved | all subs proved
| |
| step-I17-I20 | proved | all subs proved
| |
| step-I17-I18 | proved | all subs proved
| |
| step-I16-I17 | proved | all subs proved
| |
| step-I15-idle | proved | all subs proved
| |
| step-I14-I15 | proved | all subs proved
| |
| step-I13-I16 | proved | all subs proved
| |
| step-I13-I14 | proved | all subs proved
| |
| step-I12-I13 | proved | all subs proved
| |
| step-I11-I17 | proved | all subs proved
| |
| step-I10-I12 | proved | all subs proved
| |
| step-I10-I11 | proved | all subs proved
| |
| step-I9-idle | proved | all subs proved
| |
| step-I8-I9 | proved | all subs proved
| |
| step-I7-I10 | proved | all subs proved
| |
| step-I7-I8 | proved | all subs proved
| |
| step-I6-I7 | proved | all subs proved
| |
| step-I5-I21 | proved | all subs proved
| |
| step-I5-I6 | proved | all subs proved
| |
| step-I4-I5 | proved | all subs proved
| |
| step-I3-I4 | proved | all subs proved
| |
| step-I2-I3 | proved | all subs proved
| |
| step-I1-I2 | proved | all subs proved
| |
| step-idle-M1 | proved | all subs proved
| |
| step-idle-I1 | proved | all subs proved
| |
| init-state-inv | proved | all subs proved
| |