# List of theorems

List of theorems in general/Basic_arithmetic.gh:

(→ (= b0 b1) (= (+ a b0) (+ a b1)))
(→ (= a0 a1) (= (+ a0 b) (+ a1 b)))
(= a0 a1) , (= b0 b1)(= (+ a0 b0) (+ a1 b1))
(= b0 b1)(= (+ a b0) (+ a b1))
(= a0 a1)(= (+ a0 b) (+ a1 b))
(= a b)(= (succ a) (succ b))
(= (succ a) (succ b))(= a b)
(→ (= b0 b1) (= (· a b0) (· a b1)))
(→ (= a0 a1) (= (· a0 b) (· a1 b)))
(= a0 a1) , (= b0 b1)(= (· a0 b0) (· a1 b1))
(= b0 b1)(= (· a b0) (· a b1))
(= a0 a1)(= (· a0 b) (· a1 b))
(→ φ (= a0 a1)) , (→ φ (= b0 b1))(→ φ (= (+ a0 b0) (+ a1 b1)))
(→ (= n (0)) (↔ φ φ0)) , (→ (= n k) (↔ φ φk)) , (→ (= n (succ k)) (↔ φ φSk)) , φ0 , (→ φk φSk)φ
(→ (= n (0)) (↔ φ φ0)) , (→ (= n k) (↔ φ φk)) , (→ (= n (succ k)) (↔ φ φSk)) , (→ (= n a) (↔ φ φa)) , φ0 , (→ φk φSk)φa
(= (+ (0) a) a)
(= (+ a (0)) a)
(= (+ (succ a) b) (succ (+ a b)))
(= (+ a b) (+ b a))
(= (+ (+ a b) c) (+ a (+ b c)))
(→ (= n sub) (↔ (→ (= (+ a n) (+ b n)) (= a b)) (→ (= (+ a sub) (+ b sub)) (= a b))))
(→ (= (+ a c) (+ b c)) (= a b))
(↔ (= (+ a c) (+ b c)) (= a b))
(= (+ a c) (+ b c))(= a b)
(↔ (= (+ c a) (+ c b)) (= a b))
(= (+ c a) (+ c b))(= a b)
(= (· (0) a) (0))
(= (· a (0)) (0))
(= (+ (· (succ a) kk) (succ a)) (· (succ a) (succ kk)))
(= (+ (+ (· a kk) kk) (succ a)) (+ (· a (succ kk)) (succ kk)))
(→ (= (· (succ a) kk) (+ (· a kk) kk)) (= (· (succ a) (succ kk)) (+ (· a (succ kk)) (succ kk))))
(= (· (succ a) b) (+ (· a b) b))
(= (· a b) (· b a))
(= (+ (+ a b) (+ c d)) (+ (+ a c) (+ b d)))
(= (+ (+ a b) c) (+ (+ a c) b))
(= (· a (+ b c)) (+ (· a b) (· a c)))
(= (· (+ a b) c) (+ (· a c) (· b c)))
(= (· (· a b) c) (· a (· b c)))
(= (1) (succ (0)))
(= (· a (1)) a)
(= (· (1) a) a)
(¬ (= (0) (1)))
(↔ (≤ a b) (∃ n (= (+ a n) b)))
(→ (= a0 a1) (↔ (≤ a0 b) (≤ a1 b)))
(→ (= b0 b1) (↔ (≤ a b0) (≤ a b1)))
(→ (∧ (= a0 a1) (= b0 b1)) (↔ (≤ a0 b0) (≤ a1 b1)))
(→ (= (+ a c) b) (≤ a b))
(≤ (0) a)
(→ (= a sub) (↔ (→ (¬ (= a (0))) (∃ m (= (succ m) a))) (→ (¬ (= sub (0))) (∃ m (= (succ m) sub)))))
(→ (¬ (= a (0))) (∃ m (= (succ m) a)))
(→ (∧ (= (+ a ab) b) (= (+ b bc) c)) (= (+ a (+ ab bc)) c))
(→ (∧ (≤ a b) (≤ b c)) (≤ a c))
(→ (∧ (= (+ a b) c) (= b (0))) (= a c))
(→ (= (+ a b) (0)) (= a (0)))
(→ (∧ (= (+ a n) b) (= (+ b m) a)) (= a b))
(→ (∧ (≤ a b) (≤ b a)) (= a b))
(↔ (∃ n (≤ a b)) (≤ a b))
(↔ (∃ n (∨ (≤ a b) (≤ c d))) (∨ (≤ a b) (≤ c d)))
(→ (≤ a k) (≤ a (succ k)))
(→ (≤ a k) (∨ (≤ a (succ k)) (≤ (succ k) a)))
(→ (= m (0)) (→ (= (+ k m) a) (= k a)))
(→ (= a k) (≤ a k))
(→ (= a k) (≤ a (succ k)))
(→ (= m (0)) (→ (= (+ k m) a) (∨ (≤ a (succ k)) (≤ (succ k) a))))
(→ (¬ (= m (0))) (→ (= (+ k m) a) (∨ (≤ a (succ k)) (≤ (succ k) a))))
(→ (≤ k a) (∨ (≤ a (succ k)) (≤ (succ k) a)))
(→ (= b sub) (↔ (∨ (∃ an (= (+ a an) b)) (∃ na (= (+ b na) a))) (∨ (∃ an (= (+ a an) sub)) (∃ na (= (+ sub na) a)))))
(∨ (≤ a b) (≤ b a))
(↔ (≤ a b) (≤ (+ a c) (+ b c)))
(↔ (≤ b0 b1) (≤ (+ a b0) (+ a b1)))
(→ (∧ (≤ a0 a1) (≤ b0 b1)) (≤ (+ a0 b0) (+ a1 b1)))
(↔ (< a0 a1) (< (+ a0 b) (+ a1 b)))
(↔ (< b0 b1) (< (+ a b0) (+ a b1)))
(→ (∧ (≤ a0 a1) (< b0 b1)) (< (+ a0 b0) (+ a1 b1)))
(→ (∧ (< a0 a1) (< b0 b1)) (< (+ a0 b0) (+ a1 b1)))
(→ (≤ a b) (≤ (· a c) (· b c)))
(= (+ a (1)) (succ a))
(→ (= n (0)) (↔ φ φ0)) , (→ (= n k) (↔ φ φk)) , (→ (= n (+ k (1))) (↔ φ φSk)) , (→ (= n a) (↔ φ φa)) , φ0 , (→ φk φSk)φa
(↔ (subst (+ k (1)) n φ) (subst (succ k) n φ))
(↔ (∀ k (→ (subst k n φ) (subst (+ k (1)) n φ))) (∀ k (→ (subst k n φ) (subst (succ k) n φ))))
(↔ (→ (∧ (subst (0) n φ) (∀ k (→ (subst k n φ) (subst (+ k (1)) n φ)))) (∀ n φ)) (→ (∧ (subst (0) n φ) (∀ k (→ (subst k n φ) (subst (succ k) n φ)))) (∀ n φ)))
(→ (∧ (subst (0) n φ) (∀ k (→ (subst k n φ) (subst (+ k (1)) n φ)))) (∀ n φ))