-- CTL

preds:   	P Q true false atom not \/ /\ or and `then`
	        EX <> EF AF `EU` `AU`
copreds: 	AX # EG AG `EW` `AW` `ER` `AR`
fovars:  	at st st' act
hovars:  	P Q

axioms:

   (true$st <==> True)
 & (false$st <==> False)
 & (atom(at)$st <==> at -> st)
 & (not(P)$st <==> Not(P$st))
 & ((P\/Q)$st <==> P$st | Q$st)
 & ((P/\Q)$st <==> P$st & Q$st)
 & ((P`then`Q)$st <==> (P$st ==> Q$st))
 & (or <==> foldl(\/)$false)
 & (and <==> foldl(/\)$true)

 & (EX(P)$st <=== st -> st' & P(st'))
 & (AX(P)$st ===> (st -> st' ==> P(st')))
 & ((act<>P)$st <=== (st,act) -> st' & P(st'))
 & ((act#P)$st ===> ((st,act) -> st' ==> P(st')))

 & (EF(P)$st <=== P$st | EX(EF(P))$st)		  	-- finally  	
 & (AF(P)$st <=== P$st | AX(AF(P))$st & EX(true)$st)		  	
 & (EG(P)$st ===> P$st & (EX(EG(P))$st | AX(false)$st)) -- generally
 & (AG(P)$st ===> P$st & AX(AG(P))$st)	  	
 & ((P`EU`Q)$st <=== Q$st | P$st & EX(P`EU`Q)$st)	-- until
 & ((P`AU`Q)$st <=== Q$st | P$st & AX(P`AU`Q)$st)		
 & ((P`EW`Q)$st ===> Q$st | P$st & EX(P`EW`Q)$st)	-- weak until
 & ((P`AW`Q)$st ===> Q$st | P$st & AX(P`AW`Q)$st)
 & ((P`ER`Q)$st ===> Q$st & (P$st | EX(P`ER`Q)$st))	-- release
 & ((P`AR`Q)$st ===> Q$st & (P$st | AX(P`AR`Q)$st))