--- a/chop.pl	Sun Jan 21 10:21:43 2001 +0900
+++ b/chop.pl	Thu Aug 30 12:44:35 2007 +0900
@@ -32,18 +32,12 @@
 def(infinite, (true & false)).			% 
 def(finite, ~((true & false))).			% 
 def(length(I), X):- I>=0 ,def_length(I,X).	% length operator
-    def_length(I,empty):-I=<0,!.
-    def_length(I,@ X):-I1 is I-1,def_length(I1,X).
 def(less(I), X):- I>=0 ,def_less(I,X).		% less than N length
-    def_less(I,false):-I=<0,!.
-    def_less(I,next(X)):-I1 is I-1,def_less(I1,X).
 def(next(P),(empty; @(P))).
 % temporal assignments
 def(gets(A,B),keep(@A<->B)).
 def(stable(A),keep(@A<->A)).
 def(state(A),(share(A),'[]'(L))):- def_state(A,L).
-    def_state([H],H):-!.
-    def_state([H|L],(H;L1)):-def_state(L,L1).
 % def(Q=>P,exists(R,(Q = R,stable(R),fin(P = R)))).
 %   easier one
 % def(Q=>P,(Q & (empty,P); ~Q & (empty, ~P))).
@@ -57,11 +51,6 @@
 def(local(P), (P = (P&true))):- !.
 % test predicates
 def(trace(X,List),L) :- !,make_trace(List,X,L).
-    make_trace([],_,true):-!.
-    make_trace([1|T],X,(X,@L)):-!, make_trace(T,X,L).
-    make_trace([true|T],X,(X,@L)):-!, make_trace(T,X,L).
-    make_trace([0|T],X,(not(X),@L)):-!, make_trace(T,X,L).
-    make_trace([_|T],X,(not(X),@L)):-!, make_trace(T,X,L).
 def(even(P),
 	exists(Q,(Q, keep( @Q = ~Q),'[]'((Q->P))))).
 def(evenp(P),(
@@ -71,6 +60,18 @@
        +('[]'((~L, ~R)) & @ (L, ~R,@ (L,R, @ (R,'[]'( ~L)))) )).
 def(X,Y) :- define(X,Y).
 
+def_length(I,empty):-I=<0,!.
+def_length(I,@ X):-I1 is I-1,def_length(I1,X).
+def_less(I,false):-I=<0,!.
+def_less(I,next(X)):-I1 is I-1,def_less(I1,X).
+def_state([H],H):-!.
+def_state([H|L],(H;L1)):-def_state(L,L1).
+make_trace([],_,true):-!.
+make_trace([1|T],X,(X,@L)):-!, make_trace(T,X,L).
+make_trace([true|T],X,(X,@L)):-!, make_trace(T,X,L).
+make_trace([0|T],X,(not(X),@L)):-!, make_trace(T,X,L).
+make_trace([_|T],X,(not(X),@L)):-!, make_trace(T,X,L).
+
 :-dynamic variable/1.
 
 expand(X,Y) :- init_variable,expand1(X,Y).
@@ -82,10 +83,6 @@
 % expand1([P|Q],R) :- !,expand1(P,P1),expand1(Q,Q1),and(P1,Q1,R).
 expand1((P;Q),R) :- !,expand1(P,P1),expand1(Q,Q1),or(P1,Q1,R).
 expand1((P&Q),R) :- !,expand1(P,P1),expand1(Q,Q1),chop_expand1(P1,Q1,R).
-   chop_expand1(false,_,false):-!.
-%   chop_expand1(_,false,false):-!.
-   chop_expand1(true,true,true):-!.
-   chop_expand1(P,Q,(P&Q)):-!.
 expand1(not(Q),NQ):-!,expand1(Q,Q1),negate(Q1,NQ).
 expand1(exists(P,Q),exists(P,Q1)):-
 	nonvar(P),name(P,[X|_]),X = 95,!, % "_"  % reuse it...
@@ -101,31 +98,36 @@
 	expand_list([H|L],L1),
 	all_and(L1,And),
 	all_not(L1,NAnd).
-    expand_list([],[]) :-!.
-    expand_list([H|L],[H1|L1]) :-
-	expand1(H,H1), expand_list(L,L1).
-    all_and([],true):-!.
-    all_and([H|L],F):- all_and(L,F1),and(H,F1,F).
-    all_not([],true):-!.
-    all_not([H|L],F):- all_not(L,F1),negate(H,H1),and(H1,F1,F).
 expand1(^(R),^(R)):-!,           % 2nd order variable
 	add_2var(R).
 expand1(P,R) :- def(P,Q),!,expand1(Q,R).
 expand1(P,P) :- atomic(P),!,     % for empty or skip
 	check_atomic(P).
-  check_atomic(empty):-!.
-  check_atomic(more):-!.
-  check_atomic(true):-!.
-  check_atomic(false):-!.
-  check_atomic(true_false):-!.
-  check_atomic(P) :- name(P,PL),PL=[95|_],!.
-  check_atomic(P) :- add_variable(P). % "_"
 expand1(P,R) :- functor(P,H,N),functor(R,H,N),
 	expand_arg(N,P,R).
 expand_arg(0,_P,_R):-!.
 expand_arg(N,P,R):-arg(N,P,PA),arg(N,R,RA),
 	N1 is N-1,expand1(PA,RA),expand_arg(N1,P,R).
 
+chop_expand1(false,_,false):-!.
+%   chop_expand1(_,false,false):-!.
+chop_expand1(true,true,true):-!.
+chop_expand1(P,Q,(P&Q)):-!.
+expand_list([],[]) :-!.
+expand_list([H|L],[H1|L1]) :-
+    expand1(H,H1), expand_list(L,L1).
+all_and([],true):-!.
+all_and([H|L],F):- all_and(L,F1),and(H,F1,F).
+all_not([],true):-!.
+all_not([H|L],F):- all_not(L,F1),negate(H,H1),and(H1,F1,F).
+check_atomic(empty):-!.
+check_atomic(more):-!.
+check_atomic(true):-!.
+check_atomic(false):-!.
+check_atomic(true_false):-!.
+check_atomic(P) :- name(P,PL),PL=[95|_],!.
+check_atomic(P) :- add_variable(P). % "_"
+
 % do not use abolish here to avoid erase dynamic property of variable/1
 init_variable :- retract(variable(_)),fail;true.
 add_variable([]):-!.