Skip to content

Instantly share code, notes, and snippets.

@tizoc

tizoc/0-prenex.shen

Last active September 23, 2019 19:27
Show Gist options
  • Save tizoc/7076846b7e727fb2a534733ee26e8bbe to your computer and use it in GitHub Desktop.
Save tizoc/7076846b7e727fb2a534733ee26e8bbe to your computer and use it in GitHub Desktop.
Download ZIP
Raw
0-prenex.shen
(define prenex*
{wff --> wff}
[~ [all X P]] -> [exists X [~ P]]
[~ [exists X P]] -> [all X [~ P]]
[[all X P] & Q] -> [all X [P & Q]]
[[exists X P] & Q] -> [exists X [P & Q]]
[P & [all X Q]] -> [all X [P & Q]]
[P & [exists X Q]] -> [exists X [P & Q]]
[[all X P] v Q] -> [all X [P v Q]]
[[exists X P] v Q] -> [exists X [P v Q]]
[P v [all X Q]] -> [all X [P v Q]]
[P v [exists X Q]] -> [exists X [P v Q]]
[P => Q] -> [[~ P] v Q]
[P <=> Q] -> (rectify [[P => Q] & [Q => P]])
[P v [Q & R]] -> (rectify [[P v Q] & [P v R]])
[[Q & R] v P] -> (rectify [[P v Q] & [P v R]])
[~ [P & Q]] -> [[~ P] v [~ Q]]
[~ [P v Q]] -> [[~ P] & [~ Q]]
[~ [~ P]] -> P
[P v Q] -> [(prenex* P) v (prenex* Q)]
[P & Q] -> [(prenex* P) & (prenex* Q)]
[~ P] -> [~ (prenex* P)]
[all X P] -> [all X (prenex* P)]
[exists X P] -> [exists X (prenex* P)]
P -> P)
Raw
1-prenex.kl
(defun prenex* (V1178)
(cond
[(and (cons? V1178)
(and (= ~ (hd V1178))
(and (cons? (tl V1178))
(and (cons? (hd (tl V1178)))
(and (= all (hd (hd (tl V1178))))
(and (cons? (tl (hd (tl V1178))))
(and (cons? (tl (tl (hd (tl V1178)))))
(and (= ()
(tl (tl (tl (hd (tl V1178))))))
(= () (tl (tl V1178)))))))))))
(cons
exists
(cons
(hd (tl (hd (tl V1178))))
(cons (cons ~ (tl (tl (hd (tl V1178))))) ())))]
[(and (cons? V1178)
(and (= ~ (hd V1178))
(and (cons? (tl V1178))
(and (cons? (hd (tl V1178)))
(and (= exists (hd (hd (tl V1178))))
(and (cons? (tl (hd (tl V1178))))
(and (cons? (tl (tl (hd (tl V1178)))))
(and (= ()
(tl (tl (tl (hd (tl V1178))))))
(= () (tl (tl V1178)))))))))))
(cons
all
(cons
(hd (tl (hd (tl V1178))))
(cons (cons ~ (tl (tl (hd (tl V1178))))) ())))]
[(and (cons? V1178)
(and (cons? (hd V1178))
(and (= all (hd (hd V1178)))
(and (cons? (tl (hd V1178)))
(and (cons? (tl (tl (hd V1178))))
(and (= () (tl (tl (tl (hd V1178)))))
(and (cons? (tl V1178))
(and (= & (hd (tl V1178)))
(and (cons? (tl (tl V1178)))
(= ()
(tl (tl (tl V1178)))))))))))))
(cons
all
(cons
(hd (tl (hd V1178)))
(cons (cons (hd (tl (tl (hd V1178)))) (tl V1178)) ())))]
[(and (cons? V1178)
(and (cons? (hd V1178))
(and (= exists (hd (hd V1178)))
(and (cons? (tl (hd V1178)))
(and (cons? (tl (tl (hd V1178))))
(and (= () (tl (tl (tl (hd V1178)))))
(and (cons? (tl V1178))
(and (= & (hd (tl V1178)))
(and (cons? (tl (tl V1178)))
(= ()
(tl (tl (tl V1178)))))))))))))
(cons
exists
(cons
(hd (tl (hd V1178)))
(cons (cons (hd (tl (tl (hd V1178)))) (tl V1178)) ())))]
[(and (cons? V1178)
(and (cons? (tl V1178))
(and (= & (hd (tl V1178)))
(and (cons? (tl (tl V1178)))
(and (cons? (hd (tl (tl V1178))))
(and (= all (hd (hd (tl (tl V1178)))))
(and (cons? (tl (hd (tl (tl V1178)))))
(and (cons?
(tl (tl (hd (tl (tl V1178))))))
(and (= ()
(tl (tl (tl (hd (tl (tl V1178)))))))
(= ()
(tl (tl (tl V1178)))))))))))))
(cons
all
(cons
(hd (tl (hd (tl (tl V1178)))))
(cons
(cons (hd V1178) (cons & (tl (tl (hd (tl (tl V1178)))))))
())))]
[(and (cons? V1178)
(and (cons? (tl V1178))
(and (= & (hd (tl V1178)))
(and (cons? (tl (tl V1178)))
(and (cons? (hd (tl (tl V1178))))
(and (= exists (hd (hd (tl (tl V1178)))))
(and (cons? (tl (hd (tl (tl V1178)))))
(and (cons?
(tl (tl (hd (tl (tl V1178))))))
(and (= ()
(tl (tl (tl (hd (tl (tl V1178)))))))
(= ()
(tl (tl (tl V1178)))))))))))))
(cons
exists
(cons
(hd (tl (hd (tl (tl V1178)))))
(cons
(cons (hd V1178) (cons & (tl (tl (hd (tl (tl V1178)))))))
())))]
[(and (cons? V1178)
(and (cons? (hd V1178))
(and (= all (hd (hd V1178)))
(and (cons? (tl (hd V1178)))
(and (cons? (tl (tl (hd V1178))))
(and (= () (tl (tl (tl (hd V1178)))))
(and (cons? (tl V1178))
(and (= v (hd (tl V1178)))
(and (cons? (tl (tl V1178)))
(= ()
(tl (tl (tl V1178)))))))))))))
(cons
all
(cons
(hd (tl (hd V1178)))
(cons (cons (hd (tl (tl (hd V1178)))) (tl V1178)) ())))]
[(and (cons? V1178)
(and (cons? (hd V1178))
(and (= exists (hd (hd V1178)))
(and (cons? (tl (hd V1178)))
(and (cons? (tl (tl (hd V1178))))
(and (= () (tl (tl (tl (hd V1178)))))
(and (cons? (tl V1178))
(and (= v (hd (tl V1178)))
(and (cons? (tl (tl V1178)))
(= ()
(tl (tl (tl V1178)))))))))))))
(cons
exists
(cons
(hd (tl (hd V1178)))
(cons (cons (hd (tl (tl (hd V1178)))) (tl V1178)) ())))]
[(and (cons? V1178)
(and (cons? (tl V1178))
(and (= v (hd (tl V1178)))
(and (cons? (tl (tl V1178)))
(and (cons? (hd (tl (tl V1178))))
(and (= all (hd (hd (tl (tl V1178)))))
(and (cons? (tl (hd (tl (tl V1178)))))
(and (cons?
(tl (tl (hd (tl (tl V1178))))))
(and (= ()
(tl (tl (tl (hd (tl (tl V1178)))))))
(= ()
(tl (tl (tl V1178)))))))))))))
(cons
all
(cons
(hd (tl (hd (tl (tl V1178)))))
(cons
(cons (hd V1178) (cons v (tl (tl (hd (tl (tl V1178)))))))
())))]
[(and (cons? V1178)
(and (cons? (tl V1178))
(and (= v (hd (tl V1178)))
(and (cons? (tl (tl V1178)))
(and (cons? (hd (tl (tl V1178))))
(and (= exists (hd (hd (tl (tl V1178)))))
(and (cons? (tl (hd (tl (tl V1178)))))
(and (cons?
(tl (tl (hd (tl (tl V1178))))))
(and (= ()
(tl (tl (tl (hd (tl (tl V1178)))))))
(= ()
(tl (tl (tl V1178)))))))))))))
(cons
exists
(cons
(hd (tl (hd (tl (tl V1178)))))
(cons
(cons (hd V1178) (cons v (tl (tl (hd (tl (tl V1178)))))))
())))]
[(and (cons? V1178)
(and (cons? (tl V1178))
(and (= => (hd (tl V1178)))
(and (cons? (tl (tl V1178)))
(= () (tl (tl (tl V1178))))))))
(cons
(cons ~ (cons (hd V1178) ()))
(cons v (tl (tl V1178))))]
[(and (cons? V1178)
(and (cons? (tl V1178))
(and (= <=> (hd (tl V1178)))
(and (cons? (tl (tl V1178)))
(= () (tl (tl (tl V1178))))))))
(rectify
(cons
(cons (hd V1178) (cons => (tl (tl V1178))))
(cons
&
(cons
(cons (hd (tl (tl V1178))) (cons => (cons (hd V1178) ())))
()))))]
[(and (cons? V1178)
(and (cons? (tl V1178))
(and (= v (hd (tl V1178)))
(and (cons? (tl (tl V1178)))
(and (cons? (hd (tl (tl V1178))))
(and (cons? (tl (hd (tl (tl V1178)))))
(and (= &
(hd (tl (hd (tl (tl V1178))))))
(and (cons?
(tl (tl (hd (tl (tl V1178))))))
(and (= ()
(tl (tl (tl (hd (tl (tl V1178)))))))
(= ()
(tl (tl (tl V1178)))))))))))))
(rectify
(cons
(cons
(hd V1178)
(cons v (cons (hd (hd (tl (tl V1178)))) ())))
(cons
&
(cons
(cons (hd V1178) (cons v (tl (tl (hd (tl (tl V1178)))))))
()))))]
[(and (cons? V1178)
(and (cons? (hd V1178))
(and (cons? (tl (hd V1178)))
(and (= & (hd (tl (hd V1178))))
(and (cons? (tl (tl (hd V1178))))
(and (= () (tl (tl (tl (hd V1178)))))
(and (cons? (tl V1178))
(and (= v (hd (tl V1178)))
(and (cons? (tl (tl V1178)))
(= ()
(tl (tl (tl V1178)))))))))))))
(rectify
(cons
(cons
(hd (tl (tl V1178)))
(cons v (cons (hd (hd V1178)) ())))
(cons
&
(cons
(cons (hd (tl (tl V1178))) (cons v (tl (tl (hd V1178)))))
()))))]
[(and (cons? V1178)
(and (= ~ (hd V1178))
(and (cons? (tl V1178))
(and (cons? (hd (tl V1178)))
(and (cons? (tl (hd (tl V1178))))
(and (= & (hd (tl (hd (tl V1178)))))
(and (cons? (tl (tl (hd (tl V1178)))))
(and (= ()
(tl (tl (tl (hd (tl V1178))))))
(= () (tl (tl V1178)))))))))))
(cons
(cons ~ (cons (hd (hd (tl V1178))) ()))
(cons v (cons (cons ~ (tl (tl (hd (tl V1178))))) ())))]
[(and (cons? V1178)
(and (= ~ (hd V1178))
(and (cons? (tl V1178))
(and (cons? (hd (tl V1178)))
(and (cons? (tl (hd (tl V1178))))
(and (= v (hd (tl (hd (tl V1178)))))
(and (cons? (tl (tl (hd (tl V1178)))))
(and (= ()
(tl (tl (tl (hd (tl V1178))))))
(= () (tl (tl V1178)))))))))))
(cons
(cons ~ (cons (hd (hd (tl V1178))) ()))
(cons & (cons (cons ~ (tl (tl (hd (tl V1178))))) ())))]
[(and (cons? V1178)
(and (= ~ (hd V1178))
(and (cons? (tl V1178))
(and (cons? (hd (tl V1178)))
(and (= ~ (hd (hd (tl V1178))))
(and (cons? (tl (hd (tl V1178))))
(and (= () (tl (tl (hd (tl V1178)))))
(= () (tl (tl V1178))))))))))
(hd (tl (hd (tl V1178))))]
[(and (cons? V1178)
(and (cons? (tl V1178))
(and (= v (hd (tl V1178)))
(and (cons? (tl (tl V1178)))
(= () (tl (tl (tl V1178))))))))
(cons
(prenex* (hd V1178))
(cons v (cons (prenex* (hd (tl (tl V1178)))) ())))]
[(and (cons? V1178)
(and (cons? (tl V1178))
(and (= & (hd (tl V1178)))
(and (cons? (tl (tl V1178)))
(= () (tl (tl (tl V1178))))))))
(cons
(prenex* (hd V1178))
(cons & (cons (prenex* (hd (tl (tl V1178)))) ())))]
[(and (cons? V1178)
(and (= ~ (hd V1178))
(and (cons? (tl V1178)) (= () (tl (tl V1178))))))
(cons ~ (cons (prenex* (hd (tl V1178))) ()))]
[(and (cons? V1178)
(and (= all (hd V1178))
(and (cons? (tl V1178))
(and (cons? (tl (tl V1178)))
(= () (tl (tl (tl V1178))))))))
(cons
all
(cons
(hd (tl V1178))
(cons (prenex* (hd (tl (tl V1178)))) ())))]
[(and (cons? V1178)
(and (= exists (hd V1178))
(and (cons? (tl V1178))
(and (cons? (tl (tl V1178)))
(= () (tl (tl (tl V1178))))))))
(cons
exists
(cons
(hd (tl V1178))
(cons (prenex* (hd (tl (tl V1178)))) ())))]
[true V1178]))
Raw
2-prenex-unfactorized.scm
(define (kl:prenex* V1178)
(cond
[(and (pair? V1178)
(eq? '~ (car V1178))
(pair? (cdr V1178))
(pair? (car (cdr V1178)))
(eq? 'all (car (car (cdr V1178))))
(pair? (cdr (car (cdr V1178))))
(pair? (cdr (cdr (car (cdr V1178)))))
(null? (cdr (cdr (cdr (car (cdr V1178))))))
(null? (cdr (cdr V1178))))
(list
'exists
(car (cdr (car (cdr V1178))))
(cons '~ (cdr (cdr (car (cdr V1178))))))]
[(and (pair? V1178)
(eq? '~ (car V1178))
(pair? (cdr V1178))
(pair? (car (cdr V1178)))
(eq? 'exists (car (car (cdr V1178))))
(pair? (cdr (car (cdr V1178))))
(pair? (cdr (cdr (car (cdr V1178)))))
(null? (cdr (cdr (cdr (car (cdr V1178))))))
(null? (cdr (cdr V1178))))
(list
'all
(car (cdr (car (cdr V1178))))
(cons '~ (cdr (cdr (car (cdr V1178))))))]
[(and (pair? V1178)
(pair? (car V1178))
(eq? 'all (car (car V1178)))
(pair? (cdr (car V1178)))
(pair? (cdr (cdr (car V1178))))
(null? (cdr (cdr (cdr (car V1178)))))
(pair? (cdr V1178))
(eq? '& (car (cdr V1178)))
(pair? (cdr (cdr V1178)))
(null? (cdr (cdr (cdr V1178)))))
(list
'all
(car (cdr (car V1178)))
(cons (car (cdr (cdr (car V1178)))) (cdr V1178)))]
[(and (pair? V1178)
(pair? (car V1178))
(eq? 'exists (car (car V1178)))
(pair? (cdr (car V1178)))
(pair? (cdr (cdr (car V1178))))
(null? (cdr (cdr (cdr (car V1178)))))
(pair? (cdr V1178))
(eq? '& (car (cdr V1178)))
(pair? (cdr (cdr V1178)))
(null? (cdr (cdr (cdr V1178)))))
(list
'exists
(car (cdr (car V1178)))
(cons (car (cdr (cdr (car V1178)))) (cdr V1178)))]
[(and (pair? V1178)
(pair? (cdr V1178))
(eq? '& (car (cdr V1178)))
(pair? (cdr (cdr V1178)))
(pair? (car (cdr (cdr V1178))))
(eq? 'all (car (car (cdr (cdr V1178)))))
(pair? (cdr (car (cdr (cdr V1178)))))
(pair? (cdr (cdr (car (cdr (cdr V1178))))))
(null? (cdr (cdr (cdr (car (cdr (cdr V1178)))))))
(null? (cdr (cdr (cdr V1178)))))
(list
'all
(car (cdr (car (cdr (cdr V1178)))))
(cons
(car V1178)
(cons '& (cdr (cdr (car (cdr (cdr V1178))))))))]
[(and (pair? V1178)
(pair? (cdr V1178))
(eq? '& (car (cdr V1178)))
(pair? (cdr (cdr V1178)))
(pair? (car (cdr (cdr V1178))))
(eq? 'exists (car (car (cdr (cdr V1178)))))
(pair? (cdr (car (cdr (cdr V1178)))))
(pair? (cdr (cdr (car (cdr (cdr V1178))))))
(null? (cdr (cdr (cdr (car (cdr (cdr V1178)))))))
(null? (cdr (cdr (cdr V1178)))))
(list
'exists
(car (cdr (car (cdr (cdr V1178)))))
(cons
(car V1178)
(cons '& (cdr (cdr (car (cdr (cdr V1178))))))))]
[(and (pair? V1178)
(pair? (car V1178))
(eq? 'all (car (car V1178)))
(pair? (cdr (car V1178)))
(pair? (cdr (cdr (car V1178))))
(null? (cdr (cdr (cdr (car V1178)))))
(pair? (cdr V1178))
(eq? 'v (car (cdr V1178)))
(pair? (cdr (cdr V1178)))
(null? (cdr (cdr (cdr V1178)))))
(list
'all
(car (cdr (car V1178)))
(cons (car (cdr (cdr (car V1178)))) (cdr V1178)))]
[(and (pair? V1178)
(pair? (car V1178))
(eq? 'exists (car (car V1178)))
(pair? (cdr (car V1178)))
(pair? (cdr (cdr (car V1178))))
(null? (cdr (cdr (cdr (car V1178)))))
(pair? (cdr V1178))
(eq? 'v (car (cdr V1178)))
(pair? (cdr (cdr V1178)))
(null? (cdr (cdr (cdr V1178)))))
(list
'exists
(car (cdr (car V1178)))
(cons (car (cdr (cdr (car V1178)))) (cdr V1178)))]
[(and (pair? V1178)
(pair? (cdr V1178))
(eq? 'v (car (cdr V1178)))
(pair? (cdr (cdr V1178)))
(pair? (car (cdr (cdr V1178))))
(eq? 'all (car (car (cdr (cdr V1178)))))
(pair? (cdr (car (cdr (cdr V1178)))))
(pair? (cdr (cdr (car (cdr (cdr V1178))))))
(null? (cdr (cdr (cdr (car (cdr (cdr V1178)))))))
(null? (cdr (cdr (cdr V1178)))))
(list
'all
(car (cdr (car (cdr (cdr V1178)))))
(cons
(car V1178)
(cons 'v (cdr (cdr (car (cdr (cdr V1178))))))))]
[(and (pair? V1178)
(pair? (cdr V1178))
(eq? 'v (car (cdr V1178)))
(pair? (cdr (cdr V1178)))
(pair? (car (cdr (cdr V1178))))
(eq? 'exists (car (car (cdr (cdr V1178)))))
(pair? (cdr (car (cdr (cdr V1178)))))
(pair? (cdr (cdr (car (cdr (cdr V1178))))))
(null? (cdr (cdr (cdr (car (cdr (cdr V1178)))))))
(null? (cdr (cdr (cdr V1178)))))
(list
'exists
(car (cdr (car (cdr (cdr V1178)))))
(cons
(car V1178)
(cons 'v (cdr (cdr (car (cdr (cdr V1178))))))))]
[(and (pair? V1178)
(pair? (cdr V1178))
(eq? '=> (car (cdr V1178)))
(pair? (cdr (cdr V1178)))
(null? (cdr (cdr (cdr V1178)))))
(cons (list '~ (car V1178)) (cons 'v (cdr (cdr V1178))))]
[(and (pair? V1178)
(pair? (cdr V1178))
(eq? '<=> (car (cdr V1178)))
(pair? (cdr (cdr V1178)))
(null? (cdr (cdr (cdr V1178)))))
(kl:rectify
(list
(cons (car V1178) (cons '=> (cdr (cdr V1178))))
'&
(list (car (cdr (cdr V1178))) '=> (car V1178))))]
[(and (pair? V1178)
(pair? (cdr V1178))
(eq? 'v (car (cdr V1178)))
(pair? (cdr (cdr V1178)))
(pair? (car (cdr (cdr V1178))))
(pair? (cdr (car (cdr (cdr V1178)))))
(eq? '& (car (cdr (car (cdr (cdr V1178))))))
(pair? (cdr (cdr (car (cdr (cdr V1178))))))
(null? (cdr (cdr (cdr (car (cdr (cdr V1178)))))))
(null? (cdr (cdr (cdr V1178)))))
(kl:rectify
(list
(list (car V1178) 'v (car (car (cdr (cdr V1178)))))
'&
(cons
(car V1178)
(cons 'v (cdr (cdr (car (cdr (cdr V1178)))))))))]
[(and (pair? V1178)
(pair? (car V1178))
(pair? (cdr (car V1178)))
(eq? '& (car (cdr (car V1178))))
(pair? (cdr (cdr (car V1178))))
(null? (cdr (cdr (cdr (car V1178)))))
(pair? (cdr V1178))
(eq? 'v (car (cdr V1178)))
(pair? (cdr (cdr V1178)))
(null? (cdr (cdr (cdr V1178)))))
(kl:rectify
(list
(list (car (cdr (cdr V1178))) 'v (car (car V1178)))
'&
(cons
(car (cdr (cdr V1178)))
(cons 'v (cdr (cdr (car V1178)))))))]
[(and (pair? V1178)
(eq? '~ (car V1178))
(pair? (cdr V1178))
(pair? (car (cdr V1178)))
(pair? (cdr (car (cdr V1178))))
(eq? '& (car (cdr (car (cdr V1178)))))
(pair? (cdr (cdr (car (cdr V1178)))))
(null? (cdr (cdr (cdr (car (cdr V1178))))))
(null? (cdr (cdr V1178))))
(list
(list '~ (car (car (cdr V1178))))
'v
(cons '~ (cdr (cdr (car (cdr V1178))))))]
[(and (pair? V1178)
(eq? '~ (car V1178))
(pair? (cdr V1178))
(pair? (car (cdr V1178)))
(pair? (cdr (car (cdr V1178))))
(eq? 'v (car (cdr (car (cdr V1178)))))
(pair? (cdr (cdr (car (cdr V1178)))))
(null? (cdr (cdr (cdr (car (cdr V1178))))))
(null? (cdr (cdr V1178))))
(list
(list '~ (car (car (cdr V1178))))
'&
(cons '~ (cdr (cdr (car (cdr V1178))))))]
[(and (pair? V1178)
(eq? '~ (car V1178))
(pair? (cdr V1178))
(pair? (car (cdr V1178)))
(eq? '~ (car (car (cdr V1178))))
(pair? (cdr (car (cdr V1178))))
(null? (cdr (cdr (car (cdr V1178)))))
(null? (cdr (cdr V1178))))
(car (cdr (car (cdr V1178))))]
[(and (pair? V1178)
(pair? (cdr V1178))
(eq? 'v (car (cdr V1178)))
(pair? (cdr (cdr V1178)))
(null? (cdr (cdr (cdr V1178)))))
(list
(kl:prenex* (car V1178))
'v
(kl:prenex* (car (cdr (cdr V1178)))))]
[(and (pair? V1178)
(pair? (cdr V1178))
(eq? '& (car (cdr V1178)))
(pair? (cdr (cdr V1178)))
(null? (cdr (cdr (cdr V1178)))))
(list
(kl:prenex* (car V1178))
'&
(kl:prenex* (car (cdr (cdr V1178)))))]
[(and (pair? V1178)
(eq? '~ (car V1178))
(pair? (cdr V1178))
(null? (cdr (cdr V1178))))
(list '~ (kl:prenex* (car (cdr V1178))))]
[(and (pair? V1178)
(eq? 'all (car V1178))
(pair? (cdr V1178))
(pair? (cdr (cdr V1178)))
(null? (cdr (cdr (cdr V1178)))))
(list
'all
(car (cdr V1178))
(kl:prenex* (car (cdr (cdr V1178)))))]
[(and (pair? V1178)
(eq? 'exists (car V1178))
(pair? (cdr V1178))
(pair? (cdr (cdr V1178)))
(null? (cdr (cdr (cdr V1178)))))
(list
'exists
(car (cdr V1178))
(kl:prenex* (car (cdr (cdr V1178)))))]
[#t V1178]))
Raw
3-prenex-factorized.scm
(define (kl:prenex* V1178)
(define (prenex*$label1200 V1178/hd V1178/tl V1178)
(if (and (eq? 'exists V1178/hd) (pair? V1178/tl))
(let ([V1178/tl/tl (cdr V1178/tl)])
(if (and (pair? V1178/tl/tl) (null? (cdr V1178/tl/tl)))
(list 'exists (car V1178/tl) (kl:prenex* (car V1178/tl/tl)))
V1178))
V1178))
(define (prenex*$label1202 V1178/hd V1178/tl V1178)
(if (and (eq? '~ V1178/hd)
(pair? V1178/tl)
(null? (cdr V1178/tl)))
(list '~ (kl:prenex* (car V1178/tl)))
(if (and (eq? 'all V1178/hd) (pair? V1178/tl))
(let ([V1178/tl/tl (cdr V1178/tl)])
(if (and (pair? V1178/tl/tl) (null? (cdr V1178/tl/tl)))
(list 'all (car V1178/tl) (kl:prenex* (car V1178/tl/tl)))
(prenex*$label1200 V1178/hd V1178/tl V1178)))
(prenex*$label1200 V1178/hd V1178/tl V1178))))
(define (prenex*$label1204 V1178/hd V1178/tl V1178)
(if (pair? V1178/tl)
(let* ([V1178/tl/hd (car V1178/tl)]
[V1178/tl/tl (cdr V1178/tl)])
(if (and (eq? 'v V1178/tl/hd)
(pair? V1178/tl/tl)
(null? (cdr V1178/tl/tl)))
(list
(kl:prenex* V1178/hd)
'v
(kl:prenex* (car V1178/tl/tl)))
(if (and (eq? '& V1178/tl/hd)
(pair? V1178/tl/tl)
(null? (cdr V1178/tl/tl)))
(list
(kl:prenex* V1178/hd)
'&
(kl:prenex* (car V1178/tl/tl)))
(prenex*$label1202 V1178/hd V1178/tl V1178))))
(prenex*$label1202 V1178/hd V1178/tl V1178)))
(define (prenex*$label1205 V1178/tl/hd/hd V1178/tl/hd/tl
V1178/tl/tl V1178/hd V1178/tl V1178)
(if (and (eq? '~ V1178/tl/hd/hd)
(pair? V1178/tl/hd/tl)
(null? (cdr V1178/tl/hd/tl))
(null? V1178/tl/tl))
(car V1178/tl/hd/tl)
(prenex*$label1204 V1178/hd V1178/tl V1178)))
(define (prenex*$label1207 V1178/hd V1178/tl V1178)
(if (and (eq? '~ V1178/hd) (pair? V1178/tl))
(let* ([V1178/tl/hd (car V1178/tl)]
[V1178/tl/tl (cdr V1178/tl)])
(if (pair? V1178/tl/hd)
(let* ([V1178/tl/hd/hd (car V1178/tl/hd)]
[V1178/tl/hd/tl (cdr V1178/tl/hd)])
(if (pair? V1178/tl/hd/tl)
(let* ([V1178/tl/hd/tl/hd (car V1178/tl/hd/tl)]
[V1178/tl/hd/tl/tl (cdr V1178/tl/hd/tl)])
(if (and (eq? '& V1178/tl/hd/tl/hd)
(pair? V1178/tl/hd/tl/tl)
(null? (cdr V1178/tl/hd/tl/tl))
(null? V1178/tl/tl))
(list
(list '~ V1178/tl/hd/hd)
'v
(cons '~ V1178/tl/hd/tl/tl))
(if (and (eq? 'v V1178/tl/hd/tl/hd)
(pair? V1178/tl/hd/tl/tl)
(null? (cdr V1178/tl/hd/tl/tl))
(null? V1178/tl/tl))
(list
(list '~ V1178/tl/hd/hd)
'&
(cons '~ V1178/tl/hd/tl/tl))
(prenex*$label1205 V1178/tl/hd/hd V1178/tl/hd/tl V1178/tl/tl
V1178/hd V1178/tl V1178))))
(prenex*$label1205 V1178/tl/hd/hd V1178/tl/hd/tl
V1178/tl/tl V1178/hd V1178/tl V1178)))
(prenex*$label1204 V1178/hd V1178/tl V1178)))
(prenex*$label1204 V1178/hd V1178/tl V1178)))
(define (prenex*$label1208 V1178/hd V1178/tl V1178)
(if (pair? V1178/hd)
(let ([V1178/hd/tl (cdr V1178/hd)])
(if (pair? V1178/hd/tl)
(let ([V1178/hd/tl/tl (cdr V1178/hd/tl)])
(if (and (eq? '& (car V1178/hd/tl))
(pair? V1178/hd/tl/tl)
(null? (cdr V1178/hd/tl/tl))
(pair? V1178/tl))
(let ([V1178/tl/tl (cdr V1178/tl)])
(if (and (eq? 'v (car V1178/tl)) (pair? V1178/tl/tl))
(let ([V1178/tl/tl/hd (car V1178/tl/tl)])
(if (null? (cdr V1178/tl/tl))
(kl:rectify
(list
(list V1178/tl/tl/hd 'v (car V1178/hd))
'&
(cons
V1178/tl/tl/hd
(cons 'v V1178/hd/tl/tl))))
(prenex*$label1207
V1178/hd
V1178/tl
V1178)))
(prenex*$label1207 V1178/hd V1178/tl V1178)))
(prenex*$label1207 V1178/hd V1178/tl V1178)))
(prenex*$label1207 V1178/hd V1178/tl V1178)))
(prenex*$label1207 V1178/hd V1178/tl V1178)))
(define (prenex*$label1211 V1178/tl/hd V1178/tl/tl V1178/hd
V1178/tl V1178)
(if (and (eq? '=> V1178/tl/hd)
(pair? V1178/tl/tl)
(null? (cdr V1178/tl/tl)))
(cons (list '~ V1178/hd) (cons 'v V1178/tl/tl))
(if (and (eq? '<=> V1178/tl/hd)
(pair? V1178/tl/tl)
(null? (cdr V1178/tl/tl)))
(kl:rectify
(list
(cons V1178/hd (cons '=> V1178/tl/tl))
'&
(list (car V1178/tl/tl) '=> V1178/hd)))
(if (and (eq? 'v V1178/tl/hd) (pair? V1178/tl/tl))
(let ([V1178/tl/tl/hd (car V1178/tl/tl)])
(if (pair? V1178/tl/tl/hd)
(let ([V1178/tl/tl/hd/tl (cdr V1178/tl/tl/hd)])
(if (pair? V1178/tl/tl/hd/tl)
(let ([V1178/tl/tl/hd/tl/tl (cdr V1178/tl/tl/hd/tl)])
(if (and (eq? '& (car V1178/tl/tl/hd/tl))
(pair? V1178/tl/tl/hd/tl/tl)
(null? (cdr V1178/tl/tl/hd/tl/tl))
(null? (cdr V1178/tl/tl)))
(kl:rectify
(list
(list
V1178/hd
'v
(car V1178/tl/tl/hd))
'&
(cons
V1178/hd
(cons 'v V1178/tl/tl/hd/tl/tl))))
(prenex*$label1208
V1178/hd
V1178/tl
V1178)))
(prenex*$label1208 V1178/hd V1178/tl V1178)))
(prenex*$label1208 V1178/hd V1178/tl V1178)))
(prenex*$label1208 V1178/hd V1178/tl V1178)))))
(define (prenex*$label1212 V1178/tl/tl/hd/hd V1178/tl/tl/hd/tl
V1178/tl/tl/tl V1178/hd V1178/tl/hd V1178/tl/tl V1178/tl
V1178)
(if (and (eq? 'exists V1178/tl/tl/hd/hd)
(pair? V1178/tl/tl/hd/tl))
(let ([V1178/tl/tl/hd/tl/tl (cdr V1178/tl/tl/hd/tl)])
(if (and (pair? V1178/tl/tl/hd/tl/tl)
(null? (cdr V1178/tl/tl/hd/tl/tl))
(null? V1178/tl/tl/tl))
(list
'exists
(car V1178/tl/tl/hd/tl)
(cons V1178/hd (cons 'v V1178/tl/tl/hd/tl/tl)))
(prenex*$label1211 V1178/tl/hd V1178/tl/tl V1178/hd V1178/tl
V1178)))
(prenex*$label1211 V1178/tl/hd V1178/tl/tl V1178/hd V1178/tl
V1178)))
(define (prenex*$label1213 V1178/hd V1178/tl V1178)
(if (pair? V1178/tl)
(let* ([V1178/tl/hd (car V1178/tl)]
[V1178/tl/tl (cdr V1178/tl)])
(if (and (eq? 'v V1178/tl/hd) (pair? V1178/tl/tl))
(let* ([V1178/tl/tl/hd (car V1178/tl/tl)]
[V1178/tl/tl/tl (cdr V1178/tl/tl)])
(if (pair? V1178/tl/tl/hd)
(let* ([V1178/tl/tl/hd/hd (car V1178/tl/tl/hd)]
[V1178/tl/tl/hd/tl (cdr V1178/tl/tl/hd)])
(if (and (eq? 'all V1178/tl/tl/hd/hd)
(pair? V1178/tl/tl/hd/tl))
(let ([V1178/tl/tl/hd/tl/tl (cdr V1178/tl/tl/hd/tl)])
(if (and (pair? V1178/tl/tl/hd/tl/tl)
(null? (cdr V1178/tl/tl/hd/tl/tl))
(null? V1178/tl/tl/tl))
(list
'all
(car V1178/tl/tl/hd/tl)
(cons
V1178/hd
(cons 'v V1178/tl/tl/hd/tl/tl)))
(prenex*$label1212 V1178/tl/tl/hd/hd V1178/tl/tl/hd/tl
V1178/tl/tl/tl V1178/hd V1178/tl/hd
V1178/tl/tl V1178/tl V1178)))
(prenex*$label1212 V1178/tl/tl/hd/hd V1178/tl/tl/hd/tl
V1178/tl/tl/tl V1178/hd V1178/tl/hd V1178/tl/tl
V1178/tl V1178)))
(prenex*$label1211 V1178/tl/hd V1178/tl/tl V1178/hd
V1178/tl V1178)))
(prenex*$label1211 V1178/tl/hd V1178/tl/tl V1178/hd V1178/tl
V1178)))
(prenex*$label1208 V1178/hd V1178/tl V1178)))
(define (prenex*$label1214 V1178/hd/hd V1178/hd/tl V1178/tl
V1178/hd V1178)
(if (and (eq? 'exists V1178/hd/hd) (pair? V1178/hd/tl))
(let ([V1178/hd/tl/tl (cdr V1178/hd/tl)])
(if (and (pair? V1178/hd/tl/tl)
(null? (cdr V1178/hd/tl/tl))
(pair? V1178/tl))
(let ([V1178/tl/tl (cdr V1178/tl)])
(if (and (eq? 'v (car V1178/tl))
(pair? V1178/tl/tl)
(null? (cdr V1178/tl/tl)))
(list
'exists
(car V1178/hd/tl)
(cons (car V1178/hd/tl/tl) V1178/tl))
(prenex*$label1213 V1178/hd V1178/tl V1178)))
(prenex*$label1213 V1178/hd V1178/tl V1178)))
(prenex*$label1213 V1178/hd V1178/tl V1178)))
(define (prenex*$label1215 V1178/hd V1178/tl V1178)
(if (pair? V1178/hd)
(let* ([V1178/hd/hd (car V1178/hd)]
[V1178/hd/tl (cdr V1178/hd)])
(if (and (eq? 'all V1178/hd/hd) (pair? V1178/hd/tl))
(let ([V1178/hd/tl/tl (cdr V1178/hd/tl)])
(if (and (pair? V1178/hd/tl/tl)
(null? (cdr V1178/hd/tl/tl))
(pair? V1178/tl))
(let ([V1178/tl/tl (cdr V1178/tl)])
(if (and (eq? 'v (car V1178/tl))
(pair? V1178/tl/tl)
(null? (cdr V1178/tl/tl)))
(list
'all
(car V1178/hd/tl)
(cons (car V1178/hd/tl/tl) V1178/tl))
(prenex*$label1214 V1178/hd/hd V1178/hd/tl
V1178/tl V1178/hd V1178)))
(prenex*$label1214 V1178/hd/hd V1178/hd/tl V1178/tl
V1178/hd V1178)))
(prenex*$label1214 V1178/hd/hd V1178/hd/tl V1178/tl V1178/hd
V1178)))
(prenex*$label1213 V1178/hd V1178/tl V1178)))
(define (prenex*$label1216 V1178/tl/tl/hd/hd
V1178/tl/tl/hd/tl V1178/tl/tl/tl V1178/hd V1178/tl V1178)
(if (and (eq? 'exists V1178/tl/tl/hd/hd)
(pair? V1178/tl/tl/hd/tl))
(let ([V1178/tl/tl/hd/tl/tl (cdr V1178/tl/tl/hd/tl)])
(if (and (pair? V1178/tl/tl/hd/tl/tl)
(null? (cdr V1178/tl/tl/hd/tl/tl))
(null? V1178/tl/tl/tl))
(list
'exists
(car V1178/tl/tl/hd/tl)
(cons V1178/hd (cons '& V1178/tl/tl/hd/tl/tl)))
(prenex*$label1215 V1178/hd V1178/tl V1178)))
(prenex*$label1215 V1178/hd V1178/tl V1178)))
(define (prenex*$label1217 V1178/hd V1178/tl V1178)
(if (pair? V1178/tl)
(let ([V1178/tl/tl (cdr V1178/tl)])
(if (and (eq? '& (car V1178/tl)) (pair? V1178/tl/tl))
(let* ([V1178/tl/tl/hd (car V1178/tl/tl)]
[V1178/tl/tl/tl (cdr V1178/tl/tl)])
(if (pair? V1178/tl/tl/hd)
(let* ([V1178/tl/tl/hd/hd (car V1178/tl/tl/hd)]
[V1178/tl/tl/hd/tl (cdr V1178/tl/tl/hd)])
(if (and (eq? 'all V1178/tl/tl/hd/hd)
(pair? V1178/tl/tl/hd/tl))
(let ([V1178/tl/tl/hd/tl/tl (cdr V1178/tl/tl/hd/tl)])
(if (and (pair? V1178/tl/tl/hd/tl/tl)
(null? (cdr V1178/tl/tl/hd/tl/tl))
(null? V1178/tl/tl/tl))
(list
'all
(car V1178/tl/tl/hd/tl)
(cons
V1178/hd
(cons '& V1178/tl/tl/hd/tl/tl)))
(prenex*$label1216 V1178/tl/tl/hd/hd V1178/tl/tl/hd/tl
V1178/tl/tl/tl V1178/hd V1178/tl V1178)))
(prenex*$label1216 V1178/tl/tl/hd/hd V1178/tl/tl/hd/tl
V1178/tl/tl/tl V1178/hd V1178/tl V1178)))
(prenex*$label1215 V1178/hd V1178/tl V1178)))
(prenex*$label1215 V1178/hd V1178/tl V1178)))
(prenex*$label1215 V1178/hd V1178/tl V1178)))
(define (prenex*$label1218 V1178/hd/hd V1178/hd/tl V1178/tl
V1178/hd V1178)
(if (and (eq? 'exists V1178/hd/hd) (pair? V1178/hd/tl))
(let ([V1178/hd/tl/tl (cdr V1178/hd/tl)])
(if (and (pair? V1178/hd/tl/tl)
(null? (cdr V1178/hd/tl/tl))
(pair? V1178/tl))
(let ([V1178/tl/tl (cdr V1178/tl)])
(if (and (eq? '& (car V1178/tl))
(pair? V1178/tl/tl)
(null? (cdr V1178/tl/tl)))
(list
'exists
(car V1178/hd/tl)
(cons (car V1178/hd/tl/tl) V1178/tl))
(prenex*$label1217 V1178/hd V1178/tl V1178)))
(prenex*$label1217 V1178/hd V1178/tl V1178)))
(prenex*$label1217 V1178/hd V1178/tl V1178)))
(define (prenex*$label1219 V1178/hd V1178/tl V1178)
(if (pair? V1178/hd)
(let* ([V1178/hd/hd (car V1178/hd)]
[V1178/hd/tl (cdr V1178/hd)])
(if (and (eq? 'all V1178/hd/hd) (pair? V1178/hd/tl))
(let ([V1178/hd/tl/tl (cdr V1178/hd/tl)])
(if (and (pair? V1178/hd/tl/tl)
(null? (cdr V1178/hd/tl/tl))
(pair? V1178/tl))
(let ([V1178/tl/tl (cdr V1178/tl)])
(if (and (eq? '& (car V1178/tl))
(pair? V1178/tl/tl)
(null? (cdr V1178/tl/tl)))
(list
'all
(car V1178/hd/tl)
(cons (car V1178/hd/tl/tl) V1178/tl))
(prenex*$label1218 V1178/hd/hd V1178/hd/tl
V1178/tl V1178/hd V1178)))
(prenex*$label1218 V1178/hd/hd V1178/hd/tl V1178/tl
V1178/hd V1178)))
(prenex*$label1218 V1178/hd/hd V1178/hd/tl V1178/tl V1178/hd
V1178)))
(prenex*$label1217 V1178/hd V1178/tl V1178)))
(define (prenex*$label1220 V1178/tl/hd/hd V1178/tl/hd/tl
V1178/tl/tl V1178/hd V1178/tl V1178)
(if (and (eq? 'exists V1178/tl/hd/hd)
(pair? V1178/tl/hd/tl))
(let ([V1178/tl/hd/tl/tl (cdr V1178/tl/hd/tl)])
(if (and (pair? V1178/tl/hd/tl/tl)
(null? (cdr V1178/tl/hd/tl/tl))
(null? V1178/tl/tl))
(list 'all (car V1178/tl/hd/tl) (cons '~ V1178/tl/hd/tl/tl))
(prenex*$label1219 V1178/hd V1178/tl V1178)))
(prenex*$label1219 V1178/hd V1178/tl V1178)))
(if (pair? V1178)
(let* ([V1178/hd (car V1178)] [V1178/tl (cdr V1178)])
(if (and (eq? '~ V1178/hd) (pair? V1178/tl))
(let* ([V1178/tl/hd (car V1178/tl)]
[V1178/tl/tl (cdr V1178/tl)])
(if (pair? V1178/tl/hd)
(let* ([V1178/tl/hd/hd (car V1178/tl/hd)]
[V1178/tl/hd/tl (cdr V1178/tl/hd)])
(if (and (eq? 'all V1178/tl/hd/hd)
(pair? V1178/tl/hd/tl))
(let ([V1178/tl/hd/tl/tl (cdr V1178/tl/hd/tl)])
(if (and (pair? V1178/tl/hd/tl/tl)
(null? (cdr V1178/tl/hd/tl/tl))
(null? V1178/tl/tl))
(list
'exists
(car V1178/tl/hd/tl)
(cons '~ V1178/tl/hd/tl/tl))
(prenex*$label1220 V1178/tl/hd/hd V1178/tl/hd/tl V1178/tl/tl
V1178/hd V1178/tl V1178)))
(prenex*$label1220 V1178/tl/hd/hd V1178/tl/hd/tl
V1178/tl/tl V1178/hd V1178/tl V1178)))
(prenex*$label1219 V1178/hd V1178/tl V1178)))
(prenex*$label1219 V1178/hd V1178/tl V1178)))
V1178))
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment