[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,

Lemma dependency for Specification int-min

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:
max-02provedall subs proved max-c, max-a, Max-right, max,
odd-addprovedall subs proved even-add, odd-even-rew,
odd-even-rewprovedall subs proved not-even-odd,
even-addprovedall subs proved odd-def-mod, even-def-mod,
maxprovedall subs proved max-c, max-a, Max-left, Max-right,
sgn-08provedall subs proved Sign-neg, sgn+1,
max-04provedall subs proved max-c, max-a, max-01,
sgn-05provedall subs proved sgn-04,
sgn-09provedall subs proved sgn+1,
sgn-03provedall subs proved Sign-neg, sgn-01,
srprovedall subs proved sgn+1, sgn-02,
sgn-02-01provedall subs proved sgn-1, sgn+1,
not-even-oddprovedall subs proved even-def, not-odd-ex,
odd-def-modprovedall subs proved not-odd-ex,
sgn-01provedall subs proved sgn-1, sgn-02, sgn,
sgn-04provedall subs proved sgn-02, sgn,
max-cprovedall subs proved Max-left, max-a, Max-right,
sgn+1provedall subs proved sgn-02, sgn,
sgn-07provedall subs proved sgn-06,
even-multprovedall subs proved even-def-mod,
not-even-mod2provedall subs proved even-def-mod,
min-rightprovedall subs proved Min-right, min-c, min-a, Min-left,
minprovedall subs proved Min-right, min-c, min-a, Min-left,
min-cprovedall subs proved Min-right, min-a, Min-left,
not-odd-exprovedall subs proved odd-def,
sgnprovedall subs proved Sign-pos, sgn-02, Sign-neg,
max-aprovedall subs proved max-01, Max-left, Max-right,
even-def-modprovedall subs proved even-def,
sgn-06provedall subs proved sgn-02,
max-03provedall subs proved max-01,
odd-recprovedall subs proved odd-def,
even-defprovedall subs proved Even,
odd-defprovedall subs proved Odd,
min-aprovedall subs proved Min-right, Min-left,
sgn-1provedall subs proved Sign-neg,
sgn-02provedall subs proved Sign-neg, Sign-pos,
max-01provedall subs proved Max-left, Max-right,
sgn-01-01provedall subs proved Sign-neg,
min-03provedall subs proved Min-right, Min-left,
min-01provedall subs proved Min-right, Min-left,
min-02provedall subs proved Min-right, Min-left,
Oddaxiom
Evenaxiom
Min-leftaxiom
Min-rightaxiom
Sign-posaxiom
Max-rightaxiom
Max-leftaxiom
Sign-negaxiom