analyse(M, Ones, Hops, Status) :- !, analyse(M, 0, 0, going, Ones, Hops, Status). 
analyse(_Machine, Ones, Hops, halts, Ones, Hops, halts) :- !. 
analyse(_Machine, Ones, Hops, halts(T), Ones, Hops, halts(T)) :- !. 
analyse(_Machine, Ones, Hops, abort, Ones, Hops, abort) :- !. 
analyse(_Machine, Ones, Hops, blank, Ones, Hops, blank) :- !. 
analyse(_Machine, Ones, Hops, loops(T), Ones, Hops, loops(T)) :- !. 
analyse(_Machine, Ones, Hops, loops, Ones, Hops, loops) :- !, true. 
analyse(Machine, _Ones, _Hops, Doing, 0, 0, loops) :-  
	\+ member(Doing, [halts,blank,abort,loops,loops(_)]), 
	loops(Machine), !. % Machine has a statically detected loop
analyse(Machine, _Ones, _Hops, Doing, 0, 0, meander) :-  
	\+ member(Doing, [halts,blank,abort]), 
	\+ loops(Machine), 
	meandering(Machine), !. % Machine cannot reach halt state 

analyse(Machine, _Ones, _Hops, Doing, NewOnes, NewHops, NewStatus) :- 
	% Analyse short version of history ...
	\+ member(Doing, [halts,blank,abort]), 
	\+ loops(Machine), 
	smallhist(MaxHist), 
	emulate(Machine, MaxHist, [naive,loop], Ones, Hops, Status, Outputs), 
	historical_analysis(Machine, Ones, Hops, Status, small, Outputs, NewOnes, NewHops, NewStatus), !. 

analyse(Machine, _Ones, _Hops, Doing, NewOnes, NewHops, NewStatus) :- 
	% Analyse long version of history ...
   	\+ member(Doing, [halts,blank,abort]), 
     	\+ loops(Machine), 
     	largehist(MaxHist), %
     	emulate(Machine, MaxHist, [naive,hist], Ones, Hops, Status, Outputs), 
     	historical_analysis(Machine, Ones, Hops, Status, large, Outputs, NewOnes, NewHops, NewStatus), !. 

analyse(Machine, _Ones, _Hops, going, NewOnes, NewHops, NewStatus) :-
	% Punt that it is a monster ... 
   	!, 
 	maxsteps(Max), 
   	emulate(Machine, Max, [flex], NewOnes, NewHops, NewStatus, _), !. 

analyse(_Machine, _Ones, _Hops, Doing, 0, 0, going) :- 
	% Otherwise, give up!
	\+ member(Doing, [halts,blank,abort]),
	!. 

historical_analysis(_Machine, Ones, Hops, halts, _, _, Ones, Hops, halts) :- !. 
historical_analysis(_Machine, Ones, Hops, halts(T), _, _, Ones, Hops, halts(T)) :- !. 
historical_analysis(_Machine, Ones, Hops, abort, _, _, Ones, Hops, abort) :- !. 
historical_analysis(_Machine, Ones, Hops, loops(T), _, _, Ones, Hops, loops(T)) :- !. 
historical_analysis(_Machine, Ones, Hops, loops, _, _, Ones, Hops, loops) :- !, true. 
historical_analysis(_Machine, Ones, Hops, blank, _, _, Ones, Hops, blank) :- !. 
historical_analysis(Machine,  _Ones, _Hops, going, _, _Outputs, 0, 0, loops) :- loops(Machine), !. 
historical_analysis(Machine,  _Ones, _Hops, Status, _Mode, _Outputs, 0, 0, meander) :-  
	\+ member(Status, [halts,abort,loops,loops(_),blank]), 
	meandering(Machine), !. % Machine cannot reach halt state 

historical_analysis(Machine, _Ones, _Hops, Status, small, Outputs, NewOnes, NewHops, NewStatus) :-
	\+ member(Status, [halts,abort,loops,loops(_),blank]), 
	history(Outputs, History), 
	patterns(Machine, History, NewOnes, NewHops, NewStatus), !. % try for cycle or growing loop. 

historical_analysis(Machine, _Ones, _Hops, going, Mode, Outputs, NewOnes, NewHops, NewStatus) :- 
 	member(Mode, [small,large]), 
 	history(Outputs, History), 	
 	pivotal_history(Machine, History, Hist), % try for pivotal state ...
        clean_history(Hist, Clean), pivot(Mode, Max), firstN(Max, Clean, C), 
 	induction(Machine, Mode, [], C, NewOnes, NewHops, NewStatus), % try inductive prover
      	!, true. 
 
historical_analysis(Machine, _Ones, _Hops, going, Mode, Outputs, NewOnes, NewHops, NewStatus) :- 
	member(Mode, [small,large]), 
 	history(Outputs, History), 
	non_pivotal_history(Machine, History, Hist), % try non-pivotal states ...
        clean_history(Hist, Clean), nonpivot(Mode, Max), firstN(Max,Clean, C), 
 	induction(Machine, Mode, [], C, NewOnes, NewHops, NewStatus), % try inductive prover
      	!, true. 

% Finds all hypotheses for machine M. Only really useful for debugging. 
hypanalyse(M, PHyps, OHyps) :-
	smallhist(Max), 
	emulate(M, Max, [naive,loop], _Ones, _Hops,_Status, Outputs), !, 	
	history(Outputs, History), 
	format("Hist:~n", []), print_history(History), 
	pivotal_history(M, History, PHist), % try for pivotal state ...
	format("Pivotal done~n", []), 
	non_pivotal_history(M, History, OHist), % try non-pivotal states ...
	format("Non-Pivotal done~n", []), 
	clean_history(PHist, PClean), format("More Cleaning ...~n", []), 
	clean_history(OHist, OClean),
	pivot(small, PMax), nonpivot(small, NMax),
	firstN(PMax, PClean, PC), firstN(NMax, OClean, NC), 
	format("Hypothesising ...~n", []), ttyflush, 
	hypotheses(M, [], PC, [], PHyps), 
	format("Pivotal hypotheses~n", []), 
        print_hyps(PHyps), 
	hypotheses(M, [], NC, [], OHyps), 
	format("Other hypotheses~n", []), 
	print_hyps(OHyps), 
	true. 

hypotheses(_Machine, _, [], SoFar, SoFar).
hypotheses(Machine, Prev, [state(L1,S,[I|R1])|Rest], SoFar, Hypotheses) :- 
	length(Prev, P), L is P + 1, 
	findall(hyp(induction(pos(L,Pos),Initial,Final)), extract_hypothesis(state(L1,S,[I|R1]), Rest, state(_L2, S, [I|_R2]), _N, Initial, Final,Pos), Hyps), 
	append(SoFar, Hyps, NewSoFar), 
	append(Prev, [state(L1,S,[I|R1])], NewPrev), 
	hypotheses(Machine, NewPrev, Rest, NewSoFar, Hypotheses), 
	true.

history(Outputs, History) :-
	member(history(H), Outputs), 
     	member(now(State), Outputs), 
        append([State], H, List), 
      	reverse(List, History), 
        !. 

