[Imprint][Data Privacy Statement][E-Mail]
Back to main index.
View the specification.
View theorem base summary,
View theorem base listing,
the used properties by spec,
the dependency list,
the symbol table,
Used simplifier rules/spec theorems by specification
Used from specification nat-basic
- nat-basic/a
is used by
step-I16-I17,
step-M13-M14,
- nat-basic/c
is used by
step-I16-I17,
step-M13-M14,
- nat-basic/f
is used by
step-I14-I15,
step-M16-idle,
stable-I16,
step-I8-I9,
stable-M9,
step-M4-M5,
stable-I13,
step-I20-I5,
stable-I7,
step-I7-I8,
step-I10-I12,
step-I16-I17,
step-M14-M17,
definedness-M13,
step-I17-I18,
step-M3-M4,
stable-M10,
step-I6-I7,
step-I18-I19,
stable-I14,
step-I15-idle,
step-I7-I10,
stable-I20,
stable-I8,
definedness-I11,
stable-I11,
step-M2-M3,
stable-I17,
step-I5-I6,
step-M8-M9,
stable-M13,
stable-M4,
step-M10-M11,
init-state-inv,
step-M11-M12,
step-M7-M8,
step-I19-idle,
step-I4-I5,
stable-M7,
definedness-I12,
step-I11-I17,
step-M13-M14,
step-M17-M5,
stable-I18,
rely-I12-I13,
step-M6-M7,
step-M14-M15,
step-I9-idle,
stable-I15,
stable-I9,
stable-M11,
step-I13-I16,
stable-I12,
step-M15-M16,
stable-M17,
stable-M14,
step-I10-I11,
step-M5-M6,
stable-I3,
step-M12-idle,
stable-M5,
step-M7-M10,
definedness-I16,
step-I3-I4,
step-I17-I20,
stable-M8,
step-I12-I13,
step-I2-I3,
stable-M15,
step-M9-idle,
step-I13-I14,
step-M10-M13,
stable-I4,
stable-I10,
- nat-basic/lf-01
is used by
step-I14-I15,
step-M16-idle,
stable-I16,
step-I8-I9,
stable-M9,
step-M4-M5,
stable-I13,
step-I20-I5,
stable-I7,
step-I7-I8,
step-I10-I12,
step-I16-I17,
step-M14-M17,
definedness-M13,
step-I17-I18,
step-M3-M4,
stable-M10,
stable-I14,
step-I15-idle,
step-I7-I10,
stable-I20,
stable-I8,
definedness-I11,
stable-I11,
stable-I17,
step-I5-I6,
step-M8-M9,
stable-M13,
step-M10-M11,
step-M11-M12,
step-M7-M8,
step-I19-idle,
step-I4-I5,
stable-M7,
step-I11-I17,
step-M13-M14,
step-M17-M5,
stable-I18,
rely-I12-I13,
step-M14-M15,
step-I9-idle,
stable-I15,
stable-I9,
step-I13-I16,
stable-I12,
step-M15-M16,
step-I10-I11,
step-M5-M6,
step-M12-idle,
step-M7-M10,
definedness-I16,
step-I3-I4,
step-I17-I20,
stable-M8,
step-I12-I13,
step-M9-idle,
step-I13-I14,
step-M10-M13,
stable-I4,
stable-I10,
- nat-basic/lf-02
is used by
step-I14-I15,
step-M16-idle,
stable-I16,
step-I8-I9,
stable-M9,
step-M4-M5,
stable-I13,
step-I20-I5,
stable-I7,
step-I7-I8,
step-I10-I12,
step-I16-I17,
step-M14-M17,
definedness-M13,
step-I17-I18,
step-M3-M4,
stable-M10,
stable-I14,
step-I15-idle,
step-I7-I10,
stable-I20,
stable-I8,
definedness-I11,
stable-I11,
stable-I17,
step-I5-I6,
step-M8-M9,
stable-M13,
step-M10-M11,
step-M11-M12,
step-M7-M8,
step-I19-idle,
step-I4-I5,
stable-M7,
step-I11-I17,
step-M13-M14,
step-M17-M5,
stable-I18,
rely-I12-I13,
step-M14-M15,
step-I9-idle,
stable-I15,
stable-I9,
step-I13-I16,
stable-I12,
step-M15-M16,
step-I10-I11,
step-M5-M6,
step-M12-idle,
step-M7-M10,
definedness-I16,
step-I3-I4,
step-I17-I20,
stable-M8,
step-I12-I13,
step-M9-idle,
step-I13-I14,
step-M10-M13,
stable-I4,
stable-I10,
- nat-basic/refl-Nat
is used by
step-I17-I18,
step-M14-M15,
- nat-basic/zero
is used by
init-state-inv,
Used from specification Hashset
- Hashset/HashsetGInv
is used by
init-state-inv,
- Hashset/HashsetInv
is used by
init-state-inv,
- Hashset/HashsetLInv
is used by
init-state-inv,
- Hashset/disj-I1-M1
is used by
step-idle-M1,
- Hashset/disj-I1-idle
is used by
init-state-inv,
- Hashset/disj-I10-idle
is used by
init-state-inv,
- Hashset/disj-I11-I12
is used by
step-I10-I12,
step-I10-I11,
- Hashset/disj-I11-idle
is used by
init-state-inv,
- Hashset/disj-I12-idle
is used by
init-state-inv,
- Hashset/disj-I13-idle
is used by
init-state-inv,
- Hashset/disj-I14-I16
is used by
step-I13-I16,
step-I13-I14,
- Hashset/disj-I14-idle
is used by
init-state-inv,
- Hashset/disj-I15-idle
is used by
init-state-inv,
- Hashset/disj-I16-idle
is used by
init-state-inv,
- Hashset/disj-I17-idle
is used by
init-state-inv,
- Hashset/disj-I18-I20
is used by
step-I17-I18,
step-I17-I20,
- Hashset/disj-I18-idle
is used by
init-state-inv,
- Hashset/disj-I19-idle
is used by
init-state-inv,
- Hashset/disj-I2-idle
is used by
init-state-inv,
- Hashset/disj-I20-idle
is used by
init-state-inv,
- Hashset/disj-I21-idle
is used by
init-state-inv,
- Hashset/disj-I3-idle
is used by
init-state-inv,
- Hashset/disj-I4-idle
is used by
init-state-inv,
- Hashset/disj-I5-idle
is used by
init-state-inv,
- Hashset/disj-I6-I21
is used by
step-I5-I21,
- Hashset/disj-I6-idle
is used by
init-state-inv,
- Hashset/disj-I7-idle
is used by
init-state-inv,
- Hashset/disj-I8-I10
is used by
step-I7-I8,
step-I7-I10,
- Hashset/disj-I8-idle
is used by
init-state-inv,
- Hashset/disj-I9-idle
is used by
init-state-inv,
- Hashset/disj-M1-idle
is used by
init-state-inv,
- Hashset/disj-M10-idle
is used by
init-state-inv,
- Hashset/disj-M11-M13
is used by
step-M10-M11,
step-M10-M13,
- Hashset/disj-M11-idle
is used by
init-state-inv,
- Hashset/disj-M12-idle
is used by
init-state-inv,
- Hashset/disj-M13-idle
is used by
init-state-inv,
- Hashset/disj-M14-idle
is used by
init-state-inv,
- Hashset/disj-M15-M17
is used by
step-M14-M17,
step-M14-M15,
- Hashset/disj-M15-idle
is used by
init-state-inv,
- Hashset/disj-M16-idle
is used by
init-state-inv,
- Hashset/disj-M17-idle
is used by
init-state-inv,
- Hashset/disj-M18-idle
is used by
init-state-inv,
- Hashset/disj-M2-idle
is used by
init-state-inv,
- Hashset/disj-M3-idle
is used by
init-state-inv,
- Hashset/disj-M4-idle
is used by
init-state-inv,
- Hashset/disj-M5-idle
is used by
init-state-inv,
- Hashset/disj-M6-M18
is used by
step-M5-M18,
- Hashset/disj-M6-idle
is used by
init-state-inv,
- Hashset/disj-M7-idle
is used by
init-state-inv,
- Hashset/disj-M8-M10
is used by
step-M7-M8,
step-M7-M10,
- Hashset/disj-M8-idle
is used by
init-state-inv,
- Hashset/disj-M9-idle
is used by
init-state-inv,
- Hashset/disj-invINSERT-invMEMBER
is used by
step-idle-I1,
- Hashset/gstepf-I1
is used by
step-I1-I2,
- Hashset/gstepf-I10
is used by
step-I10-I12,
step-I10-I11,
- Hashset/gstepf-I11
is used by
step-I11-I17,
- Hashset/gstepf-I12
is used by
rely-I12-I13,
step-I12-I13,
- Hashset/gstepf-I13
is used by
step-I13-I16,
step-I13-I14,
- Hashset/gstepf-I14
is used by
step-I14-I15,
- Hashset/gstepf-I15
is used by
step-I15-idle,
- Hashset/gstepf-I16
is used by
step-I16-I17,
- Hashset/gstepf-I17
is used by
step-I17-I18,
step-I17-I20,
- Hashset/gstepf-I18
is used by
step-I18-I19,
- Hashset/gstepf-I19
is used by
step-I19-idle,
- Hashset/gstepf-I2
is used by
step-I2-I3,
- Hashset/gstepf-I20
is used by
step-I20-I5,
- Hashset/gstepf-I3
is used by
step-I3-I4,
- Hashset/gstepf-I4
is used by
step-I4-I5,
- Hashset/gstepf-I5
is used by
step-I5-I6,
- Hashset/gstepf-I6
is used by
step-I6-I7,
- Hashset/gstepf-I7
is used by
step-I7-I8,
step-I7-I10,
- Hashset/gstepf-I8
is used by
step-I8-I9,
- Hashset/gstepf-I9
is used by
step-I9-idle,
- Hashset/gstepf-M1
is used by
step-M1-M2,
- Hashset/gstepf-M10
is used by
step-M10-M11,
step-M10-M13,
- Hashset/gstepf-M11
is used by
step-M11-M12,
- Hashset/gstepf-M12
is used by
step-M12-idle,
- Hashset/gstepf-M13
is used by
step-M13-M14,
- Hashset/gstepf-M14
is used by
step-M14-M17,
step-M14-M15,
- Hashset/gstepf-M15
is used by
step-M15-M16,
- Hashset/gstepf-M16
is used by
step-M16-idle,
- Hashset/gstepf-M17
is used by
step-M17-M5,
- Hashset/gstepf-M2
is used by
step-M2-M3,
- Hashset/gstepf-M3
is used by
step-M3-M4,
- Hashset/gstepf-M4
is used by
step-M4-M5,
- Hashset/gstepf-M5
is used by
step-M5-M6,
- Hashset/gstepf-M6
is used by
step-M6-M7,
- Hashset/gstepf-M7
is used by
step-M7-M8,
step-M7-M10,
- Hashset/gstepf-M8
is used by
step-M8-M9,
- Hashset/gstepf-M9
is used by
step-M9-idle,
- Hashset/gstepf-idle
is used by
step-idle-M1,
step-idle-I1,
- Hashset/lstepf-I1
is used by
step-I1-I2,
- Hashset/lstepf-I10
is used by
step-I10-I12,
step-I10-I11,
- Hashset/lstepf-I11
is used by
step-I11-I17,
- Hashset/lstepf-I12
is used by
step-I12-I13,
- Hashset/lstepf-I13
is used by
step-I13-I16,
step-I13-I14,
- Hashset/lstepf-I14
is used by
step-I14-I15,
- Hashset/lstepf-I15-b
is used by
step-I15-idle,
- Hashset/lstepf-I16
is used by
step-I16-I17,
- Hashset/lstepf-I17
is used by
step-I17-I18,
step-I17-I20,
- Hashset/lstepf-I18
is used by
step-I18-I19,
- Hashset/lstepf-I19-b
is used by
step-I19-idle,
- Hashset/lstepf-I2
is used by
step-I2-I3,
- Hashset/lstepf-I20
is used by
step-I20-I5,
- Hashset/lstepf-I3
is used by
step-I3-I4,
- Hashset/lstepf-I4
is used by
step-I4-I5,
- Hashset/lstepf-I5
is used by
step-I5-I6,
- Hashset/lstepf-I6
is used by
step-I6-I7,
- Hashset/lstepf-I7
is used by
step-I7-I8,
step-I7-I10,
- Hashset/lstepf-I8
is used by
step-I8-I9,
- Hashset/lstepf-I9-b
is used by
step-I9-idle,
- Hashset/lstepf-M1
is used by
step-M1-M2,
- Hashset/lstepf-M10
is used by
step-M10-M11,
step-M10-M13,
- Hashset/lstepf-M11
is used by
step-M11-M12,
- Hashset/lstepf-M12-b
is used by
step-M12-idle,
- Hashset/lstepf-M13
is used by
step-M13-M14,
- Hashset/lstepf-M14
is used by
step-M14-M17,
step-M14-M15,
- Hashset/lstepf-M15
is used by
step-M15-M16,
- Hashset/lstepf-M16-b
is used by
step-M16-idle,
- Hashset/lstepf-M17
is used by
step-M17-M5,
- Hashset/lstepf-M2
is used by
step-M2-M3,
- Hashset/lstepf-M3
is used by
step-M3-M4,
- Hashset/lstepf-M4
is used by
step-M4-M5,
- Hashset/lstepf-M5
is used by
step-M5-M6,
- Hashset/lstepf-M6
is used by
step-M6-M7,
- Hashset/lstepf-M7
is used by
step-M7-M8,
step-M7-M10,
- Hashset/lstepf-M8
is used by
step-M8-M9,
- Hashset/lstepf-M9-b
is used by
step-M9-idle,
- Hashset/lstepf-idle-INSERT
is used by
step-idle-I1,
- Hashset/lstepf-idle-MEMBER
is used by
step-idle-M1,
step-idle-I1,
- Hashset/pcstepf-I1
is used by
step-I1-I2,
- Hashset/pcstepf-I10
is used by
step-I10-I12,
step-I10-I11,
- Hashset/pcstepf-I11
is used by
step-I11-I17,
- Hashset/pcstepf-I12
is used by
rely-I12-I13,
step-I12-I13,
- Hashset/pcstepf-I13
is used by
step-I13-I16,
step-I13-I14,
- Hashset/pcstepf-I14
is used by
step-I14-I15,
- Hashset/pcstepf-I15
is used by
step-I15-idle,
- Hashset/pcstepf-I16
is used by
step-I16-I17,
- Hashset/pcstepf-I17
is used by
step-I17-I18,
step-I17-I20,
- Hashset/pcstepf-I18
is used by
step-I18-I19,
- Hashset/pcstepf-I19
is used by
step-I19-idle,
- Hashset/pcstepf-I2
is used by
step-I2-I3,
- Hashset/pcstepf-I20
is used by
step-I20-I5,
- Hashset/pcstepf-I3
is used by
step-I3-I4,
- Hashset/pcstepf-I4
is used by
step-I4-I5,
- Hashset/pcstepf-I5
is used by
step-I5-I6,
step-I5-I21,
- Hashset/pcstepf-I6
is used by
step-I6-I7,
- Hashset/pcstepf-I7
is used by
step-I7-I8,
step-I7-I10,
- Hashset/pcstepf-I8
is used by
step-I8-I9,
- Hashset/pcstepf-I9
is used by
step-I9-idle,
- Hashset/pcstepf-M1
is used by
step-M1-M2,
- Hashset/pcstepf-M10
is used by
step-M10-M11,
step-M10-M13,
- Hashset/pcstepf-M11
is used by
step-M11-M12,
- Hashset/pcstepf-M12
is used by
step-M12-idle,
- Hashset/pcstepf-M13
is used by
step-M13-M14,
- Hashset/pcstepf-M14
is used by
step-M14-M17,
step-M14-M15,
- Hashset/pcstepf-M15
is used by
step-M15-M16,
- Hashset/pcstepf-M16
is used by
step-M16-idle,
- Hashset/pcstepf-M17
is used by
step-M17-M5,
- Hashset/pcstepf-M2
is used by
step-M2-M3,
- Hashset/pcstepf-M3
is used by
step-M3-M4,
- Hashset/pcstepf-M4
is used by
step-M4-M5,
- Hashset/pcstepf-M5
is used by
step-M5-M18,
step-M5-M6,
- Hashset/pcstepf-M6
is used by
step-M6-M7,
- Hashset/pcstepf-M7
is used by
step-M7-M8,
step-M7-M10,
- Hashset/pcstepf-M8
is used by
step-M8-M9,
- Hashset/pcstepf-M9
is used by
step-M9-idle,
- Hashset/pcstepf-idle-INSERT
is used by
step-idle-M1,
step-idle-I1,
- Hashset/pre-I1
is used by
step-I1-I2,
- Hashset/pre-I10
is used by
step-I10-I12,
step-I10-I11,
- Hashset/pre-I11
is used by
definedness-I11,
step-I11-I17,
- Hashset/pre-I12
is used by
definedness-I12,
rely-I12-I13,
step-I12-I13,
- Hashset/pre-I13
is used by
step-I13-I16,
step-I13-I14,
- Hashset/pre-I14
is used by
step-I14-I15,
- Hashset/pre-I15
is used by
step-I15-idle,
- Hashset/pre-I16
is used by
step-I16-I17,
definedness-I16,
- Hashset/pre-I17
is used by
step-I17-I18,
step-I17-I20,
- Hashset/pre-I18
is used by
step-I18-I19,
- Hashset/pre-I19
is used by
step-I19-idle,
- Hashset/pre-I2
is used by
step-I2-I3,
- Hashset/pre-I20
is used by
step-I20-I5,
- Hashset/pre-I3
is used by
step-I3-I4,
- Hashset/pre-I4
is used by
step-I4-I5,
- Hashset/pre-I5
is used by
step-I5-I6,
- Hashset/pre-I6
is used by
step-I6-I7,
- Hashset/pre-I7
is used by
step-I7-I8,
step-I7-I10,
- Hashset/pre-I8
is used by
step-I8-I9,
- Hashset/pre-I9
is used by
step-I9-idle,
- Hashset/pre-M1
is used by
step-M1-M2,
- Hashset/pre-M10
is used by
step-M10-M11,
step-M10-M13,
- Hashset/pre-M11
is used by
step-M11-M12,
- Hashset/pre-M12
is used by
step-M12-idle,
- Hashset/pre-M13
is used by
definedness-M13,
step-M13-M14,
- Hashset/pre-M14
is used by
step-M14-M17,
step-M14-M15,
- Hashset/pre-M15
is used by
step-M15-M16,
- Hashset/pre-M16
is used by
step-M16-idle,
- Hashset/pre-M17
is used by
step-M17-M5,
- Hashset/pre-M2
is used by
step-M2-M3,
- Hashset/pre-M3
is used by
step-M3-M4,
- Hashset/pre-M4
is used by
step-M4-M5,
- Hashset/pre-M5
is used by
step-M5-M6,
- Hashset/pre-M6
is used by
step-M6-M7,
- Hashset/pre-M7
is used by
step-M7-M8,
step-M7-M10,
- Hashset/pre-M8
is used by
step-M8-M9,
- Hashset/pre-M9
is used by
step-M9-idle,
- Hashset/pre-idle
is used by
step-idle-M1,
step-idle-I1,
- Hashset/updsel--dotar-dotar
is used by
rely-I12-I13,
step-I12-I13,
- Hashset/updsel--dotb-dotb
is used by
step-I14-I15,
step-I8-I9,
step-M4-M5,
step-I18-I19,
step-M8-M9,
step-M11-M12,
step-I4-I5,
step-M15-M16,
- Hashset/updsel--dotb-dote
is used by
step-I14-I15,
step-I8-I9,
step-M4-M5,
step-I18-I19,
step-M8-M9,
step-M11-M12,
step-I4-I5,
step-M15-M16,
- Hashset/updsel--dotb-dote0
is used by
step-M11-M12,
- Hashset/updsel--dotb-dotn
is used by
step-I14-I15,
step-I8-I9,
step-M4-M5,
step-I18-I19,
step-M8-M9,
step-M11-M12,
step-I4-I5,
step-M15-M16,
- Hashset/updsel--dotb-dotn0
is used by
step-I14-I15,
step-I8-I9,
step-M4-M5,
step-I18-I19,
step-M8-M9,
step-M11-M12,
step-I4-I5,
step-M15-M16,
- Hashset/updsel--dotb-dotsz
is used by
step-I14-I15,
step-I8-I9,
step-M4-M5,
step-I18-I19,
step-M8-M9,
step-M11-M12,
step-I4-I5,
step-M15-M16,
- Hashset/updsel--dote-dote
is used by
step-idle-M1,
step-idle-I1,
- Hashset/updsel--dote0-dotb
is used by
step-I6-I7,
step-M6-M7,
step-I12-I13,
- Hashset/updsel--dote0-dote
is used by
step-I6-I7,
step-M6-M7,
step-I12-I13,
- Hashset/updsel--dote0-dote0
is used by
step-I6-I7,
step-M6-M7,
step-I12-I13,
- Hashset/updsel--dote0-dotn
is used by
step-I6-I7,
step-M6-M7,
step-I12-I13,
- Hashset/updsel--dote0-dotn0
is used by
step-I6-I7,
step-M6-M7,
step-I12-I13,
- Hashset/updsel--dote0-dotsz
is used by
step-I6-I7,
step-M6-M7,
step-I12-I13,
- Hashset/updsel--dotn-dotb
is used by
step-I16-I17,
step-I11-I17,
step-M13-M14,
- Hashset/updsel--dotn-dote
is used by
step-I16-I17,
step-M3-M4,
step-I11-I17,
step-M13-M14,
step-I3-I4,
- Hashset/updsel--dotn-dotn
is used by
step-I16-I17,
step-M3-M4,
step-I11-I17,
step-M13-M14,
step-I3-I4,
- Hashset/updsel--dotn-dotn0
is used by
step-I16-I17,
step-M3-M4,
step-I11-I17,
step-M13-M14,
step-I3-I4,
- Hashset/updsel--dotn-dotsz
is used by
step-I16-I17,
step-M3-M4,
step-I11-I17,
step-M13-M14,
step-I3-I4,
- Hashset/updsel--dotn0-dote
is used by
step-M2-M3,
step-I2-I3,
- Hashset/updsel--dotn0-dotn0
is used by
step-M2-M3,
step-I2-I3,
- Hashset/updsel--dotn0-dotsz
is used by
step-M2-M3,
step-I2-I3,
- Hashset/updsel--dotsz-dote
is used by
step-I1-I2,
step-M1-M2,
- Hashset/updsel--dotsz-dotsz
is used by
step-I1-I2,
step-M1-M2,
- hashset-preds/allslotsfull-def
is used by
step-I12-I13,
- hashset-preds/allslotsfull-inctrue
is used by
step-I11-I17,
- hashset-preds/htok-add
is used by
step-I12-I13,
- hashset-preds/htok-def
is used by
init-state-inv,
- hashset-preds/rely-def
is used by
rely-I12-I13,
- hashset-preds/allslotsfull-final-close
is used by
step-I19-idle,
- hashset-preds/allslotsfull-inctrue
is used by
step-I16-I17,
step-M13-M14,
- hashset-preds/allslotsfull-init
is used by
step-M3-M4,
step-I3-I4,
- hashset-preds/allslotsfull-iterate
is used by
step-M14-M17,
step-I17-I20,
- hashset-preds/get-mkar
is used by
init-state-inv,
- hashset-preds/hash-ok-lem
is used by
step-M2-M3,
step-I2-I3,
- hashset-preds/rely-allslotsfull
is used by
stable-I16,
stable-M9,
stable-I13,
stable-I7,
stable-M10,
stable-I14,
stable-I20,
stable-I8,
stable-I11,
stable-I17,
stable-M13,
stable-M4,
stable-M7,
stable-I18,
stable-I15,
stable-I9,
stable-I12,
stable-M17,
stable-M14,
stable-M5,
stable-M8,
stable-M15,
stable-I4,
stable-I10,
- hashset-preds/rely-notinvkey-f
is used by
stable-I16,
stable-M13,
- hashset-preds/rely-notinvkey-unchanged
is used by
stable-I16,
stable-M13,
- hashset-preds/rely-notinvkey-unchanged-f
is used by
stable-M9,
stable-I13,
stable-I7,
stable-M10,
stable-I14,
stable-I8,
stable-I11,
stable-M7,
stable-I15,
stable-I9,
stable-M8,
stable-I10,
- hashset-preds/rely-refl
is used by
rely-reflexive,
- hashset-preds/rely-size
is used by
stable-I16,
stable-M9,
stable-I13,
stable-I7,
stable-M10,
stable-I14,
stable-I20,
stable-I8,
stable-I11,
stable-I17,
stable-I2,
stable-M13,
stable-M4,
stable-M7,
stable-I18,
stable-I15,
stable-I9,
stable-M11,
stable-I12,
stable-M17,
stable-M14,
stable-I3,
stable-M5,
stable-M8,
stable-M15,
stable-I4,
stable-I10,
- hashset-preds/size-mkar
is used by
init-state-inv,
Used from specification nat
- nat/fle
is used by
step-M4-M5,
step-I16-I17,
step-I17-I18,
step-I4-I5,
step-M13-M14,
step-M14-M15,
- nat/fle-01
is used by
stable-I16,
stable-M9,
step-M4-M5,
stable-I13,
stable-I7,
step-I17-I18,
stable-I14,
stable-I20,
stable-I8,
stable-I11,
stable-I17,
stable-M13,
step-I4-I5,
stable-I18,
step-M14-M15,
stable-I15,
stable-I9,
stable-I12,
stable-M8,
stable-I4,
stable-I10,
- nat/gr-def
is used by
init-state-inv,
- nat/le-ls-simp
is used by
stable-I16,
stable-M9,
step-M4-M5,
stable-I13,
stable-I7,
stable-I14,
stable-I20,
stable-I8,
stable-I11,
stable-I17,
stable-M13,
step-I4-I5,
stable-I18,
stable-I15,
stable-I9,
stable-I12,
stable-M8,
stable-I4,
stable-I10,
- nat/lels
is used by
stable-I16,
stable-M9,
step-M4-M5,
stable-I13,
stable-I7,
step-I16-I17,
step-I17-I18,
stable-M10,
stable-I14,
stable-I20,
stable-I8,
stable-I11,
step-M2-M3,
stable-I17,
stable-M13,
step-I4-I5,
stable-M7,
step-M13-M14,
stable-I18,
step-M14-M15,
stable-I15,
stable-I9,
stable-I12,
stable-M8,
step-I12-I13,
step-I2-I3,
stable-I4,
stable-I10,
- nat/ls-le-simp
is used by
stable-I16,
stable-M9,
stable-I13,
stable-I7,
stable-M10,
stable-I14,
stable-I8,
stable-I11,
stable-M13,
stable-M7,
stable-I15,
stable-I9,
stable-M8,
step-I12-I13,
stable-I10,
Used from specification nat-div
Used from specification array