# List of theorems

List of theorems in peano_new/arithmetic/common/calculations/decimal.gh:

df-.1 # <title> Definition of One-Tenth </title>
(= (.1) (/ (1) (10)))
EqReplaceEq1Mul1 # <title> Substitution </title> # <table> # (= A (* B [ C ] ] ] )) # (= [ C ] [ D ] ) # (= A (* B [ [ [ D ] )) # </table>
(= A (* B C)) , (= C D)(= A (* B D))
fracToDecimal # <title> Convert Fraction to Decimal </title>
(= (/ A (10)) (* A (.1)))
EqReplaceEq1Div0 # <title> Substitution </title> # <table> # (= A (/ [ B ] ] ] D)) # (= [ B ] [ C ] ) # (= A (/ [ [ [ C ] D)) # </table>
(= A (/ B D)) , (= B C)(= A (/ C D))
EqReplaceEq1Div1 # <title> Substitution </title> # <table> # (= A (/ B [ C ] ] ] )) # (= [ C ] [ D ] ) # (= A (/ B [ [ [ D ] )) # </table>
(= A (/ B C)) , (= C D)(= A (/ B D))
halfDecimal # <title> One-Half in Decimal Form </title>
(= (/ (1) (2)) (* (5) (.1)))
oneFifthDecimal # <title> One-Fifth in Decimal Form </title>
(= (/ (1) (5)) (* (2) (.1)))
fractionExample1 # <summary> An example of simplifying a fraction </summary>
(= (/ (4) (8)) (/ (1) (2)))
fractionExample2 # <summary> An example of simplifying a fraction </summary>
(= (/ (+ (* (2) (10)) (1)) (3)) (7))
EqReplaceEq1Add1 # <title> Substitution </title> # <table> # (= A (+ B [ C ] ] ] )) # (= [ C ] [ D ] ) # (= A (+ B [ [ [ D ] )) # </table>
(= A (+ B C)) , (= C D)(= A (+ B D))
EqReplaceEq1Mul0 # <title> Substitution </title> # <table> # (= A (* [ B ] ] ] D)) # (= [ B ] [ C ] ) # (= A (* [ [ [ C ] D)) # </table>
(= A (* B D)) , (= B C)(= A (* C D))
EqReplaceEq1Add0 # <title> Substitution </title> # <table> # (= A (+ [ B ] ] ] D)) # (= [ B ] [ C ] ) # (= A (+ [ [ [ C ] D)) # </table>
(= A (+ B D)) , (= B C)(= A (+ C D))
EqReplaceEq1Add0Add1 # <title> Substitution </title> # <table> # (= A (+ (+ B [ C ] ] ] ) A')) # (= [ C ] [ D ] ) # (= A (+ (+ B [ [ [ D ] ) A')) # </table>
(= A (+ (+ B C) A')) , (= C D)(= A (+ (+ B D) A'))
EqReplaceEq1Add0Add1Mul0 # <title> Substitution </title> # <table> # (= A (+ (+ B (* [ C ] ] ] A')) B')) # (= [ C ] [ D ] ) # (= A (+ (+ B (* [ [ [ D ] A')) B')) # </table>
(= A (+ (+ B (* C A')) B')) , (= C D)(= A (+ (+ B (* D A')) B'))
EqReplaceEq1Add0Mul0 # <title> Substitution </title> # <table> # (= A (+ (* [ B ] ] ] D) A')) # (= [ B ] [ C ] ) # (= A (+ (* [ [ [ C ] D) A')) # </table>
(= A (+ (* B D) A')) , (= B C)(= A (+ (* C D) A'))
fractionExample3 # <summary> An example of simplifying a fraction </summary>
(= (/ (+ (* (4) (* (10) (10))) (2)) (+ (* (5) (10)) (4))) (/ (+ (* (6) (10)) (7)) (9)))
multiplyFractions1 # <summary> An example of multiplying two fractions. </summary>
(= (* (/ (1) (2)) (/ (4) (5))) (/ (2) (5)))
EqReplaceEq1Add0Add0 # <title> Substitution </title> # <table> # (= A (+ (+ [ B ] ] ] D) A')) # (= [ B ] [ C ] ) # (= A (+ (+ [ [ [ C ] D) A')) # </table>
(= A (+ (+ B D) A')) , (= B C)(= A (+ (+ C D) A'))
EqReplaceEq1Add0Add0Mul0 # <title> Substitution </title> # <table> # (= A (+ (+ (* [ B ] ] ] D) A') B')) # (= [ B ] [ C ] ) # (= A (+ (+ (* [ [ [ C ] D) A') B')) # </table>
(= A (+ (+ (* B D) A') B')) , (= B C)(= A (+ (+ (* C D) A') B'))
EqReplaceEq1Add0Add0Add0 # <title> Substitution </title> # <table> # (= A (+ (+ (+ [ B ] ] ] D) A') B')) # (= [ B ] [ C ] ) # (= A (+ (+ (+ [ [ [ C ] D) A') B')) # </table>
(= A (+ (+ (+ B D) A') B')) , (= B C)(= A (+ (+ (+ C D) A') B'))
EqReplaceEq1Add0Add0Add1 # <title> Substitution </title> # <table> # (= A (+ (+ (+ B [ C ] ] ] ) A') B')) # (= [ C ] [ D ] ) # (= A (+ (+ (+ B [ [ [ D ] ) A') B')) # </table>
(= A (+ (+ (+ B C) A') B')) , (= C D)(= A (+ (+ (+ B D) A') B'))
EqReplaceEq1Add0Add0Add1Mul0 # <title> Substitution </title> # <table> # (= A (+ (+ (+ B (* [ C ] ] ] A')) B') C')) # (= [ C ] [ D ] ) # (= A (+ (+ (+ B (* [ [ [ D ] A')) B') C')) # </table>
(= A (+ (+ (+ B (* C A')) B') C')) , (= C D)(= A (+ (+ (+ B (* D A')) B') C'))
multiplyFractions2 # <summary> An example of multiplying two fractions. </summary>
(= (* (/ (+ (* (3) (10)) (6)) (5)) (/ (+ (* (6) (10)) (7)) (3))) (/ (+ (* (8) (* (10) (10))) (4)) (5)))
addFractions1 # <summary> This is an example of adding two fractions. </summary>
(= (+ (/ (1) (2)) (/ (1) (4))) (/ (3) (4)))
addFractions2 # <summary> This is an example of adding two fractions. </summary>
(= (+ (/ (5) (6)) (/ (7) (6))) (2))
EqReplaceGt0 # <title> Substitution </title> # <table> # (> [ A ] ] ] C) # (= [ A ] [ B ] ) # (> [ [ [ B ] C) # </table>
(> A C) , (= A B)(> B C)
EqReplaceGt1 # <title> Substitution </title> # <table> # (> A [ B ] ] ] ) # (= [ B ] [ C ] ) # (> A [ [ [ C ] ) # </table>
(> A B) , (= B C)(> A C)
2greater1 # <title> One-Digit Inequality </title>
(> (2) (1))
GtReplaceGt1 # <title> Substitution </title> # <table> # (> A [ B ] ] ] ) # (> [ B ] [ C ] ) # (> A [ [ [ C ] ) # </table>
(> A B) , (> B C)(> A C)
2greater0 # <title> One-Digit Inequality </title>
(> (2) (0))
9greater8 # <title> One-Digit Inequality </title>
(> (9) (8))
8greater7 # <title> One-Digit Inequality </title>
(> (8) (7))
7greater6 # <title> One-Digit Inequality </title>
(> (7) (6))
6greater5 # <title> One-Digit Inequality </title>
(> (6) (5))
5greater4 # <title> One-Digit Inequality </title>
(> (5) (4))
4greater3 # <title> One-Digit Inequality </title>
(> (4) (3))
3greater2 # <title> One-Digit Inequality </title>
(> (3) (2))
3greater0 # <title> One-Digit Inequality </title>
(> (3) (0))
4greater0 # <title> One-Digit Inequality </title>
(> (4) (0))
5greater0 # <title> One-Digit Inequality </title>
(> (5) (0))
6greater0 # <title> One-Digit Inequality </title>
(> (6) (0))
7greater0 # <title> One-Digit Inequality </title>
(> (7) (0))
8greater0 # <title> One-Digit Inequality </title>
(> (8) (0))
9greater0 # <title> One-Digit Inequality </title>
(> (9) (0))
10greater1 # <title> One-Digit Inequality </title>
(> (10) (1))
addFractions3 # <summary> This is an example of adding two fractions. </summary>
(= (+ (/ (5) (+ (10) (2))) (/ (1) (4))) (/ (2) (3)))
4greater1 # <title> One-Digit Inequality </title>
(> (4) (1))
10greater9 # <title> One-Digit Inequality </title>
(> (10) (9))
10greater0 # <title> One-Digit Inequality </title>
(> (10) (0))
5greater1 # <title> One-Digit Inequality </title>
(> (5) (1))
7greater1 # <title> One-Digit Inequality </title>
(> (7) (1))
addFractions4 # <summary> This is an example of adding two fractions. </summary>
(= (+ (/ (+ (10) (3)) (+ (10) (6))) (/ (5) (+ (* (4) (10)) (7)))) (/ (+ (* (6) (* (10) (10))) (+ (* (9) (10)) (1))) (+ (* (7) (* (10) (10))) (+ (* (5) (10)) (2)))))
subtractFractions1 # <summary> This is an example of subtracting a fraction. </summary>
(= (- (2) (/ (1) (3))) (/ (5) (3)))
EqReplaceEq1Minus1 # <title> Substitution </title> # <table> # (= A (- B [ C ] ] ] )) # (= [ C ] [ D ] ) # (= A (- B [ [ [ D ] )) # </table>
(= A (- B C)) , (= C D)(= A (- B D))
EqReplaceEq1Add0Add0Add0Add1 # <title> Substitution </title> # <table> # (= A (+ (+ (+ (+ B [ C ] ] ] ) A') B') C')) # (= [ C ] [ D ] ) # (= A (+ (+ (+ (+ B [ [ [ D ] ) A') B') C')) # </table>
(= A (+ (+ (+ (+ B C) A') B') C')) , (= C D)(= A (+ (+ (+ (+ B D) A') B') C'))
subtractFractions2 # <summary> This is used just for convenience to get an empty theorem. </summary>
(= (- (/ (+ (10) (7)) (+ (* (2) (10)) (3))) (/ (7) (+ (10) (8)))) (/ (+ (* (10) (10)) (+ (* (4) (10)) (5))) (+ (* (4) (* (10) (10))) (+ (10) (4)))))
emptyThm # <summary> This is used just for convenience to get an empty theorem. </summary>
(T)