-- TRANS2

specs:		CTL
constructs: 	a b A
defuncts:   	states labels atoms
preds:		three six seven'
copreds:	NOTthree four five seven eight

axioms:

states == [1] & labels == [a] & atoms == [A] &

(1,a) -> 1<+>2 & (2,a) -> 3 & (3,a) -> 1<+>4 & (4,a) -> 4 &

A -> branch[2,3,4] &

(three(st) <=== (a#(atom(A)\/three))(st)) &
(NOTthree(st) ===> (a<>(not(atom(A))/\NOTthree))(st)) &
(four(st) ===> (a#(atom(A)/\four))(st)) &
(five(st) ===> ((a#five)/\six)(st)) &
(six(st) <=== (atom(A)\/(a#six))(st)) &
(eight(st) ===> (a#eight)(st)) &

(seven(st) ===> seven'(st)) &			-- alternating fixpoints
(seven'(st) <=== (a#((atom(A)/\seven)\/seven'))(st)) 

conjects: 

all(three)[2,4] & 		        --> True   narrow match
all(NOTthree)[1,3] &			--> True   coinduction + narrow match
(three(st) & st `in` states ==> st = 2 | st = 4) &   
					--> True   fixpoint induction + narrow match
(NOTthree(st) & st `in` states ==> st = 1 | st = 3)  
					--> True   narrow match