YES Problem: c(c(x)) -> a(c(x)) c(b(x)) -> c(c(x)) b(a(x)) -> c(b(x)) a(b(x)) -> b(a(x)) c(a(x)) -> c(a(x)) b(c(x)) -> c(c(x)) c(c(x)) -> b(c(x)) c(a(x)) -> b(c(x)) Proof: Church Rosser Transformation Processor (no redundant rules): strict: weak: critical peaks: 20 c(b(c(x99))) <-0|0[]- c(c(a(x99))) -1|[]-> b(c(a(x99))) b(b(c(x100))) <-0|0[]- b(c(a(x100))) -2|[]-> c(c(a(x100))) c(b(c(x101))) <-0|0[]- c(c(a(x101))) -6|[]-> a(c(a(x101))) c(b(c(x102))) <-1|0[]- c(c(c(x102))) -1|[]-> b(c(c(x102))) b(b(c(x103))) <-1|0[]- b(c(c(x103))) -2|[]-> c(c(c(x103))) b(c(x)) <-1|[]- c(c(x)) -6|[]-> a(c(x)) c(b(c(x105))) <-1|0[]- c(c(c(x105))) -6|[]-> a(c(c(x105))) a(c(c(x106))) <-2|0[]- a(b(c(x106))) -3|[]-> b(a(c(x106))) c(c(c(x107))) <-2|0[]- c(b(c(x107))) -5|[]-> c(c(c(x107))) c(b(a(x108))) <-3|0[]- c(a(b(x108))) -0|[]-> b(c(b(x108))) b(b(a(x109))) <-3|0[]- b(a(b(x109))) -4|[]-> c(b(b(x109))) a(c(b(x110))) <-4|0[]- a(b(a(x110))) -3|[]-> b(a(a(x110))) c(c(b(x111))) <-4|0[]- c(b(a(x111))) -5|[]-> c(c(a(x111))) c(c(c(x112))) <-5|0[]- c(c(b(x112))) -1|[]-> b(c(b(x112))) b(c(c(x113))) <-5|0[]- b(c(b(x113))) -2|[]-> c(c(b(x113))) c(c(c(x114))) <-5|0[]- c(c(b(x114))) -6|[]-> a(c(b(x114))) a(c(x)) <-6|[]- c(c(x)) -1|[]-> b(c(x)) c(a(c(x116))) <-6|0[]- c(c(c(x116))) -1|[]-> b(c(c(x116))) b(a(c(x117))) <-6|0[]- b(c(c(x117))) -2|[]-> c(c(c(x117))) c(a(c(x118))) <-6|0[]- c(c(c(x118))) -6|[]-> a(c(c(x118))) Redundant Rules Transformation: c(a(x)) -> b(c(x)) c(c(x)) -> b(c(x)) b(c(x)) -> c(c(x)) a(b(x)) -> b(a(x)) b(a(x)) -> c(b(x)) c(b(x)) -> c(c(x)) c(c(x)) -> a(c(x)) c(a(x)) -> c(c(x)) c(c(x)) -> c(c(x)) b(c(x)) -> b(c(x)) b(c(x)) -> a(c(x)) a(b(x)) -> c(b(x)) b(a(x)) -> c(c(x)) c(b(x)) -> b(c(x)) c(b(x)) -> a(c(x)) Church Rosser Transformation Processor (redex): strict: weak: c(b(x)) -> a(c(x)) c(b(x)) -> b(c(x)) b(a(x)) -> c(c(x)) a(b(x)) -> c(b(x)) b(c(x)) -> a(c(x)) b(c(x)) -> b(c(x)) c(c(x)) -> c(c(x)) c(a(x)) -> c(c(x)) c(c(x)) -> a(c(x)) c(b(x)) -> c(c(x)) b(a(x)) -> c(b(x)) a(b(x)) -> b(a(x)) b(c(x)) -> c(c(x)) c(c(x)) -> b(c(x)) c(a(x)) -> b(c(x)) critical peaks: 105 c(b(c(x569))) <-0|0[]- c(c(a(x569))) -1|[]-> b(c(a(x569))) b(b(c(x570))) <-0|0[]- b(c(a(x570))) -2|[]-> c(c(a(x570))) c(b(c(x571))) <-0|0[]- c(c(a(x571))) -6|[]-> a(c(a(x571))) b(c(x)) <-0|[]- c(a(x)) -7|[]-> c(c(x)) c(b(c(x573))) <-0|0[]- c(c(a(x573))) -8|[]-> c(c(a(x573))) b(b(c(x574))) <-0|0[]- b(c(a(x574))) -9|[]-> b(c(a(x574))) b(b(c(x575))) <-0|0[]- b(c(a(x575))) -10|[]-> a(c(a(x575))) c(b(c(x576))) <-1|0[]- c(c(c(x576))) -1|[]-> b(c(c(x576))) b(b(c(x577))) <-1|0[]- b(c(c(x577))) -2|[]-> c(c(c(x577))) b(c(x)) <-1|[]- c(c(x)) -6|[]-> a(c(x)) c(b(c(x579))) <-1|0[]- c(c(c(x579))) -6|[]-> a(c(c(x579))) b(c(x)) <-1|[]- c(c(x)) -8|[]-> c(c(x)) c(b(c(x581))) <-1|0[]- c(c(c(x581))) -8|[]-> c(c(c(x581))) b(b(c(x582))) <-1|0[]- b(c(c(x582))) -9|[]-> b(c(c(x582))) b(b(c(x583))) <-1|0[]- b(c(c(x583))) -10|[]-> a(c(c(x583))) a(c(c(x584))) <-2|0[]- a(b(c(x584))) -3|[]-> b(a(c(x584))) c(c(c(x585))) <-2|0[]- c(b(c(x585))) -5|[]-> c(c(c(x585))) c(c(x)) <-2|[]- b(c(x)) -9|[]-> b(c(x)) c(c(x)) <-2|[]- b(c(x)) -10|[]-> a(c(x)) a(c(c(x588))) <-2|0[]- a(b(c(x588))) -11|[]-> c(b(c(x588))) c(c(c(x589))) <-2|0[]- c(b(c(x589))) -13|[]-> b(c(c(x589))) c(c(c(x590))) <-2|0[]- c(b(c(x590))) -14|[]-> a(c(c(x590))) c(b(a(x591))) <-3|0[]- c(a(b(x591))) -0|[]-> b(c(b(x591))) b(b(a(x592))) <-3|0[]- b(a(b(x592))) -4|[]-> c(b(b(x592))) c(b(a(x593))) <-3|0[]- c(a(b(x593))) -7|[]-> c(c(b(x593))) b(a(x)) <-3|[]- a(b(x)) -11|[]-> c(b(x)) b(b(a(x595))) <-3|0[]- b(a(b(x595))) -12|[]-> c(c(b(x595))) a(c(b(x596))) <-4|0[]- a(b(a(x596))) -3|[]-> b(a(a(x596))) c(c(b(x597))) <-4|0[]- c(b(a(x597))) -5|[]-> c(c(a(x597))) a(c(b(x598))) <-4|0[]- a(b(a(x598))) -11|[]-> c(b(a(x598))) c(b(x)) <-4|[]- b(a(x)) -12|[]-> c(c(x)) c(c(b(x600))) <-4|0[]- c(b(a(x600))) -13|[]-> b(c(a(x600))) c(c(b(x601))) <-4|0[]- c(b(a(x601))) -14|[]-> a(c(a(x601))) c(c(c(x602))) <-5|0[]- c(c(b(x602))) -1|[]-> b(c(b(x602))) b(c(c(x603))) <-5|0[]- b(c(b(x603))) -2|[]-> c(c(b(x603))) c(c(c(x604))) <-5|0[]- c(c(b(x604))) -6|[]-> a(c(b(x604))) c(c(c(x605))) <-5|0[]- c(c(b(x605))) -8|[]-> c(c(b(x605))) b(c(c(x606))) <-5|0[]- b(c(b(x606))) -9|[]-> b(c(b(x606))) b(c(c(x607))) <-5|0[]- b(c(b(x607))) -10|[]-> a(c(b(x607))) c(c(x)) <-5|[]- c(b(x)) -13|[]-> b(c(x)) c(c(x)) <-5|[]- c(b(x)) -14|[]-> a(c(x)) a(c(x)) <-6|[]- c(c(x)) -1|[]-> b(c(x)) c(a(c(x611))) <-6|0[]- c(c(c(x611))) -1|[]-> b(c(c(x611))) b(a(c(x612))) <-6|0[]- b(c(c(x612))) -2|[]-> c(c(c(x612))) c(a(c(x613))) <-6|0[]- c(c(c(x613))) -6|[]-> a(c(c(x613))) a(c(x)) <-6|[]- c(c(x)) -8|[]-> c(c(x)) c(a(c(x615))) <-6|0[]- c(c(c(x615))) -8|[]-> c(c(c(x615))) b(a(c(x616))) <-6|0[]- b(c(c(x616))) -9|[]-> b(c(c(x616))) b(a(c(x617))) <-6|0[]- b(c(c(x617))) -10|[]-> a(c(c(x617))) c(c(x)) <-7|[]- c(a(x)) -0|[]-> b(c(x)) c(c(c(x619))) <-7|0[]- c(c(a(x619))) -1|[]-> b(c(a(x619))) b(c(c(x620))) <-7|0[]- b(c(a(x620))) -2|[]-> c(c(a(x620))) c(c(c(x621))) <-7|0[]- c(c(a(x621))) -6|[]-> a(c(a(x621))) c(c(c(x622))) <-7|0[]- c(c(a(x622))) -8|[]-> c(c(a(x622))) b(c(c(x623))) <-7|0[]- b(c(a(x623))) -9|[]-> b(c(a(x623))) b(c(c(x624))) <-7|0[]- b(c(a(x624))) -10|[]-> a(c(a(x624))) c(c(x)) <-8|[]- c(c(x)) -1|[]-> b(c(x)) c(c(c(x626))) <-8|0[]- c(c(c(x626))) -1|[]-> b(c(c(x626))) b(c(c(x627))) <-8|0[]- b(c(c(x627))) -2|[]-> c(c(c(x627))) c(c(x)) <-8|[]- c(c(x)) -6|[]-> a(c(x)) c(c(c(x629))) <-8|0[]- c(c(c(x629))) -6|[]-> a(c(c(x629))) c(c(c(x630))) <-8|0[]- c(c(c(x630))) -8|[]-> c(c(c(x630))) b(c(c(x631))) <-8|0[]- b(c(c(x631))) -9|[]-> b(c(c(x631))) b(c(c(x632))) <-8|0[]- b(c(c(x632))) -10|[]-> a(c(c(x632))) b(c(x)) <-9|[]- b(c(x)) -2|[]-> c(c(x)) a(b(c(x634))) <-9|0[]- a(b(c(x634))) -3|[]-> b(a(c(x634))) c(b(c(x635))) <-9|0[]- c(b(c(x635))) -5|[]-> c(c(c(x635))) b(c(x)) <-9|[]- b(c(x)) -10|[]-> a(c(x)) a(b(c(x637))) <-9|0[]- a(b(c(x637))) -11|[]-> c(b(c(x637))) c(b(c(x638))) <-9|0[]- c(b(c(x638))) -13|[]-> b(c(c(x638))) c(b(c(x639))) <-9|0[]- c(b(c(x639))) -14|[]-> a(c(c(x639))) a(c(x)) <-10|[]- b(c(x)) -2|[]-> c(c(x)) a(a(c(x641))) <-10|0[]- a(b(c(x641))) -3|[]-> b(a(c(x641))) c(a(c(x642))) <-10|0[]- c(b(c(x642))) -5|[]-> c(c(c(x642))) a(c(x)) <-10|[]- b(c(x)) -9|[]-> b(c(x)) a(a(c(x644))) <-10|0[]- a(b(c(x644))) -11|[]-> c(b(c(x644))) c(a(c(x645))) <-10|0[]- c(b(c(x645))) -13|[]-> b(c(c(x645))) c(a(c(x646))) <-10|0[]- c(b(c(x646))) -14|[]-> a(c(c(x646))) c(c(b(x647))) <-11|0[]- c(a(b(x647))) -0|[]-> b(c(b(x647))) c(b(x)) <-11|[]- a(b(x)) -3|[]-> b(a(x)) b(c(b(x649))) <-11|0[]- b(a(b(x649))) -4|[]-> c(b(b(x649))) c(c(b(x650))) <-11|0[]- c(a(b(x650))) -7|[]-> c(c(b(x650))) b(c(b(x651))) <-11|0[]- b(a(b(x651))) -12|[]-> c(c(b(x651))) a(c(c(x652))) <-12|0[]- a(b(a(x652))) -3|[]-> b(a(a(x652))) c(c(x)) <-12|[]- b(a(x)) -4|[]-> c(b(x)) c(c(c(x654))) <-12|0[]- c(b(a(x654))) -5|[]-> c(c(a(x654))) a(c(c(x655))) <-12|0[]- a(b(a(x655))) -11|[]-> c(b(a(x655))) c(c(c(x656))) <-12|0[]- c(b(a(x656))) -13|[]-> b(c(a(x656))) c(c(c(x657))) <-12|0[]- c(b(a(x657))) -14|[]-> a(c(a(x657))) c(b(c(x658))) <-13|0[]- c(c(b(x658))) -1|[]-> b(c(b(x658))) b(b(c(x659))) <-13|0[]- b(c(b(x659))) -2|[]-> c(c(b(x659))) b(c(x)) <-13|[]- c(b(x)) -5|[]-> c(c(x)) c(b(c(x661))) <-13|0[]- c(c(b(x661))) -6|[]-> a(c(b(x661))) c(b(c(x662))) <-13|0[]- c(c(b(x662))) -8|[]-> c(c(b(x662))) b(b(c(x663))) <-13|0[]- b(c(b(x663))) -9|[]-> b(c(b(x663))) b(b(c(x664))) <-13|0[]- b(c(b(x664))) -10|[]-> a(c(b(x664))) b(c(x)) <-13|[]- c(b(x)) -14|[]-> a(c(x)) c(a(c(x666))) <-14|0[]- c(c(b(x666))) -1|[]-> b(c(b(x666))) b(a(c(x667))) <-14|0[]- b(c(b(x667))) -2|[]-> c(c(b(x667))) a(c(x)) <-14|[]- c(b(x)) -5|[]-> c(c(x)) c(a(c(x669))) <-14|0[]- c(c(b(x669))) -6|[]-> a(c(b(x669))) c(a(c(x670))) <-14|0[]- c(c(b(x670))) -8|[]-> c(c(b(x670))) b(a(c(x671))) <-14|0[]- b(c(b(x671))) -9|[]-> b(c(b(x671))) b(a(c(x672))) <-14|0[]- b(c(b(x672))) -10|[]-> a(c(b(x672))) a(c(x)) <-14|[]- c(b(x)) -13|[]-> b(c(x)) Shift Processor (no label): strict: weak: Shift Processor lab=left (dd): strict: c(c(a(x569))) -> c(b(c(x569))) c(c(a(x569))) -> b(c(a(x569))) c(b(c(x569))) -> b(c(c(x569))) b(c(a(x569))) -> b(c(c(x569))) b(c(a(x570))) -> b(b(c(x570))) b(c(a(x570))) -> c(c(a(x570))) c(c(a(x570))) -> b(c(a(x570))) b(c(a(x570))) -> b(b(c(x570))) b(b(c(x570))) -> b(c(c(x570))) c(c(a(x570))) -> c(b(c(x570))) c(b(c(x570))) -> b(c(c(x570))) b(b(c(x570))) -> b(c(c(x570))) c(c(a(x570))) -> b(c(a(x570))) b(c(a(x570))) -> b(c(c(x570))) b(b(c(x570))) -> b(c(c(x570))) c(c(a(x570))) -> c(c(c(x570))) c(c(c(x570))) -> b(c(c(x570))) b(b(c(x570))) -> b(c(c(x570))) b(c(c(x570))) -> b(c(c(x570))) c(c(a(x570))) -> c(b(c(x570))) c(b(c(x570))) -> b(c(c(x570))) b(b(c(x570))) -> b(c(c(x570))) b(c(c(x570))) -> b(c(c(x570))) c(c(a(x570))) -> b(c(a(x570))) b(c(a(x570))) -> b(c(c(x570))) b(b(c(x570))) -> b(c(c(x570))) b(c(c(x570))) -> b(c(c(x570))) c(c(a(x570))) -> c(c(c(x570))) c(c(c(x570))) -> b(c(c(x570))) b(b(c(x570))) -> b(c(c(x570))) b(c(c(x570))) -> c(c(c(x570))) c(c(a(x570))) -> c(c(c(x570))) b(b(c(x570))) -> b(c(c(x570))) b(c(c(x570))) -> c(c(c(x570))) c(c(a(x570))) -> c(b(c(x570))) c(b(c(x570))) -> c(c(c(x570))) b(b(c(x570))) -> b(c(c(x570))) b(c(c(x570))) -> c(c(c(x570))) c(c(a(x570))) -> c(c(c(x570))) c(c(c(x570))) -> c(c(c(x570))) b(b(c(x570))) -> b(a(c(x570))) b(a(c(x570))) -> c(c(c(x570))) c(c(a(x570))) -> c(c(c(x570))) b(b(c(x570))) -> b(a(c(x570))) b(a(c(x570))) -> c(c(c(x570))) c(c(a(x570))) -> c(b(c(x570))) c(b(c(x570))) -> c(c(c(x570))) b(b(c(x570))) -> b(a(c(x570))) b(a(c(x570))) -> c(c(c(x570))) c(c(a(x570))) -> c(c(c(x570))) c(c(c(x570))) -> c(c(c(x570))) b(b(c(x570))) -> b(c(c(x570))) b(c(c(x570))) -> a(c(c(x570))) c(c(a(x570))) -> c(b(c(x570))) c(b(c(x570))) -> a(c(c(x570))) b(b(c(x570))) -> b(c(c(x570))) b(c(c(x570))) -> a(c(c(x570))) c(c(a(x570))) -> a(c(a(x570))) a(c(a(x570))) -> a(c(c(x570))) b(b(c(x570))) -> b(c(c(x570))) b(c(c(x570))) -> a(c(c(x570))) c(c(a(x570))) -> c(c(c(x570))) c(c(c(x570))) -> a(c(c(x570))) b(b(c(x570))) -> b(a(c(x570))) b(a(c(x570))) -> c(b(c(x570))) c(c(a(x570))) -> c(b(c(x570))) b(b(c(x570))) -> b(a(c(x570))) b(a(c(x570))) -> c(b(c(x570))) c(c(a(x570))) -> c(b(c(x570))) c(b(c(x570))) -> c(b(c(x570))) b(b(c(x570))) -> b(a(c(x570))) b(a(c(x570))) -> c(b(c(x570))) c(c(a(x570))) -> c(c(c(x570))) c(c(c(x570))) -> c(b(c(x570))) c(c(a(x571))) -> c(b(c(x571))) c(c(a(x571))) -> a(c(a(x571))) c(b(c(x571))) -> a(c(c(x571))) a(c(a(x571))) -> a(c(c(x571))) c(a(x)) -> b(c(x)) c(a(x)) -> c(c(x)) c(c(x)) -> b(c(x)) b(c(x)) -> c(c(x)) b(c(x)) -> a(c(x)) c(c(x)) -> a(c(x)) c(c(a(x573))) -> c(b(c(x573))) c(c(a(x573))) -> c(c(a(x573))) c(c(a(x573))) -> c(b(c(x573))) c(b(c(x573))) -> c(c(c(x573))) c(c(a(x573))) -> c(c(c(x573))) b(c(a(x574))) -> b(b(c(x574))) b(c(a(x574))) -> b(c(a(x574))) b(c(a(x574))) -> b(b(c(x574))) b(b(c(x574))) -> b(c(c(x574))) b(c(a(x574))) -> b(c(c(x574))) b(c(a(x575))) -> b(b(c(x575))) b(c(a(x575))) -> a(c(a(x575))) b(b(c(x575))) -> b(a(c(x575))) a(c(a(x575))) -> a(b(c(x575))) a(b(c(x575))) -> b(a(c(x575))) b(b(c(x575))) -> b(c(c(x575))) b(c(c(x575))) -> b(a(c(x575))) a(c(a(x575))) -> a(b(c(x575))) a(b(c(x575))) -> b(a(c(x575))) b(b(c(x575))) -> b(c(c(x575))) b(c(c(x575))) -> a(c(c(x575))) a(c(a(x575))) -> a(c(c(x575))) b(b(c(x575))) -> b(c(c(x575))) b(c(c(x575))) -> a(c(c(x575))) a(c(a(x575))) -> a(b(c(x575))) a(b(c(x575))) -> a(c(c(x575))) b(b(c(x575))) -> b(c(c(x575))) b(c(c(x575))) -> a(c(c(x575))) a(c(a(x575))) -> a(c(c(x575))) a(c(c(x575))) -> a(c(c(x575))) b(b(c(x575))) -> b(a(c(x575))) b(a(c(x575))) -> c(b(c(x575))) a(c(a(x575))) -> a(b(c(x575))) a(b(c(x575))) -> c(b(c(x575))) c(c(c(x576))) -> c(b(c(x576))) c(c(c(x576))) -> b(c(c(x576))) c(b(c(x576))) -> c(c(c(x576))) b(c(c(x576))) -> c(c(c(x576))) c(b(c(x576))) -> b(c(c(x576))) c(b(c(x576))) -> a(c(c(x576))) b(c(c(x576))) -> a(c(c(x576))) b(c(c(x577))) -> b(b(c(x577))) b(c(c(x577))) -> c(c(c(x577))) b(b(c(x577))) -> b(c(c(x577))) c(c(c(x577))) -> b(c(c(x577))) c(c(x)) -> b(c(x)) c(c(x)) -> a(c(x)) b(c(x)) -> a(c(x)) c(c(c(x579))) -> c(b(c(x579))) c(c(c(x579))) -> a(c(c(x579))) c(b(c(x579))) -> a(c(c(x579))) c(c(x)) -> b(c(x)) c(c(x)) -> c(c(x)) c(c(x)) -> b(c(x)) b(c(x)) -> c(c(x)) b(c(x)) -> a(c(x)) c(c(x)) -> a(c(x)) c(c(c(x581))) -> c(b(c(x581))) c(c(c(x581))) -> c(c(c(x581))) c(c(c(x581))) -> c(b(c(x581))) c(b(c(x581))) -> c(c(c(x581))) c(b(c(x581))) -> c(a(c(x581))) c(c(c(x581))) -> c(a(c(x581))) c(b(c(x581))) -> b(c(c(x581))) c(c(c(x581))) -> b(c(c(x581))) c(b(c(x581))) -> a(c(c(x581))) c(c(c(x581))) -> a(c(c(x581))) b(c(c(x582))) -> b(b(c(x582))) b(c(c(x582))) -> b(c(c(x582))) b(c(c(x582))) -> b(b(c(x582))) b(b(c(x582))) -> b(c(c(x582))) b(b(c(x582))) -> b(a(c(x582))) b(c(c(x582))) -> b(a(c(x582))) b(c(c(x583))) -> b(b(c(x583))) b(c(c(x583))) -> a(c(c(x583))) b(b(c(x583))) -> b(a(c(x583))) a(c(c(x583))) -> a(b(c(x583))) a(b(c(x583))) -> b(a(c(x583))) b(b(c(x583))) -> b(c(c(x583))) b(c(c(x583))) -> b(a(c(x583))) a(c(c(x583))) -> a(b(c(x583))) a(b(c(x583))) -> b(a(c(x583))) b(b(c(x583))) -> b(c(c(x583))) b(c(c(x583))) -> a(c(c(x583))) b(b(c(x583))) -> b(a(c(x583))) b(a(c(x583))) -> c(b(c(x583))) a(c(c(x583))) -> a(b(c(x583))) a(b(c(x583))) -> c(b(c(x583))) a(b(c(x584))) -> a(c(c(x584))) a(b(c(x584))) -> b(a(c(x584))) b(a(c(x584))) -> c(b(c(x584))) c(b(c(x584))) -> a(c(c(x584))) b(a(c(x584))) -> c(c(c(x584))) c(c(c(x584))) -> a(c(c(x584))) a(c(c(x584))) -> a(b(c(x584))) a(b(c(x584))) -> b(a(c(x584))) a(c(c(x584))) -> a(b(c(x584))) a(b(c(x584))) -> c(b(c(x584))) b(a(c(x584))) -> c(b(c(x584))) a(c(c(x584))) -> a(b(c(x584))) a(b(c(x584))) -> c(b(c(x584))) b(a(c(x584))) -> c(b(c(x584))) c(b(c(x584))) -> c(b(c(x584))) a(c(c(x584))) -> a(b(c(x584))) a(b(c(x584))) -> c(b(c(x584))) b(a(c(x584))) -> c(c(c(x584))) c(c(c(x584))) -> c(b(c(x584))) c(b(c(x585))) -> c(c(c(x585))) c(b(c(x585))) -> c(c(c(x585))) b(c(x)) -> c(c(x)) b(c(x)) -> b(c(x)) b(c(x)) -> c(c(x)) c(c(x)) -> b(c(x)) c(c(x)) -> a(c(x)) b(c(x)) -> a(c(x)) b(c(x)) -> c(c(x)) b(c(x)) -> a(c(x)) c(c(x)) -> a(c(x)) a(b(c(x588))) -> a(c(c(x588))) a(b(c(x588))) -> c(b(c(x588))) c(b(c(x588))) -> a(c(c(x588))) c(b(c(x589))) -> c(c(c(x589))) c(b(c(x589))) -> b(c(c(x589))) b(c(c(x589))) -> c(c(c(x589))) c(c(c(x589))) -> b(c(c(x589))) c(c(c(x589))) -> a(c(c(x589))) b(c(c(x589))) -> a(c(c(x589))) c(b(c(x590))) -> c(c(c(x590))) c(b(c(x590))) -> a(c(c(x590))) c(c(c(x590))) -> a(c(c(x590))) c(a(b(x591))) -> c(b(a(x591))) c(a(b(x591))) -> b(c(b(x591))) c(b(a(x591))) -> c(c(b(x591))) b(c(b(x591))) -> c(c(b(x591))) b(a(b(x592))) -> b(b(a(x592))) b(a(b(x592))) -> c(b(b(x592))) b(b(a(x592))) -> b(c(b(x592))) c(b(b(x592))) -> b(c(b(x592))) c(a(b(x593))) -> c(b(a(x593))) c(a(b(x593))) -> c(c(b(x593))) c(b(a(x593))) -> c(c(b(x593))) c(b(a(x593))) -> c(c(c(x593))) c(c(b(x593))) -> c(c(c(x593))) a(b(x)) -> b(a(x)) a(b(x)) -> c(b(x)) b(a(x)) -> c(b(x)) b(a(x)) -> c(c(x)) c(b(x)) -> c(c(x)) b(a(b(x595))) -> b(b(a(x595))) b(a(b(x595))) -> c(c(b(x595))) b(b(a(x595))) -> b(c(b(x595))) c(c(b(x595))) -> b(c(b(x595))) a(b(a(x596))) -> a(c(b(x596))) a(b(a(x596))) -> b(a(a(x596))) a(c(b(x596))) -> a(b(c(x596))) a(b(c(x596))) -> c(b(c(x596))) b(a(a(x596))) -> c(c(a(x596))) c(c(a(x596))) -> c(b(c(x596))) c(b(a(x597))) -> c(c(b(x597))) c(b(a(x597))) -> c(c(a(x597))) c(c(b(x597))) -> c(c(c(x597))) c(c(a(x597))) -> c(c(c(x597))) c(c(b(x597))) -> c(b(c(x597))) c(c(a(x597))) -> c(b(c(x597))) a(b(a(x598))) -> a(c(b(x598))) a(b(a(x598))) -> c(b(a(x598))) c(b(a(x598))) -> c(c(b(x598))) c(c(b(x598))) -> a(c(b(x598))) a(c(b(x598))) -> a(c(c(x598))) c(b(a(x598))) -> c(c(c(x598))) c(c(c(x598))) -> a(c(c(x598))) a(c(b(x598))) -> a(c(c(x598))) c(b(a(x598))) -> a(c(a(x598))) a(c(a(x598))) -> a(c(c(x598))) a(c(b(x598))) -> a(c(c(x598))) a(c(c(x598))) -> a(c(c(x598))) c(b(a(x598))) -> c(c(c(x598))) c(c(c(x598))) -> a(c(c(x598))) a(c(b(x598))) -> a(c(c(x598))) a(c(c(x598))) -> a(c(c(x598))) c(b(a(x598))) -> a(c(a(x598))) a(c(a(x598))) -> a(c(c(x598))) a(c(b(x598))) -> a(b(c(x598))) a(b(c(x598))) -> a(c(c(x598))) c(b(a(x598))) -> c(c(c(x598))) c(c(c(x598))) -> a(c(c(x598))) a(c(b(x598))) -> a(b(c(x598))) a(b(c(x598))) -> a(c(c(x598))) c(b(a(x598))) -> a(c(a(x598))) a(c(a(x598))) -> a(c(c(x598))) a(c(b(x598))) -> a(b(c(x598))) c(b(a(x598))) -> a(c(a(x598))) a(c(a(x598))) -> a(b(c(x598))) a(c(b(x598))) -> a(c(c(x598))) a(c(c(x598))) -> a(b(c(x598))) c(b(a(x598))) -> a(c(a(x598))) a(c(a(x598))) -> a(b(c(x598))) a(c(b(x598))) -> a(b(c(x598))) a(b(c(x598))) -> a(b(c(x598))) c(b(a(x598))) -> a(c(a(x598))) a(c(a(x598))) -> a(b(c(x598))) a(c(b(x598))) -> a(b(c(x598))) a(b(c(x598))) -> c(b(c(x598))) c(b(a(x598))) -> c(c(b(x598))) c(c(b(x598))) -> c(b(c(x598))) a(c(b(x598))) -> a(b(c(x598))) a(b(c(x598))) -> c(b(c(x598))) c(b(a(x598))) -> c(c(a(x598))) c(c(a(x598))) -> c(b(c(x598))) a(c(b(x598))) -> a(b(c(x598))) a(b(c(x598))) -> c(b(c(x598))) c(b(a(x598))) -> c(c(c(x598))) c(c(c(x598))) -> c(b(c(x598))) b(a(x)) -> c(b(x)) b(a(x)) -> c(c(x)) c(b(x)) -> c(c(x)) c(b(x)) -> b(c(x)) c(c(x)) -> b(c(x)) c(b(x)) -> a(c(x)) c(c(x)) -> a(c(x)) c(b(a(x600))) -> c(c(b(x600))) c(b(a(x600))) -> b(c(a(x600))) c(c(b(x600))) -> c(c(c(x600))) b(c(a(x600))) -> c(c(a(x600))) c(c(a(x600))) -> c(c(c(x600))) c(c(b(x600))) -> c(c(c(x600))) b(c(a(x600))) -> b(c(c(x600))) b(c(c(x600))) -> c(c(c(x600))) c(c(b(x600))) -> c(c(c(x600))) c(c(c(x600))) -> c(c(c(x600))) b(c(a(x600))) -> c(c(a(x600))) c(c(a(x600))) -> c(c(c(x600))) c(c(b(x600))) -> c(c(c(x600))) c(c(c(x600))) -> c(c(c(x600))) b(c(a(x600))) -> b(c(c(x600))) b(c(c(x600))) -> c(c(c(x600))) c(c(b(x600))) -> c(b(c(x600))) c(b(c(x600))) -> c(c(c(x600))) b(c(a(x600))) -> c(c(a(x600))) c(c(a(x600))) -> c(c(c(x600))) c(c(b(x600))) -> c(b(c(x600))) c(b(c(x600))) -> c(c(c(x600))) b(c(a(x600))) -> b(c(c(x600))) b(c(c(x600))) -> c(c(c(x600))) c(c(b(x600))) -> c(a(c(x600))) c(a(c(x600))) -> c(c(c(x600))) b(c(a(x600))) -> c(c(a(x600))) c(c(a(x600))) -> c(c(c(x600))) c(c(b(x600))) -> c(a(c(x600))) c(a(c(x600))) -> c(c(c(x600))) b(c(a(x600))) -> b(c(c(x600))) b(c(c(x600))) -> c(c(c(x600))) c(c(b(x600))) -> c(b(c(x600))) b(c(a(x600))) -> c(c(a(x600))) c(c(a(x600))) -> c(b(c(x600))) c(c(b(x600))) -> c(c(c(x600))) c(c(c(x600))) -> c(b(c(x600))) b(c(a(x600))) -> c(c(a(x600))) c(c(a(x600))) -> c(b(c(x600))) c(c(b(x600))) -> c(b(c(x600))) c(b(c(x600))) -> c(b(c(x600))) b(c(a(x600))) -> c(c(a(x600))) c(c(a(x600))) -> c(b(c(x600))) c(c(b(x600))) -> b(c(b(x600))) b(c(b(x600))) -> b(c(c(x600))) b(c(a(x600))) -> b(c(c(x600))) c(c(b(x600))) -> b(c(b(x600))) b(c(b(x600))) -> b(c(c(x600))) b(c(a(x600))) -> b(b(c(x600))) b(b(c(x600))) -> b(c(c(x600))) c(c(b(x600))) -> b(c(b(x600))) b(c(b(x600))) -> b(c(c(x600))) b(c(a(x600))) -> b(c(c(x600))) b(c(c(x600))) -> b(c(c(x600))) c(c(b(x600))) -> c(c(c(x600))) c(c(c(x600))) -> b(c(c(x600))) b(c(a(x600))) -> b(c(c(x600))) c(c(b(x600))) -> c(c(c(x600))) c(c(c(x600))) -> b(c(c(x600))) b(c(a(x600))) -> b(b(c(x600))) b(b(c(x600))) -> b(c(c(x600))) c(c(b(x600))) -> c(c(c(x600))) c(c(c(x600))) -> b(c(c(x600))) b(c(a(x600))) -> b(c(c(x600))) b(c(c(x600))) -> b(c(c(x600))) c(c(b(x600))) -> c(b(c(x600))) c(b(c(x600))) -> b(c(c(x600))) b(c(a(x600))) -> b(c(c(x600))) c(c(b(x600))) -> c(b(c(x600))) c(b(c(x600))) -> b(c(c(x600))) b(c(a(x600))) -> b(b(c(x600))) b(b(c(x600))) -> b(c(c(x600))) c(c(b(x600))) -> c(b(c(x600))) c(b(c(x600))) -> b(c(c(x600))) b(c(a(x600))) -> b(c(c(x600))) b(c(c(x600))) -> b(c(c(x600))) c(c(b(x600))) -> c(a(c(x600))) c(a(c(x600))) -> b(c(c(x600))) b(c(a(x600))) -> b(c(c(x600))) c(c(b(x600))) -> c(a(c(x600))) c(a(c(x600))) -> b(c(c(x600))) b(c(a(x600))) -> b(b(c(x600))) b(b(c(x600))) -> b(c(c(x600))) c(c(b(x600))) -> c(a(c(x600))) c(a(c(x600))) -> b(c(c(x600))) b(c(a(x600))) -> b(c(c(x600))) b(c(c(x600))) -> b(c(c(x600))) c(c(b(x600))) -> b(c(b(x600))) b(c(b(x600))) -> b(b(c(x600))) b(c(a(x600))) -> b(b(c(x600))) c(c(b(x600))) -> b(c(b(x600))) b(c(b(x600))) -> b(b(c(x600))) b(c(a(x600))) -> b(b(c(x600))) b(b(c(x600))) -> b(b(c(x600))) c(c(b(x600))) -> b(c(b(x600))) b(c(b(x600))) -> b(b(c(x600))) b(c(a(x600))) -> b(c(c(x600))) b(c(c(x600))) -> b(b(c(x600))) c(c(b(x600))) -> b(c(b(x600))) b(c(b(x600))) -> b(a(c(x600))) b(c(a(x600))) -> b(b(c(x600))) b(b(c(x600))) -> b(a(c(x600))) c(c(b(x600))) -> b(c(b(x600))) b(c(b(x600))) -> b(a(c(x600))) b(c(a(x600))) -> b(c(c(x600))) b(c(c(x600))) -> b(a(c(x600))) c(c(b(x600))) -> c(c(c(x600))) c(c(c(x600))) -> a(c(c(x600))) b(c(a(x600))) -> b(c(c(x600))) b(c(c(x600))) -> a(c(c(x600))) c(c(b(x600))) -> c(c(c(x600))) c(c(c(x600))) -> a(c(c(x600))) b(c(a(x600))) -> a(c(a(x600))) a(c(a(x600))) -> a(c(c(x600))) c(c(b(x600))) -> a(c(b(x600))) a(c(b(x600))) -> a(c(c(x600))) b(c(a(x600))) -> b(c(c(x600))) b(c(c(x600))) -> a(c(c(x600))) c(c(b(x600))) -> a(c(b(x600))) a(c(b(x600))) -> a(c(c(x600))) b(c(a(x600))) -> a(c(a(x600))) a(c(a(x600))) -> a(c(c(x600))) c(c(b(x600))) -> c(b(c(x600))) c(b(c(x600))) -> a(c(c(x600))) b(c(a(x600))) -> b(c(c(x600))) b(c(c(x600))) -> a(c(c(x600))) c(c(b(x600))) -> c(b(c(x600))) c(b(c(x600))) -> a(c(c(x600))) b(c(a(x600))) -> a(c(a(x600))) a(c(a(x600))) -> a(c(c(x600))) c(c(b(x600))) -> a(c(b(x600))) a(c(b(x600))) -> a(b(c(x600))) b(c(a(x600))) -> a(c(a(x600))) a(c(a(x600))) -> a(b(c(x600))) c(b(a(x601))) -> c(c(b(x601))) c(b(a(x601))) -> a(c(a(x601))) c(c(b(x601))) -> c(b(c(x601))) a(c(a(x601))) -> a(b(c(x601))) a(b(c(x601))) -> c(b(c(x601))) c(c(b(x601))) -> c(c(c(x601))) c(c(c(x601))) -> c(b(c(x601))) a(c(a(x601))) -> a(b(c(x601))) a(b(c(x601))) -> c(b(c(x601))) c(c(b(x601))) -> c(b(c(x601))) c(b(c(x601))) -> c(b(c(x601))) a(c(a(x601))) -> a(b(c(x601))) a(b(c(x601))) -> c(b(c(x601))) c(c(b(x601))) -> b(c(b(x601))) b(c(b(x601))) -> b(a(c(x601))) a(c(a(x601))) -> a(b(c(x601))) a(b(c(x601))) -> b(a(c(x601))) c(c(b(x601))) -> c(c(c(x601))) c(c(c(x601))) -> a(c(c(x601))) a(c(a(x601))) -> a(c(c(x601))) c(c(b(x601))) -> c(c(c(x601))) c(c(c(x601))) -> a(c(c(x601))) a(c(a(x601))) -> a(b(c(x601))) a(b(c(x601))) -> a(c(c(x601))) c(c(b(x601))) -> c(c(c(x601))) c(c(c(x601))) -> a(c(c(x601))) a(c(a(x601))) -> a(c(c(x601))) a(c(c(x601))) -> a(c(c(x601))) c(c(b(x601))) -> a(c(b(x601))) a(c(b(x601))) -> a(c(c(x601))) a(c(a(x601))) -> a(c(c(x601))) c(c(b(x601))) -> a(c(b(x601))) a(c(b(x601))) -> a(c(c(x601))) a(c(a(x601))) -> a(b(c(x601))) a(b(c(x601))) -> a(c(c(x601))) c(c(b(x601))) -> a(c(b(x601))) a(c(b(x601))) -> a(c(c(x601))) a(c(a(x601))) -> a(c(c(x601))) a(c(c(x601))) -> a(c(c(x601))) c(c(b(x601))) -> c(b(c(x601))) c(b(c(x601))) -> a(c(c(x601))) a(c(a(x601))) -> a(c(c(x601))) c(c(b(x601))) -> c(b(c(x601))) c(b(c(x601))) -> a(c(c(x601))) a(c(a(x601))) -> a(b(c(x601))) a(b(c(x601))) -> a(c(c(x601))) c(c(b(x601))) -> c(b(c(x601))) c(b(c(x601))) -> a(c(c(x601))) a(c(a(x601))) -> a(c(c(x601))) a(c(c(x601))) -> a(c(c(x601))) c(c(b(x601))) -> a(c(b(x601))) a(c(b(x601))) -> a(b(c(x601))) a(c(a(x601))) -> a(b(c(x601))) c(c(b(x601))) -> a(c(b(x601))) a(c(b(x601))) -> a(b(c(x601))) a(c(a(x601))) -> a(b(c(x601))) a(b(c(x601))) -> a(b(c(x601))) c(c(b(x601))) -> a(c(b(x601))) a(c(b(x601))) -> a(b(c(x601))) a(c(a(x601))) -> a(c(c(x601))) a(c(c(x601))) -> a(b(c(x601))) c(c(b(x601))) -> a(c(b(x601))) a(c(b(x601))) -> a(a(c(x601))) a(c(a(x601))) -> a(b(c(x601))) a(b(c(x601))) -> a(a(c(x601))) c(c(b(x601))) -> a(c(b(x601))) a(c(b(x601))) -> a(a(c(x601))) a(c(a(x601))) -> a(c(c(x601))) a(c(c(x601))) -> a(a(c(x601))) c(c(b(x602))) -> c(c(c(x602))) c(c(b(x602))) -> b(c(b(x602))) c(c(c(x602))) -> b(c(c(x602))) b(c(b(x602))) -> b(c(c(x602))) b(c(b(x603))) -> b(c(c(x603))) b(c(b(x603))) -> c(c(b(x603))) b(c(c(x603))) -> c(c(c(x603))) c(c(b(x603))) -> c(c(c(x603))) c(c(b(x604))) -> c(c(c(x604))) c(c(b(x604))) -> a(c(b(x604))) c(c(c(x604))) -> a(c(c(x604))) a(c(b(x604))) -> a(c(c(x604))) c(c(b(x605))) -> c(c(c(x605))) c(c(b(x605))) -> c(c(b(x605))) c(c(b(x605))) -> c(c(c(x605))) c(c(c(x605))) -> c(b(c(x605))) c(c(b(x605))) -> c(b(c(x605))) c(c(c(x605))) -> c(a(c(x605))) c(c(b(x605))) -> c(a(c(x605))) b(c(b(x606))) -> b(c(c(x606))) b(c(b(x606))) -> b(c(b(x606))) b(c(b(x606))) -> b(c(c(x606))) b(c(c(x606))) -> b(b(c(x606))) b(c(b(x606))) -> b(b(c(x606))) b(c(c(x606))) -> b(a(c(x606))) b(c(b(x606))) -> b(a(c(x606))) b(c(b(x607))) -> b(c(c(x607))) b(c(b(x607))) -> a(c(b(x607))) b(c(c(x607))) -> a(c(c(x607))) a(c(b(x607))) -> a(c(c(x607))) c(b(x)) -> c(c(x)) c(b(x)) -> b(c(x)) b(c(x)) -> c(c(x)) c(c(x)) -> b(c(x)) c(c(x)) -> a(c(x)) b(c(x)) -> a(c(x)) c(b(x)) -> c(c(x)) c(b(x)) -> a(c(x)) c(c(x)) -> a(c(x)) c(c(x)) -> a(c(x)) c(c(x)) -> b(c(x)) b(c(x)) -> a(c(x)) c(c(c(x611))) -> c(a(c(x611))) c(c(c(x611))) -> b(c(c(x611))) c(a(c(x611))) -> b(c(c(x611))) c(a(c(x611))) -> c(c(c(x611))) b(c(c(x611))) -> c(c(c(x611))) b(c(c(x612))) -> b(a(c(x612))) b(c(c(x612))) -> c(c(c(x612))) b(a(c(x612))) -> c(b(c(x612))) c(c(c(x612))) -> c(b(c(x612))) b(a(c(x612))) -> c(c(c(x612))) c(c(c(x613))) -> c(a(c(x613))) c(c(c(x613))) -> a(c(c(x613))) c(a(c(x613))) -> b(c(c(x613))) b(c(c(x613))) -> b(a(c(x613))) a(c(c(x613))) -> a(b(c(x613))) a(b(c(x613))) -> b(a(c(x613))) c(a(c(x613))) -> b(c(c(x613))) b(c(c(x613))) -> a(c(c(x613))) c(a(c(x613))) -> c(c(c(x613))) c(c(c(x613))) -> a(c(c(x613))) c(a(c(x613))) -> c(c(c(x613))) c(c(c(x613))) -> c(b(c(x613))) a(c(c(x613))) -> a(b(c(x613))) a(b(c(x613))) -> c(b(c(x613))) c(c(x)) -> a(c(x)) c(c(x)) -> c(c(x)) c(c(x)) -> a(c(x)) c(c(c(x615))) -> c(a(c(x615))) c(c(c(x615))) -> c(c(c(x615))) c(c(c(x615))) -> c(a(c(x615))) c(a(c(x615))) -> b(c(c(x615))) c(c(c(x615))) -> b(c(c(x615))) c(a(c(x615))) -> c(c(c(x615))) b(c(c(x616))) -> b(a(c(x616))) b(c(c(x616))) -> b(c(c(x616))) b(c(c(x616))) -> b(a(c(x616))) b(a(c(x616))) -> c(c(c(x616))) b(c(c(x616))) -> c(c(c(x616))) b(c(c(x617))) -> b(a(c(x617))) b(c(c(x617))) -> a(c(c(x617))) a(c(c(x617))) -> a(b(c(x617))) a(b(c(x617))) -> b(a(c(x617))) b(a(c(x617))) -> c(b(c(x617))) a(c(c(x617))) -> a(b(c(x617))) a(b(c(x617))) -> c(b(c(x617))) b(a(c(x617))) -> c(b(c(x617))) c(b(c(x617))) -> c(b(c(x617))) a(c(c(x617))) -> a(b(c(x617))) a(b(c(x617))) -> c(b(c(x617))) b(a(c(x617))) -> c(c(c(x617))) c(c(c(x617))) -> c(b(c(x617))) a(c(c(x617))) -> a(b(c(x617))) a(b(c(x617))) -> c(b(c(x617))) b(a(c(x617))) -> c(b(c(x617))) c(b(c(x617))) -> a(c(c(x617))) b(a(c(x617))) -> c(c(c(x617))) c(c(c(x617))) -> a(c(c(x617))) c(a(x)) -> c(c(x)) c(a(x)) -> b(c(x)) b(c(x)) -> c(c(x)) c(c(x)) -> b(c(x)) c(c(x)) -> a(c(x)) b(c(x)) -> a(c(x)) c(c(a(x619))) -> c(c(c(x619))) c(c(a(x619))) -> b(c(a(x619))) c(c(c(x619))) -> b(c(c(x619))) b(c(a(x619))) -> b(c(c(x619))) b(c(a(x620))) -> b(c(c(x620))) b(c(a(x620))) -> c(c(a(x620))) b(c(c(x620))) -> c(c(c(x620))) c(c(a(x620))) -> c(c(c(x620))) c(c(a(x621))) -> c(c(c(x621))) c(c(a(x621))) -> a(c(a(x621))) c(c(c(x621))) -> a(c(c(x621))) a(c(a(x621))) -> a(c(c(x621))) c(c(a(x622))) -> c(c(c(x622))) c(c(a(x622))) -> c(c(a(x622))) c(c(a(x622))) -> c(c(c(x622))) c(c(c(x622))) -> c(b(c(x622))) c(c(a(x622))) -> c(b(c(x622))) b(c(a(x623))) -> b(c(c(x623))) b(c(a(x623))) -> b(c(a(x623))) b(c(a(x623))) -> b(c(c(x623))) b(c(c(x623))) -> b(b(c(x623))) b(c(a(x623))) -> b(b(c(x623))) b(c(a(x624))) -> b(c(c(x624))) b(c(a(x624))) -> a(c(a(x624))) b(c(c(x624))) -> a(c(c(x624))) a(c(a(x624))) -> a(c(c(x624))) c(c(x)) -> c(c(x)) c(c(x)) -> b(c(x)) b(c(x)) -> c(c(x)) c(c(x)) -> b(c(x)) c(c(x)) -> a(c(x)) b(c(x)) -> a(c(x)) c(c(c(x626))) -> c(c(c(x626))) c(c(c(x626))) -> b(c(c(x626))) b(c(c(x626))) -> c(c(c(x626))) c(c(c(x626))) -> b(c(c(x626))) c(c(c(x626))) -> a(c(c(x626))) b(c(c(x626))) -> a(c(c(x626))) b(c(c(x627))) -> b(c(c(x627))) b(c(c(x627))) -> c(c(c(x627))) c(c(c(x627))) -> b(c(c(x627))) b(c(c(x627))) -> c(c(c(x627))) b(c(c(x627))) -> a(c(c(x627))) c(c(c(x627))) -> a(c(c(x627))) c(c(x)) -> c(c(x)) c(c(x)) -> a(c(x)) c(c(x)) -> a(c(x)) c(c(c(x629))) -> c(c(c(x629))) c(c(c(x629))) -> a(c(c(x629))) c(c(c(x629))) -> a(c(c(x629))) c(c(c(x630))) -> c(c(c(x630))) c(c(c(x630))) -> c(c(c(x630))) b(c(c(x631))) -> b(c(c(x631))) b(c(c(x631))) -> b(c(c(x631))) b(c(c(x632))) -> b(c(c(x632))) b(c(c(x632))) -> a(c(c(x632))) b(c(c(x632))) -> a(c(c(x632))) b(c(x)) -> b(c(x)) b(c(x)) -> c(c(x)) c(c(x)) -> b(c(x)) b(c(x)) -> c(c(x)) b(c(x)) -> a(c(x)) c(c(x)) -> a(c(x)) a(b(c(x634))) -> a(b(c(x634))) a(b(c(x634))) -> b(a(c(x634))) a(b(c(x634))) -> b(a(c(x634))) a(b(c(x634))) -> c(b(c(x634))) b(a(c(x634))) -> c(b(c(x634))) c(b(c(x635))) -> c(b(c(x635))) c(b(c(x635))) -> c(c(c(x635))) c(c(c(x635))) -> c(b(c(x635))) c(b(c(x635))) -> c(c(c(x635))) c(b(c(x635))) -> c(a(c(x635))) c(c(c(x635))) -> c(a(c(x635))) c(b(c(x635))) -> b(c(c(x635))) c(c(c(x635))) -> b(c(c(x635))) c(b(c(x635))) -> a(c(c(x635))) c(c(c(x635))) -> a(c(c(x635))) b(c(x)) -> b(c(x)) b(c(x)) -> a(c(x)) b(c(x)) -> a(c(x)) a(b(c(x637))) -> a(b(c(x637))) a(b(c(x637))) -> c(b(c(x637))) a(b(c(x637))) -> a(c(c(x637))) c(b(c(x637))) -> a(c(c(x637))) a(b(c(x637))) -> c(b(c(x637))) c(b(c(x638))) -> c(b(c(x638))) c(b(c(x638))) -> b(c(c(x638))) c(b(c(x638))) -> c(c(c(x638))) b(c(c(x638))) -> c(c(c(x638))) c(b(c(x638))) -> b(c(c(x638))) c(b(c(x638))) -> a(c(c(x638))) b(c(c(x638))) -> a(c(c(x638))) c(b(c(x639))) -> c(b(c(x639))) c(b(c(x639))) -> a(c(c(x639))) c(b(c(x639))) -> a(c(c(x639))) b(c(x)) -> a(c(x)) b(c(x)) -> c(c(x)) c(c(x)) -> a(c(x)) a(b(c(x641))) -> a(a(c(x641))) a(b(c(x641))) -> b(a(c(x641))) b(a(c(x641))) -> c(b(c(x641))) c(b(c(x641))) -> a(c(c(x641))) a(c(c(x641))) -> a(a(c(x641))) b(a(c(x641))) -> c(c(c(x641))) c(c(c(x641))) -> a(c(c(x641))) a(c(c(x641))) -> a(a(c(x641))) c(b(c(x642))) -> c(a(c(x642))) c(b(c(x642))) -> c(c(c(x642))) c(c(c(x642))) -> c(a(c(x642))) c(a(c(x642))) -> b(c(c(x642))) c(c(c(x642))) -> b(c(c(x642))) c(a(c(x642))) -> c(c(c(x642))) b(c(x)) -> a(c(x)) b(c(x)) -> b(c(x)) b(c(x)) -> a(c(x)) a(b(c(x644))) -> a(a(c(x644))) a(b(c(x644))) -> c(b(c(x644))) c(b(c(x644))) -> a(c(c(x644))) a(c(c(x644))) -> a(a(c(x644))) c(b(c(x645))) -> c(a(c(x645))) c(b(c(x645))) -> b(c(c(x645))) c(a(c(x645))) -> b(c(c(x645))) c(a(c(x645))) -> c(c(c(x645))) b(c(c(x645))) -> c(c(c(x645))) c(b(c(x646))) -> c(a(c(x646))) c(b(c(x646))) -> a(c(c(x646))) c(a(c(x646))) -> b(c(c(x646))) b(c(c(x646))) -> b(a(c(x646))) a(c(c(x646))) -> a(b(c(x646))) a(b(c(x646))) -> b(a(c(x646))) c(a(c(x646))) -> b(c(c(x646))) b(c(c(x646))) -> a(c(c(x646))) c(a(c(x646))) -> c(c(c(x646))) c(c(c(x646))) -> a(c(c(x646))) c(a(c(x646))) -> c(c(c(x646))) c(c(c(x646))) -> c(b(c(x646))) a(c(c(x646))) -> a(b(c(x646))) a(b(c(x646))) -> c(b(c(x646))) c(a(b(x647))) -> c(c(b(x647))) c(a(b(x647))) -> b(c(b(x647))) b(c(b(x647))) -> c(c(b(x647))) c(c(b(x647))) -> b(c(b(x647))) c(c(b(x647))) -> a(c(b(x647))) b(c(b(x647))) -> a(c(b(x647))) a(b(x)) -> c(b(x)) a(b(x)) -> b(a(x)) b(a(x)) -> c(b(x)) c(b(x)) -> c(c(x)) b(a(x)) -> c(c(x)) b(a(b(x649))) -> b(c(b(x649))) b(a(b(x649))) -> c(b(b(x649))) c(b(b(x649))) -> b(c(b(x649))) b(c(b(x649))) -> c(c(b(x649))) c(b(b(x649))) -> c(c(b(x649))) b(c(b(x649))) -> a(c(b(x649))) c(b(b(x649))) -> a(c(b(x649))) c(a(b(x650))) -> c(c(b(x650))) c(a(b(x650))) -> c(c(b(x650))) b(a(b(x651))) -> b(c(b(x651))) b(a(b(x651))) -> c(c(b(x651))) c(c(b(x651))) -> b(c(b(x651))) b(c(b(x651))) -> c(c(b(x651))) b(c(b(x651))) -> a(c(b(x651))) c(c(b(x651))) -> a(c(b(x651))) a(b(a(x652))) -> a(c(c(x652))) a(b(a(x652))) -> b(a(a(x652))) a(c(c(x652))) -> a(b(c(x652))) a(b(c(x652))) -> c(b(c(x652))) b(a(a(x652))) -> c(c(a(x652))) c(c(a(x652))) -> c(b(c(x652))) b(a(x)) -> c(c(x)) b(a(x)) -> c(b(x)) c(b(x)) -> c(c(x)) c(c(x)) -> b(c(x)) c(b(x)) -> b(c(x)) c(c(x)) -> a(c(x)) c(b(x)) -> a(c(x)) c(b(a(x654))) -> c(c(c(x654))) c(b(a(x654))) -> c(c(a(x654))) c(c(a(x654))) -> c(c(c(x654))) c(c(c(x654))) -> c(b(c(x654))) c(c(a(x654))) -> c(b(c(x654))) a(b(a(x655))) -> a(c(c(x655))) a(b(a(x655))) -> c(b(a(x655))) c(b(a(x655))) -> c(c(c(x655))) c(c(c(x655))) -> a(c(c(x655))) c(b(a(x655))) -> a(c(a(x655))) a(c(a(x655))) -> a(c(c(x655))) a(c(c(x655))) -> a(b(c(x655))) c(b(a(x655))) -> a(c(a(x655))) a(c(a(x655))) -> a(b(c(x655))) a(c(c(x655))) -> a(b(c(x655))) a(b(c(x655))) -> a(b(c(x655))) c(b(a(x655))) -> a(c(a(x655))) a(c(a(x655))) -> a(b(c(x655))) a(c(c(x655))) -> a(b(c(x655))) a(b(c(x655))) -> c(b(c(x655))) c(b(a(x655))) -> c(c(b(x655))) c(c(b(x655))) -> c(b(c(x655))) a(c(c(x655))) -> a(b(c(x655))) a(b(c(x655))) -> c(b(c(x655))) c(b(a(x655))) -> c(c(a(x655))) c(c(a(x655))) -> c(b(c(x655))) a(c(c(x655))) -> a(b(c(x655))) a(b(c(x655))) -> c(b(c(x655))) c(b(a(x655))) -> c(c(c(x655))) c(c(c(x655))) -> c(b(c(x655))) c(b(a(x656))) -> c(c(c(x656))) c(b(a(x656))) -> b(c(a(x656))) c(c(c(x656))) -> b(c(c(x656))) b(c(a(x656))) -> b(c(c(x656))) c(b(a(x657))) -> c(c(c(x657))) c(b(a(x657))) -> a(c(a(x657))) c(c(c(x657))) -> a(c(c(x657))) a(c(a(x657))) -> a(c(c(x657))) c(c(b(x658))) -> c(b(c(x658))) c(c(b(x658))) -> b(c(b(x658))) c(b(c(x658))) -> b(c(c(x658))) b(c(b(x658))) -> b(c(c(x658))) b(c(b(x659))) -> b(b(c(x659))) b(c(b(x659))) -> c(c(b(x659))) c(c(b(x659))) -> b(c(b(x659))) b(c(b(x659))) -> b(b(c(x659))) b(b(c(x659))) -> b(c(c(x659))) c(c(b(x659))) -> b(c(b(x659))) b(c(b(x659))) -> b(c(c(x659))) b(b(c(x659))) -> b(c(c(x659))) c(c(b(x659))) -> c(c(c(x659))) c(c(c(x659))) -> b(c(c(x659))) b(b(c(x659))) -> b(c(c(x659))) c(c(b(x659))) -> c(b(c(x659))) c(b(c(x659))) -> b(c(c(x659))) b(b(c(x659))) -> b(c(c(x659))) c(c(b(x659))) -> c(a(c(x659))) c(a(c(x659))) -> b(c(c(x659))) b(b(c(x659))) -> b(c(c(x659))) b(c(c(x659))) -> b(c(c(x659))) c(c(b(x659))) -> b(c(b(x659))) b(c(b(x659))) -> b(c(c(x659))) b(b(c(x659))) -> b(c(c(x659))) b(c(c(x659))) -> b(c(c(x659))) c(c(b(x659))) -> c(c(c(x659))) c(c(c(x659))) -> b(c(c(x659))) b(b(c(x659))) -> b(c(c(x659))) b(c(c(x659))) -> b(c(c(x659))) c(c(b(x659))) -> c(b(c(x659))) c(b(c(x659))) -> b(c(c(x659))) b(b(c(x659))) -> b(c(c(x659))) b(c(c(x659))) -> b(c(c(x659))) c(c(b(x659))) -> c(a(c(x659))) c(a(c(x659))) -> b(c(c(x659))) b(b(c(x659))) -> b(a(c(x659))) c(c(b(x659))) -> b(c(b(x659))) b(c(b(x659))) -> b(a(c(x659))) b(b(c(x659))) -> b(c(c(x659))) b(c(c(x659))) -> b(a(c(x659))) c(c(b(x659))) -> b(c(b(x659))) b(c(b(x659))) -> b(a(c(x659))) b(b(c(x659))) -> b(c(c(x659))) b(c(c(x659))) -> c(c(c(x659))) c(c(b(x659))) -> c(c(c(x659))) b(b(c(x659))) -> b(c(c(x659))) b(c(c(x659))) -> c(c(c(x659))) c(c(b(x659))) -> c(c(c(x659))) c(c(c(x659))) -> c(c(c(x659))) b(b(c(x659))) -> b(c(c(x659))) b(c(c(x659))) -> c(c(c(x659))) c(c(b(x659))) -> c(b(c(x659))) c(b(c(x659))) -> c(c(c(x659))) b(b(c(x659))) -> b(c(c(x659))) b(c(c(x659))) -> c(c(c(x659))) c(c(b(x659))) -> c(a(c(x659))) c(a(c(x659))) -> c(c(c(x659))) b(b(c(x659))) -> b(a(c(x659))) b(a(c(x659))) -> c(c(c(x659))) c(c(b(x659))) -> c(c(c(x659))) b(b(c(x659))) -> b(a(c(x659))) b(a(c(x659))) -> c(c(c(x659))) c(c(b(x659))) -> c(c(c(x659))) c(c(c(x659))) -> c(c(c(x659))) b(b(c(x659))) -> b(a(c(x659))) b(a(c(x659))) -> c(c(c(x659))) c(c(b(x659))) -> c(b(c(x659))) c(b(c(x659))) -> c(c(c(x659))) b(b(c(x659))) -> b(a(c(x659))) b(a(c(x659))) -> c(c(c(x659))) c(c(b(x659))) -> c(a(c(x659))) c(a(c(x659))) -> c(c(c(x659))) b(b(c(x659))) -> b(c(c(x659))) b(c(c(x659))) -> a(c(c(x659))) c(c(b(x659))) -> c(c(c(x659))) c(c(c(x659))) -> a(c(c(x659))) b(b(c(x659))) -> b(c(c(x659))) b(c(c(x659))) -> a(c(c(x659))) c(c(b(x659))) -> a(c(b(x659))) a(c(b(x659))) -> a(c(c(x659))) b(b(c(x659))) -> b(c(c(x659))) b(c(c(x659))) -> a(c(c(x659))) c(c(b(x659))) -> c(b(c(x659))) c(b(c(x659))) -> a(c(c(x659))) b(b(c(x659))) -> b(a(c(x659))) b(a(c(x659))) -> c(b(c(x659))) c(c(b(x659))) -> c(b(c(x659))) b(b(c(x659))) -> b(a(c(x659))) b(a(c(x659))) -> c(b(c(x659))) c(c(b(x659))) -> c(c(c(x659))) c(c(c(x659))) -> c(b(c(x659))) b(b(c(x659))) -> b(a(c(x659))) b(a(c(x659))) -> c(b(c(x659))) c(c(b(x659))) -> c(b(c(x659))) c(b(c(x659))) -> c(b(c(x659))) c(b(x)) -> b(c(x)) c(b(x)) -> c(c(x)) c(c(x)) -> b(c(x)) b(c(x)) -> c(c(x)) b(c(x)) -> a(c(x)) c(c(x)) -> a(c(x)) c(c(b(x661))) -> c(b(c(x661))) c(c(b(x661))) -> a(c(b(x661))) c(b(c(x661))) -> a(c(c(x661))) a(c(b(x661))) -> a(c(c(x661))) c(c(b(x662))) -> c(b(c(x662))) c(c(b(x662))) -> c(c(b(x662))) c(c(b(x662))) -> c(b(c(x662))) c(b(c(x662))) -> c(c(c(x662))) c(c(b(x662))) -> c(c(c(x662))) c(b(c(x662))) -> c(a(c(x662))) c(c(b(x662))) -> c(a(c(x662))) b(c(b(x663))) -> b(b(c(x663))) b(c(b(x663))) -> b(c(b(x663))) b(c(b(x663))) -> b(b(c(x663))) b(b(c(x663))) -> b(c(c(x663))) b(c(b(x663))) -> b(c(c(x663))) b(b(c(x663))) -> b(a(c(x663))) b(c(b(x663))) -> b(a(c(x663))) b(c(b(x664))) -> b(b(c(x664))) b(c(b(x664))) -> a(c(b(x664))) b(b(c(x664))) -> b(a(c(x664))) a(c(b(x664))) -> a(b(c(x664))) a(b(c(x664))) -> b(a(c(x664))) b(b(c(x664))) -> b(c(c(x664))) b(c(c(x664))) -> b(a(c(x664))) a(c(b(x664))) -> a(b(c(x664))) a(b(c(x664))) -> b(a(c(x664))) b(b(c(x664))) -> b(c(c(x664))) b(c(c(x664))) -> a(c(c(x664))) a(c(b(x664))) -> a(c(c(x664))) b(b(c(x664))) -> b(c(c(x664))) b(c(c(x664))) -> a(c(c(x664))) a(c(b(x664))) -> a(c(c(x664))) a(c(c(x664))) -> a(c(c(x664))) b(b(c(x664))) -> b(c(c(x664))) b(c(c(x664))) -> a(c(c(x664))) a(c(b(x664))) -> a(b(c(x664))) a(b(c(x664))) -> a(c(c(x664))) b(b(c(x664))) -> b(a(c(x664))) b(a(c(x664))) -> c(b(c(x664))) a(c(b(x664))) -> a(b(c(x664))) a(b(c(x664))) -> c(b(c(x664))) c(b(x)) -> b(c(x)) c(b(x)) -> a(c(x)) b(c(x)) -> a(c(x)) c(c(b(x666))) -> c(a(c(x666))) c(c(b(x666))) -> b(c(b(x666))) c(a(c(x666))) -> b(c(c(x666))) b(c(b(x666))) -> b(c(c(x666))) b(c(b(x667))) -> b(a(c(x667))) b(c(b(x667))) -> c(c(b(x667))) b(a(c(x667))) -> c(b(c(x667))) c(c(b(x667))) -> c(b(c(x667))) b(a(c(x667))) -> c(c(c(x667))) c(c(b(x667))) -> c(c(c(x667))) c(b(x)) -> a(c(x)) c(b(x)) -> c(c(x)) c(c(x)) -> a(c(x)) c(c(b(x669))) -> c(a(c(x669))) c(c(b(x669))) -> a(c(b(x669))) c(a(c(x669))) -> b(c(c(x669))) b(c(c(x669))) -> b(a(c(x669))) a(c(b(x669))) -> a(b(c(x669))) a(b(c(x669))) -> b(a(c(x669))) c(a(c(x669))) -> b(c(c(x669))) b(c(c(x669))) -> a(c(c(x669))) a(c(b(x669))) -> a(c(c(x669))) c(a(c(x669))) -> b(c(c(x669))) b(c(c(x669))) -> a(c(c(x669))) a(c(b(x669))) -> a(c(c(x669))) a(c(c(x669))) -> a(c(c(x669))) c(a(c(x669))) -> b(c(c(x669))) b(c(c(x669))) -> a(c(c(x669))) a(c(b(x669))) -> a(b(c(x669))) a(b(c(x669))) -> a(c(c(x669))) c(a(c(x669))) -> c(c(c(x669))) c(c(c(x669))) -> a(c(c(x669))) a(c(b(x669))) -> a(c(c(x669))) c(a(c(x669))) -> c(c(c(x669))) c(c(c(x669))) -> a(c(c(x669))) a(c(b(x669))) -> a(c(c(x669))) a(c(c(x669))) -> a(c(c(x669))) c(a(c(x669))) -> c(c(c(x669))) c(c(c(x669))) -> a(c(c(x669))) a(c(b(x669))) -> a(b(c(x669))) a(b(c(x669))) -> a(c(c(x669))) c(a(c(x669))) -> c(c(c(x669))) c(c(c(x669))) -> c(b(c(x669))) a(c(b(x669))) -> a(b(c(x669))) a(b(c(x669))) -> c(b(c(x669))) c(c(b(x670))) -> c(a(c(x670))) c(c(b(x670))) -> c(c(b(x670))) c(c(b(x670))) -> c(a(c(x670))) c(a(c(x670))) -> c(c(c(x670))) c(c(b(x670))) -> c(c(c(x670))) b(c(b(x671))) -> b(a(c(x671))) b(c(b(x671))) -> b(c(b(x671))) b(c(b(x671))) -> b(a(c(x671))) b(c(b(x672))) -> b(a(c(x672))) b(c(b(x672))) -> a(c(b(x672))) a(c(b(x672))) -> a(b(c(x672))) a(b(c(x672))) -> b(a(c(x672))) b(a(c(x672))) -> c(b(c(x672))) a(c(b(x672))) -> a(b(c(x672))) a(b(c(x672))) -> c(b(c(x672))) b(a(c(x672))) -> c(b(c(x672))) c(b(c(x672))) -> c(b(c(x672))) a(c(b(x672))) -> a(b(c(x672))) a(b(c(x672))) -> c(b(c(x672))) b(a(c(x672))) -> c(c(c(x672))) c(c(c(x672))) -> c(b(c(x672))) a(c(b(x672))) -> a(b(c(x672))) a(b(c(x672))) -> c(b(c(x672))) b(a(c(x672))) -> c(b(c(x672))) c(b(c(x672))) -> a(c(c(x672))) a(c(b(x672))) -> a(c(c(x672))) b(a(c(x672))) -> c(b(c(x672))) c(b(c(x672))) -> a(c(c(x672))) a(c(b(x672))) -> a(c(c(x672))) a(c(c(x672))) -> a(c(c(x672))) b(a(c(x672))) -> c(b(c(x672))) c(b(c(x672))) -> a(c(c(x672))) a(c(b(x672))) -> a(b(c(x672))) a(b(c(x672))) -> a(c(c(x672))) b(a(c(x672))) -> c(c(c(x672))) c(c(c(x672))) -> a(c(c(x672))) a(c(b(x672))) -> a(c(c(x672))) b(a(c(x672))) -> c(c(c(x672))) c(c(c(x672))) -> a(c(c(x672))) a(c(b(x672))) -> a(c(c(x672))) a(c(c(x672))) -> a(c(c(x672))) b(a(c(x672))) -> c(c(c(x672))) c(c(c(x672))) -> a(c(c(x672))) a(c(b(x672))) -> a(b(c(x672))) a(b(c(x672))) -> a(c(c(x672))) c(b(x)) -> a(c(x)) c(b(x)) -> b(c(x)) b(c(x)) -> a(c(x)) weak: c(a(x)) -> b(c(x)) c(c(x)) -> b(c(x)) b(c(x)) -> c(c(x)) a(b(x)) -> b(a(x)) b(a(x)) -> c(b(x)) c(b(x)) -> c(c(x)) c(c(x)) -> a(c(x)) c(a(x)) -> c(c(x)) c(c(x)) -> c(c(x)) b(c(x)) -> b(c(x)) b(c(x)) -> a(c(x)) a(b(x)) -> c(b(x)) b(a(x)) -> c(c(x)) c(b(x)) -> b(c(x)) c(b(x)) -> a(c(x)) Shift Processor (ldh) lab=left (force): strict: weak: Rule Labeling Processor: strict: weak: rule labeling (right): c(a(x)) -> b(c(x)): 2 c(c(x)) -> b(c(x)): 4 b(c(x)) -> c(c(x)): 1 a(b(x)) -> b(a(x)): 4 b(a(x)) -> c(b(x)): 0 c(b(x)) -> c(c(x)): 0 c(c(x)) -> a(c(x)): 1 c(a(x)) -> c(c(x)): 0 c(c(x)) -> c(c(x)): 1 b(c(x)) -> b(c(x)): 1 b(c(x)) -> a(c(x)): 1 a(b(x)) -> c(b(x)): 2 b(a(x)) -> c(c(x)): 0 c(b(x)) -> b(c(x)): 4 c(b(x)) -> a(c(x)): 1 Decreasing Processor: The following diagrams are decreasing: peak: c(b(c(x569))) <-0|0[==1,=>2]- c(c(a(x569))) -1|[==1,?=4]-> b(c(a(x569))) joins (1): c(b(c(x569))) -13|[==1,?=4]-> b(c(c(x569))) b(c(a(x569))) -7|0[==1,>>0]-> b(c(c(x569))) peak: b(b(c(x570))) <-0|0[==1,=?2]- b(c(a(x570))) -2|[==1,>=1]-> c(c(a(x570))) joins (1): b(b(c(x570))) -2|0[==1,>=1]-> b(c(c(x570))) -2|[==1,>=1]-> c(c(c(x570))) c(c(a(x570))) -7|0[==1,>>0]-> c(c(c(x570))) peak: c(b(c(x571))) <-0|0[==1,=?2]- c(c(a(x571))) -6|[==1,>=1]-> a(c(a(x571))) joins (1): c(b(c(x571))) -14|[==1,>=1]-> a(c(c(x571))) a(c(a(x571))) -7|0[==1,>>0]-> a(c(c(x571))) peak: b(c(x)) <-0|[==1,=?2]- c(a(x)) -7|[==1,>=0]-> c(c(x)) joins (1): b(c(x)) -2|[==1,>?1]-> c(c(x)) peak: c(b(c(x573))) <-0|0[==1,=?2]- c(c(a(x573))) -8|[==1,>=1]-> c(c(a(x573))) joins (1): c(c(a(x573))) -0|0[==1,=?2]-> c(b(c(x573))) peak: b(b(c(x574))) <-0|0[==1,=?2]- b(c(a(x574))) -9|[==1,>=1]-> b(c(a(x574))) joins (1): b(c(a(x574))) -0|0[==1,=?2]-> b(b(c(x574))) peak: b(b(c(x575))) <-0|0[==1,=?2]- b(c(a(x575))) -10|[==1,>=1]-> a(c(a(x575))) joins (1): b(b(c(x575))) -2|0[==1,>=1]-> b(c(c(x575))) -10|[==1,>=1]-> a(c(c(x575))) a(c(a(x575))) -7|0[==1,>>0]-> a(c(c(x575))) peak: c(b(c(x576))) <-1|0[==1,==4]- c(c(c(x576))) -1|[==1,==4]-> b(c(c(x576))) joins (1): c(b(c(x576))) -13|[==1,==4]-> b(c(c(x576))) peak: b(b(c(x577))) <-1|0[==1,=?4]- b(c(c(x577))) -2|[==1,>=1]-> c(c(c(x577))) joins (1): b(b(c(x577))) -2|0[==1,>=1]-> b(c(c(x577))) c(c(c(x577))) -1|[==1,=?4]-> b(c(c(x577))) peak: b(c(x)) <-1|[==1,=?4]- c(c(x)) -6|[==1,>=1]-> a(c(x)) joins (1): b(c(x)) -10|[==1,>=1]-> a(c(x)) peak: c(b(c(x579))) <-1|0[==1,=?4]- c(c(c(x579))) -6|[==1,>=1]-> a(c(c(x579))) joins (1): c(b(c(x579))) -14|[==1,>=1]-> a(c(c(x579))) peak: b(c(x)) <-1|[==1,=?4]- c(c(x)) -8|[==1,>=1]-> c(c(x)) joins (1): c(c(x)) -1|[==1,=?4]-> b(c(x)) peak: c(b(c(x581))) <-1|0[==1,=?4]- c(c(c(x581))) -8|[==1,>=1]-> c(c(c(x581))) joins (1): c(c(c(x581))) -1|0[==1,=?4]-> c(b(c(x581))) peak: b(b(c(x582))) <-1|0[==1,=?4]- b(c(c(x582))) -9|[==1,>=1]-> b(c(c(x582))) joins (1): b(c(c(x582))) -1|0[==1,=?4]-> b(b(c(x582))) peak: b(b(c(x583))) <-1|0[==1,=?4]- b(c(c(x583))) -10|[==1,>=1]-> a(c(c(x583))) joins (1): b(b(c(x583))) -2|0[==1,>=1]-> b(c(c(x583))) -10|[==1,>=1]-> a(c(c(x583))) peak: a(c(c(x584))) <-2|0[==1,=>1]- a(b(c(x584))) -3|[==1,?=4]-> b(a(c(x584))) joins (1): b(a(c(x584))) -4|[==1,>>0]-> c(b(c(x584))) -14|[==1,=>1]-> a(c(c(x584))) peak: c(c(c(x585))) <-2|0[==1,=?1]- c(b(c(x585))) -5|[==1,>=0]-> c(c(c(x585))) joins (1): peak: c(c(x)) <-2|[==1,==1]- b(c(x)) -9|[==1,==1]-> b(c(x)) joins (1): b(c(x)) -2|[==1,==1]-> c(c(x)) peak: c(c(x)) <-2|[==1,==1]- b(c(x)) -10|[==1,==1]-> a(c(x)) joins (1): c(c(x)) -6|[==1,==1]-> a(c(x)) peak: a(c(c(x588))) <-2|0[==1,=>1]- a(b(c(x588))) -11|[==1,?=2]-> c(b(c(x588))) joins (1): c(b(c(x588))) -14|[==1,=>1]-> a(c(c(x588))) peak: c(c(c(x589))) <-2|0[==1,=>1]- c(b(c(x589))) -13|[==1,?=4]-> b(c(c(x589))) joins (1): b(c(c(x589))) -2|[==1,=>1]-> c(c(c(x589))) peak: c(c(c(x590))) <-2|0[==1,==1]- c(b(c(x590))) -14|[==1,==1]-> a(c(c(x590))) joins (1): c(c(c(x590))) -6|[==1,==1]-> a(c(c(x590))) peak: c(b(a(x591))) <-3|0[==1,=?4]- c(a(b(x591))) -0|[==1,>=2]-> b(c(b(x591))) joins (1): c(b(a(x591))) -4|0[==1,>>0]-> c(c(b(x591))) b(c(b(x591))) -2|[==1,>>1]-> c(c(b(x591))) peak: b(b(a(x592))) <-3|0[==1,=?4]- b(a(b(x592))) -4|[==1,>=0]-> c(b(b(x592))) joins (1): b(b(a(x592))) -4|0[==1,>=0]-> b(c(b(x592))) c(b(b(x592))) -13|[==1,=?4]-> b(c(b(x592))) peak: c(b(a(x593))) <-3|0[==1,=?4]- c(a(b(x593))) -7|[==1,>=0]-> c(c(b(x593))) joins (1): c(b(a(x593))) -4|0[==1,>=0]-> c(c(b(x593))) peak: b(a(x)) <-3|[==1,=?4]- a(b(x)) -11|[==1,>=2]-> c(b(x)) joins (1): b(a(x)) -4|[==1,>>0]-> c(b(x)) peak: b(b(a(x595))) <-3|0[==1,=?4]- b(a(b(x595))) -12|[==1,>=0]-> c(c(b(x595))) joins (1): b(b(a(x595))) -4|0[==1,>=0]-> b(c(b(x595))) c(c(b(x595))) -1|[==1,=?4]-> b(c(b(x595))) peak: a(c(b(x596))) <-4|0[==1,=>0]- a(b(a(x596))) -3|[==1,?=4]-> b(a(a(x596))) joins (1): a(c(b(x596))) -13|0[==1,?=4]-> a(b(c(x596))) -11|[==1,?>2]-> c(b(c(x596))) b(a(a(x596))) -12|[==1,=>0]-> c(c(a(x596))) -0|0[==1,?>2]-> c(b(c(x596))) peak: c(c(b(x597))) <-4|0[==1,==0]- c(b(a(x597))) -5|[==1,==0]-> c(c(a(x597))) joins (1): c(c(b(x597))) -5|0[==1,==0]-> c(c(c(x597))) c(c(a(x597))) -7|0[==1,==0]-> c(c(c(x597))) peak: a(c(b(x598))) <-4|0[==1,=>0]- a(b(a(x598))) -11|[==1,?=2]-> c(b(a(x598))) joins (1): c(b(a(x598))) -4|0[==1,=>0]-> c(c(b(x598))) -6|[==1,?>1]-> a(c(b(x598))) peak: c(b(x)) <-4|[==1,==0]- b(a(x)) -12|[==1,==0]-> c(c(x)) joins (1): c(b(x)) -5|[==1,==0]-> c(c(x)) peak: c(c(b(x600))) <-4|0[==1,=>0]- c(b(a(x600))) -13|[==1,?=4]-> b(c(a(x600))) joins (1): c(c(b(x600))) -5|0[==1,=>0]-> c(c(c(x600))) b(c(a(x600))) -2|[==1,?>1]-> c(c(a(x600))) -7|0[==1,=>0]-> c(c(c(x600))) peak: c(c(b(x601))) <-4|0[==1,=>0]- c(b(a(x601))) -14|[==1,?=1]-> a(c(a(x601))) joins (1): c(c(b(x601))) -6|[==1,?=1]-> a(c(b(x601))) -5|0[==1,=>0]-> a(c(c(x601))) a(c(a(x601))) -7|0[==1,=>0]-> a(c(c(x601))) peak: c(c(c(x602))) <-5|0[==1,=>0]- c(c(b(x602))) -1|[==1,?=4]-> b(c(b(x602))) joins (1): c(c(c(x602))) -1|[==1,?=4]-> b(c(c(x602))) b(c(b(x602))) -5|0[==1,=>0]-> b(c(c(x602))) peak: b(c(c(x603))) <-5|0[==1,=>0]- b(c(b(x603))) -2|[==1,?=1]-> c(c(b(x603))) joins (1): b(c(c(x603))) -2|[==1,?=1]-> c(c(c(x603))) c(c(b(x603))) -5|0[==1,=>0]-> c(c(c(x603))) peak: c(c(c(x604))) <-5|0[==1,=>0]- c(c(b(x604))) -6|[==1,?=1]-> a(c(b(x604))) joins (1): c(c(c(x604))) -6|[==1,?=1]-> a(c(c(x604))) a(c(b(x604))) -5|0[==1,=>0]-> a(c(c(x604))) peak: c(c(c(x605))) <-5|0[==1,=>0]- c(c(b(x605))) -8|[==1,?=1]-> c(c(b(x605))) joins (1): c(c(b(x605))) -5|0[==1,=>0]-> c(c(c(x605))) peak: b(c(c(x606))) <-5|0[==1,=>0]- b(c(b(x606))) -9|[==1,?=1]-> b(c(b(x606))) joins (1): b(c(b(x606))) -5|0[==1,=>0]-> b(c(c(x606))) peak: b(c(c(x607))) <-5|0[==1,=>0]- b(c(b(x607))) -10|[==1,?=1]-> a(c(b(x607))) joins (1): b(c(c(x607))) -10|[==1,?=1]-> a(c(c(x607))) a(c(b(x607))) -5|0[==1,=>0]-> a(c(c(x607))) peak: c(c(x)) <-5|[==1,=>0]- c(b(x)) -13|[==1,?=4]-> b(c(x)) joins (1): b(c(x)) -2|[==1,?>1]-> c(c(x)) peak: c(c(x)) <-5|[==1,=>0]- c(b(x)) -14|[==1,?=1]-> a(c(x)) joins (1): c(c(x)) -6|[==1,?=1]-> a(c(x)) peak: a(c(x)) <-6|[==1,=>1]- c(c(x)) -1|[==1,?=4]-> b(c(x)) joins (1): b(c(x)) -10|[==1,=>1]-> a(c(x)) peak: c(a(c(x611))) <-6|0[==1,=>1]- c(c(c(x611))) -1|[==1,?=4]-> b(c(c(x611))) joins (1): c(a(c(x611))) -0|[==1,?>2]-> b(c(c(x611))) peak: b(a(c(x612))) <-6|0[==1,==1]- b(c(c(x612))) -2|[==1,==1]-> c(c(c(x612))) joins (1): b(a(c(x612))) -12|[==1,>>0]-> c(c(c(x612))) peak: c(a(c(x613))) <-6|0[==1,==1]- c(c(c(x613))) -6|[==1,==1]-> a(c(c(x613))) joins (1): c(a(c(x613))) -7|[==1,>>0]-> c(c(c(x613))) -6|[==1,==1]-> a(c(c(x613))) peak: a(c(x)) <-6|[==1,==1]- c(c(x)) -8|[==1,==1]-> c(c(x)) joins (1): c(c(x)) -6|[==1,==1]-> a(c(x)) peak: c(a(c(x615))) <-6|0[==1,==1]- c(c(c(x615))) -8|[==1,==1]-> c(c(c(x615))) joins (1): c(c(c(x615))) -6|0[==1,==1]-> c(a(c(x615))) peak: b(a(c(x616))) <-6|0[==1,==1]- b(c(c(x616))) -9|[==1,==1]-> b(c(c(x616))) joins (1): b(c(c(x616))) -6|0[==1,==1]-> b(a(c(x616))) peak: b(a(c(x617))) <-6|0[==1,==1]- b(c(c(x617))) -10|[==1,==1]-> a(c(c(x617))) joins (1): b(a(c(x617))) -4|[==1,>>0]-> c(b(c(x617))) -14|[==1,==1]-> a(c(c(x617))) peak: c(c(x)) <-7|[==1,=>0]- c(a(x)) -0|[==1,?=2]-> b(c(x)) joins (1): b(c(x)) -2|[==1,?>1]-> c(c(x)) peak: c(c(c(x619))) <-7|0[==1,=>0]- c(c(a(x619))) -1|[==1,?=4]-> b(c(a(x619))) joins (1): c(c(c(x619))) -1|[==1,?=4]-> b(c(c(x619))) b(c(a(x619))) -7|0[==1,=>0]-> b(c(c(x619))) peak: b(c(c(x620))) <-7|0[==1,=>0]- b(c(a(x620))) -2|[==1,?=1]-> c(c(a(x620))) joins (1): b(c(c(x620))) -2|[==1,?=1]-> c(c(c(x620))) c(c(a(x620))) -7|0[==1,=>0]-> c(c(c(x620))) peak: c(c(c(x621))) <-7|0[==1,=>0]- c(c(a(x621))) -6|[==1,?=1]-> a(c(a(x621))) joins (1): c(c(c(x621))) -6|[==1,?=1]-> a(c(c(x621))) a(c(a(x621))) -7|0[==1,=>0]-> a(c(c(x621))) peak: c(c(c(x622))) <-7|0[==1,=>0]- c(c(a(x622))) -8|[==1,?=1]-> c(c(a(x622))) joins (1): c(c(a(x622))) -7|0[==1,=>0]-> c(c(c(x622))) peak: b(c(c(x623))) <-7|0[==1,=>0]- b(c(a(x623))) -9|[==1,?=1]-> b(c(a(x623))) joins (1): b(c(a(x623))) -7|0[==1,=>0]-> b(c(c(x623))) peak: b(c(c(x624))) <-7|0[==1,=>0]- b(c(a(x624))) -10|[==1,?=1]-> a(c(a(x624))) joins (1): b(c(c(x624))) -10|[==1,?=1]-> a(c(c(x624))) a(c(a(x624))) -7|0[==1,=>0]-> a(c(c(x624))) peak: c(c(x)) <-8|[==1,=>1]- c(c(x)) -1|[==1,?=4]-> b(c(x)) joins (1): b(c(x)) -2|[==1,=>1]-> c(c(x)) peak: c(c(c(x626))) <-8|0[==1,=>1]- c(c(c(x626))) -1|[==1,?=4]-> b(c(c(x626))) joins (1): b(c(c(x626))) -2|[==1,=>1]-> c(c(c(x626))) peak: b(c(c(x627))) <-8|0[==1,==1]- b(c(c(x627))) -2|[==1,==1]-> c(c(c(x627))) joins (1): b(c(c(x627))) -2|[==1,==1]-> c(c(c(x627))) peak: c(c(x)) <-8|[==1,==1]- c(c(x)) -6|[==1,==1]-> a(c(x)) joins (1): c(c(x)) -6|[==1,==1]-> a(c(x)) peak: c(c(c(x629))) <-8|0[==1,==1]- c(c(c(x629))) -6|[==1,==1]-> a(c(c(x629))) joins (1): c(c(c(x629))) -6|[==1,==1]-> a(c(c(x629))) peak: c(c(c(x630))) <-8|0[==1,==1]- c(c(c(x630))) -8|[==1,==1]-> c(c(c(x630))) joins (1): peak: b(c(c(x631))) <-8|0[==1,==1]- b(c(c(x631))) -9|[==1,==1]-> b(c(c(x631))) joins (1): peak: b(c(c(x632))) <-8|0[==1,==1]- b(c(c(x632))) -10|[==1,==1]-> a(c(c(x632))) joins (1): b(c(c(x632))) -10|[==1,==1]-> a(c(c(x632))) peak: b(c(x)) <-9|[==1,==1]- b(c(x)) -2|[==1,==1]-> c(c(x)) joins (1): b(c(x)) -2|[==1,==1]-> c(c(x)) peak: a(b(c(x634))) <-9|0[==1,=>1]- a(b(c(x634))) -3|[==1,?=4]-> b(a(c(x634))) joins (1): a(b(c(x634))) -3|[==1,?=4]-> b(a(c(x634))) peak: c(b(c(x635))) <-9|0[==1,=?1]- c(b(c(x635))) -5|[==1,>=0]-> c(c(c(x635))) joins (1): c(b(c(x635))) -5|[==1,>=0]-> c(c(c(x635))) peak: b(c(x)) <-9|[==1,==1]- b(c(x)) -10|[==1,==1]-> a(c(x)) joins (1): b(c(x)) -10|[==1,==1]-> a(c(x)) peak: a(b(c(x637))) <-9|0[==1,=>1]- a(b(c(x637))) -11|[==1,?=2]-> c(b(c(x637))) joins (1): a(b(c(x637))) -11|[==1,?=2]-> c(b(c(x637))) peak: c(b(c(x638))) <-9|0[==1,=>1]- c(b(c(x638))) -13|[==1,?=4]-> b(c(c(x638))) joins (1): c(b(c(x638))) -13|[==1,?=4]-> b(c(c(x638))) peak: c(b(c(x639))) <-9|0[==1,==1]- c(b(c(x639))) -14|[==1,==1]-> a(c(c(x639))) joins (1): c(b(c(x639))) -14|[==1,==1]-> a(c(c(x639))) peak: a(c(x)) <-10|[==1,==1]- b(c(x)) -2|[==1,==1]-> c(c(x)) joins (1): c(c(x)) -6|[==1,==1]-> a(c(x)) peak: a(a(c(x641))) <-10|0[==1,=>1]- a(b(c(x641))) -3|[==1,?=4]-> b(a(c(x641))) joins (1): b(a(c(x641))) -4|[==1,>>0]-> c(b(c(x641))) -14|[==1,=>1]-> a(c(c(x641))) -6|0[==1,=>1]-> a(a(c(x641))) peak: c(a(c(x642))) <-10|0[==1,=?1]- c(b(c(x642))) -5|[==1,>=0]-> c(c(c(x642))) joins (1): c(c(c(x642))) -6|0[==1,=?1]-> c(a(c(x642))) peak: a(c(x)) <-10|[==1,==1]- b(c(x)) -9|[==1,==1]-> b(c(x)) joins (1): b(c(x)) -10|[==1,==1]-> a(c(x)) peak: a(a(c(x644))) <-10|0[==1,=>1]- a(b(c(x644))) -11|[==1,?=2]-> c(b(c(x644))) joins (1): c(b(c(x644))) -14|[==1,=>1]-> a(c(c(x644))) -6|0[==1,=>1]-> a(a(c(x644))) peak: c(a(c(x645))) <-10|0[==1,=>1]- c(b(c(x645))) -13|[==1,?=4]-> b(c(c(x645))) joins (1): c(a(c(x645))) -0|[==1,?>2]-> b(c(c(x645))) peak: c(a(c(x646))) <-10|0[==1,==1]- c(b(c(x646))) -14|[==1,==1]-> a(c(c(x646))) joins (1): c(a(c(x646))) -7|[==1,>>0]-> c(c(c(x646))) -6|[==1,==1]-> a(c(c(x646))) peak: c(c(b(x647))) <-11|0[==1,==2]- c(a(b(x647))) -0|[==1,==2]-> b(c(b(x647))) joins (1): b(c(b(x647))) -2|[==1,>>1]-> c(c(b(x647))) peak: c(b(x)) <-11|[==1,=>2]- a(b(x)) -3|[==1,?=4]-> b(a(x)) joins (1): b(a(x)) -4|[==1,>>0]-> c(b(x)) peak: b(c(b(x649))) <-11|0[==1,=?2]- b(a(b(x649))) -4|[==1,>=0]-> c(b(b(x649))) joins (1): b(c(b(x649))) -2|[==1,>?1]-> c(c(b(x649))) c(b(b(x649))) -5|[==1,>=0]-> c(c(b(x649))) peak: c(c(b(x650))) <-11|0[==1,=?2]- c(a(b(x650))) -7|[==1,>=0]-> c(c(b(x650))) joins (1): peak: b(c(b(x651))) <-11|0[==1,=?2]- b(a(b(x651))) -12|[==1,>=0]-> c(c(b(x651))) joins (1): b(c(b(x651))) -2|[==1,>?1]-> c(c(b(x651))) peak: a(c(c(x652))) <-12|0[==1,=>0]- a(b(a(x652))) -3|[==1,?=4]-> b(a(a(x652))) joins (1): a(c(c(x652))) -1|0[==1,?=4]-> a(b(c(x652))) -11|[==1,?>2]-> c(b(c(x652))) b(a(a(x652))) -12|[==1,=>0]-> c(c(a(x652))) -0|0[==1,?>2]-> c(b(c(x652))) peak: c(c(x)) <-12|[==1,==0]- b(a(x)) -4|[==1,==0]-> c(b(x)) joins (1): c(b(x)) -5|[==1,==0]-> c(c(x)) peak: c(c(c(x654))) <-12|0[==1,==0]- c(b(a(x654))) -5|[==1,==0]-> c(c(a(x654))) joins (1): c(c(a(x654))) -7|0[==1,==0]-> c(c(c(x654))) peak: a(c(c(x655))) <-12|0[==1,=>0]- a(b(a(x655))) -11|[==1,?=2]-> c(b(a(x655))) joins (1): c(b(a(x655))) -12|0[==1,=>0]-> c(c(c(x655))) -6|[==1,?>1]-> a(c(c(x655))) peak: c(c(c(x656))) <-12|0[==1,=>0]- c(b(a(x656))) -13|[==1,?=4]-> b(c(a(x656))) joins (1): c(c(c(x656))) -1|[==1,?=4]-> b(c(c(x656))) b(c(a(x656))) -7|0[==1,=>0]-> b(c(c(x656))) peak: c(c(c(x657))) <-12|0[==1,=>0]- c(b(a(x657))) -14|[==1,?=1]-> a(c(a(x657))) joins (1): c(c(c(x657))) -6|[==1,?=1]-> a(c(c(x657))) a(c(a(x657))) -7|0[==1,=>0]-> a(c(c(x657))) peak: c(b(c(x658))) <-13|0[==1,==4]- c(c(b(x658))) -1|[==1,==4]-> b(c(b(x658))) joins (1): c(b(c(x658))) -13|[==1,==4]-> b(c(c(x658))) b(c(b(x658))) -5|0[==1,>>0]-> b(c(c(x658))) peak: b(b(c(x659))) <-13|0[==1,=?4]- b(c(b(x659))) -2|[==1,>=1]-> c(c(b(x659))) joins (1): b(b(c(x659))) -2|0[==1,>=1]-> b(c(c(x659))) c(c(b(x659))) -1|[==1,=?4]-> b(c(b(x659))) -5|0[==1,>>0]-> b(c(c(x659))) peak: b(c(x)) <-13|[==1,=?4]- c(b(x)) -5|[==1,>=0]-> c(c(x)) joins (1): c(c(x)) -1|[==1,=?4]-> b(c(x)) peak: c(b(c(x661))) <-13|0[==1,=?4]- c(c(b(x661))) -6|[==1,>=1]-> a(c(b(x661))) joins (1): c(b(c(x661))) -14|[==1,>=1]-> a(c(c(x661))) a(c(b(x661))) -5|0[==1,>>0]-> a(c(c(x661))) peak: c(b(c(x662))) <-13|0[==1,=?4]- c(c(b(x662))) -8|[==1,>=1]-> c(c(b(x662))) joins (1): c(c(b(x662))) -13|0[==1,=?4]-> c(b(c(x662))) peak: b(b(c(x663))) <-13|0[==1,=?4]- b(c(b(x663))) -9|[==1,>=1]-> b(c(b(x663))) joins (1): b(c(b(x663))) -13|0[==1,=?4]-> b(b(c(x663))) peak: b(b(c(x664))) <-13|0[==1,=?4]- b(c(b(x664))) -10|[==1,>=1]-> a(c(b(x664))) joins (1): b(b(c(x664))) -2|0[==1,>=1]-> b(c(c(x664))) -10|[==1,>=1]-> a(c(c(x664))) a(c(b(x664))) -5|0[==1,>>0]-> a(c(c(x664))) peak: b(c(x)) <-13|[==1,=?4]- c(b(x)) -14|[==1,>=1]-> a(c(x)) joins (1): b(c(x)) -10|[==1,>=1]-> a(c(x)) peak: c(a(c(x666))) <-14|0[==1,=>1]- c(c(b(x666))) -1|[==1,?=4]-> b(c(b(x666))) joins (1): c(a(c(x666))) -0|[==1,?>2]-> b(c(c(x666))) b(c(b(x666))) -5|0[==1,>>0]-> b(c(c(x666))) peak: b(a(c(x667))) <-14|0[==1,==1]- b(c(b(x667))) -2|[==1,==1]-> c(c(b(x667))) joins (1): b(a(c(x667))) -12|[==1,>>0]-> c(c(c(x667))) c(c(b(x667))) -5|0[==1,>>0]-> c(c(c(x667))) peak: a(c(x)) <-14|[==1,=?1]- c(b(x)) -5|[==1,>=0]-> c(c(x)) joins (1): c(c(x)) -6|[==1,=?1]-> a(c(x)) peak: c(a(c(x669))) <-14|0[==1,==1]- c(c(b(x669))) -6|[==1,==1]-> a(c(b(x669))) joins (1): c(a(c(x669))) -7|[==1,>>0]-> c(c(c(x669))) -6|[==1,==1]-> a(c(c(x669))) a(c(b(x669))) -5|0[==1,>>0]-> a(c(c(x669))) peak: c(a(c(x670))) <-14|0[==1,==1]- c(c(b(x670))) -8|[==1,==1]-> c(c(b(x670))) joins (1): c(c(b(x670))) -14|0[==1,==1]-> c(a(c(x670))) peak: b(a(c(x671))) <-14|0[==1,==1]- b(c(b(x671))) -9|[==1,==1]-> b(c(b(x671))) joins (1): b(c(b(x671))) -14|0[==1,==1]-> b(a(c(x671))) peak: b(a(c(x672))) <-14|0[==1,==1]- b(c(b(x672))) -10|[==1,==1]-> a(c(b(x672))) joins (1): b(a(c(x672))) -4|[==1,>>0]-> c(b(c(x672))) -14|[==1,==1]-> a(c(c(x672))) a(c(b(x672))) -5|0[==1,>>0]-> a(c(c(x672))) peak: a(c(x)) <-14|[==1,=>1]- c(b(x)) -13|[==1,?=4]-> b(c(x)) joins (1): b(c(x)) -10|[==1,=>1]-> a(c(x)) Qed