2b9156e0 - 6.5610-project

Authored by: Anthony Wang
Authored at: 2026-05-07 20:49:07 -0400
Committed by: Anthony Wang
Committed at: 2026-05-07 21:18:34 -0400
Signature: View
-----BEGIN SSH SIGNATURE----- U1NIU0lHAAAAAQAAADMAAAALc3NoLWVkMjU1MTkAAAAg8Ms9qQOcB6WoVNS51AHxfRPvJz /x6RXeMaql4lvTraUAAAADZ2l0AAAAAAAAAAZzaGE1MTIAAABTAAAAC3NzaC1lZDI1NTE5 AAAAQGcdWdWrTkP91RU7TxWzD62sOnkcl3xfKqoWrtvlsoRRJshOFTWCTD+7EjvrhEEf8J Pz+bz848map+w7yGCN2QA= -----END SSH SIGNATURE-----
Object name: 2b9156e0fe23adc3d44e17c3c2af139af2faba3d
Parent: 0d7bae04

Port the dependent type checker to Lurk and Python Yeah it's AI slop but seems to work 🤷

Changes

10 changed files (+766/-4)

Dependent.lean
- @@ -177,7 +177,7 @@ theorem gensym_correct : gensym S ∉ S := by
  simp_all intro i hi by_cases h : i = pref.length - · grind [congrArg (·[pref.length]!) h_1] -- The `!` is scary but this works? + · grind [congrArg (·[pref.length]?) h_1] · exact h_3.2 i (by grind) · let T := List.range (List.range (S.size + 1) |>.length) |>.map toString have : S ∪ ofList T = S := by
- @@ -1020,7 +1020,9 @@ def fermat := la'
  -- #guard ch fermat - def main := do - -- Takes 3.5 seconds to run when compiled - IO.FS.writeFile "mul_comm" <| serialize mul_comm + -- Takes 3.5 seconds to run when compiled + def main : IO Unit := do + -- IO.FS.writeFile "mul_comm" <| serialize mul_comm + let start ← IO.monoMsNow IO.println <| ch mul_comm + IO.println s!"Took {(← IO.monoMsNow) - start}ms to check mul_comm"
dbtypes (new)
- @@ -0,0 +1,10 @@
  + ["(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))))"]
