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

!(defprotocol not_not_not_a_imp_not_a_protocol (comm_term)
    (cons
        ;; claim definition
        (cons (cons 
                ;; expression
                ;; needs to be a quoted syntax tree
                (list 'check nil (list 'open comm_term) 'statement)
                ;; environment 
                (letrec (
                    (arg1 (lambda (x) (car (cdr x))))
                    (arg1a (lambda (x) (car (arg1 x))))
                    (arg1b (lambda (x) (cdr (arg1 x))))
                    (arg2 (lambda (x) (car (cdr (cdr x)))))
                    (arg2a (lambda (x) (car (arg2 x))))
                    (arg2b (lambda (x) (cdr (arg2 x))))
                    (and (lambda (x y) (if x (if y t nil) nil)))
                    (or (lambda (x y) (if x t (if y t nil))))
                    (geti (lambda (xs i) (if (= i 0) (car xs) (geti (cdr xs) (- i 1)))))
                    (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))
                            t
                        nil))))))))))
                    
                    (statement (list 1n (list 1n (list 1n (list 1n (list 0n 0n) '(5n)) '(5n)) '(5n)) (list 1n (list 0n 0n) '(5n))))
                ) (current-env))
            )
            ;; expected output
            t )
        ;; post-verification predicate
        nil)
:description "¬¬¬A → ¬A")

!(dump-expr not_not_not_a_imp_not_a_protocol "demo_protocol")