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