1. 1
2. 2
3. 3
4. 4
5. 5
6. 6
7. 7
8. 8
9. 9
10. 10
11. 11
12. 12
13. 13
14. 14
15. 15
16. 16
17. 17
18. 18
19. 19
20. 20
21. 21
22. 22
23. 23
24. 24
25. 25
26. 26
27. 27
28. 28
29. 29
30. 30
31. 31
32. 32
33. 33
34. 34
35. 35
36. 36
37. 37
38. 38
39. 39
40. 40
41. 41
42. 42
43. 43
44. 44
45. 45
46. 46
47. 47
48. 48
49. 49
50. 50
51. 51
52. 52
53. 53
54. 54
55. 55
56. 56
57. 57
58. 58
59. 59
60. 60
61. 61
62. 62
63. 63
64. 64
65. 65
66. 66
67. 67
68. 68
69. 69
70. 70
71. 71
72. 72
73. 73
74. 74
75. 75

;; Get second element of list (0-indexed)
!(def arg1 (lambda (x) (car (cdr x))))

;; Get left element of tuple at second position in list
!(def arg1a (lambda (x) (car (arg1 x))))

!(def arg1b (lambda (x) (cdr (arg1 x))))

;; Get third element of list
!(def arg2 (lambda (x) (car (cdr (cdr x)))))

!(def arg2a (lambda (x) (car (arg2 x))))

!(def arg2b (lambda (x) (cdr (arg2 x))))

;; Boolean and
!(def and (lambda (x y) (if x (if y t nil) nil)))

;; Boolean or
!(def or (lambda (x y) (if x t (if y t nil))))

;; Get ith element of list
!(defrec geti (lambda (xs i) (if (= i 0) (car xs) (geti (cdr xs) (- i 1)))))

;; NEED defrec instead of def for recursive functions
;; TODO: Implement nats
!(defrec check (lambda (env term typ)
  ;; Variable
  (if (= (car term) 10n)
    (eq typ (geti env (arg1 term)))
  ;; Lambda
  (if (and (= (car term) 11n) (= (car typ) 1n))
    (and (eq (arg2 typ) (arg1b term))
      (check (cons (arg1 typ) env) (arg1a term) (arg1b term)))
  ;; Application
  (if (and (= (car term) 12n) (= (car (arg1b term)) 1n))
    (and (eq (arg1 (arg1b term)) (arg2b term)) (and (eq (arg2 (arg1b term)) typ)
      (and (check env (arg1a term) (arg1b term)) (check env (arg2a term) (arg2b term)))))
  ;; And
  (if (and (= (car term) 13n) (= (car typ) 2n))
    (and (eq (arg1b term) (arg1 typ)) (and (eq (arg2b term) (arg2 typ))
      (and (check env (arg1a term) (arg1b term)) (check env (arg2a term) (arg2b term)))))
  ;; And1
  (if (and (= (car term) 14n) (= (car (arg1b term)) 2n))
    (and (eq (arg1 (arg1b term)) typ)
      (check env (arg1a term) (arg1b term)))
  ;; And2
  (if (and (= (car term) 15n) (= (car (arg1b term)) 2n))
    (and (eq (arg2 (arg1b term)) typ)
      (check env (arg1a term) (arg1b term)))
  ;; Or
  (if (and (= (car term) 16n) (= (car typ) 3n))
    (and (or (eq (arg1b term) (arg1 typ)) (eq (arg1b term) (arg2 typ)))
      (check env (arg1a term) (arg1b term)))
  ;; False elim
  (if (and (= (car term) 20n) (eq (car (arg1b term)) 5n))
    (check env (arg1a term) (arg1b term))
  nil))))))))))

; Autogenerated by Main.lean
!(def a_imp_a (cons (list 11n (cons (list 10n 0) (list 0n 0n))) (list 1n (list 0n 0n) (list 0n 0n))))

(check nil (car a_imp_a) (cdr a_imp_a))

!(def a_imp_b_imp_ba (cons (list 11n (cons (list 11n (cons (list 13n (cons (list 10n 0) (list 0n 1n)) (cons (list 10n 1) (list 0n 0n))) (list 2n (list 0n 1n) (list 0n 0n)))) (list 1n (list 0n 1n) (list 2n (list 0n 1n) (list 0n 0n))))) (list 1n (list 0n 0n) (list 1n (list 0n 1n) (list 2n (list 0n 1n) (list 0n 0n))))))

(check nil (car a_imp_b_imp_ba) (cdr a_imp_b_imp_ba))

!(def ab_imp_ba (cons (list 11n (cons (list 13n (cons (list 15n (cons (list 10n 0) (list 2n (list 0n 0n) (list 0n 1n)))) (list 0n 1n)) (cons (list 14n (cons (list 10n 0) (list 2n (list 0n 0n) (list 0n 1n)))) (list 0n 0n))) (list 2n (list 0n 1n) (list 0n 0n)))) (list 1n (list 2n (list 0n 0n) (list 0n 1n)) (list 2n (list 0n 1n) (list 0n 0n)))))

(check nil (car ab_imp_ba) (cdr ab_imp_ba))

!(def not_ab_imp_not_a (cons (list 11n (cons (list 11n (cons (list 12n (cons (list 10n 1) (list 1n (list 3n (list 0n 0n) (list 0n 1n)) '(5n))) (cons (list 16n (cons (list 10n 0) (list 0n 0n))) (list 3n (list 0n 0n) (list 0n 1n)))) '(5n))) (list 1n (list 0n 0n) '(5n)))) (list 1n (list 1n (list 3n (list 0n 0n) (list 0n 1n)) '(5n)) (list 1n (list 0n 0n) '(5n)))))

(check nil (car not_ab_imp_not_a) (cdr not_ab_imp_not_a))