pivotal_history(M, History, Hist) :-
	pivotal(M, S), 
	findall(state(Left, S, Right), member(state(Left, S, Right), History), H), 
	purge(H, Hist), !. 

purge([state(Left, S, Right)|Rest], Rest) :-
	Left = [], S = a, Right = [0], !. % purge initial state from pivotal history if it occurs.
purge([state(Left, S, Right)|Rest], [state(Left, S, Right)|Rest]) :-
	\+ (Left = [], S = a, Right = [0]), !. % otherwise leave it alone. 

non_pivotal_history(M, History, Hist) :-
	pivotal(M, S), 
	findall(state(Left, State, Right), (member(state(Left, State, Right), History), State \== S), H), 
	purge(H, Hist), !. 

non_pivotal_member(S, state(Left, State, Right), History) :-
	member(state(Left, State, Right), History), State \== S. 

clean_history([], []). 
clean_history([state(Left, State, Right)|Rest], [state(CL, State, CR)|Clean]) :- 
	delete_trail_blanks(Left, CL), 
	delete_trail_blanks(Right, CR),
	clean_history(Rest, Clean). 

chunk(Machine, N) :-
	number_states(0, Machine, Number), !, 
	uprange(1, Number, N).

number_states(Count, [], Count) :- !. 
number_states(Count, [t(S,_I,_O,_D,_NS)|Rest], Number) :- 
	delete_all(S, Rest, List), C is Count + 1, !, 
	number_states(C, List, Number).

uprange(L1, L2, I) :- L1 =< L2, I = L1.
uprange(L1, L2, I) :- L1 =< L2, L is L1 + 1, !, uprange(L, L2, I).
downrange(L1, L2, I) :- L1 =< L2, I = L2.
downrange(L1, L2, I) :-	L1 =< L2, L is L2 - 1, !, downrange(L1, L, I).

transform([], _N, []) :- !. 
transform([S|Hist], N, [NS|Rest]) :-
	transform_state(S, N, NS), !, 
	transform(Hist, N, Rest), !. 

transform_state(state(Left, S, Right), N, state(NewLeft, S, NewRight)) :-
	convert_tape(Left, N, NewLeft), !, 
	convert_tape(Right, N, NewRight), !. 

delete_all(_S, [], []). 
delete_all(S, [t(S1,_I,_O,_D,_NS)|Rest], Remain) :-
	S == S1, 
	delete_all(S, Rest, Remain). 
delete_all(S, [t(S1,I,O,D,NS)|Rest], [t(S1,I,O,D,NS)|Remain]) :-
	S \== S1, 
	delete_all(S, Rest, Remain). 
	
patterns(_, History, Ones, Hops, Status) :-
	cycling([], History, Ones, Hops, Status), !. 
patterns(Machine, [_First|History], Ones, Hops, Status) :-	
	growing(Machine, [], History, Ones, Hops, Status), !. % Discard first state for growing search.

cycling(Prev, [state(L,S,[I|R])|Rest], Ones, Hops, loops(cycle(Cycle))) :-
	split([], Earlier, state(L,S,[I|R]), _Later, Rest), !, 
	length(Prev, P),
	length(Earlier, E),
	countones(L,R,Ones),!, 
	Hops is P + E + 1,
	Cycle is E + 1,
	true.

cycling(Prev, [state(L,S,[I|R])|Rest], Ones, Hops, Status) :-
	append(Prev, [state(L,S,[I|R])], NewPrev),
	cycling(NewPrev, Rest, Ones, Hops, Status). 

growing(Machine, Prev, [state(L1,S,[I|R1])|Rest], Ones, Hops, loops(dizzyduck(Cycle))) :-
	split2([], S, I, Earlier, state(L2,S,[I|R2]), _Later, Rest), 
        length(Prev, P), length(Earlier, E), 
	append([state(L1,S,[I|R1])|Earlier], [state(L2,S,[I|R2])], States), 
	movements(Machine, States, 0, Left, 0, Right, 0, Final), 
	length(R1, R),
	length(L1, L),
	growth(L1, L2, R1, R2, Left, Right, Final, L, R), 
	!, 
	length(Prev, P),
	length(Earlier, E),
	countones(L2,R2,Ones),!, 
	Hops is P + E + 1 + 1, % to allow for discarded first state
	Cycle is E + 1,
	true.

growing(Machine, Prev, [state(L,S,[I|R])|Rest], Ones, Hops, Status) :-
	append(Prev, [state(L,S,[I|R])], NewPrev),
	growing(Machine, NewPrev, Rest, Ones, Hops, Status). 

growth(L1, L2, R1, R2, Left, Right, Final, L, R) :-
	prefixtape(L1, L2),
	prefixtape(R1, R2), 
        within2(Left, Right, Final, L, R),!, 
	true. 

growth(L1, L1, _R1, _R2, _Left, 0, _Final, _L, _R) :- !. 
growth(_L1, _L2, R1, R1, 0, _Right, _Final, _L, _R) :- !. 

growth(L1, L1, R1, R2, Left, Right, Final, L, R) :-
	clean(R1,CR1), clean(R2,CR2),
	append(P1,P2, CR1),
	append(P1, PP, CR2),
	append(_, P2, PP),
	within2(Left,Right, Final,L,R), !.
	
growth(L1, L2, R1, R1, Left, Right, Final, L, R) :-
	clean(L1,CL1), clean(L2,CL2),
	append(P1,P2, CL1),
	append(P1, PP, CL2),
	append(_, P2, PP),
	within2(Left,Right, Final,L,R), !. 

within(Left, Right, Final, L, R) :-
	Final =< 0, !, 
	Final - Left =< L, 
	Right =< R. 
within(Left, Right, Final, L, R) :-
	Final > 0, !, 
	abs(Left) =< L,
	Right - Final  =< R. % Note 0 < Final =< Right

within2(Left, Right, _Final, L, R) :-
	abs(Left) =< L, 
	Right =< R. 

prefixtape(T1, T2) :-
	clean(T1, S1),
	clean(T2, S2),
	append(S1, _, S2). 
suffixtape(T1, T2) :-
	clean(T1, S1),
	clean(T2, S2),
	append(_, S1, S2). 

movements(_, [], L, L, R, R, F, F).
movements(Machine, [state(_L,S,[I|_R])|Rest], Left, NewLeft, Right, NewRight, Current, NewCurrent) :-
	member(t(S,I,_,D,_), Machine),
	updatespots(D, Left, NL, Right, NR, Current, NC),
	movements(Machine, Rest, NL, NewLeft, NR, NewRight, NC, NewCurrent). 

updatespots(l, Left, NL, R, R, Current, C1) :-
	!, C1 is Current - 1,
	setleft(C1, Left, NL).

updatespots(r, L, L, Right, NR, Current, C1) :-
	!, C1 is Current + 1,
	setright(C1, Right, NR).

setleft(C, L, L) :- L < C, !. 
setleft(C, L, C) :- L >= C.  
setright(C, R, R) :- R > C, !. 
setright(C, R, C) :- R =< C. 

