YES Problem: b(c(x)) -> c(c(x)) a(a(x)) -> a(b(x)) c(b(x)) -> c(a(x)) b(a(x)) -> c(a(x)) a(c(x)) -> c(a(x)) c(a(x)) -> a(b(x)) a(b(x)) -> c(c(x)) Proof: Church Rosser Transformation Processor (no redundant rules): strict: weak: critical peaks: 17 c(c(c(x99))) <-0|0[]- c(a(b(x99))) -1|[]-> a(b(b(x99))) b(c(c(x100))) <-0|0[]- b(a(b(x100))) -3|[]-> c(a(b(x100))) a(c(c(x101))) <-0|0[]- a(a(b(x101))) -5|[]-> a(b(b(x101))) a(a(b(x102))) <-1|0[]- a(c(a(x102))) -2|[]-> c(a(a(x102))) b(a(b(x103))) <-1|0[]- b(c(a(x103))) -6|[]-> c(c(a(x103))) c(c(a(x104))) <-2|0[]- c(a(c(x104))) -1|[]-> a(b(c(x104))) b(c(a(x105))) <-2|0[]- b(a(c(x105))) -3|[]-> c(a(c(x105))) a(c(a(x106))) <-2|0[]- a(a(c(x106))) -5|[]-> a(b(c(x106))) a(c(a(x107))) <-3|0[]- a(b(a(x107))) -0|[]-> c(c(a(x107))) c(c(a(x108))) <-3|0[]- c(b(a(x108))) -4|[]-> c(a(a(x108))) a(c(a(x109))) <-4|0[]- a(c(b(x109))) -2|[]-> c(a(b(x109))) b(c(a(x110))) <-4|0[]- b(c(b(x110))) -6|[]-> c(c(b(x110))) c(a(b(x111))) <-5|0[]- c(a(a(x111))) -1|[]-> a(b(a(x111))) b(a(b(x112))) <-5|0[]- b(a(a(x112))) -3|[]-> c(a(a(x112))) a(a(b(x113))) <-5|0[]- a(a(a(x113))) -5|[]-> a(b(a(x113))) a(c(c(x114))) <-6|0[]- a(b(c(x114))) -0|[]-> c(c(c(x114))) c(c(c(x115))) <-6|0[]- c(b(c(x115))) -4|[]-> c(a(c(x115))) Redundant Rules Transformation: a(b(x)) -> c(c(x)) c(a(x)) -> a(b(x)) a(c(x)) -> c(a(x)) b(a(x)) -> c(a(x)) c(b(x)) -> c(a(x)) a(a(x)) -> a(b(x)) b(c(x)) -> c(c(x)) c(a(x)) -> c(c(x)) a(c(x)) -> a(b(x)) b(a(x)) -> a(b(x)) c(b(x)) -> a(b(x)) a(a(x)) -> c(c(x)) Church Rosser Transformation Processor (no redundant rules): strict: weak: critical peaks: 61 a(c(c(x404))) <-0|0[]- a(a(a(x404))) -0|[]-> c(c(a(x404))) b(c(c(x405))) <-0|0[]- b(a(a(x405))) -2|[]-> a(b(a(x405))) c(c(c(x406))) <-0|0[]- c(a(a(x406))) -4|[]-> c(c(a(x406))) c(c(x)) <-0|[]- a(a(x)) -6|[]-> a(b(x)) a(c(c(x408))) <-0|0[]- a(a(a(x408))) -6|[]-> a(b(a(x408))) b(c(c(x409))) <-0|0[]- b(a(a(x409))) -8|[]-> c(a(a(x409))) c(c(c(x410))) <-0|0[]- c(a(a(x410))) -10|[]-> a(b(a(x410))) a(a(b(x411))) <-1|0[]- a(c(b(x411))) -3|[]-> a(b(b(x411))) b(a(b(x412))) <-1|0[]- b(c(b(x412))) -5|[]-> c(c(b(x412))) a(b(x)) <-1|[]- c(b(x)) -7|[]-> c(a(x)) a(a(b(x414))) <-1|0[]- a(c(b(x414))) -9|[]-> c(a(b(x414))) c(a(b(x415))) <-2|0[]- c(b(a(x415))) -1|[]-> a(b(a(x415))) c(a(b(x416))) <-2|0[]- c(b(a(x416))) -7|[]-> c(a(a(x416))) a(b(x)) <-2|[]- b(a(x)) -8|[]-> c(a(x)) a(a(b(x418))) <-2|0[]- a(b(a(x418))) -11|[]-> c(c(a(x418))) a(a(b(x419))) <-3|0[]- a(a(c(x419))) -0|[]-> c(c(c(x419))) b(a(b(x420))) <-3|0[]- b(a(c(x420))) -2|[]-> a(b(c(x420))) c(a(b(x421))) <-3|0[]- c(a(c(x421))) -4|[]-> c(c(c(x421))) a(a(b(x422))) <-3|0[]- a(a(c(x422))) -6|[]-> a(b(c(x422))) b(a(b(x423))) <-3|0[]- b(a(c(x423))) -8|[]-> c(a(c(x423))) a(b(x)) <-3|[]- a(c(x)) -9|[]-> c(a(x)) c(a(b(x425))) <-3|0[]- c(a(c(x425))) -10|[]-> a(b(c(x425))) a(c(c(x426))) <-4|0[]- a(c(a(x426))) -3|[]-> a(b(a(x426))) b(c(c(x427))) <-4|0[]- b(c(a(x427))) -5|[]-> c(c(a(x427))) a(c(c(x428))) <-4|0[]- a(c(a(x428))) -9|[]-> c(a(a(x428))) c(c(x)) <-4|[]- c(a(x)) -10|[]-> a(b(x)) c(c(c(x430))) <-5|0[]- c(b(c(x430))) -1|[]-> a(b(c(x430))) c(c(c(x431))) <-5|0[]- c(b(c(x431))) -7|[]-> c(a(c(x431))) a(c(c(x432))) <-5|0[]- a(b(c(x432))) -11|[]-> c(c(c(x432))) a(b(x)) <-6|[]- a(a(x)) -0|[]-> c(c(x)) a(a(b(x434))) <-6|0[]- a(a(a(x434))) -0|[]-> c(c(a(x434))) b(a(b(x435))) <-6|0[]- b(a(a(x435))) -2|[]-> a(b(a(x435))) c(a(b(x436))) <-6|0[]- c(a(a(x436))) -4|[]-> c(c(a(x436))) a(a(b(x437))) <-6|0[]- a(a(a(x437))) -6|[]-> a(b(a(x437))) b(a(b(x438))) <-6|0[]- b(a(a(x438))) -8|[]-> c(a(a(x438))) c(a(b(x439))) <-6|0[]- c(a(a(x439))) -10|[]-> a(b(a(x439))) c(a(x)) <-7|[]- c(b(x)) -1|[]-> a(b(x)) a(c(a(x441))) <-7|0[]- a(c(b(x441))) -3|[]-> a(b(b(x441))) b(c(a(x442))) <-7|0[]- b(c(b(x442))) -5|[]-> c(c(b(x442))) a(c(a(x443))) <-7|0[]- a(c(b(x443))) -9|[]-> c(a(b(x443))) c(c(a(x444))) <-8|0[]- c(b(a(x444))) -1|[]-> a(b(a(x444))) c(a(x)) <-8|[]- b(a(x)) -2|[]-> a(b(x)) c(c(a(x446))) <-8|0[]- c(b(a(x446))) -7|[]-> c(a(a(x446))) a(c(a(x447))) <-8|0[]- a(b(a(x447))) -11|[]-> c(c(a(x447))) a(c(a(x448))) <-9|0[]- a(a(c(x448))) -0|[]-> c(c(c(x448))) b(c(a(x449))) <-9|0[]- b(a(c(x449))) -2|[]-> a(b(c(x449))) c(a(x)) <-9|[]- a(c(x)) -3|[]-> a(b(x)) c(c(a(x451))) <-9|0[]- c(a(c(x451))) -4|[]-> c(c(c(x451))) a(c(a(x452))) <-9|0[]- a(a(c(x452))) -6|[]-> a(b(c(x452))) b(c(a(x453))) <-9|0[]- b(a(c(x453))) -8|[]-> c(a(c(x453))) c(c(a(x454))) <-9|0[]- c(a(c(x454))) -10|[]-> a(b(c(x454))) a(a(b(x455))) <-10|0[]- a(c(a(x455))) -3|[]-> a(b(a(x455))) a(b(x)) <-10|[]- c(a(x)) -4|[]-> c(c(x)) b(a(b(x457))) <-10|0[]- b(c(a(x457))) -5|[]-> c(c(a(x457))) a(a(b(x458))) <-10|0[]- a(c(a(x458))) -9|[]-> c(a(a(x458))) a(c(c(x459))) <-11|0[]- a(a(b(x459))) -0|[]-> c(c(b(x459))) b(c(c(x460))) <-11|0[]- b(a(b(x460))) -2|[]-> a(b(b(x460))) c(c(c(x461))) <-11|0[]- c(a(b(x461))) -4|[]-> c(c(b(x461))) a(c(c(x462))) <-11|0[]- a(a(b(x462))) -6|[]-> a(b(b(x462))) b(c(c(x463))) <-11|0[]- b(a(b(x463))) -8|[]-> c(a(b(x463))) c(c(c(x464))) <-11|0[]- c(a(b(x464))) -10|[]-> a(b(b(x464))) Redundant Rules Transformation: a(a(x)) -> c(c(x)) c(b(x)) -> a(b(x)) b(a(x)) -> a(b(x)) a(c(x)) -> a(b(x)) c(a(x)) -> c(c(x)) b(c(x)) -> c(c(x)) a(a(x)) -> a(b(x)) c(b(x)) -> c(a(x)) b(a(x)) -> c(a(x)) a(c(x)) -> c(a(x)) c(a(x)) -> a(b(x)) a(b(x)) -> c(c(x)) c(b(x)) -> c(c(x)) b(a(x)) -> c(c(x)) a(c(x)) -> c(c(x)) Church Rosser Transformation Processor (redex): strict: weak: a(c(x)) -> c(c(x)) b(a(x)) -> c(c(x)) c(b(x)) -> c(c(x)) a(b(x)) -> c(c(x)) c(a(x)) -> a(b(x)) a(c(x)) -> c(a(x)) b(a(x)) -> c(a(x)) c(b(x)) -> c(a(x)) a(a(x)) -> a(b(x)) b(c(x)) -> c(c(x)) c(a(x)) -> c(c(x)) a(c(x)) -> a(b(x)) b(a(x)) -> a(b(x)) c(b(x)) -> a(b(x)) a(a(x)) -> c(c(x)) critical peaks: 100 a(c(c(x915))) <-0|0[]- a(a(a(x915))) -0|[]-> c(c(a(x915))) b(c(c(x916))) <-0|0[]- b(a(a(x916))) -2|[]-> a(b(a(x916))) c(c(c(x917))) <-0|0[]- c(a(a(x917))) -4|[]-> c(c(a(x917))) c(c(x)) <-0|[]- a(a(x)) -6|[]-> a(b(x)) a(c(c(x919))) <-0|0[]- a(a(a(x919))) -6|[]-> a(b(a(x919))) b(c(c(x920))) <-0|0[]- b(a(a(x920))) -8|[]-> c(a(a(x920))) c(c(c(x921))) <-0|0[]- c(a(a(x921))) -10|[]-> a(b(a(x921))) b(c(c(x922))) <-0|0[]- b(a(a(x922))) -13|[]-> c(c(a(x922))) a(a(b(x923))) <-1|0[]- a(c(b(x923))) -3|[]-> a(b(b(x923))) b(a(b(x924))) <-1|0[]- b(c(b(x924))) -5|[]-> c(c(b(x924))) a(b(x)) <-1|[]- c(b(x)) -7|[]-> c(a(x)) a(a(b(x926))) <-1|0[]- a(c(b(x926))) -9|[]-> c(a(b(x926))) a(b(x)) <-1|[]- c(b(x)) -12|[]-> c(c(x)) a(a(b(x928))) <-1|0[]- a(c(b(x928))) -14|[]-> c(c(b(x928))) c(a(b(x929))) <-2|0[]- c(b(a(x929))) -1|[]-> a(b(a(x929))) c(a(b(x930))) <-2|0[]- c(b(a(x930))) -7|[]-> c(a(a(x930))) a(b(x)) <-2|[]- b(a(x)) -8|[]-> c(a(x)) a(a(b(x932))) <-2|0[]- a(b(a(x932))) -11|[]-> c(c(a(x932))) c(a(b(x933))) <-2|0[]- c(b(a(x933))) -12|[]-> c(c(a(x933))) a(b(x)) <-2|[]- b(a(x)) -13|[]-> c(c(x)) a(a(b(x935))) <-3|0[]- a(a(c(x935))) -0|[]-> c(c(c(x935))) b(a(b(x936))) <-3|0[]- b(a(c(x936))) -2|[]-> a(b(c(x936))) c(a(b(x937))) <-3|0[]- c(a(c(x937))) -4|[]-> c(c(c(x937))) a(a(b(x938))) <-3|0[]- a(a(c(x938))) -6|[]-> a(b(c(x938))) b(a(b(x939))) <-3|0[]- b(a(c(x939))) -8|[]-> c(a(c(x939))) a(b(x)) <-3|[]- a(c(x)) -9|[]-> c(a(x)) c(a(b(x941))) <-3|0[]- c(a(c(x941))) -10|[]-> a(b(c(x941))) b(a(b(x942))) <-3|0[]- b(a(c(x942))) -13|[]-> c(c(c(x942))) a(b(x)) <-3|[]- a(c(x)) -14|[]-> c(c(x)) a(c(c(x944))) <-4|0[]- a(c(a(x944))) -3|[]-> a(b(a(x944))) b(c(c(x945))) <-4|0[]- b(c(a(x945))) -5|[]-> c(c(a(x945))) a(c(c(x946))) <-4|0[]- a(c(a(x946))) -9|[]-> c(a(a(x946))) c(c(x)) <-4|[]- c(a(x)) -10|[]-> a(b(x)) a(c(c(x948))) <-4|0[]- a(c(a(x948))) -14|[]-> c(c(a(x948))) c(c(c(x949))) <-5|0[]- c(b(c(x949))) -1|[]-> a(b(c(x949))) c(c(c(x950))) <-5|0[]- c(b(c(x950))) -7|[]-> c(a(c(x950))) a(c(c(x951))) <-5|0[]- a(b(c(x951))) -11|[]-> c(c(c(x951))) c(c(c(x952))) <-5|0[]- c(b(c(x952))) -12|[]-> c(c(c(x952))) a(b(x)) <-6|[]- a(a(x)) -0|[]-> c(c(x)) a(a(b(x954))) <-6|0[]- a(a(a(x954))) -0|[]-> c(c(a(x954))) b(a(b(x955))) <-6|0[]- b(a(a(x955))) -2|[]-> a(b(a(x955))) c(a(b(x956))) <-6|0[]- c(a(a(x956))) -4|[]-> c(c(a(x956))) a(a(b(x957))) <-6|0[]- a(a(a(x957))) -6|[]-> a(b(a(x957))) b(a(b(x958))) <-6|0[]- b(a(a(x958))) -8|[]-> c(a(a(x958))) c(a(b(x959))) <-6|0[]- c(a(a(x959))) -10|[]-> a(b(a(x959))) b(a(b(x960))) <-6|0[]- b(a(a(x960))) -13|[]-> c(c(a(x960))) c(a(x)) <-7|[]- c(b(x)) -1|[]-> a(b(x)) a(c(a(x962))) <-7|0[]- a(c(b(x962))) -3|[]-> a(b(b(x962))) b(c(a(x963))) <-7|0[]- b(c(b(x963))) -5|[]-> c(c(b(x963))) a(c(a(x964))) <-7|0[]- a(c(b(x964))) -9|[]-> c(a(b(x964))) c(a(x)) <-7|[]- c(b(x)) -12|[]-> c(c(x)) a(c(a(x966))) <-7|0[]- a(c(b(x966))) -14|[]-> c(c(b(x966))) c(c(a(x967))) <-8|0[]- c(b(a(x967))) -1|[]-> a(b(a(x967))) c(a(x)) <-8|[]- b(a(x)) -2|[]-> a(b(x)) c(c(a(x969))) <-8|0[]- c(b(a(x969))) -7|[]-> c(a(a(x969))) a(c(a(x970))) <-8|0[]- a(b(a(x970))) -11|[]-> c(c(a(x970))) c(c(a(x971))) <-8|0[]- c(b(a(x971))) -12|[]-> c(c(a(x971))) c(a(x)) <-8|[]- b(a(x)) -13|[]-> c(c(x)) a(c(a(x973))) <-9|0[]- a(a(c(x973))) -0|[]-> c(c(c(x973))) b(c(a(x974))) <-9|0[]- b(a(c(x974))) -2|[]-> a(b(c(x974))) c(a(x)) <-9|[]- a(c(x)) -3|[]-> a(b(x)) c(c(a(x976))) <-9|0[]- c(a(c(x976))) -4|[]-> c(c(c(x976))) a(c(a(x977))) <-9|0[]- a(a(c(x977))) -6|[]-> a(b(c(x977))) b(c(a(x978))) <-9|0[]- b(a(c(x978))) -8|[]-> c(a(c(x978))) c(c(a(x979))) <-9|0[]- c(a(c(x979))) -10|[]-> a(b(c(x979))) b(c(a(x980))) <-9|0[]- b(a(c(x980))) -13|[]-> c(c(c(x980))) c(a(x)) <-9|[]- a(c(x)) -14|[]-> c(c(x)) a(a(b(x982))) <-10|0[]- a(c(a(x982))) -3|[]-> a(b(a(x982))) a(b(x)) <-10|[]- c(a(x)) -4|[]-> c(c(x)) b(a(b(x984))) <-10|0[]- b(c(a(x984))) -5|[]-> c(c(a(x984))) a(a(b(x985))) <-10|0[]- a(c(a(x985))) -9|[]-> c(a(a(x985))) a(a(b(x986))) <-10|0[]- a(c(a(x986))) -14|[]-> c(c(a(x986))) a(c(c(x987))) <-11|0[]- a(a(b(x987))) -0|[]-> c(c(b(x987))) b(c(c(x988))) <-11|0[]- b(a(b(x988))) -2|[]-> a(b(b(x988))) c(c(c(x989))) <-11|0[]- c(a(b(x989))) -4|[]-> c(c(b(x989))) a(c(c(x990))) <-11|0[]- a(a(b(x990))) -6|[]-> a(b(b(x990))) b(c(c(x991))) <-11|0[]- b(a(b(x991))) -8|[]-> c(a(b(x991))) c(c(c(x992))) <-11|0[]- c(a(b(x992))) -10|[]-> a(b(b(x992))) b(c(c(x993))) <-11|0[]- b(a(b(x993))) -13|[]-> c(c(b(x993))) c(c(x)) <-12|[]- c(b(x)) -1|[]-> a(b(x)) a(c(c(x995))) <-12|0[]- a(c(b(x995))) -3|[]-> a(b(b(x995))) b(c(c(x996))) <-12|0[]- b(c(b(x996))) -5|[]-> c(c(b(x996))) c(c(x)) <-12|[]- c(b(x)) -7|[]-> c(a(x)) a(c(c(x998))) <-12|0[]- a(c(b(x998))) -9|[]-> c(a(b(x998))) a(c(c(x999))) <-12|0[]- a(c(b(x999))) -14|[]-> c(c(b(x999))) c(c(c(x1000))) <-13|0[]- c(b(a(x1000))) -1|[]-> a(b(a(x1000))) c(c(x)) <-13|[]- b(a(x)) -2|[]-> a(b(x)) c(c(c(x1002))) <-13|0[]- c(b(a(x1002))) -7|[]-> c(a(a(x1002))) c(c(x)) <-13|[]- b(a(x)) -8|[]-> c(a(x)) a(c(c(x1004))) <-13|0[]- a(b(a(x1004))) -11|[]-> c(c(a(x1004))) c(c(c(x1005))) <-13|0[]- c(b(a(x1005))) -12|[]-> c(c(a(x1005))) a(c(c(x1006))) <-14|0[]- a(a(c(x1006))) -0|[]-> c(c(c(x1006))) b(c(c(x1007))) <-14|0[]- b(a(c(x1007))) -2|[]-> a(b(c(x1007))) c(c(x)) <-14|[]- a(c(x)) -3|[]-> a(b(x)) c(c(c(x1009))) <-14|0[]- c(a(c(x1009))) -4|[]-> c(c(c(x1009))) a(c(c(x1010))) <-14|0[]- a(a(c(x1010))) -6|[]-> a(b(c(x1010))) b(c(c(x1011))) <-14|0[]- b(a(c(x1011))) -8|[]-> c(a(c(x1011))) c(c(x)) <-14|[]- a(c(x)) -9|[]-> c(a(x)) c(c(c(x1013))) <-14|0[]- c(a(c(x1013))) -10|[]-> a(b(c(x1013))) b(c(c(x1014))) <-14|0[]- b(a(c(x1014))) -13|[]-> c(c(c(x1014))) Shift Processor (no label): strict: weak: Shift Processor lab=left (dd): strict: a(a(a(x915))) -> a(c(c(x915))) a(a(a(x915))) -> c(c(a(x915))) a(c(c(x915))) -> c(c(c(x915))) c(c(a(x915))) -> c(c(c(x915))) b(a(a(x916))) -> b(c(c(x916))) b(a(a(x916))) -> a(b(a(x916))) b(c(c(x916))) -> c(c(c(x916))) a(b(a(x916))) -> c(c(a(x916))) c(c(a(x916))) -> c(c(c(x916))) b(c(c(x916))) -> c(c(c(x916))) a(b(a(x916))) -> a(c(c(x916))) a(c(c(x916))) -> c(c(c(x916))) c(a(a(x917))) -> c(c(c(x917))) c(a(a(x917))) -> c(c(a(x917))) c(c(a(x917))) -> c(c(c(x917))) a(a(x)) -> c(c(x)) a(a(x)) -> a(b(x)) a(b(x)) -> c(c(x)) a(a(a(x919))) -> a(c(c(x919))) a(a(a(x919))) -> a(b(a(x919))) a(b(a(x919))) -> a(c(c(x919))) b(a(a(x920))) -> b(c(c(x920))) b(a(a(x920))) -> c(a(a(x920))) b(c(c(x920))) -> c(c(c(x920))) c(a(a(x920))) -> c(c(c(x920))) c(a(a(x921))) -> c(c(c(x921))) c(a(a(x921))) -> a(b(a(x921))) a(b(a(x921))) -> c(c(a(x921))) c(c(a(x921))) -> c(c(c(x921))) a(b(a(x921))) -> a(c(c(x921))) a(c(c(x921))) -> c(c(c(x921))) b(a(a(x922))) -> b(c(c(x922))) b(a(a(x922))) -> c(c(a(x922))) b(c(c(x922))) -> c(c(c(x922))) c(c(a(x922))) -> c(c(c(x922))) a(c(b(x923))) -> a(a(b(x923))) a(c(b(x923))) -> a(b(b(x923))) a(a(b(x923))) -> c(c(b(x923))) a(b(b(x923))) -> c(c(b(x923))) a(a(b(x923))) -> a(b(b(x923))) b(c(b(x924))) -> b(a(b(x924))) b(c(b(x924))) -> c(c(b(x924))) b(a(b(x924))) -> c(a(b(x924))) c(c(b(x924))) -> c(a(b(x924))) b(a(b(x924))) -> c(c(b(x924))) c(b(x)) -> a(b(x)) c(b(x)) -> c(a(x)) c(a(x)) -> a(b(x)) a(b(x)) -> c(c(x)) c(a(x)) -> c(c(x)) a(c(b(x926))) -> a(a(b(x926))) a(c(b(x926))) -> c(a(b(x926))) a(a(b(x926))) -> c(c(b(x926))) c(a(b(x926))) -> c(c(b(x926))) a(a(b(x926))) -> a(b(b(x926))) c(a(b(x926))) -> a(b(b(x926))) c(b(x)) -> a(b(x)) c(b(x)) -> c(c(x)) a(b(x)) -> c(c(x)) a(c(b(x928))) -> a(a(b(x928))) a(c(b(x928))) -> c(c(b(x928))) a(a(b(x928))) -> c(c(b(x928))) c(b(a(x929))) -> c(a(b(x929))) c(b(a(x929))) -> a(b(a(x929))) a(b(a(x929))) -> c(c(a(x929))) c(c(a(x929))) -> c(a(b(x929))) c(a(b(x929))) -> c(c(b(x929))) a(b(a(x929))) -> a(a(b(x929))) a(a(b(x929))) -> c(c(b(x929))) c(a(b(x929))) -> a(b(b(x929))) a(b(b(x929))) -> c(c(b(x929))) a(b(a(x929))) -> a(a(b(x929))) a(a(b(x929))) -> c(c(b(x929))) c(a(b(x929))) -> a(b(b(x929))) a(b(a(x929))) -> a(a(b(x929))) a(a(b(x929))) -> a(b(b(x929))) c(a(b(x929))) -> c(c(c(x929))) a(b(a(x929))) -> c(c(a(x929))) c(c(a(x929))) -> c(c(c(x929))) c(a(b(x929))) -> c(c(c(x929))) a(b(a(x929))) -> a(c(c(x929))) a(c(c(x929))) -> c(c(c(x929))) c(a(b(x929))) -> c(c(b(x929))) c(c(b(x929))) -> c(c(c(x929))) a(b(a(x929))) -> c(c(a(x929))) c(c(a(x929))) -> c(c(c(x929))) c(a(b(x929))) -> c(c(b(x929))) c(c(b(x929))) -> c(c(c(x929))) a(b(a(x929))) -> a(c(c(x929))) a(c(c(x929))) -> c(c(c(x929))) c(a(b(x929))) -> c(c(b(x929))) c(c(b(x929))) -> c(c(a(x929))) a(b(a(x929))) -> c(c(a(x929))) c(a(b(x929))) -> c(c(b(x929))) c(c(b(x929))) -> c(c(a(x929))) a(b(a(x929))) -> a(c(a(x929))) a(c(a(x929))) -> c(c(a(x929))) c(b(a(x930))) -> c(a(b(x930))) c(b(a(x930))) -> c(a(a(x930))) c(a(a(x930))) -> c(a(b(x930))) c(a(b(x930))) -> c(c(c(x930))) c(a(a(x930))) -> c(c(c(x930))) b(a(x)) -> a(b(x)) b(a(x)) -> c(a(x)) c(a(x)) -> a(b(x)) a(b(x)) -> c(c(x)) c(a(x)) -> c(c(x)) a(b(a(x932))) -> a(a(b(x932))) a(b(a(x932))) -> c(c(a(x932))) a(a(b(x932))) -> c(c(b(x932))) c(c(a(x932))) -> c(a(b(x932))) c(a(b(x932))) -> c(c(b(x932))) a(a(b(x932))) -> a(b(b(x932))) a(b(b(x932))) -> c(c(b(x932))) c(c(a(x932))) -> c(a(b(x932))) c(a(b(x932))) -> c(c(b(x932))) a(a(b(x932))) -> a(b(b(x932))) c(c(a(x932))) -> c(a(b(x932))) c(a(b(x932))) -> a(b(b(x932))) a(a(b(x932))) -> c(c(b(x932))) c(c(b(x932))) -> c(a(b(x932))) c(c(a(x932))) -> c(a(b(x932))) a(a(b(x932))) -> c(c(b(x932))) c(c(b(x932))) -> c(c(a(x932))) a(a(b(x932))) -> c(c(b(x932))) c(c(b(x932))) -> c(c(c(x932))) c(c(a(x932))) -> c(c(c(x932))) a(a(b(x932))) -> c(c(b(x932))) c(c(b(x932))) -> c(c(c(x932))) c(c(a(x932))) -> c(a(b(x932))) c(a(b(x932))) -> c(c(c(x932))) a(a(b(x932))) -> a(c(c(x932))) a(c(c(x932))) -> c(c(c(x932))) c(c(a(x932))) -> c(c(c(x932))) a(a(b(x932))) -> a(c(c(x932))) a(c(c(x932))) -> c(c(c(x932))) c(c(a(x932))) -> c(a(b(x932))) c(a(b(x932))) -> c(c(c(x932))) c(b(a(x933))) -> c(a(b(x933))) c(b(a(x933))) -> c(c(a(x933))) c(c(a(x933))) -> c(a(b(x933))) c(a(b(x933))) -> c(c(c(x933))) c(c(a(x933))) -> c(c(c(x933))) b(a(x)) -> a(b(x)) b(a(x)) -> c(c(x)) a(b(x)) -> c(c(x)) a(a(c(x935))) -> a(a(b(x935))) a(a(c(x935))) -> c(c(c(x935))) a(a(b(x935))) -> c(c(b(x935))) c(c(b(x935))) -> c(c(c(x935))) a(a(b(x935))) -> a(c(c(x935))) a(c(c(x935))) -> c(c(c(x935))) b(a(c(x936))) -> b(a(b(x936))) b(a(c(x936))) -> a(b(c(x936))) b(a(b(x936))) -> c(a(b(x936))) c(a(b(x936))) -> c(c(c(x936))) a(b(c(x936))) -> c(c(c(x936))) b(a(b(x936))) -> c(a(b(x936))) c(a(b(x936))) -> c(c(c(x936))) a(b(c(x936))) -> a(c(c(x936))) a(c(c(x936))) -> c(c(c(x936))) b(a(b(x936))) -> b(c(c(x936))) b(c(c(x936))) -> c(c(c(x936))) a(b(c(x936))) -> c(c(c(x936))) b(a(b(x936))) -> b(c(c(x936))) b(c(c(x936))) -> c(c(c(x936))) a(b(c(x936))) -> a(c(c(x936))) a(c(c(x936))) -> c(c(c(x936))) b(a(b(x936))) -> c(c(b(x936))) c(c(b(x936))) -> c(c(c(x936))) a(b(c(x936))) -> c(c(c(x936))) b(a(b(x936))) -> c(c(b(x936))) c(c(b(x936))) -> c(c(c(x936))) a(b(c(x936))) -> a(c(c(x936))) a(c(c(x936))) -> c(c(c(x936))) c(a(c(x937))) -> c(a(b(x937))) c(a(c(x937))) -> c(c(c(x937))) c(a(b(x937))) -> c(c(c(x937))) a(a(c(x938))) -> a(a(b(x938))) a(a(c(x938))) -> a(b(c(x938))) a(a(b(x938))) -> a(c(c(x938))) a(b(c(x938))) -> a(c(c(x938))) b(a(c(x939))) -> b(a(b(x939))) b(a(c(x939))) -> c(a(c(x939))) b(a(b(x939))) -> c(a(b(x939))) c(a(c(x939))) -> c(a(b(x939))) a(c(x)) -> a(b(x)) a(c(x)) -> c(a(x)) c(a(x)) -> a(b(x)) a(b(x)) -> c(c(x)) c(a(x)) -> c(c(x)) c(a(c(x941))) -> c(a(b(x941))) c(a(c(x941))) -> a(b(c(x941))) c(a(b(x941))) -> c(c(c(x941))) a(b(c(x941))) -> c(c(c(x941))) b(a(c(x942))) -> b(a(b(x942))) b(a(c(x942))) -> c(c(c(x942))) b(a(b(x942))) -> c(a(b(x942))) c(a(b(x942))) -> c(c(c(x942))) b(a(b(x942))) -> b(c(c(x942))) b(c(c(x942))) -> c(c(c(x942))) b(a(b(x942))) -> c(c(b(x942))) c(c(b(x942))) -> c(c(c(x942))) a(c(x)) -> a(b(x)) a(c(x)) -> c(c(x)) a(b(x)) -> c(c(x)) a(c(a(x944))) -> a(c(c(x944))) a(c(a(x944))) -> a(b(a(x944))) a(b(a(x944))) -> a(c(c(x944))) b(c(a(x945))) -> b(c(c(x945))) b(c(a(x945))) -> c(c(a(x945))) b(c(c(x945))) -> c(c(c(x945))) c(c(a(x945))) -> c(c(c(x945))) a(c(a(x946))) -> a(c(c(x946))) a(c(a(x946))) -> c(a(a(x946))) a(c(c(x946))) -> c(c(c(x946))) c(a(a(x946))) -> c(c(c(x946))) c(a(x)) -> c(c(x)) c(a(x)) -> a(b(x)) a(b(x)) -> c(c(x)) a(c(a(x948))) -> a(c(c(x948))) a(c(a(x948))) -> c(c(a(x948))) a(c(c(x948))) -> c(c(c(x948))) c(c(a(x948))) -> c(c(c(x948))) c(b(c(x949))) -> c(c(c(x949))) c(b(c(x949))) -> a(b(c(x949))) a(b(c(x949))) -> c(c(c(x949))) c(b(c(x950))) -> c(c(c(x950))) c(b(c(x950))) -> c(a(c(x950))) c(a(c(x950))) -> c(c(c(x950))) a(b(c(x951))) -> a(c(c(x951))) a(b(c(x951))) -> c(c(c(x951))) a(c(c(x951))) -> c(c(c(x951))) c(b(c(x952))) -> c(c(c(x952))) c(b(c(x952))) -> c(c(c(x952))) a(a(x)) -> a(b(x)) a(a(x)) -> c(c(x)) a(b(x)) -> c(c(x)) a(a(a(x954))) -> a(a(b(x954))) a(a(a(x954))) -> c(c(a(x954))) a(a(b(x954))) -> c(c(b(x954))) c(c(a(x954))) -> c(a(b(x954))) c(a(b(x954))) -> c(c(b(x954))) a(a(b(x954))) -> a(b(b(x954))) a(b(b(x954))) -> c(c(b(x954))) c(c(a(x954))) -> c(a(b(x954))) c(a(b(x954))) -> c(c(b(x954))) a(a(b(x954))) -> a(b(b(x954))) c(c(a(x954))) -> c(a(b(x954))) c(a(b(x954))) -> a(b(b(x954))) a(a(b(x954))) -> c(c(b(x954))) c(c(b(x954))) -> c(a(b(x954))) c(c(a(x954))) -> c(a(b(x954))) a(a(b(x954))) -> c(c(b(x954))) c(c(b(x954))) -> c(c(a(x954))) a(a(b(x954))) -> c(c(b(x954))) c(c(b(x954))) -> c(c(c(x954))) c(c(a(x954))) -> c(c(c(x954))) a(a(b(x954))) -> c(c(b(x954))) c(c(b(x954))) -> c(c(c(x954))) c(c(a(x954))) -> c(a(b(x954))) c(a(b(x954))) -> c(c(c(x954))) a(a(b(x954))) -> a(c(c(x954))) a(c(c(x954))) -> c(c(c(x954))) c(c(a(x954))) -> c(c(c(x954))) a(a(b(x954))) -> a(c(c(x954))) a(c(c(x954))) -> c(c(c(x954))) c(c(a(x954))) -> c(a(b(x954))) c(a(b(x954))) -> c(c(c(x954))) b(a(a(x955))) -> b(a(b(x955))) b(a(a(x955))) -> a(b(a(x955))) b(a(b(x955))) -> a(b(b(x955))) a(b(a(x955))) -> a(a(b(x955))) a(a(b(x955))) -> a(b(b(x955))) b(a(b(x955))) -> c(a(b(x955))) c(a(b(x955))) -> a(b(b(x955))) a(b(a(x955))) -> a(a(b(x955))) a(a(b(x955))) -> a(b(b(x955))) b(a(b(x955))) -> c(a(b(x955))) a(b(a(x955))) -> c(c(a(x955))) c(c(a(x955))) -> c(a(b(x955))) b(a(b(x955))) -> c(c(b(x955))) c(c(b(x955))) -> c(a(b(x955))) a(b(a(x955))) -> c(c(a(x955))) c(c(a(x955))) -> c(a(b(x955))) b(a(b(x955))) -> c(c(b(x955))) a(b(a(x955))) -> a(a(b(x955))) a(a(b(x955))) -> c(c(b(x955))) b(a(b(x955))) -> a(b(b(x955))) a(b(b(x955))) -> c(c(b(x955))) a(b(a(x955))) -> a(a(b(x955))) a(a(b(x955))) -> c(c(b(x955))) b(a(b(x955))) -> c(a(b(x955))) c(a(b(x955))) -> c(c(b(x955))) a(b(a(x955))) -> a(a(b(x955))) a(a(b(x955))) -> c(c(b(x955))) b(a(b(x955))) -> c(a(b(x955))) c(a(b(x955))) -> c(c(c(x955))) a(b(a(x955))) -> c(c(a(x955))) c(c(a(x955))) -> c(c(c(x955))) b(a(b(x955))) -> c(a(b(x955))) c(a(b(x955))) -> c(c(c(x955))) a(b(a(x955))) -> a(c(c(x955))) a(c(c(x955))) -> c(c(c(x955))) b(a(b(x955))) -> b(c(c(x955))) b(c(c(x955))) -> c(c(c(x955))) a(b(a(x955))) -> c(c(a(x955))) c(c(a(x955))) -> c(c(c(x955))) b(a(b(x955))) -> b(c(c(x955))) b(c(c(x955))) -> c(c(c(x955))) a(b(a(x955))) -> a(c(c(x955))) a(c(c(x955))) -> c(c(c(x955))) b(a(b(x955))) -> c(c(b(x955))) c(c(b(x955))) -> c(c(c(x955))) a(b(a(x955))) -> c(c(a(x955))) c(c(a(x955))) -> c(c(c(x955))) b(a(b(x955))) -> c(c(b(x955))) c(c(b(x955))) -> c(c(c(x955))) a(b(a(x955))) -> a(c(c(x955))) a(c(c(x955))) -> c(c(c(x955))) b(a(b(x955))) -> c(c(b(x955))) c(c(b(x955))) -> c(c(a(x955))) a(b(a(x955))) -> c(c(a(x955))) b(a(b(x955))) -> c(c(b(x955))) c(c(b(x955))) -> c(c(a(x955))) a(b(a(x955))) -> a(c(a(x955))) a(c(a(x955))) -> c(c(a(x955))) c(a(a(x956))) -> c(a(b(x956))) c(a(a(x956))) -> c(c(a(x956))) c(c(a(x956))) -> c(a(b(x956))) c(a(b(x956))) -> c(c(c(x956))) c(c(a(x956))) -> c(c(c(x956))) a(a(a(x957))) -> a(a(b(x957))) a(a(a(x957))) -> a(b(a(x957))) a(b(a(x957))) -> a(a(b(x957))) a(a(b(x957))) -> a(c(c(x957))) a(b(a(x957))) -> a(c(c(x957))) b(a(a(x958))) -> b(a(b(x958))) b(a(a(x958))) -> c(a(a(x958))) b(a(b(x958))) -> c(a(b(x958))) c(a(a(x958))) -> c(a(b(x958))) c(a(a(x959))) -> c(a(b(x959))) c(a(a(x959))) -> a(b(a(x959))) a(b(a(x959))) -> c(c(a(x959))) c(c(a(x959))) -> c(a(b(x959))) c(a(b(x959))) -> c(c(b(x959))) a(b(a(x959))) -> a(a(b(x959))) a(a(b(x959))) -> c(c(b(x959))) c(a(b(x959))) -> a(b(b(x959))) a(b(b(x959))) -> c(c(b(x959))) a(b(a(x959))) -> a(a(b(x959))) a(a(b(x959))) -> c(c(b(x959))) c(a(b(x959))) -> a(b(b(x959))) a(b(a(x959))) -> a(a(b(x959))) a(a(b(x959))) -> a(b(b(x959))) c(a(b(x959))) -> c(c(c(x959))) a(b(a(x959))) -> c(c(a(x959))) c(c(a(x959))) -> c(c(c(x959))) c(a(b(x959))) -> c(c(c(x959))) a(b(a(x959))) -> a(c(c(x959))) a(c(c(x959))) -> c(c(c(x959))) c(a(b(x959))) -> c(c(b(x959))) c(c(b(x959))) -> c(c(c(x959))) a(b(a(x959))) -> c(c(a(x959))) c(c(a(x959))) -> c(c(c(x959))) c(a(b(x959))) -> c(c(b(x959))) c(c(b(x959))) -> c(c(c(x959))) a(b(a(x959))) -> a(c(c(x959))) a(c(c(x959))) -> c(c(c(x959))) c(a(b(x959))) -> c(c(b(x959))) c(c(b(x959))) -> c(c(a(x959))) a(b(a(x959))) -> c(c(a(x959))) c(a(b(x959))) -> c(c(b(x959))) c(c(b(x959))) -> c(c(a(x959))) a(b(a(x959))) -> a(c(a(x959))) a(c(a(x959))) -> c(c(a(x959))) b(a(a(x960))) -> b(a(b(x960))) b(a(a(x960))) -> c(c(a(x960))) b(a(b(x960))) -> c(a(b(x960))) c(c(a(x960))) -> c(a(b(x960))) c(b(x)) -> c(a(x)) c(b(x)) -> a(b(x)) c(a(x)) -> c(c(x)) a(b(x)) -> c(c(x)) c(a(x)) -> a(b(x)) a(c(b(x962))) -> a(c(a(x962))) a(c(b(x962))) -> a(b(b(x962))) a(c(a(x962))) -> c(c(a(x962))) a(b(b(x962))) -> c(c(b(x962))) c(c(b(x962))) -> c(c(a(x962))) a(c(a(x962))) -> a(b(a(x962))) a(b(a(x962))) -> c(c(a(x962))) a(b(b(x962))) -> c(c(b(x962))) c(c(b(x962))) -> c(c(a(x962))) a(c(a(x962))) -> c(a(a(x962))) c(a(a(x962))) -> c(c(a(x962))) a(b(b(x962))) -> c(c(b(x962))) c(c(b(x962))) -> c(c(a(x962))) a(c(a(x962))) -> a(c(c(x962))) a(c(c(x962))) -> c(c(c(x962))) a(b(b(x962))) -> c(c(b(x962))) c(c(b(x962))) -> c(c(c(x962))) a(c(a(x962))) -> c(a(a(x962))) c(a(a(x962))) -> c(c(c(x962))) a(b(b(x962))) -> c(c(b(x962))) c(c(b(x962))) -> c(c(c(x962))) a(c(a(x962))) -> c(c(a(x962))) c(c(a(x962))) -> c(c(c(x962))) a(b(b(x962))) -> c(c(b(x962))) c(c(b(x962))) -> c(c(c(x962))) a(c(a(x962))) -> c(a(a(x962))) c(a(a(x962))) -> c(a(b(x962))) a(b(b(x962))) -> c(c(b(x962))) c(c(b(x962))) -> c(a(b(x962))) a(c(a(x962))) -> c(c(a(x962))) c(c(a(x962))) -> c(a(b(x962))) a(b(b(x962))) -> c(c(b(x962))) c(c(b(x962))) -> c(a(b(x962))) a(c(a(x962))) -> a(a(b(x962))) a(a(b(x962))) -> c(c(b(x962))) a(b(b(x962))) -> c(c(b(x962))) a(c(a(x962))) -> a(a(b(x962))) a(a(b(x962))) -> a(b(b(x962))) b(c(b(x963))) -> b(c(a(x963))) b(c(b(x963))) -> c(c(b(x963))) b(c(a(x963))) -> c(c(a(x963))) c(c(b(x963))) -> c(c(a(x963))) a(c(b(x964))) -> a(c(a(x964))) a(c(b(x964))) -> c(a(b(x964))) a(c(a(x964))) -> c(c(a(x964))) c(a(b(x964))) -> c(c(b(x964))) c(c(b(x964))) -> c(c(a(x964))) a(c(a(x964))) -> a(b(a(x964))) a(b(a(x964))) -> c(c(a(x964))) c(a(b(x964))) -> c(c(b(x964))) c(c(b(x964))) -> c(c(a(x964))) a(c(a(x964))) -> c(a(a(x964))) c(a(a(x964))) -> c(c(a(x964))) c(a(b(x964))) -> c(c(b(x964))) c(c(b(x964))) -> c(c(a(x964))) a(c(a(x964))) -> a(c(c(x964))) a(c(c(x964))) -> c(c(c(x964))) c(a(b(x964))) -> c(c(c(x964))) a(c(a(x964))) -> a(c(c(x964))) a(c(c(x964))) -> c(c(c(x964))) c(a(b(x964))) -> c(c(b(x964))) c(c(b(x964))) -> c(c(c(x964))) a(c(a(x964))) -> c(a(a(x964))) c(a(a(x964))) -> c(c(c(x964))) c(a(b(x964))) -> c(c(c(x964))) a(c(a(x964))) -> c(a(a(x964))) c(a(a(x964))) -> c(c(c(x964))) c(a(b(x964))) -> c(c(b(x964))) c(c(b(x964))) -> c(c(c(x964))) a(c(a(x964))) -> c(c(a(x964))) c(c(a(x964))) -> c(c(c(x964))) c(a(b(x964))) -> c(c(c(x964))) a(c(a(x964))) -> c(c(a(x964))) c(c(a(x964))) -> c(c(c(x964))) c(a(b(x964))) -> c(c(b(x964))) c(c(b(x964))) -> c(c(c(x964))) a(c(a(x964))) -> c(a(a(x964))) c(a(a(x964))) -> c(a(b(x964))) a(c(a(x964))) -> c(c(a(x964))) c(c(a(x964))) -> c(a(b(x964))) a(c(a(x964))) -> a(a(b(x964))) a(a(b(x964))) -> c(c(b(x964))) c(a(b(x964))) -> c(c(b(x964))) a(c(a(x964))) -> a(a(b(x964))) a(a(b(x964))) -> c(c(b(x964))) c(a(b(x964))) -> a(b(b(x964))) a(b(b(x964))) -> c(c(b(x964))) a(c(a(x964))) -> a(a(b(x964))) a(a(b(x964))) -> a(b(b(x964))) c(a(b(x964))) -> a(b(b(x964))) c(b(x)) -> c(a(x)) c(b(x)) -> c(c(x)) c(a(x)) -> c(c(x)) a(c(b(x966))) -> a(c(a(x966))) a(c(b(x966))) -> c(c(b(x966))) a(c(a(x966))) -> c(c(a(x966))) c(c(b(x966))) -> c(c(a(x966))) c(b(a(x967))) -> c(c(a(x967))) c(b(a(x967))) -> a(b(a(x967))) a(b(a(x967))) -> c(c(a(x967))) b(a(x)) -> c(a(x)) b(a(x)) -> a(b(x)) c(a(x)) -> c(c(x)) a(b(x)) -> c(c(x)) c(a(x)) -> a(b(x)) c(b(a(x969))) -> c(c(a(x969))) c(b(a(x969))) -> c(a(a(x969))) c(a(a(x969))) -> c(c(a(x969))) c(c(a(x969))) -> c(c(c(x969))) c(a(a(x969))) -> c(c(c(x969))) c(c(a(x969))) -> c(a(b(x969))) c(a(a(x969))) -> c(a(b(x969))) a(b(a(x970))) -> a(c(a(x970))) a(b(a(x970))) -> c(c(a(x970))) a(c(a(x970))) -> c(c(a(x970))) c(b(a(x971))) -> c(c(a(x971))) c(b(a(x971))) -> c(c(a(x971))) b(a(x)) -> c(a(x)) b(a(x)) -> c(c(x)) c(a(x)) -> c(c(x)) a(a(c(x973))) -> a(c(a(x973))) a(a(c(x973))) -> c(c(c(x973))) a(c(a(x973))) -> a(c(c(x973))) a(c(c(x973))) -> c(c(c(x973))) a(c(a(x973))) -> c(a(a(x973))) c(a(a(x973))) -> c(c(c(x973))) a(c(a(x973))) -> c(c(a(x973))) c(c(a(x973))) -> c(c(c(x973))) b(a(c(x974))) -> b(c(a(x974))) b(a(c(x974))) -> a(b(c(x974))) b(c(a(x974))) -> b(c(c(x974))) b(c(c(x974))) -> c(c(c(x974))) a(b(c(x974))) -> c(c(c(x974))) b(c(a(x974))) -> b(c(c(x974))) b(c(c(x974))) -> c(c(c(x974))) a(b(c(x974))) -> a(c(c(x974))) a(c(c(x974))) -> c(c(c(x974))) b(c(a(x974))) -> c(c(a(x974))) c(c(a(x974))) -> c(c(c(x974))) a(b(c(x974))) -> c(c(c(x974))) b(c(a(x974))) -> c(c(a(x974))) c(c(a(x974))) -> c(c(c(x974))) a(b(c(x974))) -> a(c(c(x974))) a(c(c(x974))) -> c(c(c(x974))) a(c(x)) -> c(a(x)) a(c(x)) -> a(b(x)) c(a(x)) -> c(c(x)) a(b(x)) -> c(c(x)) c(a(x)) -> a(b(x)) c(a(c(x976))) -> c(c(a(x976))) c(a(c(x976))) -> c(c(c(x976))) c(c(a(x976))) -> c(c(c(x976))) a(a(c(x977))) -> a(c(a(x977))) a(a(c(x977))) -> a(b(c(x977))) a(c(a(x977))) -> a(c(c(x977))) a(b(c(x977))) -> a(c(c(x977))) b(a(c(x978))) -> b(c(a(x978))) b(a(c(x978))) -> c(a(c(x978))) b(c(a(x978))) -> c(c(a(x978))) c(a(c(x978))) -> c(c(a(x978))) c(a(c(x979))) -> c(c(a(x979))) c(a(c(x979))) -> a(b(c(x979))) c(c(a(x979))) -> c(c(c(x979))) a(b(c(x979))) -> c(c(c(x979))) b(a(c(x980))) -> b(c(a(x980))) b(a(c(x980))) -> c(c(c(x980))) b(c(a(x980))) -> b(c(c(x980))) b(c(c(x980))) -> c(c(c(x980))) b(c(a(x980))) -> c(c(a(x980))) c(c(a(x980))) -> c(c(c(x980))) a(c(x)) -> c(a(x)) a(c(x)) -> c(c(x)) c(a(x)) -> c(c(x)) a(c(a(x982))) -> a(a(b(x982))) a(c(a(x982))) -> a(b(a(x982))) a(b(a(x982))) -> a(a(b(x982))) a(a(b(x982))) -> a(c(c(x982))) a(b(a(x982))) -> a(c(c(x982))) c(a(x)) -> a(b(x)) c(a(x)) -> c(c(x)) a(b(x)) -> c(c(x)) b(c(a(x984))) -> b(a(b(x984))) b(c(a(x984))) -> c(c(a(x984))) b(a(b(x984))) -> c(a(b(x984))) c(c(a(x984))) -> c(a(b(x984))) a(c(a(x985))) -> a(a(b(x985))) a(c(a(x985))) -> c(a(a(x985))) c(a(a(x985))) -> a(b(a(x985))) a(b(a(x985))) -> a(a(b(x985))) a(a(b(x985))) -> c(c(b(x985))) c(a(a(x985))) -> c(a(b(x985))) c(a(b(x985))) -> c(c(b(x985))) a(a(b(x985))) -> a(b(b(x985))) a(b(b(x985))) -> c(c(b(x985))) c(a(a(x985))) -> c(a(b(x985))) c(a(b(x985))) -> c(c(b(x985))) a(a(b(x985))) -> a(b(b(x985))) c(a(a(x985))) -> c(a(b(x985))) c(a(b(x985))) -> a(b(b(x985))) a(a(b(x985))) -> a(c(c(x985))) c(a(a(x985))) -> a(b(a(x985))) a(b(a(x985))) -> a(c(c(x985))) a(a(b(x985))) -> c(c(b(x985))) c(c(b(x985))) -> c(a(b(x985))) c(a(a(x985))) -> c(a(b(x985))) a(a(b(x985))) -> c(c(b(x985))) c(c(b(x985))) -> c(a(b(x985))) c(a(a(x985))) -> c(c(a(x985))) c(c(a(x985))) -> c(a(b(x985))) a(a(b(x985))) -> c(c(b(x985))) c(c(b(x985))) -> c(c(a(x985))) c(a(a(x985))) -> c(c(a(x985))) a(a(b(x985))) -> c(c(b(x985))) c(c(b(x985))) -> c(c(a(x985))) c(a(a(x985))) -> a(b(a(x985))) a(b(a(x985))) -> c(c(a(x985))) a(a(b(x985))) -> c(c(b(x985))) c(c(b(x985))) -> c(c(c(x985))) c(a(a(x985))) -> c(c(c(x985))) a(a(b(x985))) -> c(c(b(x985))) c(c(b(x985))) -> c(c(c(x985))) c(a(a(x985))) -> c(c(a(x985))) c(c(a(x985))) -> c(c(c(x985))) a(a(b(x985))) -> c(c(b(x985))) c(c(b(x985))) -> c(c(c(x985))) c(a(a(x985))) -> c(a(b(x985))) c(a(b(x985))) -> c(c(c(x985))) a(a(b(x985))) -> a(c(c(x985))) a(c(c(x985))) -> c(c(c(x985))) c(a(a(x985))) -> c(c(c(x985))) a(a(b(x985))) -> a(c(c(x985))) a(c(c(x985))) -> c(c(c(x985))) c(a(a(x985))) -> c(c(a(x985))) c(c(a(x985))) -> c(c(c(x985))) a(a(b(x985))) -> a(c(c(x985))) a(c(c(x985))) -> c(c(c(x985))) c(a(a(x985))) -> c(a(b(x985))) c(a(b(x985))) -> c(c(c(x985))) a(c(a(x986))) -> a(a(b(x986))) a(c(a(x986))) -> c(c(a(x986))) a(a(b(x986))) -> c(c(b(x986))) c(c(a(x986))) -> c(a(b(x986))) c(a(b(x986))) -> c(c(b(x986))) a(a(b(x986))) -> a(b(b(x986))) a(b(b(x986))) -> c(c(b(x986))) c(c(a(x986))) -> c(a(b(x986))) c(a(b(x986))) -> c(c(b(x986))) a(a(b(x986))) -> a(b(b(x986))) c(c(a(x986))) -> c(a(b(x986))) c(a(b(x986))) -> a(b(b(x986))) a(a(b(x986))) -> c(c(b(x986))) c(c(b(x986))) -> c(a(b(x986))) c(c(a(x986))) -> c(a(b(x986))) a(a(b(x986))) -> c(c(b(x986))) c(c(b(x986))) -> c(c(a(x986))) a(a(b(x986))) -> c(c(b(x986))) c(c(b(x986))) -> c(c(c(x986))) c(c(a(x986))) -> c(c(c(x986))) a(a(b(x986))) -> c(c(b(x986))) c(c(b(x986))) -> c(c(c(x986))) c(c(a(x986))) -> c(a(b(x986))) c(a(b(x986))) -> c(c(c(x986))) a(a(b(x986))) -> a(c(c(x986))) a(c(c(x986))) -> c(c(c(x986))) c(c(a(x986))) -> c(c(c(x986))) a(a(b(x986))) -> a(c(c(x986))) a(c(c(x986))) -> c(c(c(x986))) c(c(a(x986))) -> c(a(b(x986))) c(a(b(x986))) -> c(c(c(x986))) a(a(b(x987))) -> a(c(c(x987))) a(a(b(x987))) -> c(c(b(x987))) a(c(c(x987))) -> c(c(c(x987))) c(c(b(x987))) -> c(c(c(x987))) b(a(b(x988))) -> b(c(c(x988))) b(a(b(x988))) -> a(b(b(x988))) b(c(c(x988))) -> c(c(c(x988))) a(b(b(x988))) -> c(c(b(x988))) c(c(b(x988))) -> c(c(c(x988))) c(a(b(x989))) -> c(c(c(x989))) c(a(b(x989))) -> c(c(b(x989))) c(c(b(x989))) -> c(c(c(x989))) a(a(b(x990))) -> a(c(c(x990))) a(a(b(x990))) -> a(b(b(x990))) a(c(c(x990))) -> c(c(c(x990))) a(b(b(x990))) -> c(c(b(x990))) c(c(b(x990))) -> c(c(c(x990))) a(c(c(x990))) -> a(b(c(x990))) a(b(c(x990))) -> c(c(c(x990))) a(b(b(x990))) -> c(c(b(x990))) c(c(b(x990))) -> c(c(c(x990))) a(c(c(x990))) -> c(a(c(x990))) c(a(c(x990))) -> c(c(c(x990))) a(b(b(x990))) -> c(c(b(x990))) c(c(b(x990))) -> c(c(c(x990))) a(c(c(x990))) -> c(a(c(x990))) c(a(c(x990))) -> c(a(b(x990))) a(b(b(x990))) -> c(c(b(x990))) c(c(b(x990))) -> c(a(b(x990))) a(c(c(x990))) -> c(a(c(x990))) c(a(c(x990))) -> c(c(a(x990))) a(b(b(x990))) -> c(c(b(x990))) c(c(b(x990))) -> c(c(a(x990))) b(a(b(x991))) -> b(c(c(x991))) b(a(b(x991))) -> c(a(b(x991))) b(c(c(x991))) -> c(c(c(x991))) c(a(b(x991))) -> c(c(c(x991))) c(a(b(x992))) -> c(c(c(x992))) c(a(b(x992))) -> a(b(b(x992))) a(b(b(x992))) -> c(c(b(x992))) c(c(b(x992))) -> c(c(c(x992))) b(a(b(x993))) -> b(c(c(x993))) b(a(b(x993))) -> c(c(b(x993))) b(c(c(x993))) -> c(c(c(x993))) c(c(b(x993))) -> c(c(c(x993))) c(b(x)) -> c(c(x)) c(b(x)) -> a(b(x)) a(b(x)) -> c(c(x)) a(c(b(x995))) -> a(c(c(x995))) a(c(b(x995))) -> a(b(b(x995))) a(c(c(x995))) -> c(c(c(x995))) a(b(b(x995))) -> c(c(b(x995))) c(c(b(x995))) -> c(c(c(x995))) a(c(c(x995))) -> a(b(c(x995))) a(b(c(x995))) -> c(c(c(x995))) a(b(b(x995))) -> c(c(b(x995))) c(c(b(x995))) -> c(c(c(x995))) a(c(c(x995))) -> c(a(c(x995))) c(a(c(x995))) -> c(c(c(x995))) a(b(b(x995))) -> c(c(b(x995))) c(c(b(x995))) -> c(c(c(x995))) a(c(c(x995))) -> c(a(c(x995))) c(a(c(x995))) -> c(a(b(x995))) a(b(b(x995))) -> c(c(b(x995))) c(c(b(x995))) -> c(a(b(x995))) a(c(c(x995))) -> c(a(c(x995))) c(a(c(x995))) -> c(c(a(x995))) a(b(b(x995))) -> c(c(b(x995))) c(c(b(x995))) -> c(c(a(x995))) b(c(b(x996))) -> b(c(c(x996))) b(c(b(x996))) -> c(c(b(x996))) b(c(c(x996))) -> c(c(c(x996))) c(c(b(x996))) -> c(c(c(x996))) c(b(x)) -> c(c(x)) c(b(x)) -> c(a(x)) c(a(x)) -> c(c(x)) a(c(b(x998))) -> a(c(c(x998))) a(c(b(x998))) -> c(a(b(x998))) a(c(c(x998))) -> c(c(c(x998))) c(a(b(x998))) -> c(c(c(x998))) a(c(b(x999))) -> a(c(c(x999))) a(c(b(x999))) -> c(c(b(x999))) a(c(c(x999))) -> c(c(c(x999))) c(c(b(x999))) -> c(c(c(x999))) c(b(a(x1000))) -> c(c(c(x1000))) c(b(a(x1000))) -> a(b(a(x1000))) a(b(a(x1000))) -> c(c(a(x1000))) c(c(a(x1000))) -> c(c(c(x1000))) a(b(a(x1000))) -> a(c(c(x1000))) a(c(c(x1000))) -> c(c(c(x1000))) b(a(x)) -> c(c(x)) b(a(x)) -> a(b(x)) a(b(x)) -> c(c(x)) c(b(a(x1002))) -> c(c(c(x1002))) c(b(a(x1002))) -> c(a(a(x1002))) c(a(a(x1002))) -> c(c(c(x1002))) b(a(x)) -> c(c(x)) b(a(x)) -> c(a(x)) c(a(x)) -> c(c(x)) a(b(a(x1004))) -> a(c(c(x1004))) a(b(a(x1004))) -> c(c(a(x1004))) a(c(c(x1004))) -> c(c(c(x1004))) c(c(a(x1004))) -> c(c(c(x1004))) c(b(a(x1005))) -> c(c(c(x1005))) c(b(a(x1005))) -> c(c(a(x1005))) c(c(a(x1005))) -> c(c(c(x1005))) a(a(c(x1006))) -> a(c(c(x1006))) a(a(c(x1006))) -> c(c(c(x1006))) a(c(c(x1006))) -> c(c(c(x1006))) b(a(c(x1007))) -> b(c(c(x1007))) b(a(c(x1007))) -> a(b(c(x1007))) b(c(c(x1007))) -> c(c(c(x1007))) a(b(c(x1007))) -> c(c(c(x1007))) a(c(x)) -> c(c(x)) a(c(x)) -> a(b(x)) a(b(x)) -> c(c(x)) c(a(c(x1009))) -> c(c(c(x1009))) c(a(c(x1009))) -> c(c(c(x1009))) a(a(c(x1010))) -> a(c(c(x1010))) a(a(c(x1010))) -> a(b(c(x1010))) a(b(c(x1010))) -> a(c(c(x1010))) a(c(c(x1010))) -> a(b(c(x1010))) a(c(c(x1010))) -> c(c(c(x1010))) a(b(c(x1010))) -> c(c(c(x1010))) b(a(c(x1011))) -> b(c(c(x1011))) b(a(c(x1011))) -> c(a(c(x1011))) b(c(c(x1011))) -> c(c(c(x1011))) c(a(c(x1011))) -> c(c(c(x1011))) a(c(x)) -> c(c(x)) a(c(x)) -> c(a(x)) c(a(x)) -> c(c(x)) c(a(c(x1013))) -> c(c(c(x1013))) c(a(c(x1013))) -> a(b(c(x1013))) a(b(c(x1013))) -> c(c(c(x1013))) b(a(c(x1014))) -> b(c(c(x1014))) b(a(c(x1014))) -> c(c(c(x1014))) b(c(c(x1014))) -> c(c(c(x1014))) weak: a(a(x)) -> c(c(x)) c(b(x)) -> a(b(x)) b(a(x)) -> a(b(x)) a(c(x)) -> a(b(x)) c(a(x)) -> c(c(x)) b(c(x)) -> c(c(x)) a(a(x)) -> a(b(x)) c(b(x)) -> c(a(x)) b(a(x)) -> c(a(x)) a(c(x)) -> c(a(x)) c(a(x)) -> a(b(x)) a(b(x)) -> c(c(x)) c(b(x)) -> c(c(x)) b(a(x)) -> c(c(x)) a(c(x)) -> c(c(x)) Shift Processor (ldh) lab=left (force): strict: weak: Rule Labeling Processor: strict: weak: rule labeling (right): a(a(x)) -> c(c(x)): 5 c(b(x)) -> a(b(x)): 7 b(a(x)) -> a(b(x)): 9 a(c(x)) -> a(b(x)): 15 c(a(x)) -> c(c(x)): 0 b(c(x)) -> c(c(x)): 0 a(a(x)) -> a(b(x)): 12 c(b(x)) -> c(a(x)): 7 b(a(x)) -> c(a(x)): 1 a(c(x)) -> c(a(x)): 15 c(a(x)) -> a(b(x)): 9 a(b(x)) -> c(c(x)): 0 c(b(x)) -> c(c(x)): 0 b(a(x)) -> c(c(x)): 0 a(c(x)) -> c(c(x)): 0 Decreasing Processor: The following diagrams are decreasing: peak: a(c(c(x915))) <-0|0[==1,==5]- a(a(a(x915))) -0|[==1,==5]-> c(c(a(x915))) joins (1): a(c(c(x915))) -14|[==1,>>0]-> c(c(c(x915))) c(c(a(x915))) -4|0[==1,>>0]-> c(c(c(x915))) peak: b(c(c(x916))) <-0|0[==1,=>5]- b(a(a(x916))) -2|[==1,?=9]-> a(b(a(x916))) joins (1): b(c(c(x916))) -5|[==1,>>0]-> c(c(c(x916))) a(b(a(x916))) -11|[==1,>>0]-> c(c(a(x916))) -4|0[==1,>>0]-> c(c(c(x916))) peak: c(c(c(x917))) <-0|0[==1,=?5]- c(a(a(x917))) -4|[==1,>=0]-> c(c(a(x917))) joins (1): c(c(a(x917))) -4|0[==1,>=0]-> c(c(c(x917))) peak: c(c(x)) <-0|[==1,=>5]- a(a(x)) -6|[==1,?=12]-> a(b(x)) joins (1): a(b(x)) -11|[==1,>>0]-> c(c(x)) peak: a(c(c(x919))) <-0|0[==1,=>5]- a(a(a(x919))) -6|[==1,?=12]-> a(b(a(x919))) joins (1): a(b(a(x919))) -13|0[==1,>>0]-> a(c(c(x919))) peak: b(c(c(x920))) <-0|0[==1,=?5]- b(a(a(x920))) -8|[==1,>=1]-> c(a(a(x920))) joins (1): b(c(c(x920))) -5|[==1,>>0]-> c(c(c(x920))) c(a(a(x920))) -0|0[==1,=?5]-> c(c(c(x920))) peak: c(c(c(x921))) <-0|0[==1,=>5]- c(a(a(x921))) -10|[==1,?=9]-> a(b(a(x921))) joins (1): a(b(a(x921))) -11|[==1,>>0]-> c(c(a(x921))) -4|0[==1,>>0]-> c(c(c(x921))) peak: b(c(c(x922))) <-0|0[==1,=?5]- b(a(a(x922))) -13|[==1,>=0]-> c(c(a(x922))) joins (1): b(c(c(x922))) -5|[==1,>=0]-> c(c(c(x922))) c(c(a(x922))) -4|0[==1,>=0]-> c(c(c(x922))) peak: a(a(b(x923))) <-1|0[==1,=>7]- a(c(b(x923))) -3|[==1,?=15]-> a(b(b(x923))) joins (1): a(a(b(x923))) -6|[==1,?>12]-> a(b(b(x923))) peak: b(a(b(x924))) <-1|0[==1,=?7]- b(c(b(x924))) -5|[==1,>=0]-> c(c(b(x924))) joins (1): b(a(b(x924))) -13|[==1,>=0]-> c(c(b(x924))) peak: a(b(x)) <-1|[==1,==7]- c(b(x)) -7|[==1,==7]-> c(a(x)) joins (1): a(b(x)) -11|[==1,>>0]-> c(c(x)) c(a(x)) -4|[==1,>>0]-> c(c(x)) peak: a(a(b(x926))) <-1|0[==1,=>7]- a(c(b(x926))) -9|[==1,?=15]-> c(a(b(x926))) joins (1): a(a(b(x926))) -0|[==1,>>5]-> c(c(b(x926))) c(a(b(x926))) -4|[==1,>>0]-> c(c(b(x926))) peak: a(b(x)) <-1|[==1,=?7]- c(b(x)) -12|[==1,>=0]-> c(c(x)) joins (1): a(b(x)) -11|[==1,>=0]-> c(c(x)) peak: a(a(b(x928))) <-1|0[==1,=?7]- a(c(b(x928))) -14|[==1,>=0]-> c(c(b(x928))) joins (1): a(a(b(x928))) -0|[==1,>?5]-> c(c(b(x928))) peak: c(a(b(x929))) <-2|0[==1,=?9]- c(b(a(x929))) -1|[==1,>=7]-> a(b(a(x929))) joins (1): a(b(a(x929))) -11|[==1,>>0]-> c(c(a(x929))) -10|0[==1,=?9]-> c(a(b(x929))) peak: c(a(b(x930))) <-2|0[==1,=?9]- c(b(a(x930))) -7|[==1,>=7]-> c(a(a(x930))) joins (1): c(a(b(x930))) -11|0[==1,>>0]-> c(c(c(x930))) c(a(a(x930))) -0|0[==1,>>5]-> c(c(c(x930))) peak: a(b(x)) <-2|[==1,=?9]- b(a(x)) -8|[==1,>=1]-> c(a(x)) joins (1): c(a(x)) -10|[==1,=?9]-> a(b(x)) peak: a(a(b(x932))) <-2|0[==1,=?9]- a(b(a(x932))) -11|[==1,>=0]-> c(c(a(x932))) joins (1): a(a(b(x932))) -0|[==1,>?5]-> c(c(b(x932))) -7|0[==1,>?7]-> c(c(a(x932))) peak: c(a(b(x933))) <-2|0[==1,=?9]- c(b(a(x933))) -12|[==1,>=0]-> c(c(a(x933))) joins (1): c(c(a(x933))) -10|0[==1,=?9]-> c(a(b(x933))) peak: a(b(x)) <-2|[==1,=?9]- b(a(x)) -13|[==1,>=0]-> c(c(x)) joins (1): a(b(x)) -11|[==1,>=0]-> c(c(x)) peak: a(a(b(x935))) <-3|0[==1,=?15]- a(a(c(x935))) -0|[==1,>=5]-> c(c(c(x935))) joins (1): a(a(b(x935))) -0|[==1,>=5]-> c(c(b(x935))) -12|0[==1,>>0]-> c(c(c(x935))) peak: b(a(b(x936))) <-3|0[==1,=?15]- b(a(c(x936))) -2|[==1,>=9]-> a(b(c(x936))) joins (1): b(a(b(x936))) -8|[==1,>>1]-> c(a(b(x936))) -11|0[==1,>>0]-> c(c(c(x936))) a(b(c(x936))) -11|[==1,>>0]-> c(c(c(x936))) peak: c(a(b(x937))) <-3|0[==1,=?15]- c(a(c(x937))) -4|[==1,>=0]-> c(c(c(x937))) joins (1): c(a(b(x937))) -11|0[==1,>=0]-> c(c(c(x937))) peak: a(a(b(x938))) <-3|0[==1,=?15]- a(a(c(x938))) -6|[==1,>=12]-> a(b(c(x938))) joins (1): a(a(b(x938))) -11|0[==1,>>0]-> a(c(c(x938))) a(b(c(x938))) -5|0[==1,>>0]-> a(c(c(x938))) peak: b(a(b(x939))) <-3|0[==1,=?15]- b(a(c(x939))) -8|[==1,>=1]-> c(a(c(x939))) joins (1): b(a(b(x939))) -8|[==1,>=1]-> c(a(b(x939))) c(a(c(x939))) -3|0[==1,=?15]-> c(a(b(x939))) peak: a(b(x)) <-3|[==1,==15]- a(c(x)) -9|[==1,==15]-> c(a(x)) joins (1): c(a(x)) -10|[==1,>>9]-> a(b(x)) peak: c(a(b(x941))) <-3|0[==1,=?15]- c(a(c(x941))) -10|[==1,>=9]-> a(b(c(x941))) joins (1): c(a(b(x941))) -11|0[==1,>>0]-> c(c(c(x941))) a(b(c(x941))) -11|[==1,>>0]-> c(c(c(x941))) peak: b(a(b(x942))) <-3|0[==1,=?15]- b(a(c(x942))) -13|[==1,>=0]-> c(c(c(x942))) joins (1): b(a(b(x942))) -8|[==1,>?1]-> c(a(b(x942))) -11|0[==1,>=0]-> c(c(c(x942))) peak: a(b(x)) <-3|[==1,=?15]- a(c(x)) -14|[==1,>=0]-> c(c(x)) joins (1): a(b(x)) -11|[==1,>=0]-> c(c(x)) peak: a(c(c(x944))) <-4|0[==1,=>0]- a(c(a(x944))) -3|[==1,?=15]-> a(b(a(x944))) joins (1): a(b(a(x944))) -13|0[==1,=>0]-> a(c(c(x944))) peak: b(c(c(x945))) <-4|0[==1,==0]- b(c(a(x945))) -5|[==1,==0]-> c(c(a(x945))) joins (1): b(c(c(x945))) -5|[==1,==0]-> c(c(c(x945))) c(c(a(x945))) -4|0[==1,==0]-> c(c(c(x945))) peak: a(c(c(x946))) <-4|0[==1,=>0]- a(c(a(x946))) -9|[==1,?=15]-> c(a(a(x946))) joins (1): a(c(c(x946))) -14|[==1,=>0]-> c(c(c(x946))) c(a(a(x946))) -0|0[==1,?>5]-> c(c(c(x946))) peak: c(c(x)) <-4|[==1,=>0]- c(a(x)) -10|[==1,?=9]-> a(b(x)) joins (1): a(b(x)) -11|[==1,=>0]-> c(c(x)) peak: a(c(c(x948))) <-4|0[==1,==0]- a(c(a(x948))) -14|[==1,==0]-> c(c(a(x948))) joins (1): a(c(c(x948))) -14|[==1,==0]-> c(c(c(x948))) c(c(a(x948))) -4|0[==1,==0]-> c(c(c(x948))) peak: c(c(c(x949))) <-5|0[==1,=>0]- c(b(c(x949))) -1|[==1,?=7]-> a(b(c(x949))) joins (1): a(b(c(x949))) -11|[==1,=>0]-> c(c(c(x949))) peak: c(c(c(x950))) <-5|0[==1,=>0]- c(b(c(x950))) -7|[==1,?=7]-> c(a(c(x950))) joins (1): c(a(c(x950))) -4|[==1,=>0]-> c(c(c(x950))) peak: a(c(c(x951))) <-5|0[==1,==0]- a(b(c(x951))) -11|[==1,==0]-> c(c(c(x951))) joins (1): a(c(c(x951))) -14|[==1,==0]-> c(c(c(x951))) peak: c(c(c(x952))) <-5|0[==1,==0]- c(b(c(x952))) -12|[==1,==0]-> c(c(c(x952))) joins (1): peak: a(b(x)) <-6|[==1,=?12]- a(a(x)) -0|[==1,>=5]-> c(c(x)) joins (1): a(b(x)) -11|[==1,>>0]-> c(c(x)) peak: a(a(b(x954))) <-6|0[==1,=?12]- a(a(a(x954))) -0|[==1,>=5]-> c(c(a(x954))) joins (1): a(a(b(x954))) -0|[==1,>=5]-> c(c(b(x954))) -7|0[==1,>?7]-> c(c(a(x954))) peak: b(a(b(x955))) <-6|0[==1,=?12]- b(a(a(x955))) -2|[==1,>=9]-> a(b(a(x955))) joins (1): b(a(b(x955))) -8|[==1,>>1]-> c(a(b(x955))) a(b(a(x955))) -11|[==1,>>0]-> c(c(a(x955))) -10|0[==1,>=9]-> c(a(b(x955))) peak: c(a(b(x956))) <-6|0[==1,=?12]- c(a(a(x956))) -4|[==1,>=0]-> c(c(a(x956))) joins (1): c(c(a(x956))) -10|0[==1,>?9]-> c(a(b(x956))) peak: a(a(b(x957))) <-6|0[==1,==12]- a(a(a(x957))) -6|[==1,==12]-> a(b(a(x957))) joins (1): a(b(a(x957))) -2|0[==1,>>9]-> a(a(b(x957))) peak: b(a(b(x958))) <-6|0[==1,=?12]- b(a(a(x958))) -8|[==1,>=1]-> c(a(a(x958))) joins (1): b(a(b(x958))) -8|[==1,>=1]-> c(a(b(x958))) c(a(a(x958))) -6|0[==1,=?12]-> c(a(b(x958))) peak: c(a(b(x959))) <-6|0[==1,=?12]- c(a(a(x959))) -10|[==1,>=9]-> a(b(a(x959))) joins (1): a(b(a(x959))) -11|[==1,>>0]-> c(c(a(x959))) -10|0[==1,>=9]-> c(a(b(x959))) peak: b(a(b(x960))) <-6|0[==1,=?12]- b(a(a(x960))) -13|[==1,>=0]-> c(c(a(x960))) joins (1): b(a(b(x960))) -8|[==1,>?1]-> c(a(b(x960))) c(c(a(x960))) -10|0[==1,>?9]-> c(a(b(x960))) peak: c(a(x)) <-7|[==1,==7]- c(b(x)) -1|[==1,==7]-> a(b(x)) joins (1): c(a(x)) -4|[==1,>>0]-> c(c(x)) a(b(x)) -11|[==1,>>0]-> c(c(x)) peak: a(c(a(x962))) <-7|0[==1,=>7]- a(c(b(x962))) -3|[==1,?=15]-> a(b(b(x962))) joins (1): a(c(a(x962))) -10|0[==1,?>9]-> a(a(b(x962))) -6|[==1,?>12]-> a(b(b(x962))) peak: b(c(a(x963))) <-7|0[==1,=?7]- b(c(b(x963))) -5|[==1,>=0]-> c(c(b(x963))) joins (1): b(c(a(x963))) -5|[==1,>=0]-> c(c(a(x963))) c(c(b(x963))) -7|0[==1,=?7]-> c(c(a(x963))) peak: a(c(a(x964))) <-7|0[==1,=>7]- a(c(b(x964))) -9|[==1,?=15]-> c(a(b(x964))) joins (1): a(c(a(x964))) -9|[==1,?=15]-> c(a(a(x964))) -6|0[==1,?>12]-> c(a(b(x964))) peak: c(a(x)) <-7|[==1,=?7]- c(b(x)) -12|[==1,>=0]-> c(c(x)) joins (1): c(a(x)) -4|[==1,>=0]-> c(c(x)) peak: a(c(a(x966))) <-7|0[==1,=?7]- a(c(b(x966))) -14|[==1,>=0]-> c(c(b(x966))) joins (1): a(c(a(x966))) -14|[==1,>=0]-> c(c(a(x966))) c(c(b(x966))) -7|0[==1,=?7]-> c(c(a(x966))) peak: c(c(a(x967))) <-8|0[==1,=>1]- c(b(a(x967))) -1|[==1,?=7]-> a(b(a(x967))) joins (1): a(b(a(x967))) -11|[==1,>>0]-> c(c(a(x967))) peak: c(a(x)) <-8|[==1,=>1]- b(a(x)) -2|[==1,?=9]-> a(b(x)) joins (1): c(a(x)) -10|[==1,?=9]-> a(b(x)) peak: c(c(a(x969))) <-8|0[==1,=>1]- c(b(a(x969))) -7|[==1,?=7]-> c(a(a(x969))) joins (1): c(a(a(x969))) -4|[==1,>>0]-> c(c(a(x969))) peak: a(c(a(x970))) <-8|0[==1,=?1]- a(b(a(x970))) -11|[==1,>=0]-> c(c(a(x970))) joins (1): a(c(a(x970))) -14|[==1,>=0]-> c(c(a(x970))) peak: c(c(a(x971))) <-8|0[==1,=?1]- c(b(a(x971))) -12|[==1,>=0]-> c(c(a(x971))) joins (1): peak: c(a(x)) <-8|[==1,=?1]- b(a(x)) -13|[==1,>=0]-> c(c(x)) joins (1): c(a(x)) -4|[==1,>=0]-> c(c(x)) peak: a(c(a(x973))) <-9|0[==1,=?15]- a(a(c(x973))) -0|[==1,>=5]-> c(c(c(x973))) joins (1): a(c(a(x973))) -4|0[==1,>>0]-> a(c(c(x973))) -14|[==1,>>0]-> c(c(c(x973))) peak: b(c(a(x974))) <-9|0[==1,=?15]- b(a(c(x974))) -2|[==1,>=9]-> a(b(c(x974))) joins (1): b(c(a(x974))) -4|0[==1,>>0]-> b(c(c(x974))) -5|[==1,>>0]-> c(c(c(x974))) a(b(c(x974))) -11|[==1,>>0]-> c(c(c(x974))) peak: c(a(x)) <-9|[==1,==15]- a(c(x)) -3|[==1,==15]-> a(b(x)) joins (1): c(a(x)) -10|[==1,>>9]-> a(b(x)) peak: c(c(a(x976))) <-9|0[==1,=?15]- c(a(c(x976))) -4|[==1,>=0]-> c(c(c(x976))) joins (1): c(c(a(x976))) -4|0[==1,>=0]-> c(c(c(x976))) peak: a(c(a(x977))) <-9|0[==1,=?15]- a(a(c(x977))) -6|[==1,>=12]-> a(b(c(x977))) joins (1): a(c(a(x977))) -4|0[==1,>>0]-> a(c(c(x977))) a(b(c(x977))) -5|0[==1,>>0]-> a(c(c(x977))) peak: b(c(a(x978))) <-9|0[==1,=?15]- b(a(c(x978))) -8|[==1,>=1]-> c(a(c(x978))) joins (1): b(c(a(x978))) -5|[==1,>>0]-> c(c(a(x978))) c(a(c(x978))) -9|0[==1,=?15]-> c(c(a(x978))) peak: c(c(a(x979))) <-9|0[==1,=?15]- c(a(c(x979))) -10|[==1,>=9]-> a(b(c(x979))) joins (1): c(c(a(x979))) -4|0[==1,>>0]-> c(c(c(x979))) a(b(c(x979))) -11|[==1,>>0]-> c(c(c(x979))) peak: b(c(a(x980))) <-9|0[==1,=?15]- b(a(c(x980))) -13|[==1,>=0]-> c(c(c(x980))) joins (1): b(c(a(x980))) -4|0[==1,>=0]-> b(c(c(x980))) -5|[==1,>=0]-> c(c(c(x980))) peak: c(a(x)) <-9|[==1,=?15]- a(c(x)) -14|[==1,>=0]-> c(c(x)) joins (1): c(a(x)) -4|[==1,>=0]-> c(c(x)) peak: a(a(b(x982))) <-10|0[==1,=>9]- a(c(a(x982))) -3|[==1,?=15]-> a(b(a(x982))) joins (1): a(b(a(x982))) -2|0[==1,=>9]-> a(a(b(x982))) peak: a(b(x)) <-10|[==1,=?9]- c(a(x)) -4|[==1,>=0]-> c(c(x)) joins (1): a(b(x)) -11|[==1,>=0]-> c(c(x)) peak: b(a(b(x984))) <-10|0[==1,=?9]- b(c(a(x984))) -5|[==1,>=0]-> c(c(a(x984))) joins (1): b(a(b(x984))) -8|[==1,>?1]-> c(a(b(x984))) c(c(a(x984))) -10|0[==1,=?9]-> c(a(b(x984))) peak: a(a(b(x985))) <-10|0[==1,=>9]- a(c(a(x985))) -9|[==1,?=15]-> c(a(a(x985))) joins (1): c(a(a(x985))) -10|[==1,=>9]-> a(b(a(x985))) -2|0[==1,=>9]-> a(a(b(x985))) peak: a(a(b(x986))) <-10|0[==1,=?9]- a(c(a(x986))) -14|[==1,>=0]-> c(c(a(x986))) joins (1): a(a(b(x986))) -0|[==1,>?5]-> c(c(b(x986))) -7|0[==1,>?7]-> c(c(a(x986))) peak: a(c(c(x987))) <-11|0[==1,=>0]- a(a(b(x987))) -0|[==1,?=5]-> c(c(b(x987))) joins (1): a(c(c(x987))) -14|[==1,=>0]-> c(c(c(x987))) c(c(b(x987))) -12|0[==1,=>0]-> c(c(c(x987))) peak: b(c(c(x988))) <-11|0[==1,=>0]- b(a(b(x988))) -2|[==1,?=9]-> a(b(b(x988))) joins (1): b(c(c(x988))) -5|[==1,=>0]-> c(c(c(x988))) a(b(b(x988))) -11|[==1,=>0]-> c(c(b(x988))) -12|0[==1,=>0]-> c(c(c(x988))) peak: c(c(c(x989))) <-11|0[==1,==0]- c(a(b(x989))) -4|[==1,==0]-> c(c(b(x989))) joins (1): c(c(b(x989))) -12|0[==1,==0]-> c(c(c(x989))) peak: a(c(c(x990))) <-11|0[==1,=>0]- a(a(b(x990))) -6|[==1,?=12]-> a(b(b(x990))) joins (1): a(c(c(x990))) -14|[==1,=>0]-> c(c(c(x990))) a(b(b(x990))) -11|[==1,=>0]-> c(c(b(x990))) -12|0[==1,=>0]-> c(c(c(x990))) peak: b(c(c(x991))) <-11|0[==1,=>0]- b(a(b(x991))) -8|[==1,?=1]-> c(a(b(x991))) joins (1): b(c(c(x991))) -5|[==1,=>0]-> c(c(c(x991))) c(a(b(x991))) -11|0[==1,=>0]-> c(c(c(x991))) peak: c(c(c(x992))) <-11|0[==1,=>0]- c(a(b(x992))) -10|[==1,?=9]-> a(b(b(x992))) joins (1): a(b(b(x992))) -11|[==1,=>0]-> c(c(b(x992))) -12|0[==1,=>0]-> c(c(c(x992))) peak: b(c(c(x993))) <-11|0[==1,==0]- b(a(b(x993))) -13|[==1,==0]-> c(c(b(x993))) joins (1): b(c(c(x993))) -5|[==1,==0]-> c(c(c(x993))) c(c(b(x993))) -12|0[==1,==0]-> c(c(c(x993))) peak: c(c(x)) <-12|[==1,=>0]- c(b(x)) -1|[==1,?=7]-> a(b(x)) joins (1): a(b(x)) -11|[==1,=>0]-> c(c(x)) peak: a(c(c(x995))) <-12|0[==1,=>0]- a(c(b(x995))) -3|[==1,?=15]-> a(b(b(x995))) joins (1): a(c(c(x995))) -14|[==1,=>0]-> c(c(c(x995))) a(b(b(x995))) -11|[==1,=>0]-> c(c(b(x995))) -12|0[==1,=>0]-> c(c(c(x995))) peak: b(c(c(x996))) <-12|0[==1,==0]- b(c(b(x996))) -5|[==1,==0]-> c(c(b(x996))) joins (1): b(c(c(x996))) -5|[==1,==0]-> c(c(c(x996))) c(c(b(x996))) -12|0[==1,==0]-> c(c(c(x996))) peak: c(c(x)) <-12|[==1,=>0]- c(b(x)) -7|[==1,?=7]-> c(a(x)) joins (1): c(a(x)) -4|[==1,=>0]-> c(c(x)) peak: a(c(c(x998))) <-12|0[==1,=>0]- a(c(b(x998))) -9|[==1,?=15]-> c(a(b(x998))) joins (1): a(c(c(x998))) -14|[==1,=>0]-> c(c(c(x998))) c(a(b(x998))) -11|0[==1,=>0]-> c(c(c(x998))) peak: a(c(c(x999))) <-12|0[==1,==0]- a(c(b(x999))) -14|[==1,==0]-> c(c(b(x999))) joins (1): a(c(c(x999))) -14|[==1,==0]-> c(c(c(x999))) c(c(b(x999))) -12|0[==1,==0]-> c(c(c(x999))) peak: c(c(c(x1000))) <-13|0[==1,=>0]- c(b(a(x1000))) -1|[==1,?=7]-> a(b(a(x1000))) joins (1): a(b(a(x1000))) -11|[==1,=>0]-> c(c(a(x1000))) -4|0[==1,=>0]-> c(c(c(x1000))) peak: c(c(x)) <-13|[==1,=>0]- b(a(x)) -2|[==1,?=9]-> a(b(x)) joins (1): a(b(x)) -11|[==1,=>0]-> c(c(x)) peak: c(c(c(x1002))) <-13|0[==1,=>0]- c(b(a(x1002))) -7|[==1,?=7]-> c(a(a(x1002))) joins (1): c(a(a(x1002))) -0|0[==1,?>5]-> c(c(c(x1002))) peak: c(c(x)) <-13|[==1,=>0]- b(a(x)) -8|[==1,?=1]-> c(a(x)) joins (1): c(a(x)) -4|[==1,=>0]-> c(c(x)) peak: a(c(c(x1004))) <-13|0[==1,==0]- a(b(a(x1004))) -11|[==1,==0]-> c(c(a(x1004))) joins (1): a(c(c(x1004))) -14|[==1,==0]-> c(c(c(x1004))) c(c(a(x1004))) -4|0[==1,==0]-> c(c(c(x1004))) peak: c(c(c(x1005))) <-13|0[==1,==0]- c(b(a(x1005))) -12|[==1,==0]-> c(c(a(x1005))) joins (1): c(c(a(x1005))) -4|0[==1,==0]-> c(c(c(x1005))) peak: a(c(c(x1006))) <-14|0[==1,=>0]- a(a(c(x1006))) -0|[==1,?=5]-> c(c(c(x1006))) joins (1): a(c(c(x1006))) -14|[==1,=>0]-> c(c(c(x1006))) peak: b(c(c(x1007))) <-14|0[==1,=>0]- b(a(c(x1007))) -2|[==1,?=9]-> a(b(c(x1007))) joins (1): b(c(c(x1007))) -5|[==1,=>0]-> c(c(c(x1007))) a(b(c(x1007))) -11|[==1,=>0]-> c(c(c(x1007))) peak: c(c(x)) <-14|[==1,=>0]- a(c(x)) -3|[==1,?=15]-> a(b(x)) joins (1): a(b(x)) -11|[==1,=>0]-> c(c(x)) peak: c(c(c(x1009))) <-14|0[==1,==0]- c(a(c(x1009))) -4|[==1,==0]-> c(c(c(x1009))) joins (1): peak: a(c(c(x1010))) <-14|0[==1,=>0]- a(a(c(x1010))) -6|[==1,?=12]-> a(b(c(x1010))) joins (1): a(b(c(x1010))) -5|0[==1,=>0]-> a(c(c(x1010))) peak: b(c(c(x1011))) <-14|0[==1,=>0]- b(a(c(x1011))) -8|[==1,?=1]-> c(a(c(x1011))) joins (1): b(c(c(x1011))) -5|[==1,=>0]-> c(c(c(x1011))) c(a(c(x1011))) -4|[==1,=>0]-> c(c(c(x1011))) peak: c(c(x)) <-14|[==1,=>0]- a(c(x)) -9|[==1,?=15]-> c(a(x)) joins (1): c(a(x)) -4|[==1,=>0]-> c(c(x)) peak: c(c(c(x1013))) <-14|0[==1,=>0]- c(a(c(x1013))) -10|[==1,?=9]-> a(b(c(x1013))) joins (1): a(b(c(x1013))) -11|[==1,=>0]-> c(c(c(x1013))) peak: b(c(c(x1014))) <-14|0[==1,==0]- b(a(c(x1014))) -13|[==1,==0]-> c(c(c(x1014))) joins (1): b(c(c(x1014))) -5|[==1,==0]-> c(c(c(x1014))) Qed