Problem: +(x,0()) -> x +(x,x) -> 0() *(x,1()) -> x *(x,x) -> x *(x,0()) -> 0() *(x,+(y,z)) -> +(*(x,y),*(x,z)) or(x,y) -> +(*(x,y),+(x,y)) implies(x,y) -> +(*(x,y),+(x,1())) equivalent(x,y) -> +(+(x,y),1()) not(x) -> +(x,1()) +(+(x,y),z) -> +(x,+(y,z)) +(x,+(y,z)) -> +(+(x,y),z) +(x,y) -> +(y,x) *(*(x,y),z) -> *(x,*(y,z)) *(x,*(y,z)) -> *(*(x,y),z) *(x,y) -> *(y,x) Proof: Church Rosser Transformation Processor: strict: weak: critical peaks: 77 0() <-0|[]- +(0(),0()) -1|[]-> 0() *(x,y) <-0|1[]- *(x,+(y,0())) -5|[]-> +(*(x,y),*(x,0())) +(x,y) <-0|[]- +(+(x,y),0()) -10|[]-> +(x,+(y,0())) +(x,z) <-0|0[]- +(+(x,0()),z) -10|[]-> +(x,+(0(),z)) +(x,y) <-0|1[]- +(x,+(y,0())) -11|[]-> +(+(x,y),0()) x <-0|[]- +(x,0()) -12|[]-> +(0(),x) 0() <-1|[]- +(0(),0()) -0|[]-> 0() *(x,0()) <-1|1[]- *(x,+(z,z)) -5|[]-> +(*(x,z),*(x,z)) 0() <-1|[]- +(+(x,y),+(x,y)) -10|[]-> +(x,+(y,+(x,y))) +(0(),z) <-1|0[]- +(+(y,y),z) -10|[]-> +(y,+(y,z)) 0() <-1|[]- +(+(y,z),+(y,z)) -11|[]-> +(+(+(y,z),y),z) +(x,0()) <-1|1[]- +(x,+(z,z)) -11|[]-> +(+(x,z),z) 0() <-1|[]- +(y,y) -12|[]-> +(y,y) 1() <-2|[]- *(1(),1()) -3|[]-> 1() *(x,y) <-2|[]- *(*(x,y),1()) -13|[]-> *(x,*(y,1())) *(x,z) <-2|0[]- *(*(x,1()),z) -13|[]-> *(x,*(1(),z)) *(x,y) <-2|1[]- *(x,*(y,1())) -14|[]-> *(*(x,y),1()) x <-2|[]- *(x,1()) -15|[]-> *(1(),x) 1() <-3|[]- *(1(),1()) -2|[]-> 1() 0() <-3|[]- *(0(),0()) -4|[]-> 0() +(y,z) <-3|[]- *(+(y,z),+(y,z)) -5|[]-> +(*(+(y,z),y),*(+(y,z),z)) *(x,y) <-3|[]- *(*(x,y),*(x,y)) -13|[]-> *(x,*(y,*(x,y))) *(y,z) <-3|0[]- *(*(y,y),z) -13|[]-> *(y,*(y,z)) *(y,z) <-3|[]- *(*(y,z),*(y,z)) -14|[]-> *(*(*(y,z),y),z) *(x,z) <-3|1[]- *(x,*(z,z)) -14|[]-> *(*(x,z),z) y <-3|[]- *(y,y) -15|[]-> *(y,y) 0() <-4|[]- *(0(),0()) -3|[]-> 0() 0() <-4|[]- *(*(x,y),0()) -13|[]-> *(x,*(y,0())) *(0(),z) <-4|0[]- *(*(x,0()),z) -13|[]-> *(x,*(0(),z)) *(x,0()) <-4|1[]- *(x,*(y,0())) -14|[]-> *(*(x,y),0()) 0() <-4|[]- *(x,0()) -15|[]-> *(0(),x) +(*(+(x779,x780),x779),*(+(x779,x780),x780)) <-5|[]- *(+(x779,x780),+(x779,x780)) -3| []-> +(x779,x780) +(*(*(x,y),x782),*(*(x,y),x783)) <-5|[]- *(*(x,y),+(x782,x783)) -13|[]-> *(x,*(y,+(x782,x783))) *(+(*(x,x785),*(x,x786)),z) <-5|0[]- *(*(x,+(x785,x786)),z) -13|[]-> *(x,*(+(x785,x786),z)) *(x,+(*(y,x788),*(y,x789))) <-5|1[]- *(x,*(y,+(x788,x789))) -14|[]-> *(*(x,y),+(x788,x789)) +(*(x,x791),*(x,x792)) <-5|[]- *(x,+(x791,x792)) -15|[]-> *(+(x791,x792),x) +(x793,+(x794,0())) <-10|[]- +(+(x793,x794),0()) -0|[]-> +(x793,x794) +(x796,+(x797,+(x796,x797))) <-10|[]- +(+(x796,x797),+(x796,x797)) -1|[]-> 0() *(x,+(x799,+(x800,z))) <-10|1[]- *(x,+(+(x799,x800),z)) -5|[]-> +(*(x,+(x799,x800)),*(x,z)) +(+(x802,+(x803,y)),z) <-10|0[]- +(+(+(x802,x803),y),z) -10|[]-> +(+(x802,x803),+(y,z)) +(x805,+(x806,+(y,z))) <-10|[]- +(+(x805,x806),+(y,z)) -11|[]-> +(+(+(x805,x806),y),z) +(x,+(x808,+(x809,z))) <-10|1[]- +(x,+(+(x808,x809),z)) -11|[]-> +(+(x,+(x808,x809)),z) +(x811,+(x812,y)) <-10|[]- +(+(x811,x812),y) -12|[]-> +(y,+(x811,x812)) +(+(+(x815,x816),x815),x816) <-11|[]- +(+(x815,x816),+(x815,x816)) -1|[]-> 0() *(x,+(+(y,x818),x819)) <-11|1[]- *(x,+(y,+(x818,x819))) -5|[]-> +(*(x,y),*(x,+(x818,x819))) +(+(+(x,y),x821),x822) <-11|[]- +(+(x,y),+(x821,x822)) -10|[]-> +(x,+(y,+(x821,x822))) +(+(+(x,x824),x825),z) <-11|0[]- +(+(x,+(x824,x825)),z) -10|[]-> +(x,+(+(x824,x825),z)) +(x,+(+(y,x827),x828)) <-11|1[]- +(x,+(y,+(x827,x828))) -11|[]-> +(+(x,y),+(x827,x828)) +(+(x,x830),x831) <-11|[]- +(x,+(x830,x831)) -12|[]-> +(+(x830,x831),x) +(0(),x) <-12|[]- +(x,0()) -0|[]-> x +(x,x) <-12|[]- +(x,x) -1|[]-> 0() *(x,+(z,y)) <-12|1[]- *(x,+(y,z)) -5|[]-> +(*(x,y),*(x,z)) +(z,+(x,y)) <-12|[]- +(+(x,y),z) -10|[]-> +(x,+(y,z)) +(+(y,x),z) <-12|0[]- +(+(x,y),z) -10|[]-> +(x,+(y,z)) +(+(y,z),x) <-12|[]- +(x,+(y,z)) -11|[]-> +(+(x,y),z) +(x,+(z,y)) <-12|1[]- +(x,+(y,z)) -11|[]-> +(+(x,y),z) *(x846,*(x847,1())) <-13|[]- *(*(x846,x847),1()) -2|[]-> *(x846,x847) *(x849,*(x850,*(x849,x850))) <-13|[]- *(*(x849,x850),*(x849,x850)) -3|[]-> *(x849,x850) *(x852,*(x853,0())) <-13|[]- *(*(x852,x853),0()) -4|[]-> 0() *(x855,*(x856,+(y,z))) <-13|[]- *(*(x855,x856),+(y,z)) -5|[]-> +(*(*(x855,x856),y), * (*(x855,x856),z)) *(*(x858,*(x859,y)),z) <-13|0[]- *(*(*(x858,x859),y),z) -13|[]-> *(*(x858,x859),*(y,z)) *(x861,*(x862,*(y,z))) <-13|[]- *(*(x861,x862),*(y,z)) -14|[]-> *(*(*(x861,x862),y),z) *(x,*(x864,*(x865,z))) <-13|1[]- *(x,*(*(x864,x865),z)) -14|[]-> *(*(x,*(x864,x865)),z) *(x867,*(x868,y)) <-13|[]- *(*(x867,x868),y) -15|[]-> *(y,*(x867,x868)) *(*(*(x871,x872),x871),x872) <-14|[]- *(*(x871,x872),*(x871,x872)) -3|[]-> *(x871,x872) *(*(*(x,y),x874),x875) <-14|[]- *(*(x,y),*(x874,x875)) -13|[]-> *(x,*(y,*(x874,x875))) *(*(*(x,x877),x878),z) <-14|0[]- *(*(x,*(x877,x878)),z) -13|[]-> *(x,*(*(x877,x878),z)) *(x,*(*(y,x880),x881)) <-14|1[]- *(x,*(y,*(x880,x881))) -14|[]-> *(*(x,y),*(x880,x881)) *(*(x,x883),x884) <-14|[]- *(x,*(x883,x884)) -15|[]-> *(*(x883,x884),x) *(1(),x) <-15|[]- *(x,1()) -2|[]-> x *(x,x) <-15|[]- *(x,x) -3|[]-> x *(0(),x) <-15|[]- *(x,0()) -4|[]-> 0() *(+(y,z),x) <-15|[]- *(x,+(y,z)) -5|[]-> +(*(x,y),*(x,z)) *(z,*(x,y)) <-15|[]- *(*(x,y),z) -13|[]-> *(x,*(y,z)) *(*(y,x),z) <-15|0[]- *(*(x,y),z) -13|[]-> *(x,*(y,z)) *(*(y,z),x) <-15|[]- *(x,*(y,z)) -14|[]-> *(*(x,y),z) *(x,*(z,y)) <-15|1[]- *(x,*(y,z)) -14|[]-> *(*(x,y),z) Redundant Rules Transformation: +(x,0()) -> x +(x,x) -> 0() *(x,1()) -> x *(x,x) -> x *(x,0()) -> 0() *(x,+(y,z)) -> +(*(x,y),*(x,z)) or(x,y) -> +(*(x,y),+(x,y)) implies(x,y) -> +(*(x,y),+(x,1())) equivalent(x,y) -> +(+(x,y),1()) not(x) -> +(x,1()) +(x,+(y,z)) -> +(+(x,y),z) +(x,y) -> +(y,x) *(x,*(y,z)) -> *(*(x,y),z) *(x,y) -> *(y,x) Church Rosser Transformation Processor (ac): f9_AC(x,0()) -> x f9_AC(x,x) -> 0() f11_AC(x,1()) -> x f11_AC(x,x) -> x f11_AC(x,0()) -> 0() f11_AC(x,f9_AC(y,z)) -> f9_AC(f11_AC(x,y),f11_AC(x,z)) or(x,y) -> f9_AC(f11_AC(x,y),f9_AC(x,y)) implies(x,y) -> f9_AC(f11_AC(x,y),f9_AC(x,1())) equivalent(x,y) -> f9_AC(f9_AC(x,y),1()) not(x) -> f9_AC(x,1()) AC critical peaks: joinable AC-RPO Processor: precedence: implies > equivalent > not > 1 > or > f11_AC > f9_AC > 0 status: equivalent:mul implies:mul or:mul problem: Qed