split(Prev, Prev, state(L,S,[I|R]), List, [state(L,S,[I|R])|List]) :- !.
split(Prev, Earlier, state(L1,S1,[I1|R1]), Later, [state(L2,S2,[I2|R2])|List]) :- 
	append(Prev, [state(L2,S2,[I2|R2])], NewPrev),
	split(NewPrev, Earlier, state(L1,S1,[I1|R1]), Later, List).

split2(Prev, S1, I1, Prev, state(L2,S2,[I2|R2]), List, [state(L2,S2,[I2|R2])|List]) :-
	S1 == S2, I1 == I2.
split2(Prev, S1, I1, Earlier, State, Later, [state(L2,S2,[I2|R2])|List]) :- 

	append(Prev, [state(L2,S2,[I2|R2])], NewPrev),
	split2(NewPrev, S1, I1, Earlier, State, Later, List).
	
subtape(ST, T) :-
	clean(ST, S1),
	clean(T, S2),
	append(_, S1, S2). 

subtape(ST, T) :-
	clean(ST, S1),
	clean(T, S2),
	append(S1, _, S2). 

clean([], []) :- !. 
clean([1|Rest], [1|Clean]) :-
	!, clean(Rest, Clean).
clean([0|Rest], [0|Clean]) :-
	member(1, Rest),!, 
	clean(Rest, Clean). 
clean([0|Rest], []) :-
	\+ member(1, Rest),!.

pivotal(M, S) :-
	member(t(S,_,_,_,h), M). 

variant(_Dir, [0],T2) :-
	delete_trail_blanks(T2, [0]). 
variant(Dir, T1,T4) :- 
	T1 \= [0], nonvar(T4), 
	blank_form(T1, T), 
	blank_form(T4, TT),
	orienttape(Dir, T, T3), 
	orienttape(Dir, TT, T2), 
	variantt(T3,T2).

variant(Dir, T1,T4) :- 
	T1 \= [0], var(T4), 
	delete_trail_blanks(T1, T), 
	orienttape(Dir, T, T3), 
	variantt(T3,T2),
	delete_trail_blanks(T2, Temp), 
	orienttape(Dir, Temp, T4). 

blank_form(T, T).
blank_form(T, T1) :- delete_trail_blanks(T, T1). 
blank_form(T, T1) :- append(T, [0], T1). 

normalise([], []) :- !. 
normalise(T, []) :- allblank(T), !. 
normalise([I], [I]) :- is_input(I), I \== 0, !. 
normalise(L1, L2) :-
	length(L1, L), L > 1, \+ allblank(L1), !, 
	delete_trail_blanks(L1, L2). 

delete_trail_blanks([], []) :- !.
delete_trail_blanks(T, [0]) :- 
	allblank(T), !. 
delete_trail_blanks([I], [I]) :- is_input(I), I \== 0, !.
delete_trail_blanks(L1, L2) :-
	length(L1, L), L > 1, \+ allblank(L1), !, 
	reverse(L1, T1),
	delete_blank(T1, T2),!, 
	reverse(T2, L2). 

delete_blank([], []) :- !.
delete_blank([I|Rest], [I|Rest]) :- is_input(I), I \== 0, !.
delete_blank([0|Rest], Rest1) :-
	!, delete_blank(Rest, Rest1). 
delete_blank([tape(In,X)|Rest], Rest1) :-
	allblank(In), 
	int(X), !, 
	delete_blank(Rest, Rest1). 
delete_blank([tape(In,X)|Rest], [tape(In,X)|Rest]) :-
	allblank(In), X = v(_,_,_,_,_), !.
delete_blank([tape(In,X)|Rest], [tape(In,X)|Rest]) :-
	\+ allblank(In), !. 

variant1(T, T) :- \+ (member(tape(_I,X), T), X = v(_,_,_,_,_)). 
variant1(T1, T2) :- member(tape(I,X), T1), X = v(_,_,_,_,_), 
	base(T1, Pre, tape(I,X), Post), % T1 = Pre.Base.Post
	prechunk(I, Pre, B, PreBase), % Pre = B.PreBase
	postchunk(I, Post, PostBase, A), % Post = PostBase.A
	splinters(I, B, A, I2, I1, Before, After), % B.A = Before.MidBase.After, I = I1.I2
	append(I2, PreBase, Temp1), append(PostBase, I1, Temp2), 
	append(Temp1, Temp2, List), newbase(I, I2, I1, NewI), 
	NewBase = tape(NewI, X), 
        vary(NewBase, [], List, Temp), 
 	append(Before, Temp, After, T2). 

append(W, X, Y, Z) :-
	append(W, X, Temp), append(Temp, Y, Z).

base(T1, Pre, tape(I,X), Post) :-
	append(Pre, [tape(I,X)|Post], T1), X = v(_,_,_,_,_), !. 

newbase(I, [], [], I) :- !. 
newbase(_I, I2, I1, NewI) :- I2 \== [], I1 \== [], append(I2, I1, NewI). 
	
prechunk(I, Pre, B, PreBase) :-
	append(Prev, I, Pre),
	prechunk(I, Prev, B, Pre1), % Prev is B1.Pre1, and Pre is B1.Pre1.I
	append(Pre1, I, PreBase). 
prechunk(I, Pre, Pre, []) :-
	\+ append(_, I, Pre).
	
postchunk(I, Post, PostBase, A1) :- % Post is PostBase.A
	append(I, PBase, Post), % Post = I.PBase
	postchunk(I, PBase, PB1, A1), % Post = I.PB1.A1
	append(I, PB1, PostBase). 
postchunk(I, Post, [], Post) :- 
	\+ append(I, _PBase, Post). 

splinters(I, Before, After, I2, I1, NewBefore, NewAfter) :-
	append(I1,I2,I), I1 \== [], I2 \== [], 
	append(NewBefore, I2,Before),
	append(I1, NewAfter, After).

splinters(I, Before, After, [], [], Before, After) :-
	\+ (append(I1,I2,I), I1 \== [], I2 \== [], append(_NewBefore, I2,Before), append(I1, _NewAfter, After)).

vary(Base, SoFar, Rest, Variant) :-
	append(SoFar, [Base], Rest, Variant). 

vary(Base, SoFar, Rest, Variant) :-
	Rest = [Next|Rest1], 
	append(SoFar, [Next], New),
	rotate(Base, NewBase),
	vary(NewBase, New, Rest1, Variant).

rotate(tape(I, X), tape(NewI, X)) :-
	I = [First|Rest],
	append(Rest, [First], NewI). 

flatten_state(state(Left,S,Dir,Right), state(FL,S,Dir,FR)) :-
	flatten(Left, TL), flatten(Right, TR),
	collapseblanks(TL, FL), collapseblanks(TR, FR). 

% flatten2(Tape, NewTape). Flattens occurrences of two or less
flatten2([], []). 
flatten2([tape(I,N)|Rest], [tape(I,N)|Result]) :-
	integer(N), N >= 3,
	flatten2(Rest, Result).
flatten2([tape(I,N)|Rest], Result) :-
	integer(N), N >= 0, N =< 2,
	multiple(I, N, [], Is), 
	flatten2(Rest, SubResult),
	append(Is, SubResult, Result). 