slop/dependent.lurk (new)
- @@ -0,0 +1,117 @@
  + !(def arg1 (lambda (x) (car (cdr x)))) + + !(def arg2 (lambda (x) (car (cdr (cdr x))))) + + !(def arg3 (lambda (x) (car (cdr (cdr (cdr x)))))) + + !(def arg4 (lambda (x) (car (cdr (cdr (cdr (cdr x))))))) + + !(defrec geti (lambda (xs i) (if (= i 0) (car xs) (geti (cdr xs) (- i 1))))) + + !(def and (lambda (x y) (if x (if y t nil) nil))) + + !(def or (lambda (x y) (if x t (if y t nil)))) + + !(def is_app1 (lambda (term op) (if (= (car term) 2n) (= (car (arg1 term)) op) nil))) + + !(def is_app2 (lambda (term op) (if (= (car term) 2n) (is_app1 (arg1 term) op) nil))) + + !(def is_app3 (lambda (term op) (if (= (car term) 2n) (is_app2 (arg1 term) op) nil))) + + !(def is_app4 (lambda (term op) (if (= (car term) 2n) (is_app3 (arg1 term) op) nil))) + + !(def is_app5 (lambda (term op) (if (= (car term) 2n) (is_app4 (arg1 term) op) nil))) + + !(defrec map (lambda (f xs) (if (eq xs nil) nil (cons (f (car xs)) (map f (cdr xs)))))) + + !(defrec len (lambda (xs) (if (eq xs nil) 0 (+ 1 (len (cdr xs)))))) + + !(def 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)))))) + + !(def 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))))))))))))))))))) + + !(defrec 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)))))))))) + + !(def incr (lambda (term) (term-rec term 0 (lambda (d) (+ d 1)) (lambda (d x) (list 0n (if (<= d x) (+ x 1) x)))))) + + !(def 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)))))))) + + !(defrec 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))))))))) + + !(defrec cumeq (lambda (a a_prime) (if (and (eq a '(3n 0)) (eq a_prime '(3n 1))) t (eq a (evaluate a_prime))))) + + !(defrec 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)))))))))))) + + !(def check_pair (lambda (term tau) (if (check nil tau '(3n 1)) (check nil term tau) nil)))
slop/generate_lurk.py (new)
- @@ -0,0 +1,215 @@
  + import os + + dbtypes_strs = [ + "(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))))" + ] + + def make_if_chain(conds_and_bodies, fallback): + if not conds_and_bodies: + return fallback + cond, body = conds_and_bodies[0] + return f"(if {cond} {body} {make_if_chain(conds_and_bodies[1:], fallback)})" + + out = [] + out.append("!(def arg1 (lambda (x) (car (cdr x))))") + out.append("!(def arg2 (lambda (x) (car (cdr (cdr x)))))") + out.append("!(def arg3 (lambda (x) (car (cdr (cdr (cdr x))))))") + out.append("!(def arg4 (lambda (x) (car (cdr (cdr (cdr (cdr x)))))))") + + out.append("!(defrec geti (lambda (xs i) (if (= i 0) (car xs) (geti (cdr xs) (- i 1)))))") + + out.append("!(def and (lambda (x y) (if x (if y t nil) nil)))") + out.append("!(def or (lambda (x y) (if x t (if y t nil))))") + + out.append("!(def is_app1 (lambda (term op) (if (= (car term) 2n) (= (car (arg1 term)) op) nil)))") + out.append("!(def is_app2 (lambda (term op) (if (= (car term) 2n) (is_app1 (arg1 term) op) nil)))") + out.append("!(def is_app3 (lambda (term op) (if (= (car term) 2n) (is_app2 (arg1 term) op) nil)))") + out.append("!(def is_app4 (lambda (term op) (if (= (car term) 2n) (is_app3 (arg1 term) op) nil)))") + out.append("!(def is_app5 (lambda (term op) (if (= (car term) 2n) (is_app4 (arg1 term) op) nil)))") + + out.append("!(defrec map (lambda (f xs) (if (eq xs nil) nil (cons (f (car xs)) (map f (cdr xs))))))") + out.append("!(defrec len (lambda (xs) (if (eq xs nil) 0 (+ 1 (len (cdr xs))))))") + + db_list = " ".join(f"'{s}" for s in dbtypes_strs) + out.append(f"!(def dbtypes (list {db_list}))") + + conds = [ + ("(= op 3n)", "(if (= (arg1 term) 0) (geti dbtypes 0) term)"), + ("(= op 6n)", "(geti dbtypes 1)"), + ("(= op 7n)", "(geti dbtypes 2)"), + ("(= op 9n)", "(geti dbtypes 3)"), + ("(= op 10n)", "(geti dbtypes 4)"), + ("(= op 11n)", "(geti dbtypes 5)"), + ("(= op 13n)", "(geti dbtypes 6)"), + ("(= op 14n)", "(geti dbtypes 7)"), + ("(= op 15n)", "(geti dbtypes 8)"), + ("(= op 16n)", "(geti dbtypes 9)"), + ("(= op 17n)", "(geti dbtypes 10)"), + ("(= op 18n)", "(geti dbtypes 11)"), + ("(= op 19n)", "(geti dbtypes 12)"), + ("(= op 20n)", "(geti dbtypes 13)"), + ("(= op 21n)", "(geti dbtypes 14)"), + ("(= op 22n)", "(geti dbtypes 15)"), + ] + out.append(f"!(def get-dbtype (lambda (term) (let ((op (car term))) {make_if_chain(conds, 'term')})))") + + conds = [ + ("(= op 0n)", "(fvar s (arg1 term))"), + ("(= op 1n)", "(list 1n (term-rec (arg1 term) (fdep s) fdep fvar) (term-rec (arg2 term) (fdep s) fdep fvar))"), + ("(= 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))"), + ("(= op 4n)", "(list 4n (term-rec (arg1 term) s fdep fvar) (term-rec (arg2 term) (fdep s) fdep fvar))"), + ("(= op 5n)", "(list 5n (term-rec (arg1 term) s fdep fvar) (term-rec (arg2 term) s fdep fvar))"), + ("(= op 8n)", "(list 8n (term-rec (arg1 term) s fdep fvar) (term-rec (arg2 term) s fdep fvar))"), + ("(= 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))") + ] + out.append(f"!(defrec term-rec (lambda (term s fdep fvar) (let ((op (car term))) {make_if_chain(conds, 'term')})))") + + out.append("!(def incr (lambda (term) (term-rec term 0 (lambda (d) (+ d 1)) (lambda (d x) (list 0n (if (<= d x) (+ x 1) x))))))") + + out.append("!(def 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))))))))") + + eval_inner_conds = [ + ("(= f_op 1n)", "(evaluate (sub (arg1 f_prime) a_prime))"), + ("(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)))"""), + ("(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)))"""), + ("(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)))"""), + ("(and (is_app5 f_prime 14n) (is_app2 a_prime 13n))", "(let ((ha (arg3 (arg1 f_prime)))) (evaluate ha))"), + ("(and (is_app3 f_prime 18n) (= (car a_prime) 16n))", "(let ((z (arg3 (arg1 f_prime)))) (evaluate z))"), + ("(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)))))""") + ] + eval_inner_fallback = "(list 2n f_prime phi_prime a_prime alpha_prime)" + eval_inner = f"""(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))) {make_if_chain(eval_inner_conds, eval_inner_fallback)}))""" + + eval_conds = [ + ("(= op 1n)", "(list 1n (evaluate (arg1 term)) (evaluate (arg2 term)))"), + ("(= op 4n)", "(list 4n (evaluate (arg1 term)) (evaluate (arg2 term)))"), + ("(= op 5n)", "(list 5n (evaluate (arg1 term)) (evaluate (arg2 term)))"), + ("(= op 8n)", "(list 8n (evaluate (arg1 term)) (evaluate (arg2 term)))"), + ("(= op 12n)", "(list 12n (evaluate (arg1 term)) (evaluate (arg2 term)) (evaluate (arg3 term)))"), + ("(= op 2n)", eval_inner), + ] + out.append(f"!(defrec evaluate (lambda (term) (let ((op (car term))) {make_if_chain(eval_conds, 'term')})))") + + out.append("!(defrec cumeq (lambda (a a_prime) (if (and (eq a '(3n 0)) (eq a_prime '(3n 1))) t (eq a (evaluate a_prime)))))") + + check_conds = [ + ("(= t_op 0n)", """(let ((x (arg1 term))) + (if (< x (len env)) + (cumeq (evaluate (geti env x)) tau) + nil))"""), + ("(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))"""), + ("(= 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)))"""), + ("(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))"""), + ("(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))"""), + ("(and (= t_op 8n) (= tau_op 3n))", """(let ((alpha (arg1 term)) + (beta (arg2 term))) + (if (check env alpha tau) + (check env beta tau) + nil))"""), + ("(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))"""), + ("(= t_op 3n)", "(if (= (arg1 term) 1) nil (cumeq (get-dbtype term) tau))") + ] + check_fallback = "(cumeq (get-dbtype term) tau)" + out.append(f"!(defrec check (lambda (env term tau) (let ((t_op (car term)) (tau_op (car tau))) {make_if_chain(check_conds, check_fallback)})))") + + out.append("!(def check_pair (lambda (term tau) (if (check nil tau '(3n 1)) (check nil term tau) nil)))") + + with open("/6.5610-project/dependent.lurk", "w") as f: + f.write("\n\n".join(out)) + + test_lurk = ['!(load "dependent.lurk")'] + proofs_dir = "/6.5610-project/proofs" + proofs = sorted(os.listdir(proofs_dir)) + for proof in proofs: + if proof == "mul_comm": + continue + filepath = os.path.join(proofs_dir, proof) + with open(filepath, 'r') as f: + content = f.read().strip() + test_lurk.append(f"!(def {proof} {content})") + test_lurk.append(f"!(assert (check_pair (car {proof}) (cdr {proof})))") + + with open("/6.5610-project/test.lurk", "w") as f: + f.write("\n".join(test_lurk)) + + print("Generated safely!")
slop/proof (new)
slop/proof.lurk (new)
- @@ -0,0 +1,7 @@
  + !(defq add_zero_eq_zero_add_protocol_loaded !(load-expr "protocol")) + + !(def add_zero_eq_zero_add_solution '(1n (2n (1n (2n (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 (12n (0n 0) (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)) (3n 0)) (4n (15n) (3n 0))) (4n (2n (1n (12n (0n 0) (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)) (3n 0)) (4n (15n) (3n 0)) (16n) (15n)) (4n (4n (15n) (4n (2n (1n (12n (0n 0) (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)) (3n 0)) (4n (15n) (3n 0)) (0n 0) (15n)) (2n (1n (12n (0n 0) (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)) (3n 0)) (4n (15n) (3n 0)) (2n (17n) (4n (15n) (15n)) (0n 1) (15n)) (15n)))) (4n (15n) (2n (1n (12n (0n 0) (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)) (3n 0)) (4n (15n) (3n 0)) (0n 0) (15n))))) (2n (2n (13n) (4n (3n 0) (4n (0n 0) (12n (0n 0) (0n 0) (0n 1)))) (15n) (3n 0)) (4n (15n) (12n (0n 0) (0n 0) (15n))) (16n) (15n)) (2n (1n (12n (0n 0) (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)) (3n 0)) (4n (15n) (3n 0)) (16n) (15n))) (4n (4n (15n) (4n (2n (1n (12n (0n 0) (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)) (3n 0)) (4n (15n) (3n 0)) (0n 0) (15n)) (2n (1n (12n (0n 0) (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)) (3n 0)) (4n (15n) (3n 0)) (2n (17n) (4n (15n) (15n)) (0n 1) (15n)) (15n)))) (4n (15n) (2n (1n (12n (0n 0) (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)) (3n 0)) (4n (15n) (3n 0)) (0n 0) (15n)))) (1n (1n (2n (2n (2n (2n (2n (2n (1n (1n (1n (1n (1n (1n (2n (2n (2n (2n (2n (2n (14n) (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))))))))) (0n 5) (3n 0)) (4n (0n 5) (4n (4n (0n 6) (4n (12n (0n 1) (0n 0) (0n 7)) (3n 0))) (4n (2n (2n (0n 0) (4n (0n 7) (4n (12n (0n 2) (0n 0) (0n 8)) (3n 0))) (0n 1) (0n 7)) (4n (12n (0n 1) (0n 1) (0n 7)) (3n 0)) (2n (2n (13n) (4n (3n 0) (4n (0n 0) (12n (0n 0) (0n 0) (0n 1)))) (0n 7) (3n 0)) (4n (0n 7) (12n (0n 0) (0n 0) (0n 8))) (0n 1) (0n 7)) (12n (0n 1) (0n 1) (0n 7))) (4n (0n 8) (4n (12n (0n 3) (0n 0) (0n 9)) (2n (2n (0n 3) (4n (0n 10) (4n (12n (0n 5) (0n 0) (0n 11)) (3n 0))) (0n 1) (0n 10)) (4n (12n (0n 4) (0n 1) (0n 10)) (3n 0)) (0n 0) (12n (0n 4) (0n 1) (0n 10)))))))) (0n 4) (0n 5)) (4n (4n (0n 5) (4n (12n (0n 5) (0n 0) (0n 6)) (3n 0))) (4n (2n (2n (0n 0) (4n (0n 6) (4n (12n (0n 6) (0n 0) (0n 7)) (3n 0))) (0n 5) (0n 6)) (4n (12n (0n 5) (0n 5) (0n 6)) (3n 0)) (2n (2n (13n) (4n (3n 0) (4n (0n 0) (12n (0n 0) (0n 0) (0n 1)))) (0n 6) (3n 0)) (4n (0n 6) (12n (0n 0) (0n 0) (0n 7))) (0n 5) (0n 6)) (12n (0n 5) (0n 5) (0n 6))) (4n (0n 7) (4n (12n (0n 7) (0n 0) (0n 8)) (2n (2n (0n 3) (4n (0n 9) (4n (12n (0n 9) (0n 0) (0n 10)) (3n 0))) (0n 1) (0n 9)) (4n (12n (0n 8) (0n 1) (0n 9)) (3n 0)) (0n 0) (12n (0n 8) (0n 1) (0n 9))))))) (1n (1n (2n (0n 4) (4n (0n 7) (3n 0)) (0n 1) (0n 7)) (3n 0)) (4n (12n (0n 5) (0n 0) (0n 6)) (3n 0))) (4n (0n 5) (4n (12n (0n 5) (0n 0) (0n 6)) (3n 0)))) (4n (2n (2n (1n (1n (2n (0n 4) (4n (0n 7) (3n 0)) (0n 1) (0n 7)) (3n 0)) (4n (12n (0n 5) (0n 0) (0n 6)) (3n 0))) (4n (0n 5) (4n (12n (0n 5) (0n 0) (0n 6)) (3n 0))) (0n 4) (0n 5)) (4n (12n (0n 4) (0n 4) (0n 5)) (3n 0)) (2n (2n (13n) (4n (3n 0) (4n (0n 0) (12n (0n 0) (0n 0) (0n 1)))) (0n 5) (3n 0)) (4n (0n 5) (12n (0n 0) (0n 0) (0n 6))) (0n 4) (0n 5)) (12n (0n 4) (0n 4) (0n 5))) (4n (0n 6) (4n (12n (0n 6) (0n 0) (0n 7)) (2n (2n (1n (1n (2n (0n 7) (4n (0n 10) (3n 0)) (0n 1) (0n 10)) (3n 0)) (4n (12n (0n 8) (0n 0) (0n 9)) (3n 0))) (4n (0n 8) (4n (12n (0n 8) (0n 0) (0n 9)) (3n 0))) (0n 1) (0n 8)) (4n (12n (0n 7) (0n 1) (0n 8)) (3n 0)) (0n 0) (12n (0n 7) (0n 1) (0n 8)))))) (0n 0) (2n (2n (1n (1n (2n (0n 4) (4n (0n 7) (3n 0)) (0n 1) (0n 7)) (3n 0)) (4n (12n (0n 5) (0n 0) (0n 6)) (3n 0))) (4n (0n 5) (4n (12n (0n 5) (0n 0) (0n 6)) (3n 0))) (0n 4) (0n 5)) (4n (12n (0n 4) (0n 4) (0n 5)) (3n 0)) (2n (2n (13n) (4n (3n 0) (4n (0n 0) (12n (0n 0) (0n 0) (0n 1)))) (0n 5) (3n 0)) (4n (0n 5) (12n (0n 0) (0n 0) (0n 6))) (0n 4) (0n 5)) (12n (0n 4) (0n 4) (0n 5)))) (4n (0n 5) (4n (12n (0n 5) (0n 0) (0n 6)) (2n (2n (1n (1n (2n (0n 6) (4n (0n 9) (3n 0)) (0n 1) (0n 9)) (3n 0)) (4n (12n (0n 7) (0n 0) (0n 8)) (3n 0))) (4n (0n 7) (4n (12n (0n 7) (0n 0) (0n 8)) (3n 0))) (0n 1) (0n 7)) (4n (12n (0n 6) (0n 1) (0n 7)) (3n 0)) (0n 0) (12n (0n 6) (0n 1) (0n 7))))) (0n 3) (0n 5)) (4n (12n (0n 4) (0n 3) (0n 5)) (2n (2n (1n (1n (2n (0n 5) (4n (0n 8) (3n 0)) (0n 1) (0n 8)) (3n 0)) (4n (12n (0n 6) (0n 0) (0n 7)) (3n 0))) (4n (0n 6) (4n (12n (0n 6) (0n 0) (0n 7)) (3n 0))) (0n 4) (0n 6)) (4n (12n (0n 5) (0n 4) (0n 6)) (3n 0)) (0n 0) (12n (0n 5) (0n 4) (0n 6)))) (0n 1) (12n (0n 4) (0n 3) (0n 5))) (2n (0n 2) (4n (0n 5) (3n 0)) (0n 3) (0n 5))) (4n (2n (0n 1) (4n (0n 4) (3n 0)) (0n 3) (0n 4)) (2n (0n 2) (4n (0n 5) (3n 0)) (0n 3) (0n 5)))) (4n (12n (0n 2) (0n 1) (0n 3)) (4n (2n (0n 1) (4n (0n 4) (3n 0)) (0n 3) (0n 4)) (2n (0n 2) (4n (0n 5) (3n 0)) (0n 3) (0n 5))))) (4n (4n (0n 2) (3n 0)) (4n (12n (0n 2) (0n 1) (0n 3)) (4n (2n (0n 1) (4n (0n 4) (3n 0)) (0n 3) (0n 4)) (2n (0n 2) (4n (0n 5) (3n 0)) (0n 3) (0n 5)))))) (4n (0n 1) (4n (4n (0n 2) (3n 0)) (4n (12n (0n 2) (0n 1) (0n 3)) (4n (2n (0n 1) (4n (0n 4) (3n 0)) (0n 3) (0n 4)) (2n (0n 2) (4n (0n 5) (3n 0)) (0n 3) (0n 5))))))) (4n (0n 0) (4n (0n 1) (4n (4n (0n 2) (3n 0)) (4n (12n (0n 2) (0n 1) (0n 3)) (4n (2n (0n 1) (4n (0n 4) (3n 0)) (0n 3) (0n 4)) (2n (0n 2) (4n (0n 5) (3n 0)) (0n 3) (0n 5)))))))) (4n (3n 0) (4n (0n 0) (4n (0n 1) (4n (4n (0n 2) (3n 0)) (4n (12n (0n 2) (0n 1) (0n 3)) (4n (2n (0n 1) (4n (0n 4) (3n 0)) (0n 3) (0n 4)) (2n (0n 2) (4n (0n 5) (3n 0)) (0n 3) (0n 5)))))))) (15n) (3n 0)) (4n (15n) (4n (15n) (4n (4n (15n) (3n 0)) (4n (12n (0n 2) (0n 1) (15n)) (4n (2n (0n 1) (4n (15n) (3n 0)) (0n 3) (15n)) (2n (0n 2) (4n (15n) (3n 0)) (0n 3) (15n))))))) (0n 1) (15n)) (4n (15n) (4n (4n (15n) (3n 0)) (4n (12n (0n 3) (0n 1) (15n)) (4n (2n (0n 1) (4n (15n) (3n 0)) (0n 4) (15n)) (2n (0n 2) (4n (15n) (3n 0)) (0n 3) (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 1) (15n)) (15n)) (4n (4n (15n) (3n 0)) (4n (12n (0n 2) (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 2) (15n)) (15n)) (4n (2n (0n 1) (4n (15n) (3n 0)) (0n 3) (15n)) (2n (0n 2) (4n (15n) (3n 0)) (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 4) (15n)) (15n))))) (1n (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 2) (15n)) (4n (15n) (15n)) (2n (17n) (4n (15n) (15n)) (16n) (15n)) (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))) (0n 0) (15n)) (4n (15n) (15n)) (2n (17n) (4n (15n) (15n)) (16n) (15n)) (15n)) (15n)) (3n 0)) (4n (15n) (3n 0))) (4n (12n (0n 1) (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 1) (15n)) (15n)) (4n (2n (1n (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 3) (15n)) (4n (15n) (15n)) (2n (17n) (4n (15n) (15n)) (16n) (15n)) (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))) (0n 0) (15n)) (4n (15n) (15n)) (2n (17n) (4n (15n) (15n)) (16n) (15n)) (15n)) (15n)) (3n 0)) (4n (15n) (3n 0)) (0n 2) (15n)) (2n (1n (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 4) (15n)) (4n (15n) (15n)) (2n (17n) (4n (15n) (15n)) (16n) (15n)) (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))) (0n 0) (15n)) (4n (15n) (15n)) (2n (17n) (4n (15n) (15n)) (16n) (15n)) (15n)) (15n)) (3n 0)) (4n (15n) (3n 0)) (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 3) (15n)) (15n)))) (0n 0) (12n (0n 1) (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 1) (15n)) (15n))) (4n (2n (1n (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 2) (15n)) (4n (15n) (15n)) (2n (17n) (4n (15n) (15n)) (16n) (15n)) (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))) (0n 0) (15n)) (4n (15n) (15n)) (2n (17n) (4n (15n) (15n)) (16n) (15n)) (15n)) (15n)) (3n 0)) (4n (15n) (3n 0)) (0n 1) (15n)) (2n (1n (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 3) (15n)) (4n (15n) (15n)) (2n (17n) (4n (15n) (15n)) (16n) (15n)) (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))) (0n 0) (15n)) (4n (15n) (15n)) (2n (17n) (4n (15n) (15n)) (16n) (15n)) (15n)) (15n)) (3n 0)) (4n (15n) (3n 0)) (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 2) (15n)) (15n))) (2n (2n (13n) (4n (3n 0) (4n (0n 0) (12n (0n 0) (0n 0) (0n 1)))) (15n) (3n 0)) (4n (15n) (12n (0n 0) (0n 0) (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))) (0n 1) (15n)) (4n (15n) (15n)) (2n (17n) (4n (15n) (15n)) (16n) (15n)) (15n)) (15n)) (2n (1n (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 2) (15n)) (4n (15n) (15n)) (2n (17n) (4n (15n) (15n)) (16n) (15n)) (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))) (0n 0) (15n)) (4n (15n) (15n)) (2n (17n) (4n (15n) (15n)) (16n) (15n)) (15n)) (15n)) (3n 0)) (4n (15n) (3n 0)) (0n 1) (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 1) (15n)) (4n (15n) (15n)) (2n (17n) (4n (15n) (15n)) (16n) (15n)) (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)) (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 1) (15n)) (4n (15n) (15n)) (2n (17n) (4n (15n) (15n)) (16n) (15n)) (15n)) (15n)) (15n))) (4n (12n (0n 0) (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)) (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 1) (15n)) (4n (15n) (15n)) (2n (17n) (4n (15n) (15n)) (16n) (15n)) (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)) (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 1) (15n)) (4n (15n) (15n)) (2n (17n) (4n (15n) (15n)) (16n) (15n)) (15n)) (15n)) (15n)))) (4n (15n) (4n (2n (1n (12n (0n 0) (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)) (3n 0)) (4n (15n) (3n 0)) (0n 0) (15n)) (2n (1n (12n (0n 0) (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)) (3n 0)) (4n (15n) (3n 0)) (2n (17n) (4n (15n) (15n)) (0n 1) (15n)) (15n))))) (4n (15n) (2n (1n (12n (0n 0) (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)) (3n 0)) (4n (15n) (3n 0)) (0n 0) (15n))) (0n 0) (15n)) (12n (0n 0) (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))) (4n (15n) (12n (0n 0) (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))) (0n 0) (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)))) + + !(def comm_term_test (hide #0x2903850943570 add_zero_eq_zero_add_solution)) + + !(prove-protocol add_zero_eq_zero_add_protocol_loaded "proof" comm_term_test)
slop/protocol (new)
slop/protocol.lurk (new)
- @@ -0,0 +1,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")
slop/typechecker.py (new)
- @@ -0,0 +1,365 @@
  + import sys + + from dataclasses import dataclass + from typing import Any + + @dataclass(frozen=True) + class Term: + pass + + @dataclass(frozen=True) + class Var(Term): + x: int + + @dataclass(frozen=True) + class Lam(Term): + b: Term + beta: Term + + @dataclass(frozen=True) + class App(Term): + f: Term + phi: Term + a: Term + alpha: Term + + @dataclass(frozen=True) + class Typ(Term): + u: int + + @dataclass(frozen=True) + class Fn(Term): + alpha: Term + beta: Term + + @dataclass(frozen=True) + class Prod(Term): + alpha: Term + beta: Term + + @dataclass(frozen=True) + class Pmk(Term): + pass + + @dataclass(frozen=True) + class ProdRec(Term): + pass + + @dataclass(frozen=True) + class Sum(Term): + alpha: Term + beta: Term + + @dataclass(frozen=True) + class Inl(Term): + pass + + @dataclass(frozen=True) + class Inr(Term): + pass + + @dataclass(frozen=True) + class SumRec(Term): + pass + + @dataclass(frozen=True) + class Eq(Term): + a: Term + a_prime: Term + alpha: Term + + @dataclass(frozen=True) + class Refl(Term): + pass + + @dataclass(frozen=True) + class EqRec(Term): + pass + + @dataclass(frozen=True) + class Nat(Term): + pass + + @dataclass(frozen=True) + class Zero(Term): + pass + + @dataclass(frozen=True) + class Succ(Term): + pass + + @dataclass(frozen=True) + class NatRec(Term): + pass + + @dataclass(frozen=True) + class Unit(Term): + pass + + @dataclass(frozen=True) + class Intro(Term): + pass + + @dataclass(frozen=True) + class Fls(Term): + pass + + @dataclass(frozen=True) + class FlsRec(Term): + pass + + def parse_sexp(s: str) -> Term: + s = s.replace("(", " ( ").replace(")", " ) ") + tokens = s.split() + + def parse_tokens(tokens, idx): + token = tokens[idx] + if token == "(": + idx += 1 + args = [] + while tokens[idx] != ")": + arg, idx = parse_tokens(tokens, idx) + args.append(arg) + idx += 1 + return args, idx + else: + return token, idx + 1 + + ast, _ = parse_tokens(tokens, 0) + + def build_term(ast) -> Term: + if not isinstance(ast, list): + return ast + op = ast[0] + if op == "0n": return Var(int(ast[1])) + elif op == "1n": return Lam(build_term(ast[1]), build_term(ast[2])) + elif op == "2n": return App(build_term(ast[1]), build_term(ast[2]), build_term(ast[3]), build_term(ast[4])) + elif op == "3n": return Typ(int(ast[1])) + elif op == "4n": return Fn(build_term(ast[1]), build_term(ast[2])) + elif op == "5n": return Prod(build_term(ast[1]), build_term(ast[2])) + elif op == "6n": return Pmk() + elif op == "7n": return ProdRec() + elif op == "8n": return Sum(build_term(ast[1]), build_term(ast[2])) + elif op == "9n": return Inl() + elif op == "10n": return Inr() + elif op == "11n": return SumRec() + elif op == "12n": return Eq(build_term(ast[1]), build_term(ast[2]), build_term(ast[3])) + elif op == "13n": return Refl() + elif op == "14n": return EqRec() + elif op == "15n": return Nat() + elif op == "16n": return Zero() + elif op == "17n": return Succ() + elif op == "18n": return NatRec() + elif op == "19n": return Unit() + elif op == "20n": return Intro() + elif op == "21n": return Fls() + elif op == "22n": return FlsRec() + else: + raise ValueError(f"Unknown op: {op}") + + return build_term(ast) + + dbtypes_strs = [ + "(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))))" + ] + + dbtypes = [parse_sexp(s) for s in dbtypes_strs] + + def get_dbtype(t: Term) -> Term: + match t: + case Typ(0): return dbtypes[0] + case Pmk(): return dbtypes[1] + case ProdRec(): return dbtypes[2] + case Inl(): return dbtypes[3] + case Inr(): return dbtypes[4] + case SumRec(): return dbtypes[5] + case Refl(): return dbtypes[6] + case EqRec(): return dbtypes[7] + case Nat(): return dbtypes[8] + case Zero(): return dbtypes[9] + case Succ(): return dbtypes[10] + case NatRec(): return dbtypes[11] + case Unit(): return dbtypes[12] + case Intro(): return dbtypes[13] + case Fls(): return dbtypes[14] + case FlsRec(): return dbtypes[15] + case _: return t + + def term_rec(t: Term, s: Any, fdep, fvar) -> Term: + def g(s, term): + match term: + case Var(x): return fvar(s, x) + case Lam(b, beta): return Lam(g(fdep(s), b), g(fdep(s), beta)) + case App(f, phi, a, alpha): return App(g(s, f), g(s, phi), g(s, a), g(s, alpha)) + case Fn(alpha, beta): return Fn(g(s, alpha), g(fdep(s), beta)) + case Prod(alpha, beta): return Prod(g(s, alpha), g(s, beta)) + case Sum(alpha, beta): return Sum(g(s, alpha), g(s, beta)) + case Eq(a, a_prime, alpha): return Eq(g(s, a), g(s, a_prime), g(s, alpha)) + case _: return term + return g(s, t) + + def incr(t: Term) -> Term: + return term_rec(t, 0, lambda d: d + 1, lambda d, x: Var(x + 1 if d <= x else x)) + + def sub(t: Term, t_prime: Term) -> Term: + def fdep(s): + d, tp = s + return (d + 1, incr(tp)) + def fvar(s, x): + d, tp = s + if x == d: + return tp + else: + return Var(x - 1 if d < x else x) + return term_rec(t, (0, t_prime), fdep, fvar) + + def evaluate(t: Term) -> Term: + match t: + case Lam(b, beta): + return Lam(evaluate(b), evaluate(beta)) + case App(f, phi, a, alpha): + f_prime = evaluate(f) + a_prime = evaluate(a) + match f_prime, a_prime: + case Lam(b, _), ap: + return evaluate(sub(b, ap)) + case App(App(App(App(ProdRec(), _, _, _), _, _, _), _, _, _), _, g, Fn(alpha_val, gamma)), \ + App(App(App(App(Pmk(), _, _, _), _, _, _), _, a_val, _), _, b, beta): + return evaluate(App(App(g, Fn(alpha_val, gamma), a_val, alpha_val), sub(gamma, a_val), b, beta)) + case App(App(App(App(App(SumRec(), _, _, _), _, _, _), _, _, _), _, g, gamma), _, _, _), \ + App(App(App(Inl(), _, _, _), _, _, _), _, a_val, alpha_val): + return evaluate(App(g, gamma, a_val, alpha_val)) + case App(App(App(App(App(SumRec(), _, _, _), _, _, _), _, _, _), _, _, _), _, g, gamma), \ + App(App(App(Inr(), _, _, _), _, _, _), _, b_val, beta_val): + return evaluate(App(g, gamma, b_val, beta_val)) + case App(App(App(App(App(EqRec(), _, _, _), _, _, _), _, _, _), _, ha, _), _, _, _), \ + App(App(Refl(), _, _, _), _, _, _): + return evaluate(ha) + case App(App(App(NatRec(), _, _, _), _, z, _), _, _, _), Zero(): + return evaluate(z) + case App(App(App(NatRec(), _, m, _), _, _, _), _, g, Fn(Nat(), gamma)), \ + App(Succ(), Fn(Nat(), Nat()), n, Nat()): + return evaluate(App(App(g, Fn(Nat(), gamma), n, Nat()), sub(gamma, n), App(f_prime, phi, n, Nat()), App(m, Fn(Nat(), Typ(0)), n, Nat()))) + case x, ap: + return App(x, evaluate(phi), ap, evaluate(alpha)) + case Fn(alpha, beta): + return Fn(evaluate(alpha), evaluate(beta)) + case Prod(alpha, beta): + return Prod(evaluate(alpha), evaluate(beta)) + case Sum(alpha, beta): + return Sum(evaluate(alpha), evaluate(beta)) + case Eq(a, a_prime, alpha): + return Eq(evaluate(a), evaluate(a_prime), evaluate(alpha)) + case _: + return t + return t # needed? No, the match is exhaustive theoretically but Python needs it + + def cumeq(a: Term, a_prime: Term) -> bool: + return (a == Typ(0) and a_prime == Typ(1)) or a == evaluate(a_prime) + + def check(env: list[Term], t: Term, tau: Term) -> bool: + match t, tau: + case Var(x), alpha: + if x < len(env): + return cumeq(evaluate(env[x]), alpha) + return False + case Lam(b, beta), Fn(alpha, beta_prime): + new_env = [incr(e) for e in [alpha] + env] + return check(new_env, b, beta) and evaluate(beta) == evaluate(beta_prime) + case App(f, Fn(alpha, beta), a, alpha_prime), beta_prime: + return (check(env, f, Fn(alpha, beta)) and check(env, a, alpha) and + evaluate(alpha) == evaluate(alpha_prime) and cumeq(evaluate(sub(beta, a)), beta_prime)) + case Fn(alpha, beta), Typ(u): + new_env = [incr(e) for e in [alpha] + env] + return check(env, alpha, Typ(u)) and check(new_env, beta, Typ(u)) + case Prod(alpha, beta), Typ(u): + return check(env, alpha, Typ(u)) and check(env, beta, Fn(alpha, Typ(0))) + case Sum(alpha, beta), Typ(u): + return check(env, alpha, Typ(u)) and check(env, beta, Typ(u)) + case Eq(a, a_prime, alpha), Typ(u): + return check(env, a, alpha) and check(env, a_prime, alpha) and check(env, alpha, Typ(u)) + case Typ(1), _: + return False + case t_val, tau_val: + return cumeq(get_dbtype(t_val), tau_val) + return False + + def check_pair(t: Term, tau: Term) -> bool: + return check([], tau, Typ(1)) and check([], t, tau) + + if __name__ == "__main__": + # Test basic checks + assert check([], get_dbtype(Pmk()), Typ(1)), "Pmk btype mismatch" + assert check([], get_dbtype(ProdRec()), Typ(1)), "ProdRec btype mismatch" + assert check([], get_dbtype(Inl()), Typ(1)), "Inl btype mismatch" + assert check([], get_dbtype(Inr()), Typ(1)), "Inr btype mismatch" + assert check([], get_dbtype(SumRec()), Typ(1)), "SumRec btype mismatch" + assert check([], get_dbtype(Refl()), Typ(1)), "Refl btype mismatch" + assert check([], get_dbtype(EqRec()), Typ(1)), "EqRec btype mismatch" + assert check([], get_dbtype(NatRec()), Typ(1)), "NatRec btype mismatch" + assert check([], get_dbtype(FlsRec()), Typ(1)), "FlsRec btype mismatch" + assert not check([], Typ(1), Typ(1)), "Typ(1) Typ(1) shouldn't pass" + print("Self test passed!") + + import os + proofs_dir = "proofs" + if os.path.isdir(proofs_dir): + passed = 0 + failed = 0 + for filename in sorted(os.listdir(proofs_dir)): + filepath = os.path.join(proofs_dir, filename) + with open(filepath, 'r') as f: + content = f.read().strip() + + if content.startswith("'("): + content = content[2:-1] + + depth = 0 + split_idx = -1 + for i, c in enumerate(content): + if c == '(': depth += 1 + elif c == ')': depth -= 1 + elif c == '.' and depth == 0: + # found the root dot + split_idx = i + break + + if split_idx == -1: + print(f"Failed to parse {filename}") + failed += 1 + continue + + t_str = content[:split_idx].strip() + tau_str = content[split_idx+1:].strip() + + try: + t = parse_sexp(t_str) + tau = parse_sexp(tau_str) + + if check_pair(t, tau): + print(f"Proof {filename} PASSED") + passed += 1 + else: + print(f"Proof {filename} FAILED") + failed += 1 + except Exception as e: + print(f"Exception on {filename}: {e}") + failed += 1 + + print(f"Results: {passed} passed, {failed} failed.") + assert failed == 0, "Some proofs failed to typecheck"
slop/verify.lurk (new)
- @@ -0,0 +1,3 @@
  + !(defq add_zero_eq_zero_add_protocol_loaded !(load-expr "protocol")) + !(inspect "3202a919bbdd68edac66b8ea53dd0c4c0ef86d00774b74b8a0dfcef7cd416f") + !(verify-protocol add_zero_eq_zero_add_protocol_loaded "proof")