program torpa(input,output); { This is the source of the Pascal version of the program TORPA for proving termination of string rewriting. This code has been written by Hans Zantema in 2003 - 2006. This version accepts the TPDB format and follows the guidelines of the competition of termination tools. It also accepts plain format. This is version 1.5 from February, 2006. For documentation see http://www.win.tue.nl/~hzantema/torpa.html } const maxrule = 1000; maxnaam = 100; maxresult = 1000; maxlen = 20; maxautom = 1000; maxloop = 100; type trs = record l,r : array[1..maxrule,1..maxlen] of byte; hib,naamhib : integer; strict : array[1..maxrule] of boolean; unlab : array[1..maxrule] of integer; naam : array[1..maxnaam] of string; end; var rtel, power, traftel : integer; mb, matr, sn, loopfound, pow : boolean; resul : array[1..maxresult] of string; function inttostr(i : integer): string; var n : integer; s : string; procedure schr(j : integer); begin if j = 0 then s := s + '0'; if j = 1 then s := s + '1'; if j = 2 then s := s + '2'; if j = 3 then s := s + '3'; if j = 4 then s := s + '4'; if j = 5 then s := s + '5'; if j = 6 then s := s + '6'; if j = 7 then s := s + '7'; if j = 8 then s := s + '8'; if j = 9 then s := s + '9'; end; begin s := ''; n := i; if n > 99 then begin schr(n div 100); n := n mod 100; end; if (s <> '') or ((n div 10) > 0) then schr(n div 10); schr(n mod 10); inttostr := s; end; function schrijfregel(var rr:trs;i:integer):string; var s : string; j : integer; begin s := ''; j := 1; while rr.l[i,j] <> 0 do begin s := s+rr.naam[rr.l[i,j]]+' '; j := j+1 end; if rr.strict[i] then s := s + ' -> ' else s := s + ' ->= '; j := 1; while rr.r[i,j] <> 0 do begin s := s+rr.naam[rr.r[i,j]]+' '; j := j+1 end; schrijfregel := s; end; procedure schrijf(s : string); begin rtel := rtel + 1; if rtel < maxresult then resul[rtel] := s; end; procedure lees(var rr : trs); var c : char; symt,t: integer; s,nm : string; function nextsym : char; begin if symt < length(s) then symt := symt + 1 else begin readln(s); symt := 1; end; nextsym := s[symt]; if length(s) = 0 then nextsym := ' '; end; {nextsym} procedure leesnaam; begin c := nextsym; while c = ' ' do c := nextsym; if not(c in [',','-',')']) then begin nm := c; c := nextsym; while not(c in [' ',',','-',')']) do begin nm := nm + c; c := nextsym end; if c <> ' ' then begin c := ' '; symt := symt -1 end; end; end; {leesnaam} function nr(c : string) : integer; var i,j : integer; begin with rr do begin i := 0; while i < naamhib do begin i := i + 1; if naam[i] = c then begin j := i; i := naamhib + 1 end; end; if i = naamhib then begin naamhib := naamhib + 1; naam[naamhib] := c; j := naamhib; end; end; nr := j; end; {nr} procedure leesplat; var c : char; j,t: integer; begin with rr do begin while (length(s) > 0) and (s[1] <> ' ') do begin hib := hib + 1; strict[hib] := true; t := 0; j := 1; c := s[j]; while not( c in [' ','-','>','=']) do begin t := t + 1; l[hib,t] := nr(c); j := j+1; c := s[j]; end; l[hib,t+1] := 0; while (c in [' ','-','>','=']) do begin if c = '=' then strict[hib] := false; j := j+1; c := s[j]; end; t := 0; while not( c in [' ','e']) do begin t := t + 1; r[hib,t] := nr(c); j := j+1; if j > length(s) then c := ' ' else c := s[j]; end; r[hib,t+1] := 0; readln(s); end; end; end;{leesplat} begin {lees} with rr do begin readln(s); symt := 0; naamhib := 0; hib := 0; if s[1] <> '(' then leesplat else begin while nextsym <> 'S' do; c := ' '; while c <> ')' do begin leesnaam; if not (c in [',',')']) then begin hib := hib + 1; strict[hib] := true; t := 0; while c <> '-' do begin t := t + 1; l[hib,t] := nr(nm); leesnaam; end; c := nextsym; c := nextsym; if c = '=' then strict[hib] := false; l[hib,t+1] := 0; t := 0; if not(c in [',',')']) then leesnaam; while not(c in [',',')']) do begin t := t + 1; r[hib,t] := nr(nm); leesnaam; end; r[hib,t+1] := 0; end; end; end; end; end; {lees} procedure rev(var rr : trs); var i,j,k,t : integer; begin with rr do begin for i := 1 to hib do begin j := 1; while l[i,j] > 0 do j := j+1; j := j-1; k := 1; while j > k do begin t := l[i,j]; l[i,j] := l[i,k]; l[i,k] := t; j := j-1; k := k+ 1; end; j := 1; while r[i,j] > 0 do j := j+1; j := j-1; k := 1; while j > k do begin t := r[i,j]; r[i,j] := r[i,k]; r[i,k] := t; j := j-1; k := k+ 1; end; end; end; end; {BREAK} procedure matchb(w : trs); var le,buur,goal,sym,lab : array[1..maxautom] of integer; mb, i, j, ehib, ehibbu, nhib, lijsthib, rulenr,startnode, maxe,regelbu : integer; lijst : array[1..50,1..maxlen] of integer; templijst : array[1..maxlen] of integer; ovflow,r : boolean; temp,rfc : trs; procedure maaklijst(node,symnr: integer); {maakt lijst van alle manieren om rfc.l[rulenr] te doorlopen} var edge,i: integer; begin if rfc.l[rulenr,symnr] = 0 then begin lijsthib := lijsthib + 1; if lijsthib >50 then ovflow := true else begin for i := 1 to symnr do lijst[lijsthib,i] := templijst[i]; lijst[lijsthib,symnr] := 0; end end else begin edge := le[node]; while edge > 0 do if sym[edge] = rfc.l[rulenr,symnr] then begin templijst[symnr] := edge; maaklijst(goal[edge],symnr+1); edge := buur[edge]; end else edge := buur[edge]; end; end; {maaklijst} procedure maakpad(lijsti:integer); var minl,endnode,i, maxok,bestj,j,innode, e : integer; procedure zoek(j,node:integer); { zoeknode(j,n) wordt alleen aangeroepen als er een goed pad is van startnode naar n van lengte j-startj} var edge: integer; begin if j > maxok then begin maxok := j; innode := node; end; if rfc.r[rulenr,j] > 0 then begin edge := le[node]; while edge > 0 do begin if (sym[edge] = rfc.r[rulenr,j]) and (lab[edge] = minl) then if (rfc.r[rulenr,j+1] > 0) or (goal[edge] = endnode) then zoek(j+1,goal[edge]); edge := buur[edge]; end; end; end; {zoek} begin {maakpad} minl := 1000; i := 1; while lijst[lijsti,i] > 0 do begin if lab[lijst[lijsti,i]] < minl then minl := lab[lijst[lijsti,i]]; endnode := goal[lijst[lijsti,i]]; i := i+1; end; minl := minl + 1; if minl > mb then mb := minl; maxok := 0; zoek(1,startnode); if rfc.r[rulenr,maxok] > 0 then begin bestj := 0; if rfc.r[rulenr,2] > 0 then for j := 1 to nhib do begin maxok := 0; zoek(2,j); if rfc.r[rulenr,maxok] = 0 then bestj := j; end; if bestj = 0 then {maak pad van startnode naar endnode} begin maxok := 1; e := le[startnode]; while buur[e] > 0 do e := buur[e]; ehib := ehib + 1; if ehib > maxe then ovflow := true; buur[e] := ehib; e := ehib; buur[e] := 0; lab[e] := minl; sym[e] := rfc.r[rulenr,maxok]; while rfc.r[rulenr,maxok+1] > 0 do begin maxok := maxok + 1; nhib := nhib + 1; goal[e] := nhib; ehib := ehib +1; e := ehib; le[nhib] := e; buur[e] := 0; lab[e] := minl; sym[e] := rfc.r[rulenr,maxok]; end; goal[e] := endnode end else {maak edge van startnode naar bestj} begin e := le[startnode]; while buur[e] > 0 do e := buur[e]; ehib := ehib + 1; if ehib > maxe then ovflow := true; buur[e] := ehib; e := ehib; buur[e] := 0; lab[e] := minl; sym[e] := rfc.r[rulenr,1]; goal[e] := bestj; end; end; end; {maakpad} procedure experhs; {expand empty rhs, from w to temp} var erhs : boolean; i,j,k : integer; begin temp := w; erhs := false; for i := 1 to w.hib do if w.r[i][1] = 0 then erhs := true; if erhs then begin schrijf('Expand empty rhs:'); temp.hib := 0; for i := 1 to w.hib do if w.r[i][1] > 0 then begin temp.hib := temp.hib + 1; temp.l[temp.hib] := w.l[i]; temp.r[temp.hib] := w.r[i]; temp.strict[temp.hib] := true; end else for j := 1 to w.naamhib do begin temp.hib := temp.hib + 1; k := 1; while w.l[i][k] > 0 do begin temp.l[temp.hib][k] := w.l[i][k]; k := k+1 end; temp.l[temp.hib][k] := j; temp.l[temp.hib][k+1] := 0; temp.r[temp.hib][1] := j; temp.r[temp.hib][2] := 0; temp.strict[temp.hib] := true; end; for j := 1 to temp.hib do schrijf(' '+schrijfregel(temp,j)); end; end; {experhs} procedure initrfc; var i,j,k,ebu : integer; begin rfc := temp; rfc.naamhib := rfc.naamhib + 1; rfc.naam[rfc.naamhib] := '#'; for i := 1 to temp.hib do begin j := 1; while temp.l[i,j+1] > 0 do begin rfc.hib := rfc.hib + 1; rfc.r[rfc.hib] := temp.r[i]; for k := 1 to j do rfc.l[rfc.hib,k] := temp.l[i,k]; rfc.l[rfc.hib,j+1] := rfc.naamhib; rfc.l[rfc.hib,j+2] := 0; j := j+1; end; end; nhib := 2; ehib := 1; le[2] := 1; goal[1] := 2; lab[1] := 0; sym[1] := rfc.naamhib; buur[1] := 0; le[1] := 2; for i := 1 to temp.hib do begin j := 1; while temp.r[i,j] > 0 do begin ehib := ehib + 1; sym[ehib] := temp.r[i,j]; lab[ehib] := 0; if j = 1 then ebu := ehib; buur[ehib] := 0; if temp.r[i,j+1] = 0 then goal[ehib] := 2 else begin nhib := nhib + 1; goal[ehib] := nhib; le[nhib] := ehib + 1; end; j := j+1; end; if i < temp.hib then buur[ebu] := ehib + 1; end; end; {initrfc} begin {matchb} regelbu := rtel; experhs; for r := false to true do if not sn then begin ovflow := false; mb := 0; if r then rev(temp); initrfc; if pow then maxe := 800 else maxe := 100; ehibbu := 0; while (not ovflow) and (ehibbu < ehib) do begin ehibbu := ehib; for rulenr := 1 to rfc.hib do for startnode := 1 to nhib do begin lijsthib := 0; maaklijst(startnode,1); for i := 1 to lijsthib do if not ovflow then maakpad(i); end; end; if not ovflow then begin sn := true; schrijf(''); if r then schrijf('Reverse every lhs and rhs of the system.'); schrijf('Terminating due to RFC match bound '+inttostr(mb)+','); schrijf('proved by the automaton defined by'); schrijf('initial state = 1, final state = 2, transitions:'); for j := 1 to nhib do begin i := le[j]; while i > 0 do begin schrijf('from '+inttostr(j)+' to '+inttostr(goal[i])+ ', label: '+rfc.naam[sym[i]]+inttostr(lab[i])); i := buur[i]; end; end; end; end; if not sn then rtel := regelbu; end; {matchb} procedure fullmatchb(w : trs); var strip : trs; i,j,k,rbu : integer; begin matchb(w); rbu := rtel; for k := 1 to w.hib do if not sn then with strip do begin rtel := rbu; schrijf(''); strip := w; if l[k,2] > 0 then if r[k,2] > 0 then if l[k,1] = r[k,1] then begin schrijf('Strip first symbol in rule '+inttostr(k)+', yielding the TRS'); i := 1; while l[k,i] > 0 do begin l[k,i] := l[k,i+1]; i := i+1; end; i := 1; while r[k,i] > 0 do begin r[k,i] := r[k,i+1]; i := i+1; end; for i := 1 to hib do schrijf(' '+schrijfregel(strip,i)); matchb(strip); end else begin i := 1; while l[k,i+1] > 0 do i := i+1; j := 1; while r[k,j+1] > 0 do j := j+1; if l[k,i] = r[k,j] then begin l[k,i] := 0; r[k,j] := 0; schrijf('Strip last symbol in rule '+inttostr(k)+', yielding the TRS'); for i := 1 to hib do schrijf(' '+schrijfregel(strip,i)); matchb(strip); end; end; end; if not sn then rtel := rbu; end; {BREAK } procedure rpo(w : trs); var preced : string; revers : boolean; procedure rpo2; var doetmee : array [1..maxnaam] of boolean; gr : array [1..maxnaam,1..maxnaam] of boolean; i,j,n,m,mbu: integer; uitg : boolean; function recpo : boolean; var i,li,ri : integer; ok : boolean; function emb : boolean; var lj,rj:integer; begin lj := li+1; rj := ri; while (w.l[i,lj] > 0) and (w.r[i,rj] > 0) do if w.l[i,lj] = w.r[i,rj] then begin lj:=lj+1; rj:=rj+1 end else lj := lj+1; emb := (w.r[i,rj] = 0); end; function neq(i : integer):boolean; var p : integer; begin p := 1; while (w.l[i,p]>0) and (w.l[i,p] = w.r[i,p]) do p := p+1; neq := (w.l[i,p] <> w.r[i,p]); end; begin {recpo} ok := true; for i := 1 to w.hib do begin li := 1; ri := 1; if w.l[i,li] = 0 then if w.strict[i] or (w.r[i,ri] > 0) then ok := false; if w.strict[i] or neq(i) then while ok and (w.r[i,ri] > 0) and not emb do if w.l[i,li] = w.r[i,ri] then begin li:=li+1;ri:=ri+1; if w.l[i,li] = 0 then ok := false; end else begin if not gr[w.l[i,li],w.r[i,ri]] then preced := preced + ' ' + w.naam[w.l[i,li]]+'>'+ w.naam[w.r[i,ri]]; gr[w.l[i,li],w.r[i,ri]] := true; ri := ri +1; end; end; recpo := ok; end; begin {rpo2} preced := ''; n := w.naamhib; for i := 1 to n do for j := 1 to n do gr[i,j] := false; if recpo then begin for i := 1 to n do doetmee[i] := true; m := n; mbu := n+1; while m < mbu do begin mbu := m; m := 0; for i := 1 to n do if doetmee[i] then begin uitg := false; for j := 1 to n do if doetmee[j] and gr[i,j] then uitg := true; if uitg then m := m+1 else doetmee[i] := false; end; end; if m = 0 then sn := true; end; end; begin {rpo} revers := false; rpo2; if not sn then begin revers := true; rev(w); rpo2; end; if sn then begin schrijf(''); if revers then begin schrijf('Terminating since rev(l) > rev(r) for all rules l -> r'); schrijf('where > is the recursive path order with precedence:'); end else schrijf('Terminating by recursive path order with precedence:'); schrijf(preced); end; end; {rpo} {BREAK } procedure schoon(var t : trs); var used : array[1..maxnaam] of boolean; nieuw : array[1..maxnaam] of integer; i,j : integer; begin for i := 1 to t.naamhib do used[i] := false; for i := 1 to t.hib do begin j := 1; while t.l[i,j] > 0 do begin used[t.l[i,j]] := true; j := j + 1; end; j := 1; while t.r[i,j] > 0 do begin used[t.r[i,j]] := true; j := j + 1; end; end; j := 0; for i := 1 to t.naamhib do if used[i] then begin j := j + 1; nieuw[i] := j; if i <> j then t.naam[j] := t.naam[i]; end; if j < t.naamhib then begin t.naamhib := j; for i := 1 to t.hib do begin j := 1; while t.l[i,j] > 0 do begin t.l[i,j] := nieuw[t.l[i,j]]; j := j+1 end; j := 1; while t.r[i,j] > 0 do begin t.r[i,j] := nieuw[t.r[i,j]]; j := j+1 end; end; end; end; {schoon} {BREAK } function dumelim(var t : trs) : boolean; var res : trs; dum: array[1..maxnaam] of boolean; duml: array[1..maxnaam] of integer; i,j,n : integer; procedure newrule; var k : integer; begin res.hib := res.hib + 1; k := 1; while t.l[i,k] >0 do begin res.l[res.hib,k] := t.l[i,k]; k := k+1; end; res.l[res.hib,k] := 0; res.strict[res.hib] := true; end; {newrule} begin {dumelim} res := t; for i := 1 to t.naamhib do dum[i] := false; for i := 1 to t.hib do if t.r[i,1] > 0 then if t.r[i,2] > 0 then begin j := 2; while t.r[i,j+1] > 0 do begin dum[t.r[i,j]] := true; j := j + 1; end; end; for i := 1 to t.hib do begin j := 1; while t.l[i,j] > 0 do begin dum[t.l[i,j]] := false; j := j + 1; end; end; for i := 1 to t.naamhib do if dum[i] then begin res.naamhib := res.naamhib + 1; res.naam[res.naamhib] := '$'+res.naam[i]; res.naam[i] := res.naam[i]+'$'; duml[i] := res.naamhib; end; if res.naamhib > t.naamhib then begin res.hib := 0; for i := 1 to t.hib do begin newrule; j := 1; n := 1; while t.r[i,j] > 0 do begin res.r[res.hib,n] := t.r[i,j]; if dum[t.r[i,j]] then begin res.r[res.hib,n+1] := 0; newrule; n := 1; res.r[res.hib,n] := duml[t.r[i,j]]; end; j := j+1; n := n+1; end; res.r[res.hib,n] := 0; end; schrijf(''); schrijf('Apply dummy elimination, result:'); for j := 1 to res.hib do schrijf(schrijfregel(res,j)); t := res; dumelim := true; end else dumelim := false; end; {dumelim} {BREAK } function traford(var t : trs):boolean; var i,j,il,ir,it,it2,k,n : integer; found : boolean; res : trs; function overl(a,b:integer): integer; var i,k,cnt :integer; begin cnt := 0; k := 0; i := 1; while t.l[a,i+k] > 0 do begin while (t.l[a,i+k] > 0) and (t.l[a,i+k] = t.l[b,i]) do i := i + 1; if ((t.l[a,i+k] = 0) or (t.l[b,i] = 0)) then cnt := cnt + 1; k := k + 1; i := 1; end; overl := cnt; end; begin {traford} res := t; found := false; for il := 1 to t.hib do for ir := 1 to t.hib do if il <> ir then if not found then begin i := 0; j := 1; while t.r[ir,i+j] > 0 do begin while (t.l[il,j] = t.r[ir,i+j]) and (t.l[il,j] > 0) do j := j + 1; if t.l[il,j] = 0 then if not found then begin k := 0; it := il; for n := 1 to t.hib do begin k := k + overl(n,it); k := k + overl(it,n); end; found := (k = 2); if found then begin it2 := ir; k := 1; while t.r[il,k] > 0 do begin res.r[ir,i+k] := t.r[il,k]; k := k+1; end; while t.r[ir,i+j] > 0 do begin res.r[ir,i+k] := t.r[ir,i+j]; j:=j+1; k := k+1; end; res.r[ir,i+k] := 0; end; end; i := i + 1; j := 1; end; end; if found then begin schrijf(''); schrijf('Reduce rhs: apply rule '+inttostr(it)+ ' on rhs of rule '+inttostr(it2)+', result:'); for j := 1 to res.hib do schrijf(schrijfregel(res,j)); t := res; traftel := traftel + 1; traford := true; end else traford := false; end;{traford} {BREAK } function ggd(a,b:integer):integer; begin if a < b then ggd := ggd(b,a) else if a = b then ggd := a else if b = 0 then ggd := a else if a < b then ggd := ggd(b,a) else ggd := ggd(a-b,b); end; function rrr(var w : trs) : boolean; var doetmee,tien,decr : array[1..maxrule] of boolean; res : array[1..maxrule] of integer; tel,n,i : integer; fd,fdbu,r,term, allstr : boolean; s : string; function ok : boolean; var i,j,tel : integer; found : boolean; begin found := false; j := 1; while j <= w.hib do begin i := 1; tel := 0; while w.l[j,i] > 0 do begin if doetmee[w.l[j,i]] then tel := tel+1; i := i+1 end; i := 1; while w.r[j,i] > 0 do begin if doetmee[w.r[j,i]] then tel := tel-1; i := i+1 end; if tel < 0 then j := w.hib + 2; if tel = 0 then decr[j] := false; if tel > 0 then begin decr[j] := true; found := true; end; j := j+1; end; ok := (j = w.hib + 1) and found; end; {ok} function okran : boolean; var i,j,tel,fac : integer; found : boolean; begin found := false; j := 1; while j <= w.hib do begin i := 1; tel := 0; fac := 1; while w.l[j,i] > 0 do begin if tien[w.l[j,i]] then fac := 4*fac else tel := tel + fac*res[w.l[j,i]]; i := i+1; end; i := 1; fac := 1; while w.r[j,i] > 0 do begin if tien[w.r[j,i]] then fac := 4*fac else tel := tel - fac*res[w.r[j,i]]; i := i+1; end; if tel < 0 then j := w.hib + 2; if tel = 0 then decr[j] := false; if tel > 0 then begin decr[j] := true; found := true; end; j := j+1; end; okran:= (j = w.hib + 1) and found; end; {okran} function ok2 : boolean; var i,j,l0,l1,r0,r1,dir : integer; ovflow,found : boolean; begin found := false; ovflow := false; j := 1; while j <= w.hib do begin i := 1; l1 := 1; l0 := 0; {polynoom: l1*X + l0} if r then dir := 1 else begin while w.l[j,i] > 0 do i := i+1; i := i-1; dir := -1; end; while (i >0) and (w.l[j,i] > 0) do begin if doetmee[w.l[j,i]] then l0 := l0 + 1; if tien[w.l[j,i]] then if l1>10000 then ovflow := true else begin l0 := 10*l0; l1 := 10* l1; end; i := i + dir; end; i := 1; r1 := 1; r0 := 0; if not r then begin while w.r[j,i] > 0 do i := i+1; i := i-1; end; while (i >0) and (w.r[j,i] > 0) do begin if doetmee[w.r[j,i]] then r0 := r0 + 1; if tien[w.r[j,i]] then if r1>10000 then ovflow := true else begin r0 := 10*r0; r1 := 10* r1; end; i := i + dir; end; if ovflow then j := w.hib + 2 else if r1 > l1 then j := w.hib + 2 else if r1 < l1 then begin decr[j] := true; found := true; end else if r0 > l0 then j := w.hib + 2 else if r0 < l0 then begin decr[j] := true; found := true; end else decr[j] := false; j := j+1; end; ok2 := (j = w.hib + 1) and found; end; {ok2} procedure linpol; var b: array[1..50,1..20] of integer; kn,kp,kmin,i1,rhib,rhibbu,histhib,maxtel,maxnoem,i,j : integer; dm : array[1..20] of boolean; ind : array[1..50] of integer; hist : array[1..20] of integer; procedure initlinpol; var i,j,fac : integer; {eerste keer: alle tien[] false; tweede keer: sommige true} begin for i := 1 to w.hib do for j := 1 to w.naamhib do begin b[i,j] := 0; i1 := 1; fac := 1; while w.l[i,i1] > 0 do begin if tien[w.l[i,i1]] then fac := fac*4 else if w.l[i,i1] = j then b[i,j] := b[i,j] + fac; i1 := i1+1; end; i1 := 1; fac := 1; while w.r[i,i1] > 0 do begin if tien[w.r[i,i1]] then fac := fac*4 else if w.r[i,i1] = j then b[i,j] := b[i,j] - fac; i1 := i1+1; end; end; end; {initlinpol} procedure mainlinpol1; var i,j,k,maxsc : integer; klaar : boolean; function score : integer; var t,k,m,s : integer; begin s := 0; for k := 1 to w.hib do begin t := 0; for m := 1 to w.naamhib do t := t + res[m]*b[k,m]; if t < 0 then s := s+t; end; score := s; end; {score} begin {mainlinpol1} klaar := false; for i := 1 to w.naamhib do res[i] := 1; while not klaar do begin maxsc := -1000; for i := 1 to w.naamhib do begin res[i] := res[i] + 1; k := score; if k > maxsc then begin j := i; maxsc := k; end; if k = 0 then klaar := true; res[i] := res[i] - 1; end; res[j] := res[j] + 1; if res[j] = 25 then klaar := true; end; end; {mainlinpol1} procedure mainlinpol; var i,j,k : integer; begin rhib := w.hib; for i := 1 to w.naamhib do begin rhib := rhib + 1; for j := 1 to w.naamhib do b[rhib,j] := 0; b[rhib,i] := 1; end; for i := 1 to w.naamhib do dm[i] := true; for i := 1 to rhib do ind[i] := 0; histhib := 0; i1 := 1; while i1 > 0 do begin kmin := 1000; i1 := 0; for i := 1 to w.naamhib do if dm[i] then begin kn := 0; kp := 0; for j := 1 to rhib do if ind[j] = 0 then if b[j,i] > 0 then kp := kp + 1 else if b[j,i] < 0 then kn := kn + 1; if kn*kp < kmin then begin kmin := kn*kp; i1 := i; end; end; if i1 > 0 then begin rhibbu := rhib; for i := 1 to rhibbu do if ind[i] = 0 then if b[i,i1] < 0 then for j := 1 to rhibbu do if ind[j] = 0 then if b[j,i1] > 0 then if rhib < 48 then begin rhib := rhib + 1; for k := 1 to w.naamhib do b[rhib,k] := b[i,k]*b[j,i1] - b[j,k]*b[i,i1]; ind[rhib] := 0; end; for i := 1 to rhibbu do if ind[i] = 0 then if b[i,i1] <> 0 then ind[i] := i1; dm[i1] := false; histhib := histhib + 1; hist[histhib] := i1; end; end; for i := 1 to w.naamhib do res[i] := 0; res[hist[histhib]] := 1; for i := 1 to rhib do if ind[i] = hist[histhib] then if b[i,ind[i]] < 0 then res[ind[i]] := 0; if histhib > 1 then for i := histhib - 1 downto 1 do begin i1 := hist[i]; maxtel := -1; maxnoem := 0; for j := 1 to rhib do if ind[j] = i1 then if b[j,i1] > 0 then begin kp := 0; for k := 1 to w.naamhib do if k <> i1 then kp := kp + b[j,k]*res[k]; if maxtel*b[j,i1] + maxnoem*kp < 0 then begin maxtel := -kp; maxnoem := b[j,i1] end; end; if maxnoem <> 0 then begin for j := 1 to w.naamhib do res[j] := res[j] * maxnoem; res[i1] := maxtel + 1; kn := 0; for j := 1 to rhib do if ind[j] = i1 then if b[j,i1] < 0 then begin kp := 0; for k := 1 to w.naamhib do kp := kp + b[j,k]*res[k]; if kp < 0 then kn := 1; end; if kn = 1 then res[i1] := res[i1] - 1; end; end; end; {mainlinpol} begin{linpol} initlinpol; mainlinpol1; if okran then fd := true else begin mainlinpol; if okran then fd := true else begin for i := 1 to w.naamhib do begin tien[i] := true; for j := 1 to w.hib do if b[j,i] <> 0 then tien[i] := false; end; initlinpol; mainlinpol; if okran then fd := true; end; end; end; {linpol} function rrr2 : boolean; var A,B,C : array[1..maxrule] of byte; tel,maxtel,i,j,oud,nieuw : integer; aa,bb,cc : byte; fd : boolean; procedure zet(i : integer); begin if random(3) = 0 then B[i] := 1-B[i] else if random(2) = 0 then C[i] := 1-C[i] else begin A[i] := random(3); if A[i] = 2 then A[i] := 4; end; end;{zet} function ok : integer; var i,j,l0,l1,l2,l3,r0,r1,r2,r3,t : integer; found : boolean; procedure fout; begin t := t+1; end; begin {ok} found := false; t := 0; for j := 1 to w.hib do begin i := 1; l1 := 1; l0 := 0; {polynoom: l1*X + l0} l2 := 0; l3 := 0; while w.l[j,i] > 0 do i := i+1; i := i-1; while i>0 do begin l3 := l3 + C[w.l[j,i]]*l1; l2 := l2 + C[w.l[j,i]]*l0; l1 := A[w.l[j,i]]*l1; l0 := A[w.l[j,i]]*l0 + B[w.l[j,i]]; i := i - 1; end; i := 1; r1 := 1; r0 := 0; r2 := 0; r3 := 0; while w.r[j,i] > 0 do i := i+1; i := i-1; while i>0 do begin r3 := r3 + C[w.r[j,i]]*r1; r2 := r2 + C[w.r[j,i]]*r0; r1 := A[w.r[j,i]]*r1; r0 := A[w.r[j,i]]*r0 + B[w.r[j,i]]; i := i - 1; end; if r3 > l3 then fout else if r2 > l2 then fout else if r1 > l1 then fout else if r0 > l0 then fout else if r2 < l2 then begin decr[j] := true; found := true; end else decr[j] := false; end; if not found then t := t + 5; ok := t; end; {ok} begin{rrr2} if r then rev(w); fd := false; tel := 0; if pow then maxtel := 200 else maxtel := 10; while ((not fd) and (tel < maxtel)) do begin for i := 1 to w.naamhib do begin A[i] := 1; B[i] := 0; C[i] := 0; end; oud := ok; j := 1; while (j < 50) and (oud > 0) do begin i := 1 + random(w.naamhib); aa := A[i]; bb := B[i]; cc := C[i]; zet(i); nieuw := ok; if nieuw > oud then begin A[i] := aa; B[i] := bb; C[i] := cc; end else oud := nieuw; j := j+1; end; if oud = 0 then fd := true; tel := tel + 1; end; if fd then begin if r then schrijf('Reverse every lhs and rhs'); schrijf('Choose interpretation in NxN,'); schrijf('order : (x,y) > (x'',y'') <==> x > x'' & y >= y'''); for tel := 1 to w.naamhib do begin s := w.naam[tel] + ' : lambda (x,y) . (x'; if C[tel] = 1 then s := s+'+y'; if A[tel]=0 then s := s+','+inttostr(B[tel])+')' else begin s := s+','; if A[tel] > 1 then s := s+ inttostr(A[tel]); s := s+'y'; if B[tel]>0 then s := s+ '+'+inttostr(B[tel]); s := s+')'; end; schrijf(s); end; end; if r then rev(w); rrr2 := fd; end; {rrr2} begin {rrr} fd := false; for tel := 1 to w.naamhib do doetmee[tel] := true; if ok then fd := true; for n := 1 to w.naamhib do if not fd then begin for tel := 1 to w.naamhib + 1 do doetmee[tel] := false; doetmee[n] := true; if ok then fd := true; end; if not fd then for n := 1 to w.naamhib -1 do for i := n+1 to w.naamhib do if not fd then begin for tel := 1 to w.naamhib + 1 do doetmee[tel] := false; doetmee[i] := true; doetmee[n] := true; if ok then fd := true; end; for n := 1 to w.naamhib do if not fd then begin for tel := 1 to w.naamhib do doetmee[tel] := true; doetmee[n] := false; if ok then fd := true; end; if not fd then for n := 1 to w.naamhib -1 do for i := n+1 to w.naamhib do if not fd then begin for tel := 1 to w.naamhib + 1 do doetmee[tel] := true; doetmee[i] := false; doetmee[n] := false; if ok then fd := true; end; if fd then begin s := 'Choose polynomial interpretation '; for tel := 1 to w.naamhib do if doetmee[tel] then s := s + ' ' + w.naam[tel]; s := s + ': lambda x.x+1'; tel := 1; while tel <= w.naamhib do if doetmee[tel] then tel := tel+1 else begin tel := w.naamhib + 1; s := s + ', rest identity'; end; schrijf(s); end; for r := false to true do if not fd then begin for n := 1 to w.naamhib do if not fd then begin for tel := 1 to w.naamhib do doetmee[tel] := true; doetmee[n] := false; for tel := 1 to w.naamhib do tien[tel] := false; tien[n] := true; if ok2 then begin fd := true; begin if r then schrijf('Reverse every lhs and rhs and choose polynomial interpretation:') else schrijf('Choose polynomial interpretation:'); s := w.naam[n] + ': lambda x.10x, rest lambda x.x+1'; schrijf(s); end; end; end; end; for r := false to true do if not fd then begin for n := 1 to w.naamhib do for i := 1 to w.naamhib do if not fd then if i <> n then begin for tel := 1 to w.naamhib do doetmee[tel] := false; doetmee[i] := true; for tel := 1 to w.naamhib do tien[tel] := false; tien[n] := true; if ok2 then begin fd := true; if r then schrijf('Reverse every lhs and rhs and choose polynomial interpretation:') else schrijf('Choose polynomial interpretation:'); s := w.naam[n] + ': lambda x.10x, ' + w.naam[i] + ': lambda x.x+1'; if w.naamhib >2 then s := s + ', rest identity'; schrijf(s); end; end; end; for r := false to true do if not fd then begin for n := 1 to w.naamhib do for i := 1 to w.naamhib do if not fd then if i <> n then begin for tel := 1 to w.naamhib do doetmee[tel] := true; doetmee[i] := false; doetmee[n] := false; for tel := 1 to w.naamhib do tien[tel] := false; tien[n] := true; if ok2 then begin fd := true; if r then schrijf('Reverse every lhs and rhs and choose polynomial interpretation:') else schrijf('Choose polynomial interpretation:'); s := w.naam[n] + ': lambda x.10x, ' + w.naam[i] + ': identity, rest lambda x.x+1'; schrijf(s); end; end; end; for r := false to true do if not fd then begin for n := 1 to w.naamhib - 1 do for i := n+1 to w.naamhib do if not fd then begin for tel := 1 to w.naamhib do doetmee[tel] := true; doetmee[i] := false; doetmee[n] := false; for tel := 1 to w.naamhib do tien[tel] := false; tien[n] := true; tien[i] := true; if ok2 then begin fd := true; if r then schrijf('Reverse every lhs and rhs and choose polynomial interpretation:') else schrijf('Choose polynomial interpretation:'); s := w.naam[n] + ' and ' + w.naam[i] + ': lambda x.10x, rest lambda x.x+1'; schrijf(s); end; end; end; for r := false to true do if not fd then begin for n := 1 to w.naamhib do if not fd then begin for tel := 1 to w.naamhib do doetmee[tel] := false; doetmee[n] := true; for tel := 1 to w.naamhib do tien[tel] := true; tien[n] := false; if ok2 then begin fd := true; if r then schrijf('Reverse every lhs and rhs and choose polynomial interpretation:') else schrijf('Choose polynomial interpretation:'); s := w.naam[n] + ': lambda x.x+1, rest lambda x.10x'; schrijf(s); end; end; end; for r := false to true do if not fd then begin for n := 1 to w.naamhib - 1 do for i := n+1 to w.naamhib do if not fd then begin for tel := 1 to w.naamhib do doetmee[tel] := false; doetmee[n] := true; doetmee[i] := true; for tel := 1 to w.naamhib do tien[tel] := true; tien[i] := false; tien[n] := false; if ok2 then begin fd := true; if r then schrijf('Reverse every lhs and rhs and choose polynomial interpretation:') else schrijf('Choose polynomial interpretation:'); s := w.naam[n] + ' and ' + w.naam[i] + ': lambda x.x+1, rest lambda x.10x'; schrijf(s); end; end; end; for r := false to true do if not fd then begin for n := 1 to w.naamhib do for i := 1 to w.naamhib do if not fd then if n <> i then begin for tel := 1 to w.naamhib do doetmee[tel] := false; doetmee[i] := true; for tel := 1 to w.naamhib do tien[tel] := true; tien[i] := false; tien[n] := false; if ok2 then begin fd := true; if r then schrijf('Reverse every lhs and rhs and choose polynomial interpretation:') else schrijf('Choose polynomial interpretation:'); s := w.naam[n] + ': identity, ' + w.naam[i] + ': lambda x.x+1, rest lambda x.10x'; schrijf(s); end; end; end; if not fd then if w.naamhib < 20 then if w.hib + w.naamhib < 48 then begin for i := 1 to w.naamhib do tien[i] := false; linpol; for i := 1 to w.naamhib do if not tien[i] then if ((res[i]<0) or (res[i] > 1000)) then fd := false; if fd then begin n := res[1]; for i := 2 to w.naamhib do if not tien[i] then n := ggd(n,res[i]); if n > 1 then for i := 1 to w.naamhib do res[i] := res[i] div n; schrijf('Choose polynomial interpretation '); for tel := 1 to w.naamhib do if tien[tel] then schrijf(w.naam[tel] + ': lambda x.4x') else if res[tel] = 0 then schrijf(w.naam[tel] + ': identity') else schrijf(w.naam[tel] + ': lambda x.x+' + inttostr(res[tel])); end; end; if matr then for r := false to true do if not fd then fd := rrr2; {end of all rrr cases} if fd then begin for i := 1 to w.hib do if decr[i] then schrijf('remove: ' + schrijfregel(w,i)); n := 0; for tel := 1 to w.hib do if not decr[tel] then begin n := n+1; w.l[n] := w.l[tel]; w.r[n] := w.r[tel]; w.strict[n] := w.strict[tel]; w.unlab[n] := w.unlab[tel]; end; w.hib := n; schoon(w); end; sn := true; if w.hib > 0 then for i := 1 to w.hib do if w.strict[i] then sn := false; allstr := true; for i := 1 to w.hib do if not w.strict[i] then allstr := false; fdbu := fd; if allstr and (not fd) and (traftel < 5) then fd := traford(w); if allstr and not fd then fd := dumelim(w); if fd and not fdbu then for i := 1 to w.hib do w.unlab[i] := -1; rrr := fd and not sn; end; {rrr} procedure remredr(var w : trs); var i,n : integer; allstr : boolean; begin n := w.hib; traftel := 0; while rrr(w) do; if sn then begin if w.hib = 0 then schrijf('Terminating since no rules remain.') else schrijf('Relatively terminating since no strict rules remain.'); end else begin {not sn} if w.hib < n then begin if w.hib = 1 then schrijf('Remaining rule:') else schrijf('Remaining rules:'); for i := 1 to w.hib do schrijf(' '+schrijfregel(w,i)); end; if not sn then rpo(w); allstr := true; for i := 1 to w.hib do if not w.strict[i] then allstr := false; if mb then if allstr then if not sn then if pow then fullmatchb(w) else matchb(w); end; end; {remredr} {BREAK} function semlab(var orig,lab : trs): boolean; var intp : array[1..maxnaam] of byte; ok,rl,rr,rulesrem,b,stoplab,frule,trule,qm,rev2 : boolean; i,j : integer; strbs,doetmee : array[1..maxrule] of boolean; s : string; function res(k : byte;c : boolean):boolean; begin if k = 0 then res := c else if k = 1 then res := false else if k = 2 then res := true else res := not(c); end;{res} begin {semlab} if random(3) = 0 then qm := true else qm := false; if random(2) = 0 then rev2 := true else rev2 := false; if rev2 then rev(orig); for i := 1 to orig.naamhib do begin lab.naam[i] := orig.naam[i]+'1'; lab.naam[orig.naamhib+i] := orig.naam[i]+'0'; end; lab.naamhib := 2* orig.naamhib; ok := false; while not ok do begin for i := 1 to orig.naamhib do if qm then intp[i] := random(3) else intp[i] := random(4); ok := true; lab.hib := 0; frule := false; trule := true; for i := 1 to orig.hib do for b := false to true do begin lab.hib := lab.hib + 1; lab.strict[lab.hib] := orig.strict[i]; lab.unlab[lab.hib] := i; rl := b; j := 1; while orig.l[i,j] > 0 do j := j+1; lab.l[lab.hib,j] := 0; while j > 1 do begin j := j-1; if rl then lab.l[lab.hib,j] := orig.l[i,j] else lab.l[lab.hib,j] := orig.l[i,j]+orig.naamhib; if b then trule := trule and rl else frule := frule or rl; rl := res(intp[orig.l[i,j]],rl); end; rr := b; j := 1; while orig.r[i,j] > 0 do j := j+1; lab.r[lab.hib,j] := 0; while j > 1 do begin j := j-1; if rr then lab.r[lab.hib,j] := orig.r[i,j] else lab.r[lab.hib,j] := orig.r[i,j]+orig.naamhib; if b then trule := trule and rr else frule := frule or rr; rr := res(intp[orig.r[i,j]],rr); end; if qm then ok := ok and (rl or (not rr)) else ok := ok and (rl = rr); end; end; {while not ok} if rev2 then rev(orig); if sn or trule or not frule then semlab := false else begin if qm then for i := 1 to orig.naamhib do begin lab.hib := lab.hib +1; lab.strict[lab.hib] := false; lab.unlab[lab.hib] := 0; lab.l[lab.hib,1] := i; lab.r[lab.hib,1] := i + orig.naamhib; lab.l[lab.hib,2] := 0; lab.r[lab.hib,2] := 0; end; schrijf(''); if rev2 then begin schrijf('Reverse every lhs and rhs of the system.'); schrijf(''); end; schrijf('Apply labelling with the following interpretation in {0,1}:'); for i := 1 to orig.naamhib do if intp[i] = 0 then schrijf(' '+ orig.naam[i] + ': identity') else if intp[i] = 3 then schrijf(' '+ orig.naam[i] + ': lambda x.1-x') else if intp[i] = 2 then schrijf(' '+ orig.naam[i] + ': constant 1') else if intp[i] = 1 then schrijf(' '+ orig.naam[i] + ': constant 0'); schrijf('and label every symbol by the value of its argument.'); schrijf(''); if qm then schrijf('This is a quasi-model for 1 > 0.') else schrijf('This interpretation is a model.'); schrijf(''); schrijf('Labelled system:'); for i := 1 to lab.hib do schrijf(' '+schrijfregel(lab,i)); schrijf(''); remredr(lab); if lab.unlab[1] >= 0 then if ((not sn) and (lab.hib >0)) then begin for i := 1 to orig.hib do doetmee[i] := false; for i := 1 to lab.hib do if lab.unlab[i] > 0 then doetmee[lab.unlab[i]] := true; stoplab := false; for i := 1 to orig.hib do if not doetmee[i] then stoplab := true; if stoplab then begin lab := orig; schrijf(''); schrijf('Remove all labels, remaining unlabelled system:'); lab.hib := 0; for i := 1 to orig.hib do if doetmee[i] then begin lab.hib := lab.hib+1; lab.l[lab.hib] := lab.l[i]; lab.r[lab.hib] := lab.r[i]; lab.strict[lab.hib] := lab.strict[i]; end; for i := 1 to lab.hib do schrijf(' '+schrijfregel(lab,i)); remredr(lab); end; end; semlab := true; end; end; {semlab} procedure reclab(var tt : trs; d : integer); var uu : trs; j : integer; begin j := 0; while (j < 20) and not semlab(tt,uu) do j := j+1; if d < 4 then if j < 20 then if (uu.hib < 10) and not sn then reclab(uu,d+1); end; {BREAK} procedure depp(var orig, dep : trs); var i,j,k : integer; def : array[1..maxnaam] of boolean; cap : array[1..maxnaam] of integer; begin dep := orig; for i := 1 to orig.naamhib do def[i] := false; for i := 1 to orig.hib do def[orig.l[i,1]] := true; for i := 1 to orig.naamhib do if def[i] then begin dep.naamhib := dep.naamhib +1; cap[i] := dep.naamhib; if (length(orig.naam[i]) = 1) and (orig.naam[i][1] in ['a'..'z']) then dep.naam[dep.naamhib] := chr(ord(orig.naam[i][1]) + ord('A') - ord('a')) else dep.naam[dep.naamhib] := '#'+orig.naam[i]; end; for i := 1 to orig.hib do begin j := 1; while orig.r[i,j] > 0 do begin if def[orig.r[i,j]] then begin dep.hib := dep.hib +1; dep.strict[dep.hib] := true; dep.l[dep.hib,1] := cap[orig.l[i,1]]; k := 2; while orig.l[i,k] >0 do begin dep.l[dep.hib,k] := orig.l[i,k]; k := k+1; end; dep.l[dep.hib,k] := 0; k := j; dep.r[dep.hib,1] := cap[orig.r[i,k]]; k := k+1; while orig.r[i,k] >0 do begin dep.r[dep.hib,k-j+1] := orig.r[i,k]; k := k+1; end; dep.r[dep.hib,k-j+1] := 0; end; j := j+1; end; end; for i := 1 to orig.hib do dep.strict[i] := false; for i := 1 to dep.hib do schrijf(' ' + schrijfregel(dep,i)); remredr(dep); end; {depp} {BREAK} procedure loopch(var tt : trs); var v : array[1..maxloop,1..20] of integer; nieuw : array[1..40] of integer; e : array[0..maxloop,1..maxloop] of boolean; vhib,vhibu, i,j,k,vi,ri : integer; s : string; procedure testloop; var i,j,m,mbu : integer; doetmee : array[1..maxloop] of boolean; uitg : boolean; begin for i := 1 to vhib do doetmee[i] := true; m := vhib; mbu := vhib+1; while m < mbu do begin mbu := m; m := 0; for i := 1 to vhib do if doetmee[i] then begin uitg := false; for j := 1 to vhib do if doetmee[j] and e[i,j] then uitg := true; if uitg then m := m+1 else doetmee[i] := false; end; end; if m >0 then begin i := 1; while not doetmee[i] do i := i+1; loopfound := true; s := 'Non-terminating; looping derivation starting in: '; j:= 1; while v[i,j] > 0 do begin s := s+tt.naam[v[i,j]]; j := j+1; end; schrijf(s); end; end; {testloop} function zoek : integer; var i,j,k : integer; begin i := 1; while i <= vhib do begin j := 1; while (v[i,j] = nieuw[j]) and (nieuw[j] > 0) do j := j+1; if v[i,j] = nieuw[j] then begin k := i; i := vhib + 10; end else i := i+1; end; if i < vhib + 10 then if vhib < maxloop then begin vhib := vhib + 1; j := 1; while nieuw[j] > 0 do begin v[vhib,j] := nieuw[j]; j := j+1; end; v[vhib,j] := 0; k := vhib; end else k := 0; zoek := k; end;{zoek} procedure prob1; {if ri = rule l -> r1 r2, v[vi] = v r1, #v = k, then add (vl,v r1) } var i : integer; begin i := 1; while (v[vi,k+i] = tt.r[ri,i]) and (v[vi,k+i] > 0) do i := i + 1; if v[vi,k+i] = 0 then begin for i := 1 to k do nieuw[i] := v[vi,i]; i := 1; while tt.l[ri,i] > 0 do begin nieuw[k+i] := tt.l[ri,i]; i := i+1; end; nieuw[k+i] := 0; if k+i <= 20 then e[zoek,vi] := true; end; end;{prob1} procedure prob4; {if ri = rule l -> r, v[vi] = w r w', #w = k, then add (wlw',wrw') } var i,j : integer; begin i := 1; while (v[vi,k+i] = tt.r[ri,i]) and (v[vi,k+i] > 0) do i := i + 1; if tt.r[ri,i] = 0 then begin j := k+i; for i := 1 to k do nieuw[i] := v[vi,i]; i := 1; while tt.l[ri,i] > 0 do begin nieuw[k+i] := tt.l[ri,i]; i := i+1; end; while v[vi,j] > 0 do begin nieuw[k+i] := v[vi,j]; i := i+1; j := j+1; end; nieuw[k+i] := 0; if k+i <= 20 then e[zoek,vi] := true; end; end;{prob4} procedure prob2; {if ri = rule l -> r1 r2, v[vi] = r2 v, #r1 = k, then add (lv,r2 v) } var i,j : integer; begin i := 1; while (tt.r[ri,k+i] = v[vi,i]) and (tt.r[ri,k+i] > 0) do i := i + 1; if tt.r[ri,k+i] = 0 then begin j := i; i := 1; while tt.l[ri,i] > 0 do begin nieuw[i] := tt.l[ri,i]; i := i+1; end; while v[vi,j] > 0 do begin nieuw[i] := v[vi,j]; i:=i+1; j:=j+1; end; nieuw[i] := 0; if i <= 20 then e[zoek,vi] := true; end; end;{prob2} procedure prob3; {if ri = rule l -> r1 r2 r3, v[vi] = r2, then add (l,r2) } var i : integer; begin i := 1; while (tt.r[ri,k+i] = v[vi,i]) and (tt.r[ri,k+i] > 0) do i := i + 1; if v[vi,i] = 0 then begin i := 1; while tt.l[ri,i] > 0 do begin nieuw[i] := tt.l[ri,i]; i := i+1; end; nieuw[i] := 0; if i <= 20 then e[zoek,vi] := true; end; end;{prob3} begin {loopch} for i := 1 to tt.hib do for j := 1 to 20 do v[i,j] := tt.l[i,j]; vhib := tt.hib; for i := 1 to maxloop do for j := 1 to maxloop do e[i,j] := false; vhibu := 0; while vhibu < vhib do begin vhibu := vhib; for vi := 1 to vhibu do for ri := 1 to tt.hib do begin k := 0; while v[vi,k+1] > 0 do begin prob1; prob4; k := k + 1; end; k := 0; while tt.r[ri,k+1] > 0 do begin prob2; prob3; k := k + 1; end; end; end; testloop; end;{loopch} {BREAK} procedure total(var tt : trs); var j, rtbu, rtdp : integer; uu : trs; begin rtbu := rtel; j := 0; while (j < 20*power) and not sn do begin rtel := rtbu; reclab(tt,1); j := j + 1; end; if not sn then begin rtel := rtbu; schrijf('Dependency pair transformation:'); depp(tt,uu); rtdp := rtel; j := 0; while (j < 10*power) and not sn do begin rtel := rtdp; reclab(uu,1); j := j + 1; end; end; if not sn then begin rtel := rtbu; schrijf('Reversed dependency pair transformation:'); rev(tt); depp(tt,uu); rtdp := rtel; j := 0; while (j < 10*power) and not sn do begin rtel := rtdp; reclab(uu,1); j := j + 1; end; rev(tt); end; if not sn then rtel := rtbu; end; {total} procedure main; var i : integer; tt : trs; allstr : boolean; begin rtel := 0; lees(tt); sn := false; loopfound := false; schrijf('TORPA 1.5 is applied to'); for i := 1 to tt.hib do schrijf(schrijfregel(tt,i)); pow := true; remredr(tt); pow := false; power := 1; if not sn then total(tt); if not sn then begin allstr := true; for i := 1 to tt.hib do allstr := allstr and tt.strict[i]; if allstr then loopch(tt); end; power := 50; if not (sn or loopfound) then total(tt); if sn then writeln('YES'); if loopfound then writeln('NO'); if sn or loopfound then begin for i := 1 to rtel do writeln(resul[i]); end else writeln('TORPA failed to find a proof'); end; {main} {main program} begin mb := true; matr := true; main; end.