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(x343)))))))) <-[0,0,0]- b(a(b(b(a(b(b(x343))))))) -[]-> b(b(b(a(b(a(b(b(x343)))))))) b(a(b(b(a(b(b(a(a(b(x344)))))))))) <-[0,0,0]- b(a(b(b(a(a(b(b(x344)))))))) -[]-> b(b(b(a(b(a(a(b(b(x344))))))))) b(a(b(b(a(a(b(b(a(a(a(b(x345)))))))))))) <-[0,0,0]- b(a(b(b(a(a(a(b(b(x345))))))))) -[]-> b(b(b(a(b(a(a(a(b(b(x345)))))))))) 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(x348)))))))))))) <-[|0,0,0,0,0,0]- b(a(b(b(a(b(b(a(b(b(x348)))))))))) -[0,0,0]-> b(a(b(b(b(b(a(b(a(b(b(x348))))))))))) b(b(b(a(b(a(b(b(a(b(b(a(a(b(x350)))))))))))))) <-[|0,0,0,0,0,0]- b(a(b(b(a(b(b(a(a(b(b(x350))))))))))) -[0,0,0]-> b(a(b(b(b(b(a(b(a(a(b(b(x350)))))))))))) b(b(b(a(b(a(b(b(a(a(b(b(a(a(a(b(x352)))))))))))))))) <-[|0,0,0,0,0,0]- b(a(b(b(a(b(b(a(a(a(b(b(x352)))))))))))) -[0,0,0]-> b(a(b(b(b(b(a(b(a(a(a(b(b(x352))))))))))))) 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(x355)))))))))))))) <-[|0,0,0,0,0,0,0]- b(a(a(b(b(a(b(b(a(b(b(x355))))))))))) -[0,0,0,0]-> b(a(a(b(b(b(b(a(b(a(b(b(x355)))))))))))) b(a(b(b(a(a(b(a(b(b(a(b(b(a(a(b(x357)))))))))))))))) <-[|0,0,0,0,0,0,0]- b(a(a(b(b(a(b(b(a(a(b(b(x357)))))))))))) -[0,0,0,0]-> b(a(a(b(b(b(b(a(b(a(a(b(b(x357))))))))))))) b(a(b(b(a(a(b(a(b(b(a(a(b(b(a(a(a(b(x359)))))))))))))))))) <-[|0,0,0,0,0,0,0]- b(a(a(b(b(a(b(b(a(a(a(b(b(x359))))))))))))) -[ 0,0,0,0]-> b(a(a(b(b(b(b(a(b(a(a(a(b(b(x359)))))))))))))) 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(x362)))))))))))))))) <-[|0,0,0,0,0,0,0,0]- b(a(a(a(b(b(a(b(b(a(b(b(x362)))))))))))) -[ 0,0,0,0,0]-> b(a(a(a(b(b(b(b(a(b(a(b(b(x362))))))))))))) b(a(a(b(b(a(a(a(b(a(b(b(a(b(b(a(a(b(x364)))))))))))))))))) <-[|0,0,0,0,0,0,0,0]- b(a(a(a(b(b(a(b(b(a(a(b(b(x364))))))))))))) -[ 0,0,0,0,0]-> b(a(a(a(b(b(b(b(a(b(a(a(b(b(x364)))))))))))))) b(a(a(b(b(a(a(a(b(a(b(b(a(a(b(b(a(a(a(b(x366)))))))))))))))))))) <-[|0,0,0,0,0,0,0,0]- b(a(a(a(b(b(a(b(b(a(a(a(b(b(x366)))))))))))))) -[ 0,0,0,0,0]-> b(a(a(a(b(b(b(b(a(b(a(a(a(b(b(x366))))))))))))))) b(a(a(b(b(b(b(a(b(x367))))))))) <-[0,0,0,0]- b(a(a(b(b(a(b(b(x367)))))))) -[]-> b(a(b(b(a(a(b(a(b(b(x367)))))))))) b(a(a(b(b(a(b(b(a(a(b(x368))))))))))) <-[0,0,0,0]- b(a(a(b(b(a(a(b(b(x368))))))))) -[]-> b(a(b(b(a(a(b(a(a(b(b(x368))))))))))) b(a(a(b(b(a(a(b(b(a(a(a(b(x369))))))))))))) <-[0,0,0,0]- b(a(a(b(b(a(a(a(b(b(x369)))))))))) -[]-> b(a(b(b(a(a(b(a(a(a(b(b(x369)))))))))))) 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(x372))))))))))))) <-[|0,0,0,0,0,0,0]- b(a(b(b(a(a(b(b(a(b(b(x372))))))))))) -[0,0,0]-> b(a(b(b(a(b(b(a(a(b(a(b(b(x372))))))))))))) b(b(b(a(b(a(a(b(b(a(b(b(a(a(b(x374))))))))))))))) <-[|0,0,0,0,0,0,0]- b(a(b(b(a(a(b(b(a(a(b(b(x374)))))))))))) -[0,0,0]-> b(a(b(b(a(b(b(a(a(b(a(a(b(b(x374)))))))))))))) b(b(b(a(b(a(a(b(b(a(a(b(b(a(a(a(b(x376))))))))))))))))) <-[|0,0,0,0,0,0,0]- b(a(b(b(a(a(b(b(a(a(a(b(b(x376))))))))))))) -[ 0,0,0]-> b(a(b(b(a(b(b(a(a(b(a(a(a(b(b(x376))))))))))))))) 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(x379))))))))))))))) <-[|0,0,0,0,0,0,0,0]- b(a(a(b(b(a(a(b(b(a(b(b(x379)))))))))))) -[ 0,0,0,0]-> b(a(a(b(b(a(b(b(a(a(b(a(b(b(x379)))))))))))))) b(a(b(b(a(a(b(a(a(b(b(a(b(b(a(a(b(x381))))))))))))))))) <-[|0,0,0,0,0,0,0,0]- b(a(a(b(b(a(a(b(b(a(a(b(b(x381))))))))))))) -[ 0,0,0,0]-> b(a(a(b(b(a(b(b(a(a(b(a(a(b(b(x381))))))))))))))) b(a(b(b(a(a(b(a(a(b(b(a(a(b(b(a(a(a(b(x383))))))))))))))))))) <-[|0,0,0,0,0,0,0,0]- b(a(a(b(b(a(a(b(b(a(a(a(b(b(x383)))))))))))))) -[ 0,0,0,0]-> b(a(a(b(b(a(b(b(a(a(b(a(a(a(b(b(x383)))))))))))))))) 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(x386))))))))))))))))) <-[|0,0,0,0,0,0,0,0,0]- b(a(a(a(b(b(a(a(b(b(a(b(b(x386))))))))))))) -[ 0,0,0,0,0]-> b(a(a(a(b(b(a(b(b(a(a(b(a(b(b(x386))))))))))))))) b(a(a(b(b(a(a(a(b(a(a(b(b(a(b(b(a(a(b(x388))))))))))))))))))) <-[|0,0,0,0,0,0,0,0,0]- b(a(a(a(b(b(a(a(b(b(a(a(b(b(x388)))))))))))))) -[ 0,0,0,0,0]-> b(a(a(a(b(b(a(b(b(a(a(b(a(a(b(b(x388)))))))))))))))) b(a(a(b(b(a(a(a(b(a(a(b(b(a(a(b(b(a(a(a(b(x390))))))))))))))))))))) <-[|0,0,0,0,0,0,0,0,0]- b(a(a(a(b(b(a(a(b(b(a(a(a(b(b(x390))))))))))))))) -[ 0,0,0,0,0]-> b(a(a(a(b(b(a(b(b(a(a(b(a(a(a(b(b(x390))))))))))))))))) b(a(a(a(b(b(b(b(a(b(x391)))))))))) <-[0,0,0,0,0]- b(a(a(a(b(b(a(b(b(x391))))))))) -[]-> b(a(a(b(b(a(a(a(b(a(b(b(x391)))))))))))) b(a(a(a(b(b(a(b(b(a(a(b(x392)))))))))))) <-[0,0,0,0,0]- b(a(a(a(b(b(a(a(b(b(x392)))))))))) -[]-> b(a(a(b(b(a(a(a(b(a(a(b(b(x392))))))))))))) b(a(a(a(b(b(a(a(b(b(a(a(a(b(x393)))))))))))))) <-[0,0,0,0,0]- b(a(a(a(b(b(a(a(a(b(b(x393))))))))))) -[]-> b(a(a(b(b(a(a(a(b(a(a(a(b(b(x393)))))))))))))) 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(x396)))))))))))))) <-[|0,0,0,0,0,0,0,0]- b(a(b(b(a(a(a(b(b(a(b(b(x396)))))))))))) -[ 0,0,0]-> b(a(b(b(a(a(b(b(a(a(a(b(a(b(b(x396))))))))))))))) b(b(b(a(b(a(a(a(b(b(a(b(b(a(a(b(x398)))))))))))))))) <-[|0,0,0,0,0,0,0,0]- b(a(b(b(a(a(a(b(b(a(a(b(b(x398))))))))))))) -[ 0,0,0]-> b(a(b(b(a(a(b(b(a(a(a(b(a(a(b(b(x398)))))))))))))))) b(b(b(a(b(a(a(a(b(b(a(a(b(b(a(a(a(b(x400)))))))))))))))))) <-[|0,0,0,0,0,0,0,0]- b(a(b(b(a(a(a(b(b(a(a(a(b(b(x400)))))))))))))) -[ 0,0,0]-> b(a(b(b(a(a(b(b(a(a(a(b(a(a(a(b(b(x400))))))))))))))))) 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(x403)))))))))))))))) <-[|0,0,0,0,0,0,0,0,0]- b(a(a(b(b(a(a(a(b(b(a(b(b(x403))))))))))))) -[ 0,0,0,0]-> b(a(a(b(b(a(a(b(b(a(a(a(b(a(b(b(x403)))))))))))))))) b(a(b(b(a(a(b(a(a(a(b(b(a(b(b(a(a(b(x405)))))))))))))))))) <-[|0,0,0,0,0,0,0,0,0]- b(a(a(b(b(a(a(a(b(b(a(a(b(b(x405)))))))))))))) -[ 0,0,0,0]-> b(a(a(b(b(a(a(b(b(a(a(a(b(a(a(b(b(x405))))))))))))))))) b(a(b(b(a(a(b(a(a(a(b(b(a(a(b(b(a(a(a(b(x407)))))))))))))))))))) <-[|0,0,0,0,0,0,0,0,0]- b(a(a(b(b(a(a(a(b(b(a(a(a(b(b(x407))))))))))))))) -[ 0,0,0,0]-> b(a(a(b(b(a(a(b(b(a(a(a(b(a(a(a(b(b(x407)))))))))))))))))) 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(x410)))))))))))))))))) <-[|0,0,0,0,0,0,0,0,0,0]- b(a(a(a(b(b(a(a(a(b(b(a(b(b(x410)))))))))))))) -[ 0,0,0,0,0]-> b(a(a(a(b(b(a(a(b(b(a(a(a(b(a(b(b(x410))))))))))))))))) b(a(a(b(b(a(a(a(b(a(a(a(b(b(a(b(b(a(a(b(x412)))))))))))))))))))) <-[|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(x412))))))))))))))) -[ 0,0,0,0,0]-> b(a(a(a(b(b(a(a(b(b(a(a(a(b(a(a(b(b(x412)))))))))))))))))) b(a(a(b(b(a(a(a(b(a(a(a(b(b(a(a(b(b(a(a(a(b(x414)))))))))))))))))))))) <-[|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(x414)))))))))))))))) -[ 0,0,0,0,0]-> b(a(a(a(b(b(a(a(b(b(a(a(a(b(a(a(a(b(b(x414))))))))))))))))))) joinable Qed