flatten([], []).
flatten([tape(I,N)|Rest], Result) :-
	integer(N), 
	multiple(I, N, [],  List),
	flatten(Rest, Remainder),
	append(List, Remainder, Result). 
flatten([tape(I,N)|Rest], [tape(I,N)|Result]) :-
	% var(N), 
	N = v(_,_,_,_,_), 
	flatten(Rest, Result).
flatten([I|Rest], [I|Result]) :-
	I \= tape(_,_), 
	flatten(Rest, Result).

multiple(_I, 0, SoFar, SoFar).
multiple(I, N, SoFar, Result) :-
	N > 0, N1 is N - 1,
	append(SoFar, I, NewSoFar),
	multiple(I, N1, NewSoFar, Result). 
	
variantt(T1, T2) :-
	chunknum(T1, N),
	chunkify(N, T1, Chunks), 
	varify(Chunks, T2).
chunknum(List, 0) :- \+ member(tape(_,_), List).
chunknum(List, N) :- 
	member(tape(I,X), List),
	delete(List, tape(I,X), Rest),
	chunknum(Rest, N1),!, 
	N is N1 + 1. 

chunkify(0, List, [List]).
chunkify(1, List, [List]).
chunkify(N, List, [Chunk|Chunks]) :-
	N > 1, 
	member(tape(I,X), List), X = v(_,_,_,_,_), % var(X), 
	base(List, Pre, tape(I,X), Post), % List = Pre.tape(I,X).Post %% Relies on base only finding the first solution! Need better code here!
	postchunk(I, Post, PostBase, Rest), % Post = PostBase.A, so List = Pre.Base.PostBase.A, Chunk 
	append(Pre, [tape(I,X)], PostBase, Chunk), 
	chunknum(Chunk, 1), 
	N1 is N - 1,
	chunkify(N1, Rest, Chunks).
 
varify([], []). 
varify([Section|Rest], List) :-
	variant1(Section, S1),
	varify(Rest, RestList),
	append(S1, RestList, List). 

firstN(N, List, List) :-
	length(List, L), L =< N.
firstN(N, List, First) :-
	length(List, L), L > N,
	append(First, _, List), length(First, N). 


% induction(Machine, Mode, Prev, History, Ones, Hops, Status). Succeeds if it can find and prove a non-termination hypothesis. 
induction(Machine, Mode, Prev, [state(L1,S,[I|R1])|Rest], Ones, Hops, Status) :- 
	Rest \== [], 
        length(Prev, P), FirstPos is P+1, 
	extract_hypothesis(state(L1,S,[I|R1]), Rest, State2, N, Initial, Final, Pos),
	NextPos is Pos + P, 
	hypmax(Mode, Max), 
	hyprun(Initial, Machine, Max, hyp(N), Initial, Final, 0, [], Stat), !, 
 	checkstatus(Stat, Initial, Final, FirstPos, NextPos, Status),  
        Hops is 1, Ones is 0, 
	true.

induction(Machine, Mode, Prev, [state(L,S,[I|R])|Rest], Ones, Hops, Status) :-
	Rest \== [], append(Prev, [state(L,S,[I|R])], NewPrev), !, % try next state.
	induction(Machine, Mode, NewPrev, Rest, Ones, Hops, Status). 

find_hypothesis(state(L1,S,[I|R1]), _P1, Rest, _State, N, Initial, Final, NextPos) :-
	extract_hypothesis(state(L1,S,[I|R1]), Rest, _State, N, Initial, Final, NextPos),
	case(0, Initial, Zero), 
	case(1, Initial, One),  
	case(2, Initial, Two),  
	member(Zero, [state(L1,S,[I|R1])|Rest]),
	member(One, Rest), 
	member(Two, Rest), % require three instances of the hypothesis to be in the list
	true. 


extract_hypothesis(state(L1,S,[I|R1]), Rest, state(L2, S, [I|R2]), N, Initial, Final, RealPos) :-
	Rest \== [], 
	% Find first matching progression ... 
	memberpos2([], state(L2, S, [I|R2]), Pos2, Rest, _Earlier, Later), 
	compact_state(state(L1, S, [I|R1]), state(CL1, S, CR1)), 
	most_compact_state(state(L2, S, [I|R2]), state(CL2, S, CR2)), 
	pad(CL1, CL2, PL), pad(CR1, CR2, PR), 
	same_shape(PL, CL2), same_shape(PR, CR2), 
	member(state(L3, S, [I|R3]), Later), 
	RealPos is Pos2 + 1, 
	most_compact_state(state(L3, S, [I|R3]), state(CL3, S, CR3)), 
	pad(CL1, CL3, PL1), 
	pad(CR1, CR3, PR1), 
	pad(CL2, CL3, PL2), pad(CR2, CR3, PR2), 
	progressive(PL1, PL2, CL3, LDiffs), 
	progressive(PR1, PR2, CR3, RDiffs), 
	find_states(S, PL1, LDiffs, PR1, RDiffs, Initial, Final),
	true. 

pattern(Pattern, [State|List], State) :-
	same_pattern(State, Pattern). 
pattern(Pattern,  [State|List], State) :-
	pattern(Pattern, List, State). 
	
setdiffs(List, Pre, Post, New, Diffs) :-
	Pre \= [], Post \= [],
	New = [tape(Pre,0), tape(List,1), tape(Post,0)], 
	Diffs = [m(1,1),m(0,0),m(1,1)]. 

setdiffs(List, Pre, Post, New, Diffs) :-
	Pre \= [], Post == [],
	New = [tape(Pre,0), tape(List,1)], 
	Diffs = [m(1,1),m(0,0)]. 

setdiffs(List, Pre, Post, New, Diffs) :-
	Pre == [], Post \= [],
	New = [tape(List,1), tape(Post,0)], 
	Diffs = [m(0,0),m(1,1)]. 

setdiffs(List, Pre, Post, New, Diffs) :-
	Pre == [], Post == [],
	New = [tape(List,1)], 
	Diffs = [m(0,0)]. 

pad([], [], []).
pad([I1|R1], [I2|R2], [I1|Rest]) :-
	is_input(I1), is_input(I2),
	I1 == I2, 
	pad(R1, R2, Rest). 
pad([I1|R1], [I2|R2], [I2|Rest]) :-
	is_input(I1), is_input(I2),
	I1 \== I2, 
	pad([I1|R1], R2, Rest). 
pad([tape(I1,N1)|R1], [tape(I2,_)|R2], [tape(I1,N1)|Rest]) :-
	I1 == I2,
	pad(R1, R2, Rest), !. 
pad([tape(I1,N1)|R1], [tape(I2,_)|R2], [tape(I2,0)|Rest]) :-
	I1 \== I2,
	pad([tape(I1,N1)|R1], R2, Rest), !. 
pad([], [tape(I2,_)|R2], [tape(I2,0)|Rest]) :-
	pad([], R2, Rest). 

same_shape([], []).
same_shape([tape(I,N1)|R1], [tape(I,N2)|R2]) :-
	N2 >= N1, 
	same_shape(R1, R2). 

