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

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:
div-def-01provedall subs proved div-neg, negate-eq, equality-def, zero-def, div-neg-01, negate-01, neg-intro, negate, equal-same, zero-num-02, denominator-zero, numerator-pos, numerator-zero, div-def, zero-num, zero-num-01, div-pos-def,
div-pos-defprovedall subs proved equality-def, denominator-zero, denominator-pos, num-pos, div-def,
root-is-irrationalprovedall subs proved equality-def, mult-def-03, denom-id, num-id, equal-same, mult-comm, mult-ass, int-mult, zero-def, exrat-gcd1,
equality-defprovedall subs proved equality-02, equality-01, equal-same, int2rat-equal,
equality-02provedall subs proved zero-num, negate-eq, negate-01, equality-pos,
div-neg-01provedall subs proved negate-eq, negate-01, numerator-zero, num-zero, exrat, zero-def, num-zero-denum-one, denom-not-zero, neg-intro, num-neg-03, denom-neg-02, div-def,
div-negprovedall subs proved negate-01, denom-neg-02, num-neg-03, div-def,
negate-01provedall subs proved negate-02, neg-neg, denom-neg, zero-denom, negate,
negate-02provedall subs proved add-comm, add-asso, add-eq, elim-sub, zero-def, neg-def,
negate-eqprovedall subs proved add-comm, add-asso, add-eq, elim-sub, zero-def, neg-def,
elim-subprovedall subs proved equal-same, add-comm, add-asso, add-zero-01, rational-add-same, sub-def-01, exrat-01,
mult-splitprovedall subs proved rational-add-same, distributivity, mult-comm, add-comm, add-asso, add-eq,
distributivityprovedall subs proved factor-rat-01, mult-comm, mult-ass, mult-def-03, add-def-03, exrat-01,
rational-add-sameprovedall subs proved factor-rat-01, add-comm, add-asso, int-add, zero-denom, add-def-03,
denom-neg-02provedall subs proved denom-neg-01, denom-id, num-id, add-comm, add-asso, add-zero-01, sub-def-01, neg-def, denominator-zero, zero-def, exrat-gcd1,
transitivityprovedall subs proved ls-def, exrat-01,
totalityprovedall subs proved factor-rat-03, equal-same, ls-def, exrat-01,
mult-one-01provedall subs proved mult-comm, mult-ass, mult-one, one-def,
irreflexivityprovedall subs proved ls-def, exrat-01,
add-zero-02provedall subs proved add-comm, add-asso, add-zero-01, gen,
add-eqprovedall subs proved equality-01, add-def-03, equal-same, factor-rat-03, exrat-01, add-comm,
mult-oneprovedall subs proved mult-def-03, exrat-01, one-def,
ls-defprovedall subs proved num-neg-02, add-def-03, sub-def-01, Ls-def,
mult-assprovedall subs proved mult-def-03, exrat-01,
add-assoprovedall subs proved add-def-03, exrat-01,
mult-def-03provedall subs proved neg-neg, denom-neg, mult-def-02,
add-def-03provedall subs proved neg-neg, denom-neg, add-def-02,
mult-def-02provedall subs proved mult-comm, factor-rat-01, zero-def, mult-zero-01, zero-num, factor-rat-03, mult-def-01,
num-neg-03provedall subs proved negate, add-zero-01, sub-def-01, denom-id, num-id, make, denominator-zero, sub-def, neg-def, numerator-zero, zero-def, exrat-gcd1,
add-def-02provedall subs proved add-zero, add-comm, zero-def, zero-num, factor-rat-02, factor-rat-01, factor-rat-03, add-def-01,
factor-ratprovedall subs proved factor-rat-01,
add-zero-01provedall subs proved add-zero, add-comm, zero-def, zero-num,
factor-rat-01provedall subs proved neg-neg, factor-rat-02,
exrat-01provedall subs proved exrat,
num-same-02provedall subs proved num-same-01, abs-num,
denum-same-02provedall subs proved denum-same, abs-num,
int-addprovedall subs proved denominator-pos, make, numerator-zero, denominator-zero, numerator-pos, Equality, add-def,
mult-def-01provedall subs proved denom-id, num-id, mult-def,
exratprovedall subs proved denom-pos-01, make,
negateprovedall subs proved make, denominator-zero, numerator-zero, zero-def, sub-def, neg-def, denom-neg-01, num-neg-01, Equality,
neg-introprovedall subs proved neg-neg,
abs-numprovedall subs proved gcd-num-one, numerator-zero, num-zero-denum-one, denom-pos-01, numerator-pos, abs-def, gen,
exrat-gcd1provedall subs proved num-zero-denum-one, gcd-num-one, denom-pos-01, make, zero-def,
sub-def-01provedall subs proved num-neg-01, denom-neg-01, add-def, sub-def,
add-def-01provedall subs proved denom-id, num-id, add-def,
factor-rat-02provedall subs proved denom-neg, factor-rat-03,
add-zeroprovedall subs proved make, denominator-zero, numerator-zero, zero-def, add-def,
oneprovedall subs proved equal-same, denom-neg, canon-any,
num-sameprovedall subs proved make,
denum-same-01provedall subs proved make,
abs-posprovedall subs proved num-zero, numerator-pos, denominator-zero, numerator-zero, denominator-pos, denum-same, num-same-01, Equality, abs-def,
canon-anyprovedall subs proved numerator-pos, denominator-pos, Equality, canon-pos,
num-neg-01provedall subs proved numerator-neg2, numerator-neg1, numerator-zero, numerator-pos, zero-denom,
mult-zero-01provedall subs proved zero-num, denominator-zero, numerator-zero, mult-def, zero-def,
int2rat-equalprovedall subs proved equal-same,
equality-posprovedall subs proved denominator-pos, num-pos, Equality,
zero-num-01provedall subs proved zero-num,
zero-num-02provedall subs proved zero-num,
denom-neg-01provedall subs proved denom-one, zero-denom, denominator-zero-den, denominator-zero, denominator-pos,
makeprovedall subs proved num-pos, denominator-pos, numerator-zero-den, denominator-zero-den, denominator-zero, numerator-zero, numerator-neg2, numerator-neg1, numerator-pos, Equality, gen,
equality-01provedall subs proved numerator-pos, numerator-zero-den, denominator-zero-den, num-zero, numerator-zero, denominator-zero, denominator-pos, Equality,
denom-negprovedall subs proved num-neg, denominator-zero, numerator-zero, denominator-pos, Equality,
neg-negprovedall subs proved denominator-zero, denominator-pos, num-neg, Equality,
denom-idprovedall subs proved denom-not-zero, denominator-zero, denominator-pos,
denum-sameprovedall subs proved denom-pos, gcd-num-one, denominator-zero, num-zero-denum-one, denom-not-zero, denominator-pos,
denom-pos-01provedall subs proved denominator-zero-den, numerator-zero-den, numerator-zero, denominator-pos, num-zero-denum-one, gen,
mult-zeroprovedall subs proved zero-num, denominator-zero, numerator-zero, mult-def, zero-def,
int-multprovedall subs proved denominator-pos, denominator-zero, numerator-zero, numerator-pos, mult-def,
num-neg-02provedall subs proved numerator-zero, numerator-pos,
num-posprovedall subs proved numerator-pos,
mult-commprovedall subs proved mult-def,
denom-posprovedall subs proved denominator-zero-den, denominator-zero, denominator-pos, gen,
zero-denomprovedall subs proved denominator-pos, denominator-zero-den, numerator-pos, denominator-zero, numerator-zero, numerator-zero-den, Equality,
denom-oneprovedall subs proved denominator-zero, denominator-pos,
num-negprovedall subs proved numerator-neg2, numerator-neg1, numerator-zero, numerator-pos,
denom-not-zeroprovedall subs proved denominator-zero-den, denominator-zero, denominator-pos, gen,
canon-posprovedall subs proved numerator-pos, denominator-zero, numerator-zero, denominator-pos, Equality,
equal-sameprovedall subs proved numerator-pos, numerator-zero, denominator-pos, Equality,
factor-rat-03provedall subs proved numerator-pos, denominator-zero, numerator-zero, denominator-pos, Equality,
zero-numprovedall subs proved denominator-zero, numerator-zero, Equality,
add-commprovedall subs proved add-def,
num-idprovedall subs proved numerator-zero, numerator-pos,
num-same-01provedall subs proved abs-def,
num-zeroprovedall subs proved numerator-neg2, numerator-zero-den, numerator-neg1, numerator-pos, numerator-zero,
num-zero-denum-oneprovedall subs proved numerator-neg1, denominator-pos, numerator-zero-den, numerator-neg2, denominator-zero, numerator-zero, numerator-pos, gen,
gcd-num-oneprovedall subs proved numerator-neg2, denominator-pos, denominator-zero-den, numerator-zero-den, numerator-neg1, denominator-zero, numerator-zero, numerator-pos, gen,
num-div-denom-01provedall subs proved numerator-neg2, numerator-neg1, denominator-pos, denominator-zero, numerator-zero, numerator-pos,
num-div-denomprovedall subs proved numerator-neg2, numerator-neg1, denominator-pos, denominator-zero, numerator-zero, numerator-pos,
Extsimpleprovedall subs proved numerator-neg2, numerator-neg1, numerator-pos, denominator-pos, Equality,
sub-defaxiom
one-defaxiom
Ls-defaxiom
mult-defaxiom
div-defaxiom
numerator-zero-denaxiom
neg-defaxiom
denominator-zero-denaxiom
zero-defaxiom
add-defaxiom
denominator-zeroaxiom
genaxiom
abs-defaxiom
numerator-zeroaxiom
Equalityaxiom
denominator-posaxiom
numerator-posaxiom
numerator-neg1axiom
numerator-neg2axiom