--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Examples/etc/solve	Thu Aug 30 14:57:44 2007 +0900
@@ -0,0 +1,69 @@
+/*
+
+	tokio interpreter on tokio
+		Thu Sep  4 11:06:06 GMT+9:00 1986
+
+*/
+
+
+% main parts
+solve((A,B)):- solve(A),solve(B).
+solve(A):- t_clause(A,B),solve(B).
+
+%% temporal operators
+solve((A && B)):-
+	solve(A) && solve(B).
+solve(#A):-
+	#solve(A).
+solve(@A):-
+	@solve(A).
+solve(next(A)):-
+	next(solve(A)).
+solve(keep(A)):-
+	keep(solve(A)).
+solve(length(N)):-
+	length(N).
+
+%% functions
+solve(A=B) :- eval(A,V),eval(B,V1),!,V=V1.
+eval(V1,V) :- atomic(V1),!,V=V1.
+eval(V1,V) :- var(V1),!,V=V1.
+eval(@A,V) :- next(eval(A,V1)), V = @V1.
+eval(A+B,V) :- eval(A,AA),eval(B,BB), V=AA+BB.
+
+%% system predicates
+solve(A):- sys(A),prolog(A).
+
+sys(write(_)).
+sys(nl).
+sys(true).
+
+%% assertions
+t_clause( counter(A) , (@A=A+1, next(counter(A)))).
+
+t_clause( ap([],A,A) , true).
+t_clause( ap([H|X],Y,[H|Z]), ap(X,Y,Z)).
+
+%% tester
+test1 :- solve((
+	length(5),#write(1)
+    )).
+
+test2 :- solve((
+	length(3),#write(0) &&
+	length(2),#write(1)
+    )).
+
+test3 :- solve((    % this does not work
+	length(5),A=1, #(@A=A+1), #write(A)
+    )).
+
+test4 :- solve((
+	length(5),A=1,counter(A),#write(A)
+    )).
+
+test5 :- solve((
+	ap(A,B,[1,2,3]),write((A,B)),nl,fail
+    )).
+
+%%