progressive([], [], [], []).
progressive([tape(I,N1)|R1], [tape(I,N2)|R2], [tape(I,N3)|R3], [m(K,L)|Rest]) :-
	N3 > N2, N2 > N1, 
	0 is (N3-N2) mod (N2-N1),
	K is (N3-N2) // (N2-N1), 
	L is N2 - K*N1,
	progressive(R1, R2, R3, Rest). 
progressive([tape(I,N1)|R1], [tape(I,N2)|R2], [tape(I,N3)|R3], [m(0,0)|Rest]) :-
	((N2 = N1);(N2 > N1, N2 = N3)), 
	progressive(R1, R2, R3, Rest). 

find_states(S, L1, LDiffs, R1, RDiffs, state(ILeft, S, l, IRight), state(FLeft, S, _Dir, FRight)) :-
 	set_tape(L1, LDiffs, IL1, FL1), leftversion(IL1, IL), leftversion(FL1, FL), 
 	set_tape(R1, RDiffs, IR, FR), 
        flatten(IL, ILeft), flatten(FL, FLeft), flatten(IR, IR1), flatten(FR, FR1), 
 	state(ILeft, S, IR1) \== state(FLeft, S, FR1),
 	contains_variable(ILeft, IR1), 
	checkstate(IR1, IRight), checkstate(FR1, FRight),
	true.

find_states2(S, L1, LDiffs, R1, RDiffs, state(ILeft, S, l, IRight), state(FLeft, S, _Dir, FRight)) :-
 	set_tape(L1, LDiffs, IL1, FL1), leftversion(IL1, ILeft), leftversion(FL1, FLeft), 
 	set_tape(R1, RDiffs, IR, FR), 
 	state(ILeft, S, IR) \== state(FLeft, S, FR),
 	contains_variable(ILeft, IR), 
	checkstate(IR, IRight), checkstate(FR, FRight),
	true.

set_tape(Tape, [], Tape, Tape)  :- !. 
set_tape([tape(I,N)|Rest1], [m(0,0)|Rest2], [tape(I,N)|Rest3], [tape(I,N)|Rest4]) :- 	
	!, 
	set_tape(Rest1, Rest2, Rest3, Rest4). 

set_tape([tape(I,N)|Rest1], [m(K,L)|Rest2], Initial, Final) :- 	
	K = 1, !, 
	set_tape(Rest1, Rest2, Rest, Others),
	number(I, L, Incr), 
	append([tape(I,N)], [tape(Incr,v(X,0,N,K,L))], Rest, Initial), 
	Num is N + L,
	append([tape(I,Num)], [tape(Incr,v(X,0,N,K,L))], Others, Final).

set_tape([tape(I,N)|Rest1], [m(K,L)|Rest2], Initial, Final) :- 	
	K > 1, !, 
	set_tape(Rest1, Rest2, Rest, Others),

	append([tape(I,N)], [tape(I,v(X,0,N,K,L))], Rest, Initial), 
	number(I, K, T1), Num is K*N + L,
	append([tape(I,Num)], [tape(T1,v(X,0,N,K,L))], Others, Final).

number(_, 0, []).
number(Item, 1, Item).
number(Item, K, KItems) :-
	K > 1, K1 is K-1,
	number(Item, K1, Rest),
        append(Item, Rest, KItems).

contains_variable(L, _) :- member(tape(_,v(_,_,_,_,_)), L), !. 
contains_variable(_, R) :- member(tape(_,v(_,_,_,_,_)), R), !.  

pivot(small,20). % Small bound for history to search for progression in pivotal states. 
pivot(large,50). % Large bound for history to search for progression in pivotal states. 
nonpivot(small,20). % Small bound for history to search for progression in non-pivotal states. 
nonpivot(large,50). % Large bound for history to search for progression in non-pivotal states. 
hypmax(small,30). % Maximum number of steps taken in the hypothetical engine. Need to experiment with this value.
hypmax(large,300). % Maximum number of steps taken in the hypothetical engine. Need to experiment with this value --- 298 is known. 
smallhist(200). % Small bound for history for dizzy duck search.  
largehist(1000). % Large bound for history for dizzy duck search.  Biggest so far is 603.
switchmax(15). % Maximum number of switches allowed in one evaluation. 
maxsteps(1000). % Maximum steps for termination attempt. 

%% Checking routines.

deterministic(M) :- \+ nondeterministic(M).

nondeterministic(M) :-
	member(t(S, I, O1, D1, NS1), M),
	member(t(S, I, O2, D2, NS2), M),
	((O1 \== O2); (D1 \== D2); (NS1 \== NS2)).

nonmonotonic(M) :- member(t(_, 1, 0, _, _), M),!.
monotonic(M) :- \+ nonmonotonic(M).

eager([]).
eager([t(_, _, 1, _, _)|Rest]) :- eager(Rest).

blanky(M) :- member(t(_, 0,0,_,_), M).

redundant(M) :- equivalent(M, _, _).

% Succeeds if states S and T in M are equivalent in Marxen's sense
equivalent(M, S, T) :- 
	pair(M, t(S,0,Db,Ob,Nsb), t(S,1,D1,O1,Ns1), t(T,0,Db, Ob, Ntb), t(T,1,D1, O1, Nt1)), 
	S \== T,  
	samestate(S,T,Nsb, Ns1, Ntb, Nt1). 

pair(Arg1, t(S,0,Db,Ob,Nsb), t(S,1,D1,O1,Ns1), t(T,0,Db, Ob, Ntb), t(T,1,D1, O1, Nt1)) :-
	Arg1 = [t(S,0,Db,Ob,Nsb)|Temp1], Temp1 = [t(S,1,D1,O1,Ns1)|M],
	member(t(T,0,Db, Ob, Ntb), M), 
	member(t(T,1,D1, O1, Nt1), M).

pair(Arg, T1, T2, T3, T4) :-
	Arg = [_|Temp], Temp = [_|M], 
	pair(M, T1, T2, T3, T4). 
	
samestate(S,T,Nsb, Ns1, Nsb, Ns1) :-
	S \== Nsb, S \== Ns1, T \== Nsb, T \== Ns1. 

samestate(S,T,Nsb, Ns1, Ntb, Ns1) :-
	Nsb \== Ntb, Nsb == S, Ntb == T.  

samestate(S,T,Nsb, Ns1, Nsb, Nt1) :-
	Ns1 \== Nt1, Ns1 == S, Nt1 == T.   

unidirect(M) :- directions(M, 0, _R). % _R > 0 due to first transition.

directions(M, L, R) :-
	  dir(M, 0, 0, L, R).

dir([], L, R, L, R).
dir([t(_,_,_,l,_)|Rest], L, R, NewL, NewR) :-
	  L1 is L+1,
	  dir(Rest, L1, R, NewL, NewR).
dir([t(_,_,_,r,_)|Rest], L, R, NewL, NewR) :-
	  R1 is R+1,
	  dir(Rest, L, R1, NewL, NewR).

































most_compact_state(state(Left, S, Right), state(CLeft, S, CRight)) :-
	findall(tapes(NewLeft,NewRight), strict_compact_state(state(Left, S, Right),state(NewLeft,S,NewRight)), States), !, 
	shortest_state(1000, tapes([], []), States, tapes(CLeft, CRight)). 

