-- LTL

preds:   	P Q true false hatom F `U` Head
copreds:        G `W` `R` `H` isPath isPathL NatStream
defuncts:	blink evens odds zip
fovars:  	at s s'
hovars:  	P Q

axioms:

   (true$s <==> True)
 & (false$s <==> False)
 & (hatom(at)$s <==> at -> head$s)

 & (F(P)$s <=== P$s | F(P)$tail$s)		  	   -- finally
 & (G(P)$s ===> P$s & G(P)$tail$s)		  	   -- generally
 & ((P`U`Q)$s <=== Q$s | P$s & (P`U`Q)$tail$s)	  	   -- until
 & ((P`W`Q)$s ===> Q$s | P$s & (P`W`Q)$tail$s) 	  	   -- weak until
 & ((P`R`Q)$s ===> Q$s & (P$s | (P`R`Q)$tail$s)) 	   -- release
 & ((P`H`Q)$s ===> P$s & ((P`H`Q)\/(Q`H`P)\/G(Q))$tail$s)  -- alternate
 & ((P->Q)$s <=== G(not(P)\/F(Q))$s)			   -- leads to

 & (isPath$s ===> head$s -> head$tail$s & isPath$tail$s) 
 & (isPathL$s ===> Any x: (head$s,x) -> head$tail$s & isPathL$tail$s)

 & (NatStream(x:s) ===> Nat(x) & NatStream(s))

 & head$x:s == x
 & tail$x:s == s

 & head$blink == 0
 & tail$blink == 1:blink

 & (blink = 1:blink <==> False)  	-- used in fairblink2 and
					-- notfairblink2
 & head(evens(s)) == head(s)
 & tail(evens(s)) == odds(tail(s))

 & head(odds(s)) == head(tail(s))
 & tail(odds(s)) == odds(tail(tail(s)))

 & head(zip(s,s')) == head(s)
 & tail(zip(s,s')) == zip(s',tail(s))

 & (not(F(P)) <==> G(not(P)))	
 & (not(G(P)) <==> F(not(P)))	
 & (not(P`R`Q) <==> not(P)`U`not(Q))	

 & (s ~ s' ===> head(s) = head(s') & tail(s) ~ tail(s'))

theorems:

   (F(Q)$s <=== (true`U`Q)$s)
 & (G(P)$s <=== (P`W`false)$s)
 & ((P`U`Q)$s <=== (P`W`Q)$s & F(Q)$s)
 & ((P`W`Q)$s <=== (P`U`Q)$s | G(P)$s)

conjects: 
   G(F$(=0).head)(blink)		--> True 	(fairblink0)
 & Not(G(F$(=0).head)(blink))           --> True	(notfairblink0)
 & G(F$(=2).head)(blink)		--> False 	(fairblink2)
 & Not(G(F$(=2).head)(blink))           --> True	(notfairblink2)
 & G(F$(=!x).head)(blink)		--> !x=0 | !x=1 (fairblinkx)
 & G(F$(=0).head)(mu s.(0:1:s))		--> True	(fairblinkmu)
 & NatStream(mu s.(1:2:3:s))		--> True 	(natstream)
 & NatStream(1:2:3:!s)			--> !s = (3:!s) | !s = (2:(3:!s)) |
					--  !s = (1:(2:(3:!s))) 
				 	--              (natstreamSol)
 & zip(evens$s,odds$s) ~ s