4.57/2.08 YES 4.57/2.10 4.57/2.10 Problem: 4.57/2.10 b(a(b(b(x)))) -> b(b(b(a(b(x))))) 4.57/2.10 b(a(a(b(b(x))))) -> b(a(b(b(a(a(b(x))))))) 4.57/2.10 b(a(a(a(b(b(x)))))) -> b(a(a(b(b(a(a(a(b(x))))))))) 4.57/2.10 4.57/2.10 Proof: 4.57/2.10 Church Rosser Transformation Processor (okui): 4.57/2.10 4.57/2.10 simultaneous critical peaks: 4.57/2.10 b(a(b(b(b(b(a(b(x289)))))))) 4.57/2.10 <-[0,0,0]- b(a(b(b(a(b(b(x289))))))) -[]-> 4.57/2.10 b(b(b(a(b(a(b(b(x289)))))))) 4.57/2.10 4.57/2.10 b(a(b(b(a(b(b(a(a(b(x290)))))))))) 4.57/2.10 <-[0,0,0]- b(a(b(b(a(a(b(b(x290)))))))) -[]-> 4.57/2.10 b(b(b(a(b(a(a(b(b(x290))))))))) 4.57/2.10 4.57/2.10 b(a(b(b(a(a(b(b(a(a(a(b(x291)))))))))))) 4.57/2.10 <-[0,0,0]- b(a(b(b(a(a(a(b(b(x291))))))))) -[]-> 4.57/2.10 b(b(b(a(b(a(a(a(b(b(x291)))))))))) 4.57/2.10 4.57/2.10 b(b(b(a(b(a(b(b(x)))))))) 4.57/2.10 <-[]- b(a(b(b(a(b(b(x))))))) -[0,0,0]-> 4.57/2.10 b(a(b(b(b(b(a(b(x)))))))) 4.57/2.10 4.57/2.10 b(b(b(a(b(a(b(b(b(b(a(b(x294)))))))))))) 4.57/2.10 <-[|0,0,0,0,0,0]- b(a(b(b(a(b(b(a(b(b(x294)))))))))) -[0,0,0]-> 4.57/2.10 b(a(b(b(b(b(a(b(a(b(b(x294))))))))))) 4.57/2.10 4.57/2.10 b(b(b(a(b(a(b(b(a(b(b(a(a(b(x296)))))))))))))) 4.57/2.10 <-[|0,0,0,0,0,0]- b(a(b(b(a(b(b(a(a(b(b(x296))))))))))) -[0,0,0]-> 4.57/2.10 b(a(b(b(b(b(a(b(a(a(b(b(x296)))))))))))) 4.57/2.10 4.57/2.10 b(b(b(a(b(a(b(b(a(a(b(b(a(a(a(b(x298)))))))))))))))) 4.57/2.10 <-[|0,0,0,0,0,0]- b(a(b(b(a(b(b(a(a(a(b(b(x298)))))))))))) -[0,0,0]-> 4.57/2.10 b(a(b(b(b(b(a(b(a(a(a(b(b(x298))))))))))))) 4.57/2.10 4.57/2.10 b(a(b(b(a(a(b(a(b(b(x)))))))))) 4.57/2.10 <-[]- b(a(a(b(b(a(b(b(x)))))))) -[0,0,0,0]-> 4.57/2.10 b(a(a(b(b(b(b(a(b(x))))))))) 4.57/2.10 4.57/2.10 b(a(b(b(a(a(b(a(b(b(b(b(a(b(x301)))))))))))))) 4.57/2.10 <-[|0,0,0,0,0,0,0]- b(a(a(b(b(a(b(b(a(b(b(x301))))))))))) -[0,0,0,0]-> 4.57/2.10 b(a(a(b(b(b(b(a(b(a(b(b(x301)))))))))))) 4.57/2.10 4.57/2.10 b(a(b(b(a(a(b(a(b(b(a(b(b(a(a(b(x303)))))))))))))))) 4.57/2.10 <-[|0,0,0,0,0,0,0]- b(a(a(b(b(a(b(b(a(a(b(b(x303)))))))))))) -[0,0,0,0]-> 4.57/2.10 b(a(a(b(b(b(b(a(b(a(a(b(b(x303))))))))))))) 4.57/2.10 4.57/2.10 b(a(b(b(a(a(b(a(b(b(a(a(b(b(a(a(a(b(x305)))))))))))))))))) 4.57/2.10 <-[|0,0,0,0,0,0,0]- b(a(a(b(b(a(b(b(a(a(a(b(b(x305))))))))))))) -[ 4.57/2.10 0,0,0,0]-> 4.57/2.10 b(a(a(b(b(b(b(a(b(a(a(a(b(b(x305)))))))))))))) 4.57/2.10 4.57/2.10 b(a(a(b(b(a(a(a(b(a(b(b(x)))))))))))) 4.57/2.10 <-[]- b(a(a(a(b(b(a(b(b(x))))))))) -[0,0,0,0,0]-> 4.57/2.10 b(a(a(a(b(b(b(b(a(b(x)))))))))) 4.57/2.10 4.57/2.10 b(a(a(b(b(a(a(a(b(a(b(b(b(b(a(b(x308)))))))))))))))) 4.57/2.10 <-[|0,0,0,0,0,0,0,0]- b(a(a(a(b(b(a(b(b(a(b(b(x308)))))))))))) -[ 4.57/2.10 0,0,0,0,0]-> 4.57/2.10 b(a(a(a(b(b(b(b(a(b(a(b(b(x308))))))))))))) 4.57/2.10 4.57/2.10 b(a(a(b(b(a(a(a(b(a(b(b(a(b(b(a(a(b(x310)))))))))))))))))) 4.57/2.10 <-[|0,0,0,0,0,0,0,0]- b(a(a(a(b(b(a(b(b(a(a(b(b(x310))))))))))))) -[ 4.57/2.10 0,0,0,0,0]-> 4.57/2.10 b(a(a(a(b(b(b(b(a(b(a(a(b(b(x310)))))))))))))) 4.57/2.10 4.57/2.10 b(a(a(b(b(a(a(a(b(a(b(b(a(a(b(b(a(a(a(b(x312)))))))))))))))))))) 4.57/2.10 <-[|0,0,0,0,0,0,0,0]- b(a(a(a(b(b(a(b(b(a(a(a(b(b(x312)))))))))))))) -[ 4.57/2.10 0,0,0,0,0]-> 4.57/2.10 b(a(a(a(b(b(b(b(a(b(a(a(a(b(b(x312))))))))))))))) 4.57/2.10 4.57/2.10 b(a(a(b(b(b(b(a(b(x313))))))))) 4.57/2.10 <-[0,0,0,0]- b(a(a(b(b(a(b(b(x313)))))))) -[]-> 4.57/2.10 b(a(b(b(a(a(b(a(b(b(x313)))))))))) 4.57/2.10 4.57/2.10 b(a(a(b(b(a(b(b(a(a(b(x314))))))))))) 4.57/2.10 <-[0,0,0,0]- b(a(a(b(b(a(a(b(b(x314))))))))) -[]-> 4.57/2.10 b(a(b(b(a(a(b(a(a(b(b(x314))))))))))) 4.57/2.10 4.57/2.10 b(a(a(b(b(a(a(b(b(a(a(a(b(x315))))))))))))) 4.57/2.10 <-[0,0,0,0]- b(a(a(b(b(a(a(a(b(b(x315)))))))))) -[]-> 4.57/2.10 b(a(b(b(a(a(b(a(a(a(b(b(x315)))))))))))) 4.57/2.10 4.57/2.10 b(b(b(a(b(a(a(b(b(x))))))))) 4.57/2.10 <-[]- b(a(b(b(a(a(b(b(x)))))))) -[0,0,0]-> 4.57/2.10 b(a(b(b(a(b(b(a(a(b(x)))))))))) 4.57/2.10 4.57/2.10 b(b(b(a(b(a(a(b(b(b(b(a(b(x318))))))))))))) 4.57/2.10 <-[|0,0,0,0,0,0,0]- b(a(b(b(a(a(b(b(a(b(b(x318))))))))))) -[0,0,0]-> 4.57/2.10 b(a(b(b(a(b(b(a(a(b(a(b(b(x318))))))))))))) 4.57/2.10 4.57/2.10 b(b(b(a(b(a(a(b(b(a(b(b(a(a(b(x320))))))))))))))) 4.57/2.10 <-[|0,0,0,0,0,0,0]- b(a(b(b(a(a(b(b(a(a(b(b(x320)))))))))))) -[0,0,0]-> 4.57/2.10 b(a(b(b(a(b(b(a(a(b(a(a(b(b(x320)))))))))))))) 4.57/2.10 4.57/2.10 b(b(b(a(b(a(a(b(b(a(a(b(b(a(a(a(b(x322))))))))))))))))) 4.57/2.10 <-[|0,0,0,0,0,0,0]- b(a(b(b(a(a(b(b(a(a(a(b(b(x322))))))))))))) -[ 4.57/2.10 0,0,0]-> 4.57/2.10 b(a(b(b(a(b(b(a(a(b(a(a(a(b(b(x322))))))))))))))) 4.57/2.10 4.57/2.10 b(a(b(b(a(a(b(a(a(b(b(x))))))))))) 4.57/2.10 <-[]- b(a(a(b(b(a(a(b(b(x))))))))) -[0,0,0,0]-> 4.57/2.10 b(a(a(b(b(a(b(b(a(a(b(x))))))))))) 4.57/2.10 4.57/2.10 b(a(b(b(a(a(b(a(a(b(b(b(b(a(b(x325))))))))))))))) 4.57/2.10 <-[|0,0,0,0,0,0,0,0]- b(a(a(b(b(a(a(b(b(a(b(b(x325)))))))))))) -[ 4.57/2.10 0,0,0,0]-> 4.57/2.10 b(a(a(b(b(a(b(b(a(a(b(a(b(b(x325)))))))))))))) 4.57/2.10 4.57/2.10 b(a(b(b(a(a(b(a(a(b(b(a(b(b(a(a(b(x327))))))))))))))))) 4.57/2.10 <-[|0,0,0,0,0,0,0,0]- b(a(a(b(b(a(a(b(b(a(a(b(b(x327))))))))))))) -[ 4.57/2.10 0,0,0,0]-> 4.57/2.10 b(a(a(b(b(a(b(b(a(a(b(a(a(b(b(x327))))))))))))))) 4.57/2.10 4.57/2.10 b(a(b(b(a(a(b(a(a(b(b(a(a(b(b(a(a(a(b(x329))))))))))))))))))) 4.57/2.10 <-[|0,0,0,0,0,0,0,0]- b(a(a(b(b(a(a(b(b(a(a(a(b(b(x329)))))))))))))) -[ 4.57/2.10 0,0,0,0]-> 4.57/2.10 b(a(a(b(b(a(b(b(a(a(b(a(a(a(b(b(x329)))))))))))))))) 4.57/2.10 4.57/2.10 b(a(a(b(b(a(a(a(b(a(a(b(b(x))))))))))))) 4.57/2.10 <-[]- b(a(a(a(b(b(a(a(b(b(x)))))))))) -[0,0,0,0,0]-> 4.57/2.10 b(a(a(a(b(b(a(b(b(a(a(b(x)))))))))))) 4.57/2.10 4.57/2.10 b(a(a(b(b(a(a(a(b(a(a(b(b(b(b(a(b(x332))))))))))))))))) 4.57/2.10 <-[|0,0,0,0,0,0,0,0,0]- b(a(a(a(b(b(a(a(b(b(a(b(b(x332))))))))))))) -[ 4.57/2.10 0,0,0,0,0]-> 4.57/2.10 b(a(a(a(b(b(a(b(b(a(a(b(a(b(b(x332))))))))))))))) 4.57/2.10 4.57/2.10 b(a(a(b(b(a(a(a(b(a(a(b(b(a(b(b(a(a(b(x334))))))))))))))))))) 4.57/2.10 <-[|0,0,0,0,0,0,0,0,0]- b(a(a(a(b(b(a(a(b(b(a(a(b(b(x334)))))))))))))) -[ 4.57/2.10 0,0,0,0,0]-> 4.57/2.10 b(a(a(a(b(b(a(b(b(a(a(b(a(a(b(b(x334)))))))))))))))) 4.57/2.10 4.57/2.10 b(a(a(b(b(a(a(a(b(a(a(b(b(a(a(b(b(a(a(a(b(x336))))))))))))))))))))) 4.57/2.10 <-[|0,0,0,0,0,0,0,0,0]- b(a(a(a(b(b(a(a(b(b(a(a(a(b(b(x336))))))))))))))) -[ 4.57/2.10 0,0,0,0,0]-> 4.57/2.10 b(a(a(a(b(b(a(b(b(a(a(b(a(a(a(b(b(x336))))))))))))))))) 4.57/2.10 4.57/2.10 b(a(a(a(b(b(b(b(a(b(x337)))))))))) 4.57/2.10 <-[0,0,0,0,0]- b(a(a(a(b(b(a(b(b(x337))))))))) -[]-> 4.57/2.10 b(a(a(b(b(a(a(a(b(a(b(b(x337)))))))))))) 4.57/2.10 4.57/2.10 b(a(a(a(b(b(a(b(b(a(a(b(x338)))))))))))) 4.57/2.10 <-[0,0,0,0,0]- b(a(a(a(b(b(a(a(b(b(x338)))))))))) -[]-> 4.57/2.10 b(a(a(b(b(a(a(a(b(a(a(b(b(x338))))))))))))) 4.57/2.10 4.57/2.10 b(a(a(a(b(b(a(a(b(b(a(a(a(b(x339)))))))))))))) 4.57/2.10 <-[0,0,0,0,0]- b(a(a(a(b(b(a(a(a(b(b(x339))))))))))) -[]-> 4.57/2.10 b(a(a(b(b(a(a(a(b(a(a(a(b(b(x339)))))))))))))) 4.57/2.10 4.57/2.10 b(b(b(a(b(a(a(a(b(b(x)))))))))) 4.57/2.10 <-[]- b(a(b(b(a(a(a(b(b(x))))))))) -[0,0,0]-> 4.57/2.10 b(a(b(b(a(a(b(b(a(a(a(b(x)))))))))))) 4.57/2.10 4.57/2.10 b(b(b(a(b(a(a(a(b(b(b(b(a(b(x342)))))))))))))) 4.57/2.10 <-[|0,0,0,0,0,0,0,0]- b(a(b(b(a(a(a(b(b(a(b(b(x342)))))))))))) -[ 4.57/2.10 0,0,0]-> 4.57/2.10 b(a(b(b(a(a(b(b(a(a(a(b(a(b(b(x342))))))))))))))) 4.57/2.10 4.57/2.10 b(b(b(a(b(a(a(a(b(b(a(b(b(a(a(b(x344)))))))))))))))) 4.57/2.10 <-[|0,0,0,0,0,0,0,0]- b(a(b(b(a(a(a(b(b(a(a(b(b(x344))))))))))))) -[ 4.57/2.10 0,0,0]-> 4.57/2.10 b(a(b(b(a(a(b(b(a(a(a(b(a(a(b(b(x344)))))))))))))))) 4.57/2.10 4.57/2.10 b(b(b(a(b(a(a(a(b(b(a(a(b(b(a(a(a(b(x346)))))))))))))))))) 4.57/2.10 <-[|0,0,0,0,0,0,0,0]- b(a(b(b(a(a(a(b(b(a(a(a(b(b(x346)))))))))))))) -[ 4.57/2.10 0,0,0]-> 4.57/2.10 b(a(b(b(a(a(b(b(a(a(a(b(a(a(a(b(b(x346))))))))))))))))) 4.57/2.10 4.57/2.10 b(a(b(b(a(a(b(a(a(a(b(b(x)))))))))))) 4.57/2.10 <-[]- b(a(a(b(b(a(a(a(b(b(x)))))))))) -[0,0,0,0]-> 4.57/2.10 b(a(a(b(b(a(a(b(b(a(a(a(b(x))))))))))))) 4.57/2.10 4.57/2.10 b(a(b(b(a(a(b(a(a(a(b(b(b(b(a(b(x349)))))))))))))))) 4.57/2.10 <-[|0,0,0,0,0,0,0,0,0]- b(a(a(b(b(a(a(a(b(b(a(b(b(x349))))))))))))) -[ 4.57/2.10 0,0,0,0]-> 4.57/2.10 b(a(a(b(b(a(a(b(b(a(a(a(b(a(b(b(x349)))))))))))))))) 4.57/2.10 4.57/2.10 b(a(b(b(a(a(b(a(a(a(b(b(a(b(b(a(a(b(x351)))))))))))))))))) 4.57/2.10 <-[|0,0,0,0,0,0,0,0,0]- b(a(a(b(b(a(a(a(b(b(a(a(b(b(x351)))))))))))))) -[ 4.57/2.10 0,0,0,0]-> 4.57/2.10 b(a(a(b(b(a(a(b(b(a(a(a(b(a(a(b(b(x351))))))))))))))))) 4.57/2.10 4.57/2.10 b(a(b(b(a(a(b(a(a(a(b(b(a(a(b(b(a(a(a(b(x353)))))))))))))))))))) 4.57/2.10 <-[|0,0,0,0,0,0,0,0,0]- b(a(a(b(b(a(a(a(b(b(a(a(a(b(b(x353))))))))))))))) -[ 4.57/2.10 0,0,0,0]-> 4.57/2.10 b(a(a(b(b(a(a(b(b(a(a(a(b(a(a(a(b(b(x353)))))))))))))))))) 4.57/2.10 4.57/2.10 b(a(a(b(b(a(a(a(b(a(a(a(b(b(x)))))))))))))) 4.57/2.10 <-[]- b(a(a(a(b(b(a(a(a(b(b(x))))))))))) -[0,0,0,0,0]-> 4.57/2.10 b(a(a(a(b(b(a(a(b(b(a(a(a(b(x)))))))))))))) 4.57/2.10 4.57/2.10 b(a(a(b(b(a(a(a(b(a(a(a(b(b(b(b(a(b(x356)))))))))))))))))) 4.57/2.10 <-[|0,0,0,0,0,0,0,0,0,0]- b(a(a(a(b(b(a(a(a(b(b(a(b(b(x356)))))))))))))) -[ 4.57/2.10 0,0,0,0,0]-> 4.57/2.10 b(a(a(a(b(b(a(a(b(b(a(a(a(b(a(b(b(x356))))))))))))))))) 4.57/2.10 4.57/2.10 b(a(a(b(b(a(a(a(b(a(a(a(b(b(a(b(b(a(a(b(x358)))))))))))))))))))) 4.57/2.10 <-[|0,0,0,0,0,0,0,0,0,0]- b(a(a(a(b(b(a(a(a(b(b(a(a(b(b(x358))))))))))))))) -[ 4.57/2.10 0,0,0,0,0]-> 4.57/2.10 b(a(a(a(b(b(a(a(b(b(a(a(a(b(a(a(b(b(x358)))))))))))))))))) 4.57/2.10 4.57/2.10 b(a(a(b(b(a(a(a(b(a(a(a(b(b(a(a(b(b(a(a(a(b(x360)))))))))))))))))))))) 4.57/2.10 <-[|0,0,0,0,0,0,0,0,0,0]- b(a(a(a(b(b(a(a(a(b(b(a(a(a(b(b(x360)))))))))))))))) -[ 4.57/2.10 0,0,0,0,0]-> 4.57/2.10 b(a(a(a(b(b(a(a(b(b(a(a(a(b(a(a(a(b(b(x360))))))))))))))))))) 4.57/2.10 joinable 4.57/2.10 Qed 4.57/2.10 EOF