shortest_state(_, T, [], T) :- !. 
shortest_state(Min, T, [tapes(Left,Right)|States], Shortest) :- 	
	tapesize(Left,L), tapesize(Right,R), Size is L+R, 
	smaller(Min, T, Size, tapes(Left,Right), NewMin, Tape), !, 
	shortest_state(NewMin, Tape, States, Shortest).

smaller(Size1, tapes(L1,R1), Size2, tapes(_L2,_R2), Size1, tapes(L1,R1)) :- Size1 < Size2, !. 
smaller(Size1, tapes(_L1,_R1), Size2, tapes(L2,R2), Size2, tapes(L2,R2)) :- Size1 > Size2, !. 
smaller(Size1, tapes(L1,R1), Size2, tapes(L2,R2), Size1, tapes(L1,R1)) :- 
	Size1 = Size2,
	length(L1,L11), length(R1,R11), Length1 is L11+R11, 
	length(L2,L22), length(R2,R22), Length2 is L22+R22, 
	Length1 =< Length2, !. 
smaller(Size1, tapes(L1,R1), Size2, tapes(L2,R2), Size2, tapes(L2,R2)) :- 
	Size1 = Size2,
	length(L1,L11), length(R1,R11), Length1 is L11+R11, 
	length(L2,L22), length(R2,R22), Length2 is L22+R22, 
	Length1 > Length2. 

tapesize([], 0) :- !.
tapesize([tape(I,_)|Rest], Size) :-
	length(I, S), 
	tapesize(Rest, S1), Size is S1 + S. 

strict_compact_state(state(Left, S, Right), state(CLeft, S, CRight)) :-
	strict_compact(Left, CLeft), 	strict_compact(Right, CRight),
	true. 


compact_state(state(Left, S, Right), state(CLeft, S, CRight)) :-
	compact(Left, CLeft), 	compact(Right, CRight),
	true. 

compact_state2(state(Left, S, Right), state(CLeft, S, CRight)) :-
	compact(Left, CLeft), 	compact(Right, CRight),!, 
	true. 

compact(List, NewList) :-
	delete_trail_blanks(List, L), 
	pick(I, L),
	compactify([], tape(I,0), List, NewList), true. 
	% sanity(NewList), !.
compact(L,L).

strict_compact([], []).
strict_compact(List, NewList) :-
	List \== [], 
	delete_trail_blanks(List, L), 
	pick(I, L),
	compactify([], tape(I,0), List, NewList), true. 
	% sanity(NewList), !.

% sanity(L) :- member(tape(I, Num), L), Num >= 3. 

compactify(Prev, tape(I,Num), [], List) :-
	append(Prev, [tape(I,Num)], List). 
compactify(Prev, tape(I,Num), Rest, List) :-
	Rest \== [], 
	append(I, Rest1, Rest), 
	N1 is Num + 1, 
	compactify(Prev, tape(I, N1), Rest1, List).
compactify(Prev, tape(I,Num), Rest, List) :-
	Rest \== [], 
	\+ append(I, _, Rest), % format("Prev is ", []), display(Prev), 
	append(Prev, [tape(I,Num)], NewPrev), % format(" Got ", []), display(I), format("^~d ", [Num]), 
	pick(NewI, Rest), % format("Picked ", []), display(NewI), format(" Rest is ", []), display(Rest), nl, 
	compactify(NewPrev, tape(NewI,0), Rest, List).
compactify(Prev, tape(I,Num), Rest, List) :-
	Rest \== [], 
	\+ append(I, _, Rest), % format("Prev is ", []), display(Prev), 
	\+ pick(_, Rest), 
	Rest = [Next|Rest1], append(Prev, [tape(I,Num)], NewPrev), % format(" Got ", []), display(I), format("^~d ", [Num]), 
	% format("Picked ", []), display(NewI), format(" Rest is ", []), display(Rest), nl, 
	compactify(NewPrev, tape([Next],1), Rest1, List).

pick(I, List) :-
	append(I, _Rest, List), %%% append(I, Rest1, Rest), append(I, _, Rest1), % I must occur three times ...
	length(I, N), N > 0, N =< 4. % or some reasonable maximum chunk

memberpos(X, 1, [X|_]).
memberpos(X, N, [_|R]) :- memberpos(X, M, R), N is M+1. 

memberpos2(Prev, X, 1, [X|Later], Prev, Later). 
memberpos2(Prev, X, N, [Y|R], Earlier, Later) :- 
	append(Prev, [Y], NewPrev), 
	memberpos2(NewPrev, X, M, R, Earlier, Later), N is M+1. 

case(N, state(Left, S, _Dir, Right), state(NLeft, S, NRight)):-
	orienttape(left, Left, L), 
	case1(N, L, NLeft),
	case1(N, Right, NRight).

case1(_N, [], []).
case1(N, [X|Rest], [X|Case]) :-
	% member(X, [0,1]), 
	is_input(X), 
	case1(N, Rest, Case).
case1(N, [tape(In,_)|Rest], NewCase) :-
	case1(N, Rest, Case),
	items(N, In, Ins),
	append(Ins, Case, NewCase). 

items(0, _, []).
items(N, I, Is) :-
	N > 0, N1 is N - 1, 
	items(N1, I, Ins),
	append(I, Ins, Is). 

checkstatus(halts, _, _, _, _, halts) :- !. 
checkstatus(halts(_), _, _, _, _, halts) :- format("Arf! Hypothetical halted~n", []), !. 
checkstatus(target(U,H), I, F, P1, P2, loops(induction(p(U,H), pos(P1,P2), I, F))) :- !. 
checkstatus(going, I, F, P1, P2, hyp(induction(pos(P1,P2), I, F))) :- !. 


get_all(_S, _I, [], []). 
get_all(S, I, [state(Left, S1, Right)|Rest], [state(Left, S1, Right)|Remain]) :-
	S == S1, Right = [tape(I,_)|_], 
	get_all(S, I, Rest, Remain). 
get_all(S, I, [state(_Left, S1, Right)|Rest], Remain) :-
	\+ (S == S1, Right = [tape(I,_)|_]),
	get_all(S, I, Rest, Remain).
 
print_history([]).
print_history([S|Rest]) :-
	print_state(S), 
	% format(" : ", []), most_compact_state(S, S1), print_state(S1), 
        nl, !, print_history(Rest).

print_state(state(Left, S, Right)) :-
	reverse(Left, L), display(L), format("{~k}", [S]), display(Right), format("  ", []). %  nl.
print_state(state(Left, S, Dir, Right)) :-
	reverse(Left, L), display(L), format("{~k~k}", [S,Dir]), display(Right), format("  ", []). %  nl.

print_hyps([]).
print_hyps([hyp(induction(S1,S2))|Rest]) :-
	print_state(S1), format(" -> ", []), print_state(S2), nl, !, print_hyps(Rest).
print_hyps([hyp(induction(pos(P1,P2),S1,S2))|Rest]) :-
	format("(~d,~d): ", [P1,P2]), print_state(S1), format(" -> ", []), print_state(S2), nl, !, print_hyps(Rest).

