cc.scm

;; First of all, notice that
(call/cc (lambda (k) e)) = (call/cc (lambda (k) (k e))) ; -- {1}
;; the type of call/cc a.k.a peirces law gives you the free theorem
(f (call/cc g)) = (call/cc (lambda (k) (f (g (compose k f))))) ;; -- {Free}
;; Continuations don't compose
(compose k k2) = k2 ;; {No Compose}
;; If a continuation is not used, we lose the form
If k not in e, then
(call/cc (lambda (k) (k e))) = (call/cc (lambda (k) e)) [k not in e] = e ;; -- {no-op}

(call/cc call/cc)
= {eta}
(call/cc (lambda (k) (call/cc k)))
= {eta}
(call/cc (lambda (k) (call/cc (lambda (k2) (k k2)))))
= {1}
(call/cc (lambda (k) (k (call/cc (lambda (k2) (k k2))))))
= {Free Theorem}
(call/cc (lambda (k) (call/cc (lambda (k3) (k ((lambda (k2) (k k2)) (compose k3 k)))))))
= {beta}
(call/cc (lambda (k) (call/cc (lambda (k3) (k (k (compose k3 k)))))))
= {No Compose}
(call/cc (lambda (k) (call/cc (lambda (k3) (k (k k))))))
= {no-op}
(call/cc (lambda (k) (k (k k))))
= {1}
(call/cc (lambda (k) (k k)))
= {1}
(call/cc (lambda (k) k))