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

!(defprotocol add_zero_eq_zero_add_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))))
(arg2 (lambda (x) (car (cdr (cdr x)))))
(arg3 (lambda (x) (car (cdr (cdr (cdr x))))))
(arg4 (lambda (x) (car (cdr (cdr (cdr (cdr x)))))))
(geti (lambda (xs i) (if (= i 0) (car xs) (geti (cdr xs) (- i 1)))))
(and (lambda (x y) (if x (if y t nil) nil)))
(or (lambda (x y) (if x t (if y t nil))))
(is_app1 (lambda (term op) (if (= (car term) 2n) (= (car (arg1 term)) op) nil)))
(is_app2 (lambda (term op) (if (= (car term) 2n) (is_app1 (arg1 term) op) nil)))
(is_app3 (lambda (term op) (if (= (car term) 2n) (is_app2 (arg1 term) op) nil)))
(is_app4 (lambda (term op) (if (= (car term) 2n) (is_app3 (arg1 term) op) nil)))
(is_app5 (lambda (term op) (if (= (car term) 2n) (is_app4 (arg1 term) op) nil)))
(map (lambda (f xs) (if (eq xs nil) nil (cons (f (car xs)) (map f (cdr xs))))))
(len (lambda (xs) (if (eq xs nil) 0 (+ 1 (len (cdr xs))))))
(dbtypes (list '(3n 1) '(4n (3n 0) (4n (4n (0n 0) (3n 0)) (4n (0n 1) (4n (2n (0n 1) (4n (0n 2) (3n 0)) (0n 0) (0n 2)) (5n (0n 3) (0n 2)))))) '(4n (3n 0) (4n (4n (0n 0) (3n 0)) (4n (4n (5n (0n 1) (0n 0)) (3n 0)) (4n (4n (0n 2) (4n (2n (0n 2) (4n (0n 3) (3n 0)) (0n 0) (0n 3)) (2n (0n 2) (4n (5n (0n 4) (0n 3)) (3n 0)) (2n (2n (2n (2n (6n) (4n (3n 0) (4n (4n (0n 0) (3n 0)) (4n (0n 1) (4n (2n (0n 1) (4n (0n 2) (3n 0)) (0n 0) (0n 2)) (5n (0n 3) (0n 2)))))) (0n 4) (3n 0)) (4n (4n (0n 4) (3n 0)) (4n (0n 5) (4n (2n (0n 1) (4n (0n 6) (3n 0)) (0n 0) (0n 6)) (5n (0n 7) (0n 2))))) (0n 3) (4n (0n 4) (3n 0))) (4n (0n 4) (4n (2n (0n 4) (4n (0n 5) (3n 0)) (0n 0) (0n 5)) (5n (0n 6) (0n 5)))) (0n 1) (0n 4)) (4n (2n (0n 3) (4n (0n 4) (3n 0)) (0n 1) (0n 4)) (5n (0n 5) (0n 4))) (0n 0) (2n (0n 3) (4n (0n 4) (3n 0)) (0n 1) (0n 4))) (5n (0n 4) (0n 3))))) (4n (5n (0n 3) (0n 2)) (2n (0n 2) (4n (5n (0n 4) (0n 3)) (3n 0)) (0n 0) (5n (0n 4) (0n 3)))))))) '(4n (3n 0) (4n (3n 0) (4n (0n 1) (8n (0n 2) (0n 1))))) '(4n (3n 0) (4n (3n 0) (4n (0n 0) (8n (0n 2) (0n 1))))) '(4n (3n 0) (4n (3n 0) (4n (4n (8n (0n 1) (0n 0)) (3n 0)) (4n (4n (0n 2) (2n (0n 1) (4n (8n (0n 3) (0n 2)) (3n 0)) (2n (2n (2n (9n) (4n (3n 0) (4n (3n 0) (4n (0n 1) (8n (0n 2) (0n 1))))) (0n 3) (3n 0)) (4n (3n 0) (4n (0n 4) (8n (0n 5) (0n 1)))) (0n 2) (3n 0)) (4n (0n 3) (8n (0n 4) (0n 3))) (0n 0) (0n 3)) (8n (0n 3) (0n 2)))) (4n (4n (0n 2) (2n (0n 2) (4n (8n (0n 4) (0n 3)) (3n 0)) (2n (2n (2n (10n) (4n (3n 0) (4n (3n 0) (4n (0n 0) (8n (0n 2) (0n 1))))) (0n 4) (3n 0)) (4n (3n 0) (4n (0n 0) (8n (0n 6) (0n 1)))) (0n 3) (3n 0)) (4n (0n 3) (8n (0n 5) (0n 4))) (0n 0) (0n 3)) (8n (0n 4) (0n 3)))) (4n (8n (0n 4) (0n 3)) (2n (0n 3) (4n (8n (0n 5) (0n 4)) (3n 0)) (0n 0) (8n (0n 5) (0n 4))))))))) '(4n (3n 0) (4n (0n 0) (12n (0n 0) (0n 0) (0n 1)))) '(4n (3n 0) (4n (0n 0) (4n (4n (0n 1) (4n (12n (0n 1) (0n 0) (0n 2)) (3n 0))) (4n (2n (2n (0n 0) (4n (0n 2) (4n (12n (0n 2) (0n 0) (0n 3)) (3n 0))) (0n 1) (0n 2)) (4n (12n (0n 1) (0n 1) (0n 2)) (3n 0)) (2n (2n (13n) (4n (3n 0) (4n (0n 0) (12n (0n 0) (0n 0) (0n 1)))) (0n 2) (3n 0)) (4n (0n 2) (12n (0n 0) (0n 0) (0n 3))) (0n 1) (0n 2)) (12n (0n 1) (0n 1) (0n 2))) (4n (0n 3) (4n (12n (0n 3) (0n 0) (0n 4)) (2n (2n (0n 3) (4n (0n 5) (4n (12n (0n 5) (0n 0) (0n 6)) (3n 0))) (0n 1) (0n 5)) (4n (12n (0n 4) (0n 1) (0n 5)) (3n 0)) (0n 0) (12n (0n 4) (0n 1) (0n 5))))))))) '(3n 0) '(15n) '(4n (15n) (15n)) '(4n (4n (15n) (3n 0)) (4n (2n (0n 0) (4n (15n) (3n 0)) (16n) (15n)) (4n (4n (15n) (4n (2n (0n 2) (4n (15n) (3n 0)) (0n 0) (15n)) (2n (0n 3) (4n (15n) (3n 0)) (2n (17n) (4n (15n) (15n)) (0n 1) (15n)) (15n)))) (4n (15n) (2n (0n 3) (4n (15n) (3n 0)) (0n 0) (15n)))))) '(3n 0) '(19n) '(3n 0) '(4n (4n (21n) (3n 0)) (4n (21n) (2n (0n 1) (4n (21n) (3n 0)) (0n 0) (21n))))))
(get-dbtype (lambda (term) (let ((op (car term))) (if (= op 3n) (if (= (arg1 term) 0) (geti dbtypes 0) term) (if (= op 6n) (geti dbtypes 1) (if (= op 7n) (geti dbtypes 2) (if (= op 9n) (geti dbtypes 3) (if (= op 10n) (geti dbtypes 4) (if (= op 11n) (geti dbtypes 5) (if (= op 13n) (geti dbtypes 6) (if (= op 14n) (geti dbtypes 7) (if (= op 15n) (geti dbtypes 8) (if (= op 16n) (geti dbtypes 9) (if (= op 17n) (geti dbtypes 10) (if (= op 18n) (geti dbtypes 11) (if (= op 19n) (geti dbtypes 12) (if (= op 20n) (geti dbtypes 13) (if (= op 21n) (geti dbtypes 14) (if (= op 22n) (geti dbtypes 15) term)))))))))))))))))))
(term-rec (lambda (term s fdep fvar) (let ((op (car term))) (if (= op 0n) (fvar s (arg1 term)) (if (= op 1n) (list 1n (term-rec (arg1 term) (fdep s) fdep fvar) (term-rec (arg2 term) (fdep s) fdep fvar)) (if (= op 2n) (list 2n (term-rec (arg1 term) s fdep fvar) (term-rec (arg2 term) s fdep fvar) (term-rec (arg3 term) s fdep fvar) (term-rec (arg4 term) s fdep fvar)) (if (= op 4n) (list 4n (term-rec (arg1 term) s fdep fvar) (term-rec (arg2 term) (fdep s) fdep fvar)) (if (= op 5n) (list 5n (term-rec (arg1 term) s fdep fvar) (term-rec (arg2 term) s fdep fvar)) (if (= op 8n) (list 8n (term-rec (arg1 term) s fdep fvar) (term-rec (arg2 term) s fdep fvar)) (if (= op 12n) (list 12n (term-rec (arg1 term) s fdep fvar) (term-rec (arg2 term) s fdep fvar) (term-rec (arg3 term) s fdep fvar)) term))))))))))
(incr (lambda (term) (term-rec term 0 (lambda (d) (+ d 1)) (lambda (d x) (list 0n (if (<= d x) (+ x 1) x))))))
(sub (lambda (term t_prime) (term-rec term (cons 0 t_prime) (lambda (s) (cons (+ (car s) 1) (incr (cdr s)))) (lambda (s x) (let ((d (car s)) (tp (cdr s))) (if (= x d) tp (list 0n (if (< d x) (- x 1) x))))))))
(evaluate (lambda (term) (let ((op (car term))) (if (= op 1n) (list 1n (evaluate (arg1 term)) (evaluate (arg2 term))) (if (= op 4n) (list 4n (evaluate (arg1 term)) (evaluate (arg2 term))) (if (= op 5n) (list 5n (evaluate (arg1 term)) (evaluate (arg2 term))) (if (= op 8n) (list 8n (evaluate (arg1 term)) (evaluate (arg2 term))) (if (= op 12n) (list 12n (evaluate (arg1 term)) (evaluate (arg2 term)) (evaluate (arg3 term))) (if (= op 2n) (let ((f_prime (evaluate (arg1 term))) (a_prime (evaluate (arg3 term))) (phi (arg2 term)) (phi_prime (evaluate phi)) (alpha_prime (evaluate (arg4 term)))) (let ((f_op (car f_prime))) (if (= f_op 1n) (evaluate (sub (arg1 f_prime) a_prime)) (if (and (is_app4 f_prime 7n) (is_app4 a_prime 6n)) (let ((g (arg3 f_prime)) (alpha_gamma (arg4 f_prime)) (a_val (arg3 (arg1 a_prime))) (b (arg3 a_prime)) (beta (arg4 a_prime)) (alpha_val (arg1 alpha_gamma)) (gamma (arg2 alpha_gamma))) (evaluate (list 2n (list 2n g (list 4n alpha_val gamma) a_val alpha_val) (sub gamma a_val) b beta))) (if (and (is_app5 f_prime 11n) (is_app3 a_prime 9n)) (let ((g (arg3 (arg1 f_prime))) (gamma (arg4 (arg1 f_prime))) (a_val (arg3 a_prime)) (alpha_val (arg4 a_prime))) (evaluate (list 2n g gamma a_val alpha_val))) (if (and (is_app5 f_prime 11n) (is_app3 a_prime 10n)) (let ((g (arg3 f_prime)) (gamma (arg4 f_prime)) (b_val (arg3 a_prime)) (beta_val (arg4 a_prime))) (evaluate (list 2n g gamma b_val beta_val))) (if (and (is_app5 f_prime 14n) (is_app2 a_prime 13n)) (let ((ha (arg3 (arg1 f_prime)))) (evaluate ha)) (if (and (is_app3 f_prime 18n) (= (car a_prime) 16n)) (let ((z (arg3 (arg1 f_prime)))) (evaluate z)) (if (and (is_app3 f_prime 18n) (is_app1 a_prime 17n)) (let ((m (arg3 (arg1 (arg1 f_prime)))) (g (arg3 f_prime)) (gamma (arg2 (arg4 f_prime))) (n (arg3 a_prime))) (evaluate (list 2n (list 2n g (list 4n '(15n) gamma) n '(15n)) (sub gamma n) (list 2n f_prime phi n '(15n)) (list 2n m (list 4n '(15n) '(3n 0)) n '(15n))))) (list 2n f_prime phi_prime a_prime alpha_prime)))))))))) term)))))))))
(cumeq (lambda (a a_prime) (if (and (eq a '(3n 0)) (eq a_prime '(3n 1))) t (eq a (evaluate a_prime)))))
(check (lambda (env term tau) (let ((t_op (car term)) (tau_op (car tau))) (if (= t_op 0n) (let ((x (arg1 term))) (if (< x (len env)) (cumeq (evaluate (geti env x)) tau) nil)) (if (and (= t_op 1n) (= tau_op 4n)) (let ((b (arg1 term)) (beta (arg2 term)) (alpha (arg1 tau)) (beta_prime (arg2 tau)) (new_env (cons (incr alpha) (map incr env)))) (if (check new_env b beta) (cumeq (evaluate beta) (evaluate beta_prime)) nil)) (if (= t_op 2n) (let ((f (arg1 term)) (phi (arg2 term)) (a (arg3 term)) (alpha_prime (arg4 term))) (if (= (car phi) 4n) (let ((alpha (arg1 phi)) (beta (arg2 phi))) (if (check env f phi) (if (check env a alpha) (if (cumeq (evaluate alpha) (evaluate alpha_prime)) (cumeq (evaluate (sub beta a)) tau) nil) nil) nil)) (cumeq (get-dbtype term) tau))) (if (and (= t_op 4n) (= tau_op 3n)) (let ((alpha (arg1 term)) (beta (arg2 term)) (new_env (cons (incr alpha) (map incr env)))) (if (check env alpha tau) (check new_env beta tau) nil)) (if (and (= t_op 5n) (= tau_op 3n)) (let ((alpha (arg1 term)) (beta (arg2 term))) (if (check env alpha tau) (check env beta (list 4n alpha '(3n 0))) nil)) (if (and (= t_op 8n) (= tau_op 3n)) (let ((alpha (arg1 term)) (beta (arg2 term))) (if (check env alpha tau) (check env beta tau) nil)) (if (and (= t_op 12n) (= tau_op 3n)) (let ((a (arg1 term)) (a_prime (arg2 term)) (alpha (arg3 term))) (if (check env a alpha) (if (check env a_prime alpha) (check env alpha tau) nil) nil)) (if (= t_op 3n) (if (= (arg1 term) 1) nil (cumeq (get-dbtype term) tau)) (cumeq (get-dbtype term) tau))))))))))))
(check_pair (lambda (term tau) (if (check nil tau '(3n 1)) (check nil term tau) nil)))
                    
                    (statement '(4n (15n) (12n (2n (2n (1n (2n (2n (2n (18n) (4n (4n (15n) (3n 0)) (4n (2n (0n 0) (4n (15n) (3n 0)) (16n) (15n)) (4n (4n (15n) (4n (2n (0n 2) (4n (15n) (3n 0)) (0n 0) (15n)) (2n (0n 3) (4n (15n) (3n 0)) (2n (17n) (4n (15n) (15n)) (0n 1) (15n)) (15n)))) (4n (15n) (2n (0n 3) (4n (15n) (3n 0)) (0n 0) (15n)))))) (1n (15n) (3n 0)) (4n (15n) (3n 0))) (4n (2n (1n (15n) (3n 0)) (4n (15n) (3n 0)) (16n) (15n)) (4n (4n (15n) (4n (2n (1n (15n) (3n 0)) (4n (15n) (3n 0)) (0n 0) (15n)) (2n (1n (15n) (3n 0)) (4n (15n) (3n 0)) (2n (17n) (4n (15n) (15n)) (0n 1) (15n)) (15n)))) (4n (15n) (2n (1n (15n) (3n 0)) (4n (15n) (3n 0)) (0n 0) (15n))))) (0n 0) (2n (1n (15n) (3n 0)) (4n (15n) (3n 0)) (16n) (15n))) (4n (4n (15n) (4n (2n (1n (15n) (3n 0)) (4n (15n) (3n 0)) (0n 0) (15n)) (2n (1n (15n) (3n 0)) (4n (15n) (3n 0)) (2n (17n) (4n (15n) (15n)) (0n 1) (15n)) (15n)))) (4n (15n) (2n (1n (15n) (3n 0)) (4n (15n) (3n 0)) (0n 0) (15n)))) (1n (1n (2n (17n) (4n (15n) (15n)) (0n 0) (15n)) (15n)) (4n (15n) (15n))) (4n (15n) (4n (2n (1n (15n) (3n 0)) (4n (15n) (3n 0)) (0n 0) (15n)) (2n (1n (15n) (3n 0)) (4n (15n) (3n 0)) (2n (17n) (4n (15n) (15n)) (0n 1) (15n)) (15n))))) (4n (15n) (15n))) (4n (15n) (4n (15n) (15n))) (0n 0) (15n)) (4n (15n) (15n)) (16n) (15n)) (2n (2n (1n (2n (2n (2n (18n) (4n (4n (15n) (3n 0)) (4n (2n (0n 0) (4n (15n) (3n 0)) (16n) (15n)) (4n (4n (15n) (4n (2n (0n 2) (4n (15n) (3n 0)) (0n 0) (15n)) (2n (0n 3) (4n (15n) (3n 0)) (2n (17n) (4n (15n) (15n)) (0n 1) (15n)) (15n)))) (4n (15n) (2n (0n 3) (4n (15n) (3n 0)) (0n 0) (15n)))))) (1n (15n) (3n 0)) (4n (15n) (3n 0))) (4n (2n (1n (15n) (3n 0)) (4n (15n) (3n 0)) (16n) (15n)) (4n (4n (15n) (4n (2n (1n (15n) (3n 0)) (4n (15n) (3n 0)) (0n 0) (15n)) (2n (1n (15n) (3n 0)) (4n (15n) (3n 0)) (2n (17n) (4n (15n) (15n)) (0n 1) (15n)) (15n)))) (4n (15n) (2n (1n (15n) (3n 0)) (4n (15n) (3n 0)) (0n 0) (15n))))) (0n 0) (2n (1n (15n) (3n 0)) (4n (15n) (3n 0)) (16n) (15n))) (4n (4n (15n) (4n (2n (1n (15n) (3n 0)) (4n (15n) (3n 0)) (0n 0) (15n)) (2n (1n (15n) (3n 0)) (4n (15n) (3n 0)) (2n (17n) (4n (15n) (15n)) (0n 1) (15n)) (15n)))) (4n (15n) (2n (1n (15n) (3n 0)) (4n (15n) (3n 0)) (0n 0) (15n)))) (1n (1n (2n (17n) (4n (15n) (15n)) (0n 0) (15n)) (15n)) (4n (15n) (15n))) (4n (15n) (4n (2n (1n (15n) (3n 0)) (4n (15n) (3n 0)) (0n 0) (15n)) (2n (1n (15n) (3n 0)) (4n (15n) (3n 0)) (2n (17n) (4n (15n) (15n)) (0n 1) (15n)) (15n))))) (4n (15n) (15n))) (4n (15n) (4n (15n) (15n))) (16n) (15n)) (4n (15n) (15n)) (0n 0) (15n)) (15n))))
                ) (current-env))
            )
            ;; expected output
            t )
        ;; post-verification predicate
        nil)
:description "n + 0 = 0 + n")

!(dump-expr add_zero_eq_zero_add_protocol "protocol")