attempt_proof(Machine, Initial, Final, Status) :-
	hyprun(Initial, Machine, 100, Initial, Final, 0, [], S), 
 	checkstatus(S, Initial, Final, Status), !. 
attempt_proof(_Machine, Initial, Final, hyp(induction(Initial, Final))).

set_states(S, L1, LDiffs, R1, RDiffs, state(ILeft, S, l, IRight), state(FLeft, S, _Dir, FRight)) :-
	set(L1, LDiffs, IL, FL), leftversion(IL, IL1), leftversion(FL, FL1), % format("Left Done~n", []), 
	% set(L1, LDiffs, ILeft, FLeft), 
	% format("IL, FL: ", []), display(IL), format(" ", []), display(FL), nl, 
        % reverse(IL, IL1), reverse(FL, FL1), 
	% format("IL1, FL1: ", []), display(IL1), format(" ", []), display(FL1), nl, 
	% format("Right stuff: ", []), display(R1), format(" ", []), display(RDiffs), nl, 
	set(R1, RDiffs, IR, FR), % format("Right Done~n", []), 
	%% collapseblanks(FL1,FLeft), collapseblanks(FR1,FRight),
	% format("ILeft, IRight: ", []), display(ILeft), format(" ", []), display(IRight), nl,    
        % format("FLeft, FRight: ", []), display(FLeft), format(" ", []), display(FRight), nl, 
        flatten(IL1, ILeft), flatten(FL1, FLeft), flatten(IR, IR1), flatten(FR, FR1), 
	% format("ILeft, IR1: ", []), display(ILeft), format(" ", []), display(IR1), nl,    
        % format("FLeft, FR1: ", []), display(FLeft), format(" ", []), display(FR1), nl, 
	% state(IL2, S, IR1) \== state(FL2, S, FR1),
	state(ILeft, S, IR1) \== state(FLeft, S, FR1),
	checkstate(IR1, IRight), checkstate(FR1, FRight), 
	% format("ILeft, IRight: ", []), display(ILeft), format(" ", []), display(IRight), nl,    
        % format("FLeft, FRight: ", []), display(FLeft), format(" ", []), display(FRight), nl, 
	%% reverse(IL2, ILeft), reverse(FL2, FLeft), 
	% format("States set~n", []),
	% single(ILeft, IRight), % reject any "double" conjectures (at least for now!)
	true. 

set(Tape, [], Tape, Tape) :- !. 
set(Tape, Diffs, I, F) :-
	Diffs \== [], 
	set1(Tape, Diffs, I, F),!.
set(Tape, Diffs, I, F) :-
	Diffs \== [], 
	reverse(Diffs, RD),
	set1(Tape, RD, I, F),!.

set1(I, [], I, I) :- !. 
set1(Init, Diff, IRight, FRight) :-
	Diff \== [], \+ member(tape(_,_), Diff), 
	% format("Expanding ...~n", []), 
	expand(Diff, 5, NewDiff), length(NewDiff, L), L < 6, % Limit size of these things!
	append(Init, [tape(NewDiff, X)], IRight),
	append(Init, NewDiff, [tape(NewDiff,X)], FRight).

set1([tape(I,N)|Rest1], [tape(I,Diff)|Rest2], [tape(I,N)|Rest3], [tape(I,N)|Rest4]) :- 	
	Diff is 0, !, 
	set1(Rest1, Rest2, Rest3, Rest4). 
% set1([El|Rest1], [tape(I,Diff)|Rest2], [tape(I,N)|Rest3], [tape(I,N)|Rest4]) :- 	
% 	(El == 1; El == b), 
% 	Diff is 0, !, 
% 	set1(Rest1, Rest2, Rest3, Rest4). 

set1([tape(I,N)|Rest1], [tape(I,Diff)|Rest2], Initial, Final) :- 	
	Diff > 0,!, 
	addextra(tape(I,N1), Diff, Element), 
	% simplify(I, Diff, NewI), 
	% format("Diff is ~d, I is ~k "), display(I), nl, 
	expand(I, Diff, NewI), 
	% format("NewI is ~k ", []), display(NewI), nl, 
        % N2 .=. N1 + Diff,
	% N1 .>=. N,
	!, 
	set1(Rest1, Rest2, Rest3, Rest4), % orient(Dir, Element, El), 
	simplify(I,N,Init), % orient(Dir, Init, In), 
	append(Element, Init, Temp), 
	append(Init, [tape(NewI,N1)], Rest3, Initial), 
	append(Temp, [tape(NewI,N1)], Rest4, Final),
	% append(Init, Rest3, NewRest3),  % orient(Dir, NewI, NI), 
	% append([tape(NewI,N1)], Temp, Rest4, Final),
	true. 

% set1([El|Rest1], [tape([El],Diff)|Rest2], Initial, Final) :- 	
% 	(El == 1; El == b), 
% 	Diff > 0,!, 
% 	addextra(tape([El],N1), Diff, Element), 
% 	% simplify(I, Diff, NewI), 
% 	% format("Diff is ~d, I is ~k "), display(I), nl, 
% 	expand([El], Diff, NewI), 
% 	% format("NewI is ~k ", []), display(NewI), nl, 
%         % N2 .=. N1 + Diff,
% 	% N1 .>=. N,
% 	!, 
% 	set1(Rest1, Rest2, Rest3, Rest4), % orient(Dir, Element, El), 
% 	simplify([El],1,Init), % orient(Dir, Init, In), 
% 	append(Element, Init, Temp), 
% 	append(Init, [tape(NewI,N1)], Rest3, Initial), 
% 	append(Temp, [tape(NewI,N1)], Rest4, Final),
% 	% append(Init, Rest3, NewRest3),  % orient(Dir, NewI, NI), 
% 	% append([tape(NewI,N1)], Temp, Rest4, Final),
% 	true. 

set1([tape(I1,N)|Rest1], [tape(I,Diff)|Rest2], [tape(NewI,N1)|Rest3], Final) :- 	
	I1 \== I, Diff > 0,!, 
	addextra(tape(I,N1), Diff, Element), 
	% format("Diff is ~d, I is ~k "), display(I), nl, 
	% simplify(I, Diff, NewI), 
	expand(I, Diff, NewI), 
	% format("NewI is ~k ", []), display(NewI), nl, 
	!, 
	set1([tape(I1,N)|Rest1], Rest2, Rest3, Rest4), % orient(Dir, Element, El), 
	append(Element, [tape(NewI,N1)], Rest4, Final).

set1([], [tape(I,Diff)|Rest2], [tape(NewI,N1)|Rest3], Final) :- 	
	Diff > 0,!, 
	addextra(tape(I,N1), Diff, Element), 
	% format("Diff is ~d, I is ~k "), display(I), nl, 
	% simplify(I, Diff, NewI), 
	expand(I, Diff, NewI), 
	% format("NewI is ~k ", []), display(NewI), nl, 
	!, 
	set1([], Rest2, Rest3, Rest4), % orient(Dir, Element, El), 
	append(Element, [tape(NewI,N1)], Rest4, Final).

