Multiset Relations: A Tool for Proving Termination

Mul ise Rela ions: a To ol o P o ing Te mina ion ? J.-L. Ruiz-Reina, J.-A. Alonso, M.-J. Hidalgo and F.-J. Ma n j uiz,jalonso,mjoseh, jesus g ia.es Depa amen o de Cienias de la Compu aion e In eligenia A iial. Faul ad de In o ma ia y Es ads ia, Uni e sidad de Se illa A da. Reina Me edes, s/n. 41012 Se illa, Spain Abs a . We p esen in his pap e a o maliza ion o mul ise ela ions in ACL2, and we show how mul ise s an b e used o p o e non- i ial e mina ion p op e ies in ACL2. In ui i ely, mul ise s a e se s ha admi mul iple o u enes o elemen s. E e y ela ion on a se A indues a ela ion on ni e mul ise s o e A and i an be shown ha he mul ise ela ion indued by a well- ounded ela ion is also well- ounded. We p o ed his p op e y in he ACL2 logi, and used i by un ional ins an ia ion in o de o p o ide well- ounded ela ions o he admissibili y es o eu si e un ions. We also de elop ed a ma o de mul , o dene well- ounded mul ise ela ions in an easy way. Finally, we p esen h ee ase s udies whe e mul ise s a e used o p o e non- i ial e mina ion p op e ies: a ail- eu si e e sion o Ake mann's un ion, a deni ion o MCa hy's 91 un ion and a p o o o Newman's lemma o abs a edu ion ela ions. In o du ion We p esen in his pap e a o maliza ion o mul ise ela ions in ACL2, and we show how hese ela ions an b e used o p o e non- i ial e mina ion p op e ies, p o iding a o ol o dening ela ions on ni e mul ise s and showing ha hese ela ions a e well- ounded. Suh well- ounded ela ions a e used in he admissibili y es o eu - si e un ions, allowing he use o p o ide a pa iula mul ise measu e in o de o p o e e mina ion o eu si ely dened un ions. Mul ise s a e usually dened in an in o mal way as se s wi h ep ea ed elemen s". De showi z and Manna [4℄ p o ed ha e e y well- ounded ela ion on a se A indues a well- ounded ela ion on he se o ni e mul ise s o elemen s aken om A . We ha e o malized his heo em using ACL2, and s a ed i in an abs a way. This allows o ins an ia e he heo em o show well- oundedness o on e e mul ise ela ions. We ha e also de elop ed a ma o de mul in o de o easily make deni ions o indued mul ise ela ions. Besides dening he mul ise ela ion indued by a gi en ela ion, his ma o p o es, by un ional ins an ia ion, well- oundedness o he de- ned mul ise ela ion, p o ided ha he o iginal ela ion is well- ounded. The  s se ion o his pap e p esen s how we ha e o malized and p o ed well- oundedness o mul ise ela ions indued by well- ounded ela ions. The seond se- ion p esen s he ma o de mul and i is shown how i an b e used o dene mul ise well- ounded ela ions. In he h ee se ions a e ha , h ee ase s udies o in eas- ing omplexi y a e p esen ed, showing how mul ise s an b e used o p o e non- i ial e mina ion p op e ies. The  s one is a ail- eu si e deni ion o Ake mann's un ion. The seond one shows admissibili y o an i e a i e e sion o MCa hy's 91 un ion. The hi d one is a p o o o Newman's lemma ab ou abs a edu ion ela ions: e mina ing and lo ally onuen edu ion ela ions a e onuen . ? This wo k has been supp o ed by DGES/MEC: P o je s PB96-0098-C04-04 and PB96-1345 We will assume he eade has a wo king knowledge o ACL2. The b es in o du- ion o ACL2 is [5℄. Due o he lak o spae, we will skip de ails o he mehanial p o o s and we will no men ion gua ds o gua ds e ia ion. The omple e b o oks a e a ailable on he web in h p://www-s.us.es/~j uiz/al2-mul/ . 1 Fo maliza ion o mul ise ela ions in ACL2 1.1 Mul ise s: deni ions and p op e ies A mul ise M o e a se A is a un ion om A o he se o na u al numb e s. This is a o mal way o dene se s wi h ep ea ed elemen s". In ui i ely, M ( x ) is he numb e o opies o x 2 A in M . This mul ise is ni e i he e a e ni ely many x suh ha M ( x ) > 0. The se o all ni e mul ise s o e A is deno ed as M ( A ). We will use s anda d se no a ion o ep esen mul ise s. Fo example, i A = a; b;  g , an example o mul ise o e A is M = a; b; b; b g , an abb e ia ion o he un ion M ( a ) = 1, M ( b ) = 3 and M (  ) = 0. Thus, a; b; b; b g is iden ial o he mul ise b; b; a; b g , bu dis in om he mul ise a; b; b g . Basi op e a ions on mul ise s a e dened o gene alize he same op e a ions on se s, aking in o aoun mul iple o u enes o elemen s: x 2 M means M ( x ) > 0, M  N means M ( x )  N ( x ), o all x 2 A , M [ N is he un ion M + N and M n N is he un ion M :  N (whe e x :  y is x  y i x  y and 0 o he wise). Fo example, a; b; b; a g [ ; ; a; b g is he mul ise a; a; a; b; b; b; ;  g and a; b; b; a g n ; ; a; b g is he mul ise a; b g . Any o de ing dened on a se A indues an o de ing on mul ise s o e A : gi en a mul ise , a smalle mul ise an b e ob ained by emo ing a non-emp y subse X and adding elemen s whih a e smalle han some elemen in X . This ons u ion an b e gene alized o bina y ela ions in gene al, no only o pa ial o de ings. This is he o mal deni ion: DEFINITION 1. Gi en a ela ion < on a se A , he mul ise ela ion indued by < on M ( A ), deno ed as < mul , is dened as N < mul M i he e exis X ; Y 2 M ( A ) suh ha ; 6 = X  M ; N = ( M n X ) [ Y and 8 y 2 Y 9 x 2 X ; y < x . Fo example, i A = a; b; ; d; e g and b < a , d <  , hen a; b; b; b; b; d; d; d; d; d; e g < mul a; a; b; ; d; e g by eplaing X = a;  g by Y = b; b; b; d; d; d; d g . I an b e easily shown ha i < is a s i o de ing, hen so is < mul . In suh ase we alk ab ou mul ise o de ings . A ela ion < on a se A is e mina ing i he e is no inni e de easing 1 sequene x 0 > x 1 > x 2 ::: . An imp o an p op e y o mul ise ela ions on ni e mul ise s is ha hey a e e mina ing when he o iginal ela ion is e mina ing, as s a ed by he ollowing heo em: THEOREM 1. Le < b e a e mina ing ela ion on a se A , and < mul he mul ise ela ion indued by < on M ( A ). Then < mul is e mina ing. The ab o e heo em p o ides a o ol o showing e mina ion o eu si e un ion deni ions, by using mul ise s: show ha some mul ise measu e de eases in eah eu si e all ompa ing mul ise s wi h esp e o he ela ion indued by a gi en e - mina ing ela ion. In he ollowing subse ion, we explain how we o malized heo em 1 in he ACL2 logi. 1 Al hough no explii ly, we will supp ose ha he ela ions gi en he e ep esen some kind o smalle han" ela ion. 1.2 Fo maliza ion o well- ounded mul ise ela ions in ACL2 Le us deal wi h o maliza ion o e mina ing ela ions in ACL2. A es i ed no ion o e mina ing ela ions is buil in o ACL2 based on he ollowing me a- heo em (axiom o hoie needed): a ela ion < on a se A is e mina ing i he e exis s a un ion F : A ! O d suh ha x < y ) F ( x ) < F ( y ), whe e O d is he lass o all o dinals. In his ase, we also say ha he ela ion is wel l- ounded . No e ha we a e deno ing he ela ion on A and he o de ing b e ween o dinals using he same symb ol < . An a bi a y well- ounded ela ion el dened on a se o ob je s sa is ying a p op e y mp an b e dened in ACL2 as shown b elow (do s a e used o omi ehnial de ails, as in he es o he pap e ): (enapsula e ((mp (x) booleanp) ( el (x y) booleanp) ( n (x) e0-o dinalp)) ... (de hm el-well- ounded- ela ion-on-mp (and (implies (mp x) (e0-o dinalp ( n x))) (implies (and (mp x) (mp y) ( el x y)) (e0-o d-< ( n x) ( n y)))) : ule-lasses :well- ounded- ela ion)) The p edia e mp eognizes he kind o ob je s (alled measu es ) ha a e o de ed in a well- ounded way by el . The embedding un ion n is an o de -p ese ing un ion mapping e e y measu e o an o dinal. One a ela ion is p o ed o sa is y hese p op e ies and he heo em is s o ed as a well- ounded ela ion ule, i an b e used in he admissibili y es o eu si e un ions. We all he heo em el-well- - ounded- ela ion-on-mp ab o e he wel l- oundedness heo em o el , mp and n . In ACL2, e e y pa iula well- ounded ela ion has o b e gi en by means o h ee un ions (a bina y ela ion, a measu e p edia e and an emb edding un ion) and he o esp onding well- oundedness heo em o suh un ions. As a pa iula ase, when mp is we an omi any e e ene o mp in he s a emen o he o esp onding well- oundedness heo em. See well- ounded- ela ion in he ACL2 manual [6℄. The ab o e no ion o e mina ion is es i ed: sine only o dinals up o " 0 a e o malized in he ACL2 logi, a limi a ion is imp osed on he maximal o de yp e o well- ounded ela ions ha an b e o malized. Consequen ly, ou o maliza ion sue s om he same es i ion (ne e heless, ou p o o s do no dep end on pa iula p op e ies o " 0 , exep well- oundedness). Le us now deal wi h o maliza ion o mul ise s ela ions. We ep esen mul ise s in ACL2 as ue lis s. Gi en a p edia e (mp x) des ibing a se A , ni e mul ise s o e A a e des ib ed by he ollowing un ion: (de un mp- ue-lis p (l) (i (a om l) (equal l nil) (and (mp (a l)) (mp- ue-lis p (d l))))) No e ha his un ion dep ends on he pa iula deni ion o he p edia e mp . Wi h his ep esen a ion, die en ue lis s an ep esen he same mul ise : wo ue lis s ep esen he same mul ise i one is a p e mu a ion o he o he . Thus, he o de in whih he elemen s app ea in a lis is no ele an , bu he numb e o o u enes o an elemen is imp o an . This mus b e aken in o aoun , o example, when dening mul ise die ene in ACL2 ( he un ion emo e-one , omi ed he e, dele es one o u ene o an elemen om a lis , whene e p ossible): (de un mul ise -di (m n) (i (a om n) m (mul ise -di ( emo e-one (a n) m) (d n)))) The deni ion o < mul gi en in he p eeding subse ion is qui e in ui i e bu , due o i s many quan ie s, diÆul o implemen . Ins ead, we will use a somewha es i ed deni ion, based on he ollowing heo em: THEOREM 2. Le < b e a s i o de ing on a se A , and M ; N wo ni e mul ise s o e A . Then N < mul M i M n N 6 = ; and 8 n 2 N n M ; 9 m 2 M n N ; suh ha n < m . F om he ompu a ional p oin o iew, he main ad an age o his al e na i e deni ion is ha he we do no ha e o sea h he mul ise s X and Y o he o iginal deni ion b eause we an ake M n N and N n M , esp e i ely. I should b e ema ked ha his equi alene is ue only when < is a s i pa ial o de ing. Take o example, he ela ion S dened on A = a; b; ; d g , suh ha dS  , S b and bS a . In his ase we ha e b; ; d g S mul a; b;  g , aking X = a; b;  g and Y = b; ; d g . Ne e heless, d 2 b; ; d g n a; b;  g , a g = a; b;  g n b; ; d g and i is no ue ha dS a . Anyway, his is no a se e e es i ion. Mo eo e , well- oundedness o < mul also holds when his es i ed deni ion is used, e en i he ela ion < is no ansi i e, as we will see. Thus, gi en a dened (o ons ained) bina y ela ion el , we dene he indued ela ion on mul ise s based on his al e na i e deni ion: (de un exis s- el-bigge (x l) (ond ((a om l) nil) (( el x (a l)) ) ( (exis s- el-bigge x (d l))))) (de un o all-exis s- el-bigge (l m) (i (a om l) (and (exis s- el-bigge (a l) m) ( o all-exis s- el-bigge (d l) m)))) (de un mul- el (n m) (le ((m-n (mul ise -di m n)) (n-m (mul ise -di n m))) (and (onsp m-n) ( o all-exis s- el-bigge n-m m-n)))) Finally, le us see how we an o malize in he ACL2 logi he heo em 1 ab o e, whih s a es well- oundedness o he ela ion mul- el . As said b e o e, in o de o es ablish well- oundedness o a ela ion in ACL2, in addi ion o he ela ion ( mul- el in his ase), we ha e o gi e he measu e p edia e and he emb edding un ion, and hen p o e he o esp onding well- oundedness heo em. Sine mul- el is in ended o b e dened on mul ise s o elemen s sa is ying mp , hen mp- ue-lis p is he measu e p edia e in his ase. Le us supp ose we ha e dened a sui able emb edding un ion alled map- n-e0-o d . Then heo em 1 is o malized as ollows: (de hm mul ise -ex ension-o - el-well- ounded (and (implies (mp- ue-lis p x) (e0-o dinalp (map- n-e0-o d x))) (implies (and (mp- ue-lis p x) (mp- ue-lis p y) (mul- el x y)) (e0-o d-< (map- n-e0-o d x) (map- n-e0-o d y)))) : ule-lasses :well- ounded- ela ion) In he nex subse ion we show a sui able deni ion o map- n-e0-o d and de- s ib e some asp e s o he ACL2 p o o o his heo em. 1.3 A p o o o well- oundedness o he mul ise ela ion In he li e a u e [1℄, heo em 1 is usually p o ed using Konig's lemma: e e y inni e and ni ely b anhed ee has an inni e pa h. Ne e heless, we ha e o nd a die - en p o o in ACL2, dening an o de -p ese ing emb edding un ion map- n-e0-o d om mp- ue-lis p ob je s o e0-o dinalp ob je s. Thus, ou p o o is based on he ollowing esul om o dinal heo y: gi en an o dinal  , he se M (  ) o ni e mul ise s o elemen s o  (o dinals less han  ), o de ed by he mul ise ela ion indued by he o de b e ween o dinals, is o de -isomo phi o he o dinal !  and he isomo phism is gi en by he un ion H whe e H (  1 ;::: ; n g ) = !  1 + ::: + !  n . This esul an b e p o ed using Can o 's no mal o m o o dinals and i s p op e ies. As a by-p o du , an in e es ing p op e y ab ou mul ise well- ounded ela ions an b e dedued. Sine   " 0 implies !   ! " 0 = " 0 , his means ha one an always p o e, in he ACL2 logi, well- oundedness o he mul ise ela ion indued by a gi en well- ounded ACL2 ela ion (i.e., using emb eddings in he o dinal " 0 ). This is no he ase, o example, o lexiog aphi p o du s, sine he maximal o dinal yp e o a lexiog aphi p o du o wo ACL2 well- ounded ela ions may b e g ea e han " 0 . The isomo phism H ab o e sugges s he ollowing deni ion o he emb edding un ion map- n-e0-o d : gi en a mul ise o elemen s sa is ying mp , apply n o e e y elemen o ob ain a mul ise o o dinals. Then apply H o ob ain an o dinal less han " 0 . I o dinals a e ep esen ed in ACL2 no a ion, hen he un ion H an b e easily dened, p o ided ha he un ion n e u ns always a non-ze o o dinal: he un ion H simply has o so he o dinals in he mul ise and add 0 as he nal d . These onside a ions lead us o he ollowing deni ion o he emb edding un ion map- n-e0-o d . No e ha he non-ze o es i ion on n is easily o e ome, dening ( he ma o) n1 equal o n exep o in ege s, whe e 1 is added. In his way n1 e u ns non-ze o o dinals o e e y measu e ob je and i is o de -p ese ing i and only i n is. (de un inse -e0-o d-< (x l) (ond ((a om l) (ons x l)) ((no (e0-o d-< x (a l))) (ons x l)) ( (ons (a l) (inse -e0-o d-< x (d l)))))) (de un add1-i -in ege (x) (i (in ege p x) (1+ x) x)) (de ma o n1 (x) `(add1-i -in ege ( n ,x))) (de un map- n-e0-o d (l) (i (onsp l) (inse -e0-o d-< ( n1 (a l)) (map- n-e0-o d (d l))) 0)) One map- n-e0-o d has b een dened, le us now deal wi h he ACL2 me- hanial p o o o he well- oundedness heo em o mul- el , mp- ue-lis p and map- n-e0-o d as s a ed a he end o subse ion 1.2 by mul ise -ex ension-o - - el-well- ounded . The  s pa o he heo em, whih es ablishes ha (map- n- -e0-o d x) is an o dinal when (mp- ue-lis p x) , i is no diÆul , and an b e p o ed in ACL2 wi h mino help o m he use . The ha d pa o he heo em is o show ha map- n-e0-o d is o de -p ese ing. He e is an in o mal p o o ske h: P o o ske h: Le us deno e, o simplii y, he un ions n1 and map- n-e0-o d , as and mul , and he ela ion el , mul- el and e0-o d-< as < el , < mul and < , esp e i ely. Le M and N b e wo mul ise s o mp elemen s suh ha N < mul M . We ha e o p o e ha mul ( N ) < mul ( M ). We an apply indu ion on he numb e o elemen s o N . No e ha M an no b e emp y, and i N is emp y he esul i ially holds. So le us supp ose ha M and N a e no emp y. Le ( x ), ( y ) b e he bigges elemen s o [ N ℄ and [ M ℄, esp e i ely. No e ha ( x ) and ( y ) a e he a elemen s o mul ( N ) and mul ( M ), esp e i ely. Sine ( x ) and ( y ) a e o dinals, h ee ases may a ise: 1. ( x ) < ( y ). Then, by deni ion o < , we ha e mul ( N ) < mul ( M ). 2. ( x ) > ( y ). This is no p ossible: in ha ase x is in N n M and by he mul ise ela ion deni ion, exis s z in M n N suh ha x < el z . Consequen ly ( z ) > ( x ) > ( y ). This on adi s he a ha ( y ) is he bigges elemen o [ M ℄. 3. ( x ) = ( y ). In ha ase, x 2 M , sine o he wise i would exis z 2 M n N suh ha x < el z and he same on adi ion as in he p e ious ase app ea s. Le M 0 = M n x g and N 0 = N n x g . We ha e N 0 < mul M 0 and, in addi ion, mul ( N 0 ) and mul ( M 0 ) a e he d o mul ( N ) and mul ( M ), esp e i ely. Indu ion hy- p o hesis an b e applied he e o onlude ha mul ( N 0 ) < mul ( M 0 ) and he e o e mul ( N ) < mul ( M ) : u To lead ACL2 o he ab o e in o mal p o o ske h, an indu ion sheme mus b e supplied as hin . This is a un ion sugges ing suh indu ion sheme ( he un ion max- n1-lis , omi ed he e, e u ns he elemen o a gi en lis wi h he g ea es alue o n1 ): (de un indu ion-mul ise (n m) (dela e (xa gs :measu e (al2::len n))) (ond ((a om n) (i (a om m) 1 2)) ((a om m) 3) ( (le * ((max-m (max- n1-lis m)) (max-n (max- n1-lis n)) ( n1-max-m ( n1 max-m)) ( n1-max-n ( n1 max-n))) (ond ((equal n1-max-m n1-max-n) (i (membe max-n m) (indu ion-mul ise ( emo e-one max-n n) ( emo e-one max-n m)) 5)) ((e0-o d-< n1-max-n n1-max-m) 6) ((e0-o d-< n1-max-m n1-max-n) 7) ( 8)))))) Using his indu ion sheme we p o ed he ollowing heo em, whih is he ha d pa o he heo em mul ise -ex ension-o - el-well- ounded . (de hm map- n-e0-o d-o de -p ese ing (implies (and (mp- ue-lis p n) (mp- ue-lis p m) (mul- el n m)) (e0-o d-< (map- n-e0-o d n) (map- n-e0-o d m))) :hin s (("Goal" :indu (indu ion-mul ise n m))))) The p o o o his esul was no easy: lemmas o handle eah o he ases gene a ed by he ab o e indu ion sheme ha e o b e p o ed, ob aining a mehanial p o o e y lose o he p e ious p o o ske h. See he b o ok mul ise .lisp in he web page o de ails ab ou he mehanial p o o . Well- oundedness o mul- el has b een p o ed in an abs a amewo k, wi h- ou assuming any pa iula p op e ies o el , mp and n , exep hose one ning well- oundedness. This allows us o un ionally ins an ia e he heo em in o de o es ablish well- oundedness o he mul ise ela ion indued by any gi en well- ounded ACL2 ela ion. We de elop ed a ma o named de mul in o de o mehanize his p o ess o un ional ins an ia ion. The ollowing se ion des ib es he ma o. 2 The de mul ma o and he mul ise b o ok We dened a ma o de mul in o de o p o ide a on enien way o dene he mul ise ela ion indued by a well- ounded ela ion, and o dela e he o esp onding well- ounded ela ion ule. We explain now how de mul is used. Le us supp ose we ha e a p e iously dened (o ons ained) ela ion my- el , whih is known o b e well- ounded on a se o ob je s sa is ying he measu e p op e y my-mp and jus ied by he emb edding un ion my- n . Tha is o say, he ollowing heo em, using a iables x and y , has b een p o ed (and s o ed as a well- ounded ela ion ule): (de hm heo em-name (and (implies ( my-mp x ) (e0-o dinalp ( my- n x ))) (implies (and ( my-mp x ) ( my-mp y ) ( my- el x y )) (e0-o d-< ( my- n x ) ( my- n y )))) : ule-lasses :well- ounded- ela ion)) In o de o dene he (well- ounded) mul ise ela ion indued by my- el , we w i e he ollowing ma o all: (de mul ( my- el heo em-name my-mp my- n x y )) The expansion o his ma o gene a es a numb e o ACL2 o ms. You may use he ACL2 ans1 ommand in o de o iew he ansla ed o m o a de mul all. The main non-lo al e en s gene a ed by his ma o all a e: { he deni ions needed o he mul ise ela ion indued by my- el : un ions exis- s- my- el -bigge , o all-exis s- my- el -bigge , and mul- my- el analogous o he un ions gi en in subse ion 1.2. { he deni ion o he mul ise measu e p op e y, my-mp - ue-lis p . { he deni ion o map- my- n -e0-o d , he emb edding un ion om mul ise s o o dinals. { he well- oundedness heo em o mul- my- el , my-mp - ue-lis p and map- my- - n -e0-o d . This heo em is p o ed by un ional ins an ia ion om mul ise - -ex ension-o - el-well- ounded and is named mul ise -ex ension-o - my- - el -well- ounded We exp e de mul o wo k wi hou assis ane om he use . A e he ab o e all o de mul , he un ion mul- my- el is dened as a well- ounded ela ion on mul ise s o elemen s sa is ying he p op e y my-mp , indued by he well- ounded ela ion my- el . F om his momen on, mul- my- el an b e used in he admissibili y es o eu si e un ions o show ha he eu sion e mina es. To know he lis o names we need o supply o a de mul all, we ha e de elop ed a o ol o ex a he in o ma ion om he ACL2 wo ld and p in i . This ma o is simply alled in his way: (de mul-omponen s my- el ) This is only an in o ma i e o ol, no a e en . This ma o lo oks up he ACL2 wo ld, and e u ns he lis o names ha a e needed in he de mul all o my- el . We ha e di ided he esul s and o ols ab ou mul ise s in o wo b o oks. The b o ok mul ise .lisp on ains he p o o o he heo em mul ise -ex ension-o - el- -well- ounded shown in subse ion 1.3. Names in his b o ok a e dened in he pakage MUL . The b o ok de mul.lisp on ains he ma o deni ions o de mul and de mul- -omponen s and inludes he mul ise b o ok. See he web page o de ails. We ha e also inluded some non-lo al ules in mul ise .lisp , whih help ed us o p o e he h ee examples p esen ed in his pap e , and we hink hey a e gene al enough o assis in o he ases. Two ele an examples o hese addi ional esul s and o ols a e: { We ha e dened he un ion equal-se as an equi alene ela ion. This un ion implemen s equali y o se s, no o mul ise s, bu i u ned ou use ul in ou ase s udies b eause i an b e p o ed o b e a ong uene wi h esp e o b o h a gumen s o o all-exis s- my- el -bigge : (de un equal-se (x y) (and (subse p x y) (subse p y x))) (de equi equal-se ) (de ong equal-se i o all-exis s- my- el -bigge l m 1) (de ong equal-se i o all-exis s- my- el -bigge l m 2) Sine he la e wo ong uene ules dep end on he pa iula deni ion o my- el , hey a e gene a ed by e e y pa iula all o de mul . { We also dene a me a ule o deal wi h die ene o mul ise s ep esen ed by lis s wi h nal ommon suÆx. This ule ew i es exp essions o he o m (mul ise -di (lis * x 1 x 2 : : : x m l) (lis * y 1 y 2 : : : y k l)) o he ollowing equi alen exp ession (wi h esp e o equal-se ): (mul ise -di (lis x 1 x 2 : : : x m ) (lis y 1 y 2 : : : y k )) This me a ule is e y use ul 2 when p o ing ha a pa iula mul ise measu e de eases in e e y eu si e all o a un ion: i is usual" ha he mul ise ob ained measu ing he a gumen s o a eu si e all is a lis wi h he same nal pa han he mul ise ob ained measu ing he a gumen s in he o iginal all. 3 Case s udies using mul ise ela ions In he nex subse ions, we show h ee examples whe e well- ounded mul ise ela ions play an imp o an ole in he ACL2 p o o o non- i ial e mina ion p op e ies. The  s example is aken om [4℄. We use a mul ise ela ion o show e mina ion o a ail- eu si e e sion o Ake mann's un ion. In he seond example, also aken om [4℄, we use a mul ise ela ion o admi an i e a i e e sion o MCa hy's 91 un ion. The hi d example is a p o o o Newman's lemma o abs a edu ion sys ems: e e y e mina ing and lo ally onuen edu ion ela ion has he Chu h- Rosse p op e y. This las example is pa o a la ge p o je de elop ed by he au ho s in o de o o malize some asp e s o equa ional easoning using ACL2 [8, 9℄. All he examples show one un ion whose e mina ion is p o ed using a well- ounded mul ise ela ion and a mul ise measu e un ion. When he un ion is p esen ed o he  s ime, i s o de is ommen ed (using semiolons), o emphasize ha a sui able measu e has s ill o b e gi en in o de o pass he admissibili y es . 3.1 A ail- eu si e e sion o Ake mann's un ion The ollowing is he s anda d deni ion o Ake mann's un ion in ACL2: (de un ak (m n) (dela e (xa gs :measu e (ons (+ (n ix m) 1) (n ix n)))) (ond ((zp m) (+ n 1)) ((zp n) (ak (- m 1) 1)) ( (ak (- m 1) (ak m (- n 1)))))) We now y o dene he ollowing i e a i e p og am o ompu e Ake man's un ion: ; (de un ak-i -aux (S z) ; (i (endp S) ; z ; (le ((head ( i s S)) 2 Due o a bug in ACL2 e sion 2.5, his me a ule ails o b e applied. This is no he ase in e sion 2.4, whe e we o iginally de elop ed his wo k. The p oblem in e sion 2.5 an b e xed by inluding a pa h ha will b e inluded in Ve sion 2.6. Thanks o Ma Kau mann o he pa h. ;;; (a) A well- ounded pa ial o de : (enapsula e (( el (x y) ) ( n (x) )) ... (de hm el-well- ounded- ela ion (and (e0-o dinalp ( n x)) (implies ( el x y) (e0-o d-< ( n x) ( n y)))) : ule-lasses (:well- ounded- ela ion : ew i e)) (de hm el- ansi i e (implies (and ( el x y) ( el y z)) ( el x z)))) ;;; (b) A e mina ing and loally on luen edu ion ela ion: (enapsula e ((legal (x u) boolean) ( edue-one-s ep (x u) elemen ) ( eduible (x) boolean) ( ans o m-loal-peak (x) p oo )) .... (de un p oo -s ep-p (s) (le ((el 1 (el 1 s)) (el 2 (el 2 s)) (ope a o (ope a o s)) (di e (di e s))) (and ( -s ep-p s) (implies di e (and (legal el 1 ope a o ) (equal ( edue-one-s ep el 1 ope a o ) el 2))) (implies (no di e ) (and (legal el 2 ope a o ) (equal ( edue-one-s ep el 2 ope a o ) el 1)))))) (de un equi -p (x y p) (i (endp p) (equal x y) (and (p oo -s ep-p (a p)) (equal x (el 1 (a p))) (equi -p (el 2 (a p)) y (d p))))) (de hm e mina ing (implies (legal x op) ( el ( edue-one-s ep x op) x))) (de hm loally-on luen (le (( alley ( ans o m-loal-peak p))) (implies (and (equi -p x y p) (loal-peak-p p)) (and (s eps- alley alley) (equi -p x y alley)))))) Fig. 1. Assump ions o Newman's lemma pa iula shap es ( al leys and loal peaks ): loal-peak-p eognizes p o o s o he o m x ! u and s eps- alley eognizes p o o s o he o m  ! x  u . To deal wi h he assump ion o lo al onuene, no e ha a edu ion is lo ally onuen i o e e y lo al p eak p o o he e is an equi alen alley p o o . The e o e, in o de o s a e lo al onuene o he gene al edu ion ela ion dened, we assume he exis ene o a un ion ans o m-loal-peak whih e u ns a alley p o o o e e y lo al p eak p o o . See again i em (b) in gu e 1 o a s a emen o his assumed p op e y. Ha ing es ablished he assump ions, in o de o p o e Newman's lemma we mus show onuene o his gene al edu ion ela ion assumed o b e e mina ing and lo ally onuen . Ins ead o onuene, we p o e he Chu h-Rosse p op e y, whih is equi alen . The e o e, we mus p o e ha o e e y p o o he e exis s an equi alen alley p o o , i.e., we ha e o dene a un ion ans o m- o- alley and p o e ha ( ans o m- o- alley p) is a alley p o o equi alen o p . This is he s a emen o Newman's lemma: (de hm Newman-lemma (le (( alley ( ans o m- o- alley p))) (implies (equi -p x y p) (and (s eps- alley alley) (equi -p x y alley))))) A sui able deni ion o ans o m- o- alley and a p o o o his heo em in ACL2 is shown in he ollowing subse ion. The ha d pa o he p o o is o show e mina ion o ans o m- o- alley . I will b e done wi h he help o a well- ounded mul ise ela ion. An ACL2 p o o o Newman's lemma: The p o o ommonly ound in he li e a- u e [1℄, is done by well- ounded indu ion on he e mina ing edu ion ela ion. Ou app oah is mo e ons u i e and is based on a p o o gi en in [7℄. We ha e o dene a un ion ans o m- o- alley whih ans o ms e e y p o o in a equi alen alley p o o . Fo ha pu p ose, we an use he un ion ans o m-loal-peak , assumed o ans o m e e y lo al p eak p o o in a equi alen alley p o o . Thus, he un ion we need is dened o i e a i ely apply eplae-loal-peak , (whih eplaes he  s lo- al p eak subp o o by he equi alen subp o o gi en by ans o m-loal-peak ) un il he e a e no lo al p eaks (heked by exis s-loal-peak ). The ollowing is he de- ni ion o ans o m- o- alley (we omi he e he deni ion o eplae-loal-peak and exis s-loal-peak ): ;(de un ans o m- o- alley (p) ; (i (no (exis s-loal-peak p)) ; p ; ( ans o m- o- alley ( eplae-loal-peak p)))) This un ion is no admi ed wi hou help om he use . The eason is ha when a lo al p eak in a p o o is eplaed by an equi alen alley subp o o , he leng h o he p o o ob ained may b e la ge han he leng h o he o iginal p o o . Ne e heless, he key p oin he e is ha e e y elemen o he new subp o o is smalle (w. . . he well- ounded ela ion el ) han he g ea es elemen o he lo al p eak. I we mea- su e a p o o as he mul ise o he elemen s in ol ed in i , hen eplaing a lo al p eak subp o o by an equi alen alley subp o o , we ob ain a p o o wi h smalle mea- su e wi h esp e o he well- ounded mul ise ela ion indued by el . The un ion p oo -measu e e u ns his measu e o a gi en p o o : i olle s he el 1 elemen s o e e y p o o s ep in a p o o . (de un p oo -measu e (p) (i (endp p) nil (ons (el 1 (a p)) (p oo -measu e (d p))))) Using de mul , we dene he well- ounded ela ion mul- el , indued by he well- ounded ela ion el in o dued in he p e ious subse ion: (de mul ( el el-well- ounded- ela ion-on-mp n x y)) The main esul we p o ed s a es ha he p o o measu e de eases (wi h esp e o he well- ounded ela ion mul- el ) i a lo al-p eak is eplaed by an equi alen alley subp o o : (de hm ans o m- o- alley-admission (implies (exis s-loal-peak p) (mul- el (p oo -measu e ( eplae-loal-peak p)) (p oo -measu e p))) : ule-lasses nil) Wi h his heo em, admission o he un ion ans o m- o- alley is now p os- sible, gi ing a sui able hin : (de un ans o m- o- alley (p) (dela e (xa gs :measu e (p oo -measu e p) :well- ounded- ela ion mul- el :hin s (("Goal" :use (:ins ane ans o m- o- alley-admission))))) (i (no (exis s-loal-peak p)) p ( ans o m- o- alley ( eplae-loal-peak p)))) One ans o m- o- alley is admi ed (whih is he ha d pa o he heo em), he ollowing wo heo ems a e p o ed, and his i ially implies Newman's lemma as s a ed a he end o subse ion 3.3. (de hm equi -p-x-y- ans o m- o- alley (implies (equi -p x y p) (equi -p x y ( ans o m- o- alley p)))) (de hm alley- ans o m- o- alley (implies (equi -p x y p) (s eps- alley ( ans o m- o- alley p)))) The mehanial p o o o Newman's lemma is he mos diÆul o he h ee exam- ples p esen ed he e. Lemmas ha e o b e p o ed o simpli y he mul ise die enes app ea ing in he onje u e gene a ed by he e mina ion p o o o ans o m- o- - alley . See he le newman.lisp in he web page o de ails. We also p o ide b o oks p o ing deidabili y o he equi alene ela ion gene a ed by a e mina ing and lo ally onuen edu ion ela ion. To see how his esul an b e exp o ed o he s udy o equa ional heo ies, see [9℄. 4 Conlusions We ha e p esen ed a o maliza ion o mul ise ela ions in ACL2, showing how hey an b e used as a o ol o p o ing non- i ial e mina ion p op e ies o eu si e un- ions in ACL2. We ha e dened he mul ise ela ion indued by a gi en ela ion and p o ed a heo em es ablishing well- oundedness o he mul ise ela ion indued by a well- ounded ela ion. This heo em is o mula ed in an abs a way, so ha un ional ins an ia ion an b e used o p o e well- oundedness o on e e mul ise ela ions. We ha e p esen ed also a ma o named de mul , implemen ed o p o ide a on e- nien o ol o dene well- ounded mul ise ela ions indued by well- ounded ela ions. This ma o allows he deni ion o hese mul ise ela ions in a single s ep. Th ee ase s udies a e p esen ed, o show how his o ol an b e use ul in ob aining p o o s o non- i ial e mina ion p op e ies o un ions dened in ACL2. The  s ase s udy is he deni ion o a ail- eu si e e sion o Ake mann's un ion. The seond is he admissibili y o a deni ion o MCa hy's 91 un ion, and a s udy o i s p op e ies. The hi d is a p o o o Newman's lemma o abs a edu ion ela ions. This wo k a ose as pa o a la ge p o je , ying o o malize p op e ies o ab- s a edu ion ela ions, equa ional heo ies and e m ew i ing sys ems [8, 9℄. In ha wo k, ACL2 is used as a me a-logi o s udy p op e ies o a o mal p o o sys em, namely equa ional logi. Newman's lemma is a key esul needed o p o e deidabili y o equa ional heo ies gi en by omple e e m ew i ing sys ems [1℄. One o malized mul ise ela ions and used in he p o o o Newman's lemma, we deided o make a o ol ( de mul ) whih allowed o exp o he esul s on mul ise s o o he on ex s. To es his implemen a ion, we applied i o wo examples des ib ed in [4℄: Ake mann's un ion and MCa hy's 91 un ion. Fu he wo k has o b e done o p o ide a go o d lib a y o lemmas o handle mul- ise s and hei op e a ions. We plan also o imp o e he use o de mul , in o de o p o ide only he name o he well- ounded ela ion, a oiding o gi e he un ions, a iables and e en asso ia ed wi h i . Up da ed e sions o he b o oks will b e in he web page. The examples p esen ed he e a e all o a heo e ial na u e. Ne e heless, a e- ma k gi en a he end o se ion I I I in [4℄, p oin ing an heu is i p o edu e o p o ing e mina ion o lo ops using mul ise s, sugges s ha his kind o o de ings ould b e applied o a wide lass o e mina ion p oblems and ha he sea h o a sui able mul ise measu e ould b e mehanized o some ex en . Ano he applia ion o mul i- se s o de ings is o p o ide he basis o some p o o s o e mina ion o e m ew i ing sys ems [1℄. We in end o make u he esea h ollowing hese wo lines. Re e enes 1. Baade , F., and Nipkow, T. Te m ew i ing and al l ha . Camb idge Uni e si y P ess, 1998. 2. B ok, B. de s u u e o ACL2 e sion 2.0. Tehnial Rep o , 1997. 3. Cowles, J. Knu h's gene aliza ion o MCa hy's 91 un ion. In Compu e -Aided Reasoning: ACL2 Case S udies , M. Kau mann, P. Manolios, and J S. Mo o e, Eds. Kluwe Aademi Publish- e s, 2000, h. 17. 4. De showi z, N., and Manna, Z. P o ing e mina ion wi h mul ise o de ings. In Annual In e na ional Col loquium on Au oma a, Languages and P og amming (1979), H. Mau e , Ed., no. 71 in LNCS, Sp inge -Ve lag, pp. 188{202. 5. Kau mann, M., Manolios, P., and Moo e, J S. Compu e -Aided Reasoning: An App oah . Kluwe Aademi Publishe s, 2000. 6. Kau mann, M., and Moo e, J S. ACL2 e sion 2.5. h p://www.s.u exas.edu/use s/mo o e- /al2/al2-do .h ml, 2000. 7. Klop, J. Te m ew i ing sys ems. Handbook o Logi in Compu e Siene (1992). 8. Ruiz-Reina, J., Alonso, J., Hidalgo, M., and Ma  n, F. h p://www-s.us.es/ ~ j uiz/al2- ew . Fo malizing equa ional easoning in he ACL2 heo em p o e , 2000. 9. Ruiz-Reina, J., Alonso, J., Hidalgo, M., and Ma  n, F. Fo malizing ew i ing in he ACL2 heo em p o e . In P oeedings o AISC'2000 (Fi h In e na ional Con e ene A iial In el ligene and Symboli Compu a ion) ( o app ea ), LNCS, Sp inge Ve lag.