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