single(Left, Right) :-
	append(Left, Right, Tape), 
	member(tape(X, Y), Tape), var(Y), 
	delete(Tape, tape(X,Y), Tape1),
	\+ (member(tape(_W,Z), Tape1), var(Z)). 

orienttape(_Dir, [], []) :- !. 
orienttape(Dir, [Element|Rest], [Element|Tape]) :- 
	Element \= tape(_,_), !, 
	orienttape(Dir, Rest, Tape). 
orienttape(Dir, [tape(I,N)|Rest], [tape(NewI,N)|Tape]) :- 
	!, 
	orient(Dir, I, NewI), 
	orienttape(Dir, Rest, Tape). 

orient(right, X, X) :- !. 
orient(left, X, Y) :- reverse(X,Y). 

leftversion(Tape, Left) :-
	leftvar(Tape, Left).

leftvar([], []). 
leftvar([X|Rest], [X|Other]) :-
	% member(X, [b,1]),
	is_input(X), 
	leftvar(Rest, Other).
leftvar([tape(I,X)|Rest], [tape(I,X)|Other]) :-
	int(X), 
	leftvar(Rest, Other).
leftvar([tape(I,X)|Rest], [tape(IL,X)|Other]) :-
	X = v(_,_,_,_,_), 
	reverse(I, IL), 
	leftvar(Rest, Other).

simplify(I, 1, I).
simplify(I, D, NewI) :-
	D > 1, D1 is D - 1, !, 
	simplify(I, D1, Rest),
	append(I, Rest, NewI). 

expand(T, N, T) :- N > 0. 
expand(T, N, NewT) :-
	N > 1,
	N1 is N - 1,
	expand(T, N1, NT),
	append(T, NT, NewT).	

addextra(_X, 0, []).
addextra(tape(I,N1), Diff, Element) :-
	Diff > 0, D1 is Diff - 1,
	addextra(tape(I,N1), D1, Rest),
	append(Rest, I, Element). 

split2comp(Prev, S1, I1, Prev, state(L2,S2,[tape(I2,Num2)|R2]), List, [state(L2,S2,[tape(I2,Num2)|R2])|List]) :-
	S1 == S2, I1 == I2.
split2comp(Prev, S1, I1, Earlier, State, Later, [state(L2,S2,[tape(I2,Num2)|R2])|List]) :- 
% 	(S1 \== S2; (S1 == S2,I1 \== I2)), 
	append(Prev, [state(L2,S2,[tape(I2,Num2)|R2])], NewPrev),
	split2comp(NewPrev, S1, I1, Earlier, State, Later, List).

progression([], [], [], []) :- !. 
progression(T, [], T, T) :- T \== [], !. 
progression(T, T, [], T) :- T \== [], !. 
progression(T1, T2, D, Init) :- 
	T2 \== [], \+ member(tape(_,_), T1), \+ member(tape(_,_), T2), 
	append(T, B2, T2), append(B1, T1, T), %T2 = B1.T1.B2
	filter([tape(B1,1), tape(T1,0), tape(B2, 1)], D, Init), 
	true,!. 
progression(T1, T2, D, T1) :- progress(T1, T2, D). 


% progression(T1, T2, D) :- progress(T1,T2,D), !. 
% % progression(T1, T2, D) :- reverse(T2,T3), progress(T1,T3,D3), reverse(D3,D). 
% 
% progress([], [], []) :- !. 
% % progress([], T, T) :- T \== [], !.
% % progress(T1, T2, T3) :- T2 \== [], append(T1, T3, T2), !.
% progress(T, [], T) :- T \== [], !.
% progress(T1, T2, D) :-
% 	T2 \== [], 
% 	append(T, B2, T2), append(B1, T1, T),!, 
% 	filter([tape(B1,1), tape(T1,0), tape(B2, 1)], D), 
% 	true. 

progress([], [], []).  
progress([tape(I1,N1)|Rest1], [tape(I2,N2)|Rest2], [tape(I1,Diff)|Rest3]) :-
	% format("Tapes are ", []), display([tape(I1,N1)|Rest1]), display([tape(I2,N2)|Rest2]), nl, 
	I1 == I2, % \+ allblank(I1), % N1 .=<. N2, Diff .=. N2 - N1, 
	N1 =< N2, Diff is N2 - N1, 
	progress(Rest1, Rest2, Rest3).
% progress([tape(I1,N1)|Rest1], [tape(I2,N2)|Rest2], [tape(I1,0)|Rest3]) :-
% 	% format("Tapes are ", []), display([tape(I1,N1)|Rest1]), display([tape(I2,N2)|Rest2]), nl, 
% 	I1 == I2, allblank(I1), % N1 .=<. N2, Diff .=. N2 - N1, 
% 	progress(Rest1, Rest2, Rest3).
% progress(T1, T2, [tape(T3,1)]) :-
% 	T1 \== tape(_,_), T2 \== tape(_,_), 
% 	append(T1, T3, T2).

filter([tape(B1,1), tape(T1,0), tape(B2, 1)], [tape(B1,1), tape(T1,0), tape(B2, 1)], [tape(T1,1)]) :-
	B1 \== [], B2 \== []. 
filter([tape(B1,1), tape(T1,0), tape(B2, 1)], [tape(T1,0), tape(B2, 1)], [tape(T1,1)]) :-
	B1 = [], B2 \== [].
filter([tape(B1,1), tape(T1,0), tape(B2, 1)], [tape(B1,1), tape(T1,0)], [tape(T1,1)]) :-
	B1 \== [], B2 = [].

% filter([], []).
% filter([tape(I,X)|Rest], [tape(I,X)|Rest1]) :-
% 	I \== [], 
%	filter(Rest, Rest1). 
% filter([tape(I,X)|Rest], Rest1) :-
% 	I = [], 
% 	filter(Rest, Rest1). 

allblank([0]) :- !. 
allblank([0|Rest]) :- allblank(Rest). 

trim([], []). 
trim([0], []). 
trim([1], [1]). 
trim([tape(I,X)], [tape(I,X)]) :- \+ allblank(I).
trim([tape(I,_X)], []) :- allblank(I).
trim(T, T1) :-
	length(T, L), L > 1,
	trim1(T, T1), 
trim1([], []).
trim1([tape(I,_X)|Rest], Result) :-
	allblank(I), 
	trim1(Rest, Result). 
trim1([tape(I,X)|Rest], [tape(I,X)|Result]) :-
	\+ allblank(I), 
	trim1(Rest, Result). 



% ?- looping(1,M,_,_), sequence2(M, M, 1, [], t(1,b,1,r,2), Seq), display(Seq), nl, fail.
% [t(2,1,1,l,2),t(2,b,b,r,3),t(3,b,1,l,1),t(3,b,1,l,1)]
% [t(2,1,1,l,2),t(2,b,b,r,3),t(3,1,1,l,4),t(4,b,1,r,1),t(4,b,1,r,1)]
% [t(2,1,1,l,2),t(2,b,b,r,3),t(3,1,1,l,4),t(4,1,1,r,h),t(4,1,1,r,h)]