\Here is most of the code used in study #4 - some is not designed
  to be type checked and where this is so, there is no type attached to
  the function.\

\**************All this stuff can be type checked. ********************\

(datatype stream

X : A; S : (A --> A); E : (A --> boolean);
===============================
[X S E] : (stream A);)

(define force
 {(stream A) --> A}
    [X S E] -> X)

(define delay
  {(stream A) --> (stream A)}
    [X S E] -> [(S X) S E])
 
(define end?
  {(stream A) --> boolean}
   [X S E] -> (E X)) 

(define push
  {A --> (stream A) --> (stream A)}
    X [Y S E] -> [X (/. Z (if (= Z X) Y (S Z))) E]) 

(define forall
{(stream A) --> (A --> boolean) --> boolean}
[X S E] P -> (if (E X) true (and (P X) (forall [(S X) S E] P))))

(define exists
{(stream A) --> (A --> boolean) --> boolean}
[X S E] P -> (if (E X) false (or (P X) (exists [(S X) S E] P))))

\super - strict\
(define super
{(stream A) --> (A --> B) --> (B --> C --> C) --> C --> C}
[X S E] P F Y -> (if (E X) Y (F (P X) (super [(S X) S E] P F Y))))

(define forall
{(stream A) --> (A --> boolean) --> boolean}
Stream P -> (super Stream P and true)) 

(define exists
{(stream A) --> (A --> boolean) --> boolean}
Stream P -> (super Stream P or false)) 

(define for
{(stream A) --> (A --> B) --> number}
Stream P -> (super Stream P progn 0))

(define progn
{A --> B --> B}
X Y -> Y)

(define filter
{(stream A) --> (A --> boolean) --> [A]}
Stream P -> (super Stream (/. X (if (P X) [X] [])) append []))

(define next-prime
{number --> number}
N -> (if (prime? (+ N 1)) (+ N 1) (next-prime (+ N 1))))

(define prime?
{number --> boolean}
X -> (prime-help X (sqrt X) 2))

(define prime-help
{number --> number --> number --> boolean}
X Max Div -> false where (integer? (/ X Div))
X Max Div -> true where (> Div Max)
X Max Div -> (prime-help X Max (+ 1 Div)))

\************************ All this stuff is not type checked. ******************************\
\Super - partly lazy\
(define super
  [X S E] P F Y -> (if (E X) Y
		   (if (= F or) 
		       (or (P X) (super [(S X) S E] P F Y)) 
		            (if (= F and) 
                                           (and (P X) (super [(S X) S E] P F Y)) 
                                           (F (P X) (super [(S X) S E] P F Y))))))

(define acr-syntax
[exists X S P] -> [exists S [/. X P]]
[forall X S P] -> [forall S [/. X P]]
X -> X) 

(sugar in acr-syntax 0)

(define quantifier-machine
[exists X [ ] P] -> false 
[exists X [Y | Z] P] -> (or (quantifier-machine (subst Y X P)) (quantifier-machine [exists X Z P]))
[forall X [ ] P] -> true 
[forall X [Y | Z] P] -> (and (quantifier-machine (subst Y X P)) (quantifier-machine [forall X Z P]))
[~ P] -> (not (quantifier-machine P))
[P & Q] -> (and (quantifier-machine P) (quantifier-machine Q))
[P v Q] -> (or (quantifier-machine P) (quantifier-machine Q))
[P => Q] -> (or (not (quantifier-machine P)) (quantifier-machine Q))
[P <=> Q] -> (and (quantifier-machine [P => Q]) (quantifier-machine [Q => P]))
[X = Y] -> (= (quantifier-machine X) (quantifier-machine Y))
[F X] -> ((quantifer-machine F) (quantifer-machine X))
[F X | Y] -> (quantifier-machine [(F X) | Y])
X -> X)

(define lazy-quantifier-machine
[exists X D P] -> false where (end? D)
[exists X D P] -> (or (lazy-quantifier-machine (subst (force D) X P)) (lazy-quantifier-machine [exists X (delay D) P]))
[forall X D P] -> true where (end? D)
[forall X D P] -> (and (lazy-quantifier-machine (subst (force D) X P)) (lazy-quantifier-machine [forall X (delay D) P]))
[~ P] -> (not (lazy-quantifier-machine P))
[P & Q] -> (and (lazy-quantifier-machine P) (lazy-quantifier-machine Q))
[P v Q] -> (or (lazy-quantifier-machine P) (lazy-quantifier-machine Q))
[P => Q] -> (or (not (lazy-quantifier-machine P)) (lazy-quantifier-machine Q))
[P <=> Q] -> (and (lazy-quantifier-machine [P => Q]) (lazy-quantifier-machine [Q => P]))
[X = Y] -> (= (lazy-quantifier-machine X) (lazy-quantifier-machine Y))
[F X] -> ((lazy-quantifier-machine F) (lazy-quantifier-machine X))
[F X Y | Z] -> (lazy-quantifier-machine [(F X) Y | Z])
X -> X)