YES Problem: a(b(a(x))) -> b(a(b(x))) b(a(b(x))) -> a(b(a(x))) p() -> a(p()) p() -> b(p()) Proof: Church Rosser Transformation Processor (no redundant rules): strict: weak: critical peaks: 6 b(p()) <-0|[]- p() -1|[]-> a(p()) a(p()) <-1|[]- p() -0|[]-> b(p()) b(a(a(b(a(x17))))) <-2|0,0[]- b(a(b(a(b(x17))))) -2|[]-> a(b(a(a(b(x17))))) a(a(b(a(x18)))) <-2|0[]- a(b(a(b(x18)))) -3|[]-> b(a(b(b(x18)))) b(b(a(b(x19)))) <-3|0[]- b(a(b(a(x19)))) -2|[]-> a(b(a(a(x19)))) a(b(b(a(b(x20))))) <-3|0,0[]- a(b(a(b(a(x20))))) -3|[]-> b(a(b(b(a(x20))))) Redundant Rules Transformation: p() -> b(p()) p() -> a(p()) b(a(b(x))) -> a(b(a(x))) a(b(a(x))) -> b(a(b(x))) p() -> b(b(p())) p() -> b(a(p())) p() -> a(b(p())) p() -> a(a(p())) b(a(b(x))) -> b(a(b(x))) a(b(a(x))) -> a(b(a(x))) Church Rosser Transformation Processor (redex): strict: weak: a(b(a(x))) -> a(b(a(x))) b(a(b(x))) -> b(a(b(x))) p() -> a(a(p())) p() -> a(b(p())) p() -> b(a(p())) p() -> b(b(p())) a(b(a(x))) -> b(a(b(x))) b(a(b(x))) -> a(b(a(x))) p() -> a(p()) p() -> b(p()) critical peaks: 50 b(p()) <-0|[]- p() -1|[]-> a(p()) b(p()) <-0|[]- p() -4|[]-> b(b(p())) b(p()) <-0|[]- p() -5|[]-> b(a(p())) b(p()) <-0|[]- p() -6|[]-> a(b(p())) b(p()) <-0|[]- p() -7|[]-> a(a(p())) a(p()) <-1|[]- p() -0|[]-> b(p()) a(p()) <-1|[]- p() -4|[]-> b(b(p())) a(p()) <-1|[]- p() -5|[]-> b(a(p())) a(p()) <-1|[]- p() -6|[]-> a(b(p())) a(p()) <-1|[]- p() -7|[]-> a(a(p())) b(a(a(b(a(x93))))) <-2|0,0[]- b(a(b(a(b(x93))))) -2|[]-> a(b(a(a(b(x93))))) a(a(b(a(x94)))) <-2|0[]- a(b(a(b(x94)))) -3|[]-> b(a(b(b(x94)))) a(b(a(x))) <-2|[]- b(a(b(x))) -8|[]-> b(a(b(x))) b(a(a(b(a(x96))))) <-2|0,0[]- b(a(b(a(b(x96))))) -8|[]-> b(a(b(a(b(x96))))) a(a(b(a(x97)))) <-2|0[]- a(b(a(b(x97)))) -9|[]-> a(b(a(b(x97)))) b(b(a(b(x98)))) <-3|0[]- b(a(b(a(x98)))) -2|[]-> a(b(a(a(x98)))) a(b(b(a(b(x99))))) <-3|0,0[]- a(b(a(b(a(x99))))) -3|[]-> b(a(b(b(a(x99))))) b(b(a(b(x100)))) <-3|0[]- b(a(b(a(x100)))) -8|[]-> b(a(b(a(x100)))) b(a(b(x))) <-3|[]- a(b(a(x))) -9|[]-> a(b(a(x))) a(b(b(a(b(x102))))) <-3|0,0[]- a(b(a(b(a(x102))))) -9|[]-> a(b(a(b(a(x102))))) b(b(p())) <-4|[]- p() -0|[]-> b(p()) b(b(p())) <-4|[]- p() -1|[]-> a(p()) b(b(p())) <-4|[]- p() -5|[]-> b(a(p())) b(b(p())) <-4|[]- p() -6|[]-> a(b(p())) b(b(p())) <-4|[]- p() -7|[]-> a(a(p())) b(a(p())) <-5|[]- p() -0|[]-> b(p()) b(a(p())) <-5|[]- p() -1|[]-> a(p()) b(a(p())) <-5|[]- p() -4|[]-> b(b(p())) b(a(p())) <-5|[]- p() -6|[]-> a(b(p())) b(a(p())) <-5|[]- p() -7|[]-> a(a(p())) a(b(p())) <-6|[]- p() -0|[]-> b(p()) a(b(p())) <-6|[]- p() -1|[]-> a(p()) a(b(p())) <-6|[]- p() -4|[]-> b(b(p())) a(b(p())) <-6|[]- p() -5|[]-> b(a(p())) a(b(p())) <-6|[]- p() -7|[]-> a(a(p())) a(a(p())) <-7|[]- p() -0|[]-> b(p()) a(a(p())) <-7|[]- p() -1|[]-> a(p()) a(a(p())) <-7|[]- p() -4|[]-> b(b(p())) a(a(p())) <-7|[]- p() -5|[]-> b(a(p())) a(a(p())) <-7|[]- p() -6|[]-> a(b(p())) b(a(b(x))) <-8|[]- b(a(b(x))) -2|[]-> a(b(a(x))) b(a(b(a(b(x104))))) <-8|0,0[]- b(a(b(a(b(x104))))) -2|[]-> a(b(a(a(b(x104))))) a(b(a(b(x105)))) <-8|0[]- a(b(a(b(x105)))) -3|[]-> b(a(b(b(x105)))) b(a(b(a(b(x106))))) <-8|0,0[]- b(a(b(a(b(x106))))) -8|[]-> b(a(b(a(b(x106))))) a(b(a(b(x107)))) <-8|0[]- a(b(a(b(x107)))) -9|[]-> a(b(a(b(x107)))) b(a(b(a(x108)))) <-9|0[]- b(a(b(a(x108)))) -2|[]-> a(b(a(a(x108)))) a(b(a(x))) <-9|[]- a(b(a(x))) -3|[]-> b(a(b(x))) a(b(a(b(a(x110))))) <-9|0,0[]- a(b(a(b(a(x110))))) -3|[]-> b(a(b(b(a(x110))))) b(a(b(a(x111)))) <-9|0[]- b(a(b(a(x111)))) -8|[]-> b(a(b(a(x111)))) a(b(a(b(a(x112))))) <-9|0,0[]- a(b(a(b(a(x112))))) -9|[]-> a(b(a(b(a(x112))))) Shift Processor (no label): strict: weak: Shift Processor lab=left (dd): strict: p() -> b(p()) p() -> a(p()) b(p()) -> b(a(b(p()))) a(p()) -> a(b(a(p()))) a(b(a(p()))) -> b(a(b(p()))) b(p()) -> b(a(p())) b(a(p())) -> b(a(b(p()))) a(p()) -> a(b(a(p()))) a(b(a(p()))) -> b(a(b(p()))) b(p()) -> b(a(b(p()))) b(a(b(p()))) -> b(a(b(p()))) a(p()) -> a(b(a(p()))) a(b(a(p()))) -> b(a(b(p()))) b(p()) -> b(a(b(p()))) b(a(b(p()))) -> a(b(a(p()))) a(p()) -> a(b(a(p()))) b(p()) -> b(a(b(p()))) b(a(b(p()))) -> a(b(a(p()))) a(p()) -> a(b(p())) a(b(p())) -> a(b(a(p()))) b(p()) -> b(a(b(p()))) b(a(b(p()))) -> a(b(a(p()))) a(p()) -> a(b(a(p()))) a(b(a(p()))) -> a(b(a(p()))) p() -> b(p()) p() -> b(b(p())) b(p()) -> b(b(p())) b(p()) -> b(b(b(p()))) b(b(p())) -> b(b(b(p()))) b(p()) -> b(b(a(p()))) b(b(p())) -> b(b(a(p()))) p() -> b(p()) p() -> b(a(p())) b(p()) -> b(a(p())) b(p()) -> b(a(b(p()))) b(a(p())) -> b(a(b(p()))) b(p()) -> b(a(a(p()))) b(a(p())) -> b(a(a(p()))) p() -> b(p()) p() -> a(b(p())) b(p()) -> b(a(b(p()))) a(b(p())) -> a(b(a(p()))) a(b(a(p()))) -> b(a(b(p()))) b(p()) -> b(a(p())) b(a(p())) -> b(a(b(p()))) a(b(p())) -> a(b(a(p()))) a(b(a(p()))) -> b(a(b(p()))) b(p()) -> b(a(b(p()))) b(a(b(p()))) -> b(a(b(p()))) a(b(p())) -> a(b(a(p()))) a(b(a(p()))) -> b(a(b(p()))) b(p()) -> b(a(p())) b(a(p())) -> b(a(b(b(p())))) a(b(p())) -> a(b(a(b(p())))) a(b(a(b(p())))) -> b(a(b(b(p())))) b(p()) -> b(a(b(p()))) b(a(b(p()))) -> b(a(b(b(p())))) a(b(p())) -> a(b(a(b(p())))) a(b(a(b(p())))) -> b(a(b(b(p())))) b(p()) -> b(a(p())) b(a(p())) -> b(a(b(a(p())))) a(b(p())) -> a(b(a(a(p())))) a(b(a(a(p())))) -> b(a(b(a(p())))) b(p()) -> b(a(b(p()))) b(a(b(p()))) -> b(a(b(a(p())))) a(b(p())) -> a(b(a(a(p())))) a(b(a(a(p())))) -> b(a(b(a(p())))) b(p()) -> b(a(b(p()))) b(a(b(p()))) -> a(b(a(p()))) a(b(p())) -> a(b(a(p()))) b(p()) -> b(a(b(p()))) b(a(b(p()))) -> a(b(a(p()))) a(b(p())) -> a(b(a(p()))) a(b(a(p()))) -> a(b(a(p()))) p() -> b(p()) p() -> a(a(p())) b(p()) -> b(a(p())) b(a(p())) -> b(a(b(b(p())))) a(a(p())) -> a(a(b(a(p())))) a(a(b(a(p())))) -> a(b(a(b(p())))) a(b(a(b(p())))) -> b(a(b(b(p())))) b(p()) -> b(a(b(p()))) b(a(b(p()))) -> b(a(b(b(p())))) a(a(p())) -> a(a(b(a(p())))) a(a(b(a(p())))) -> a(b(a(b(p())))) a(b(a(b(p())))) -> b(a(b(b(p())))) b(p()) -> b(a(p())) b(a(p())) -> b(a(b(p()))) b(a(b(p()))) -> b(a(b(b(p())))) a(a(p())) -> a(a(b(a(p())))) a(a(b(a(p())))) -> a(b(a(b(p())))) a(b(a(b(p())))) -> b(a(b(b(p())))) b(p()) -> b(a(b(p()))) b(a(b(p()))) -> b(a(b(p()))) b(a(b(p()))) -> b(a(b(b(p())))) a(a(p())) -> a(a(b(a(p())))) a(a(b(a(p())))) -> a(b(a(b(p())))) a(b(a(b(p())))) -> b(a(b(b(p())))) b(p()) -> b(a(p())) b(a(p())) -> b(a(b(b(p())))) b(a(b(b(p())))) -> b(a(b(b(p())))) a(a(p())) -> a(a(b(a(p())))) a(a(b(a(p())))) -> a(b(a(b(p())))) a(b(a(b(p())))) -> b(a(b(b(p())))) b(p()) -> b(a(b(p()))) b(a(b(p()))) -> b(a(b(b(p())))) b(a(b(b(p())))) -> b(a(b(b(p())))) a(a(p())) -> a(a(b(a(p())))) a(a(b(a(p())))) -> a(b(a(b(p())))) a(b(a(b(p())))) -> b(a(b(b(p())))) b(p()) -> b(a(p())) b(a(p())) -> b(a(b(b(p())))) b(a(b(b(p())))) -> a(b(a(b(p())))) a(a(p())) -> a(a(b(a(p())))) a(a(b(a(p())))) -> a(b(a(b(p())))) b(p()) -> b(a(p())) b(a(p())) -> b(a(b(b(p())))) b(a(b(b(p())))) -> a(b(a(b(p())))) a(a(p())) -> a(a(b(p()))) a(a(b(p()))) -> a(a(b(a(p())))) a(a(b(a(p())))) -> a(b(a(b(p())))) b(p()) -> b(a(p())) b(a(p())) -> b(a(b(b(p())))) b(a(b(b(p())))) -> a(b(a(b(p())))) a(a(p())) -> a(a(b(a(p())))) a(a(b(a(p())))) -> a(a(b(a(p())))) a(a(b(a(p())))) -> a(b(a(b(p())))) b(p()) -> b(a(p())) b(a(p())) -> b(a(b(b(p())))) b(a(b(b(p())))) -> a(b(a(b(p())))) a(a(p())) -> a(a(b(a(p())))) a(a(b(a(p())))) -> a(b(a(b(p())))) a(b(a(b(p())))) -> a(b(a(b(p())))) b(p()) -> b(a(b(p()))) b(a(b(p()))) -> b(a(b(b(p())))) b(a(b(b(p())))) -> a(b(a(b(p())))) a(a(p())) -> a(a(b(a(p())))) a(a(b(a(p())))) -> a(b(a(b(p())))) b(p()) -> b(a(b(p()))) b(a(b(p()))) -> b(a(b(b(p())))) b(a(b(b(p())))) -> a(b(a(b(p())))) a(a(p())) -> a(a(b(p()))) a(a(b(p()))) -> a(a(b(a(p())))) a(a(b(a(p())))) -> a(b(a(b(p())))) b(p()) -> b(a(b(p()))) b(a(b(p()))) -> b(a(b(b(p())))) b(a(b(b(p())))) -> a(b(a(b(p())))) a(a(p())) -> a(a(b(a(p())))) a(a(b(a(p())))) -> a(a(b(a(p())))) a(a(b(a(p())))) -> a(b(a(b(p())))) b(p()) -> b(a(b(p()))) b(a(b(p()))) -> b(a(b(b(p())))) b(a(b(b(p())))) -> a(b(a(b(p())))) a(a(p())) -> a(a(b(a(p())))) a(a(b(a(p())))) -> a(b(a(b(p())))) a(b(a(b(p())))) -> a(b(a(b(p())))) b(p()) -> b(a(b(p()))) b(a(b(p()))) -> a(b(a(p()))) a(b(a(p()))) -> a(b(a(b(p())))) a(a(p())) -> a(a(b(a(p())))) a(a(b(a(p())))) -> a(b(a(b(p())))) b(p()) -> b(a(b(p()))) b(a(b(p()))) -> a(b(a(p()))) a(b(a(p()))) -> a(b(a(b(p())))) a(a(p())) -> a(a(b(p()))) a(a(b(p()))) -> a(a(b(a(p())))) a(a(b(a(p())))) -> a(b(a(b(p())))) b(p()) -> b(a(b(p()))) b(a(b(p()))) -> a(b(a(p()))) a(b(a(p()))) -> a(b(a(b(p())))) a(a(p())) -> a(a(b(a(p())))) a(a(b(a(p())))) -> a(a(b(a(p())))) a(a(b(a(p())))) -> a(b(a(b(p())))) b(p()) -> b(a(b(p()))) b(a(b(p()))) -> a(b(a(p()))) a(b(a(p()))) -> a(b(a(b(p())))) a(a(p())) -> a(a(b(a(p())))) a(a(b(a(p())))) -> a(b(a(b(p())))) a(b(a(b(p())))) -> a(b(a(b(p())))) b(p()) -> b(a(b(p()))) b(a(b(p()))) -> a(b(a(p()))) a(b(a(p()))) -> a(b(a(b(b(p()))))) a(a(p())) -> a(a(b(p()))) a(a(b(p()))) -> a(a(b(a(b(p()))))) a(a(b(a(b(p()))))) -> a(b(a(b(b(p()))))) b(p()) -> b(a(b(p()))) b(a(b(p()))) -> a(b(a(p()))) a(b(a(p()))) -> a(b(a(b(b(p()))))) a(a(p())) -> a(a(b(a(p())))) a(a(b(a(p())))) -> a(a(b(a(b(p()))))) a(a(b(a(b(p()))))) -> a(b(a(b(b(p()))))) b(p()) -> b(a(b(p()))) b(a(b(p()))) -> a(b(a(p()))) a(b(a(p()))) -> a(b(a(b(b(p()))))) a(a(p())) -> a(a(b(a(p())))) a(a(b(a(p())))) -> a(b(a(b(p())))) a(b(a(b(p())))) -> a(b(a(b(b(p()))))) b(p()) -> b(a(b(p()))) b(a(b(p()))) -> b(a(b(b(b(p()))))) b(a(b(b(b(p()))))) -> a(b(a(b(b(p()))))) a(a(p())) -> a(a(b(p()))) a(a(b(p()))) -> a(a(b(a(b(p()))))) a(a(b(a(b(p()))))) -> a(b(a(b(b(p()))))) b(p()) -> b(a(b(p()))) b(a(b(p()))) -> b(a(b(b(b(p()))))) b(a(b(b(b(p()))))) -> a(b(a(b(b(p()))))) a(a(p())) -> a(a(b(a(p())))) a(a(b(a(p())))) -> a(a(b(a(b(p()))))) a(a(b(a(b(p()))))) -> a(b(a(b(b(p()))))) b(p()) -> b(a(b(p()))) b(a(b(p()))) -> b(a(b(b(b(p()))))) b(a(b(b(b(p()))))) -> a(b(a(b(b(p()))))) a(a(p())) -> a(a(b(a(p())))) a(a(b(a(p())))) -> a(b(a(b(p())))) a(b(a(b(p())))) -> a(b(a(b(b(p()))))) b(p()) -> b(a(b(p()))) b(a(b(p()))) -> a(b(a(p()))) a(b(a(p()))) -> a(b(a(b(a(p()))))) a(a(p())) -> a(a(b(p()))) a(a(b(p()))) -> a(a(b(a(a(p()))))) a(a(b(a(a(p()))))) -> a(b(a(b(a(p()))))) b(p()) -> b(a(b(p()))) b(a(b(p()))) -> a(b(a(p()))) a(b(a(p()))) -> a(b(a(b(a(p()))))) a(a(p())) -> a(a(b(a(p())))) a(a(b(a(p())))) -> a(a(b(a(a(p()))))) a(a(b(a(a(p()))))) -> a(b(a(b(a(p()))))) b(p()) -> b(a(b(p()))) b(a(b(p()))) -> a(b(a(p()))) a(b(a(p()))) -> a(b(a(b(a(p()))))) a(a(p())) -> a(a(b(a(p())))) a(a(b(a(p())))) -> a(b(a(b(p())))) a(b(a(b(p())))) -> a(b(a(b(a(p()))))) b(p()) -> b(a(b(p()))) b(a(b(p()))) -> b(a(b(b(a(p()))))) b(a(b(b(a(p()))))) -> a(b(a(b(a(p()))))) a(a(p())) -> a(a(b(p()))) a(a(b(p()))) -> a(a(b(a(a(p()))))) a(a(b(a(a(p()))))) -> a(b(a(b(a(p()))))) b(p()) -> b(a(b(p()))) b(a(b(p()))) -> b(a(b(b(a(p()))))) b(a(b(b(a(p()))))) -> a(b(a(b(a(p()))))) a(a(p())) -> a(a(b(a(p())))) a(a(b(a(p())))) -> a(a(b(a(a(p()))))) a(a(b(a(a(p()))))) -> a(b(a(b(a(p()))))) b(p()) -> b(a(b(p()))) b(a(b(p()))) -> b(a(b(b(a(p()))))) b(a(b(b(a(p()))))) -> a(b(a(b(a(p()))))) a(a(p())) -> a(a(b(a(p())))) a(a(b(a(p())))) -> a(b(a(b(p())))) a(b(a(b(p())))) -> a(b(a(b(a(p()))))) p() -> a(p()) p() -> b(p()) a(p()) -> a(b(a(p()))) b(p()) -> b(a(b(p()))) b(a(b(p()))) -> a(b(a(p()))) a(p()) -> a(b(p())) a(b(p())) -> a(b(a(p()))) b(p()) -> b(a(b(p()))) b(a(b(p()))) -> a(b(a(p()))) a(p()) -> a(b(a(p()))) a(b(a(p()))) -> a(b(a(p()))) b(p()) -> b(a(b(p()))) b(a(b(p()))) -> a(b(a(p()))) a(p()) -> a(b(a(p()))) a(b(a(p()))) -> b(a(b(p()))) b(p()) -> b(a(b(p()))) a(p()) -> a(b(a(p()))) a(b(a(p()))) -> b(a(b(p()))) b(p()) -> b(a(p())) b(a(p())) -> b(a(b(p()))) a(p()) -> a(b(a(p()))) a(b(a(p()))) -> b(a(b(p()))) b(p()) -> b(a(b(p()))) b(a(b(p()))) -> b(a(b(p()))) p() -> a(p()) p() -> b(b(p())) a(p()) -> a(b(p())) a(b(p())) -> a(b(a(a(p())))) b(b(p())) -> b(b(a(b(p())))) b(b(a(b(p())))) -> b(a(b(a(p())))) b(a(b(a(p())))) -> a(b(a(a(p())))) a(p()) -> a(b(a(p()))) a(b(a(p()))) -> a(b(a(a(p())))) b(b(p())) -> b(b(a(b(p())))) b(b(a(b(p())))) -> b(a(b(a(p())))) b(a(b(a(p())))) -> a(b(a(a(p())))) a(p()) -> a(b(p())) a(b(p())) -> a(b(a(p()))) a(b(a(p()))) -> a(b(a(a(p())))) b(b(p())) -> b(b(a(b(p())))) b(b(a(b(p())))) -> b(a(b(a(p())))) b(a(b(a(p())))) -> a(b(a(a(p())))) a(p()) -> a(b(a(p()))) a(b(a(p()))) -> a(b(a(p()))) a(b(a(p()))) -> a(b(a(a(p())))) b(b(p())) -> b(b(a(b(p())))) b(b(a(b(p())))) -> b(a(b(a(p())))) b(a(b(a(p())))) -> a(b(a(a(p())))) a(p()) -> a(b(p())) a(b(p())) -> a(b(a(a(p())))) a(b(a(a(p())))) -> a(b(a(a(p())))) b(b(p())) -> b(b(a(b(p())))) b(b(a(b(p())))) -> b(a(b(a(p())))) b(a(b(a(p())))) -> a(b(a(a(p())))) a(p()) -> a(b(a(p()))) a(b(a(p()))) -> a(b(a(a(p())))) a(b(a(a(p())))) -> a(b(a(a(p())))) b(b(p())) -> b(b(a(b(p())))) b(b(a(b(p())))) -> b(a(b(a(p())))) b(a(b(a(p())))) -> a(b(a(a(p())))) a(p()) -> a(b(p())) a(b(p())) -> a(b(a(a(p())))) a(b(a(a(p())))) -> b(a(b(a(p())))) b(b(p())) -> b(b(a(b(p())))) b(b(a(b(p())))) -> b(a(b(a(p())))) a(p()) -> a(b(p())) a(b(p())) -> a(b(a(a(p())))) a(b(a(a(p())))) -> b(a(b(a(p())))) b(b(p())) -> b(b(a(p()))) b(b(a(p()))) -> b(b(a(b(p())))) b(b(a(b(p())))) -> b(a(b(a(p())))) a(p()) -> a(b(p())) a(b(p())) -> a(b(a(a(p())))) a(b(a(a(p())))) -> b(a(b(a(p())))) b(b(p())) -> b(b(a(b(p())))) b(b(a(b(p())))) -> b(b(a(b(p())))) b(b(a(b(p())))) -> b(a(b(a(p())))) a(p()) -> a(b(p())) a(b(p())) -> a(b(a(a(p())))) a(b(a(a(p())))) -> b(a(b(a(p())))) b(b(p())) -> b(b(a(b(p())))) b(b(a(b(p())))) -> b(a(b(a(p())))) b(a(b(a(p())))) -> b(a(b(a(p())))) a(p()) -> a(b(a(p()))) a(b(a(p()))) -> a(b(a(a(p())))) a(b(a(a(p())))) -> b(a(b(a(p())))) b(b(p())) -> b(b(a(b(p())))) b(b(a(b(p())))) -> b(a(b(a(p())))) a(p()) -> a(b(a(p()))) a(b(a(p()))) -> a(b(a(a(p())))) a(b(a(a(p())))) -> b(a(b(a(p())))) b(b(p())) -> b(b(a(p()))) b(b(a(p()))) -> b(b(a(b(p())))) b(b(a(b(p())))) -> b(a(b(a(p())))) a(p()) -> a(b(a(p()))) a(b(a(p()))) -> a(b(a(a(p())))) a(b(a(a(p())))) -> b(a(b(a(p())))) b(b(p())) -> b(b(a(b(p())))) b(b(a(b(p())))) -> b(b(a(b(p())))) b(b(a(b(p())))) -> b(a(b(a(p())))) a(p()) -> a(b(a(p()))) a(b(a(p()))) -> a(b(a(a(p())))) a(b(a(a(p())))) -> b(a(b(a(p())))) b(b(p())) -> b(b(a(b(p())))) b(b(a(b(p())))) -> b(a(b(a(p())))) b(a(b(a(p())))) -> b(a(b(a(p())))) a(p()) -> a(b(a(p()))) a(b(a(p()))) -> b(a(b(p()))) b(a(b(p()))) -> b(a(b(a(p())))) b(b(p())) -> b(b(a(b(p())))) b(b(a(b(p())))) -> b(a(b(a(p())))) a(p()) -> a(b(a(p()))) a(b(a(p()))) -> b(a(b(p()))) b(a(b(p()))) -> b(a(b(a(p())))) b(b(p())) -> b(b(a(p()))) b(b(a(p()))) -> b(b(a(b(p())))) b(b(a(b(p())))) -> b(a(b(a(p())))) a(p()) -> a(b(a(p()))) a(b(a(p()))) -> b(a(b(p()))) b(a(b(p()))) -> b(a(b(a(p())))) b(b(p())) -> b(b(a(b(p())))) b(b(a(b(p())))) -> b(b(a(b(p())))) b(b(a(b(p())))) -> b(a(b(a(p())))) a(p()) -> a(b(a(p()))) a(b(a(p()))) -> b(a(b(p()))) b(a(b(p()))) -> b(a(b(a(p())))) b(b(p())) -> b(b(a(b(p())))) b(b(a(b(p())))) -> b(a(b(a(p())))) b(a(b(a(p())))) -> b(a(b(a(p())))) a(p()) -> a(b(a(p()))) a(b(a(p()))) -> b(a(b(p()))) b(a(b(p()))) -> b(a(b(a(b(p()))))) b(b(p())) -> b(b(a(p()))) b(b(a(p()))) -> b(b(a(b(b(p()))))) b(b(a(b(b(p()))))) -> b(a(b(a(b(p()))))) a(p()) -> a(b(a(p()))) a(b(a(p()))) -> b(a(b(p()))) b(a(b(p()))) -> b(a(b(a(b(p()))))) b(b(p())) -> b(b(a(b(p())))) b(b(a(b(p())))) -> b(b(a(b(b(p()))))) b(b(a(b(b(p()))))) -> b(a(b(a(b(p()))))) a(p()) -> a(b(a(p()))) a(b(a(p()))) -> b(a(b(p()))) b(a(b(p()))) -> b(a(b(a(b(p()))))) b(b(p())) -> b(b(a(b(p())))) b(b(a(b(p())))) -> b(a(b(a(p())))) b(a(b(a(p())))) -> b(a(b(a(b(p()))))) a(p()) -> a(b(a(p()))) a(b(a(p()))) -> a(b(a(a(b(p()))))) a(b(a(a(b(p()))))) -> b(a(b(a(b(p()))))) b(b(p())) -> b(b(a(p()))) b(b(a(p()))) -> b(b(a(b(b(p()))))) b(b(a(b(b(p()))))) -> b(a(b(a(b(p()))))) a(p()) -> a(b(a(p()))) a(b(a(p()))) -> a(b(a(a(b(p()))))) a(b(a(a(b(p()))))) -> b(a(b(a(b(p()))))) b(b(p())) -> b(b(a(b(p())))) b(b(a(b(p())))) -> b(b(a(b(b(p()))))) b(b(a(b(b(p()))))) -> b(a(b(a(b(p()))))) a(p()) -> a(b(a(p()))) a(b(a(p()))) -> a(b(a(a(b(p()))))) a(b(a(a(b(p()))))) -> b(a(b(a(b(p()))))) b(b(p())) -> b(b(a(b(p())))) b(b(a(b(p())))) -> b(a(b(a(p())))) b(a(b(a(p())))) -> b(a(b(a(b(p()))))) a(p()) -> a(b(a(p()))) a(b(a(p()))) -> b(a(b(p()))) b(a(b(p()))) -> b(a(b(a(a(p()))))) b(b(p())) -> b(b(a(p()))) b(b(a(p()))) -> b(b(a(b(a(p()))))) b(b(a(b(a(p()))))) -> b(a(b(a(a(p()))))) a(p()) -> a(b(a(p()))) a(b(a(p()))) -> b(a(b(p()))) b(a(b(p()))) -> b(a(b(a(a(p()))))) b(b(p())) -> b(b(a(b(p())))) b(b(a(b(p())))) -> b(b(a(b(a(p()))))) b(b(a(b(a(p()))))) -> b(a(b(a(a(p()))))) a(p()) -> a(b(a(p()))) a(b(a(p()))) -> b(a(b(p()))) b(a(b(p()))) -> b(a(b(a(a(p()))))) b(b(p())) -> b(b(a(b(p())))) b(b(a(b(p())))) -> b(a(b(a(p())))) b(a(b(a(p())))) -> b(a(b(a(a(p()))))) a(p()) -> a(b(a(p()))) a(b(a(p()))) -> a(b(a(a(a(p()))))) a(b(a(a(a(p()))))) -> b(a(b(a(a(p()))))) b(b(p())) -> b(b(a(p()))) b(b(a(p()))) -> b(b(a(b(a(p()))))) b(b(a(b(a(p()))))) -> b(a(b(a(a(p()))))) a(p()) -> a(b(a(p()))) a(b(a(p()))) -> a(b(a(a(a(p()))))) a(b(a(a(a(p()))))) -> b(a(b(a(a(p()))))) b(b(p())) -> b(b(a(b(p())))) b(b(a(b(p())))) -> b(b(a(b(a(p()))))) b(b(a(b(a(p()))))) -> b(a(b(a(a(p()))))) a(p()) -> a(b(a(p()))) a(b(a(p()))) -> a(b(a(a(a(p()))))) a(b(a(a(a(p()))))) -> b(a(b(a(a(p()))))) b(b(p())) -> b(b(a(b(p())))) b(b(a(b(p())))) -> b(a(b(a(p())))) b(a(b(a(p())))) -> b(a(b(a(a(p()))))) p() -> a(p()) p() -> b(a(p())) a(p()) -> a(b(a(p()))) b(a(p())) -> b(a(b(p()))) b(a(b(p()))) -> a(b(a(p()))) a(p()) -> a(b(p())) a(b(p())) -> a(b(a(p()))) b(a(p())) -> b(a(b(p()))) b(a(b(p()))) -> a(b(a(p()))) a(p()) -> a(b(a(p()))) a(b(a(p()))) -> a(b(a(p()))) b(a(p())) -> b(a(b(p()))) b(a(b(p()))) -> a(b(a(p()))) a(p()) -> a(b(p())) a(b(p())) -> a(b(a(b(p())))) b(a(p())) -> b(a(b(b(p())))) b(a(b(b(p())))) -> a(b(a(b(p())))) a(p()) -> a(b(a(p()))) a(b(a(p()))) -> a(b(a(b(p())))) b(a(p())) -> b(a(b(b(p())))) b(a(b(b(p())))) -> a(b(a(b(p())))) a(p()) -> a(b(p())) a(b(p())) -> a(b(a(a(p())))) b(a(p())) -> b(a(b(a(p())))) b(a(b(a(p())))) -> a(b(a(a(p())))) a(p()) -> a(b(a(p()))) a(b(a(p()))) -> a(b(a(a(p())))) b(a(p())) -> b(a(b(a(p())))) b(a(b(a(p())))) -> a(b(a(a(p())))) a(p()) -> a(b(a(p()))) a(b(a(p()))) -> b(a(b(p()))) b(a(p())) -> b(a(b(p()))) a(p()) -> a(b(a(p()))) a(b(a(p()))) -> b(a(b(p()))) b(a(p())) -> b(a(b(p()))) b(a(b(p()))) -> b(a(b(p()))) p() -> a(p()) p() -> a(b(p())) a(p()) -> a(b(p())) a(p()) -> a(b(b(p()))) a(b(p())) -> a(b(b(p()))) a(p()) -> a(b(a(p()))) a(b(p())) -> a(b(a(p()))) p() -> a(p()) p() -> a(a(p())) a(p()) -> a(a(p())) a(p()) -> a(a(b(p()))) a(a(p())) -> a(a(b(p()))) a(p()) -> a(a(a(p()))) a(a(p())) -> a(a(a(p()))) b(a(b(a(b(x93))))) -> b(a(a(b(a(x93))))) b(a(b(a(b(x93))))) -> a(b(a(a(b(x93))))) b(a(a(b(a(x93))))) -> b(a(b(a(b(x93))))) a(b(a(a(b(x93))))) -> b(a(b(a(b(x93))))) a(b(a(b(x94)))) -> a(a(b(a(x94)))) a(b(a(b(x94)))) -> b(a(b(b(x94)))) a(a(b(a(x94)))) -> a(b(a(b(x94)))) b(a(b(b(x94)))) -> a(b(a(b(x94)))) b(a(b(x))) -> a(b(a(x))) b(a(b(x))) -> b(a(b(x))) b(a(b(x))) -> a(b(a(x))) a(b(a(x))) -> b(a(b(x))) b(a(b(a(b(x96))))) -> b(a(a(b(a(x96))))) b(a(b(a(b(x96))))) -> b(a(b(a(b(x96))))) b(a(b(a(b(x96))))) -> b(a(a(b(a(x96))))) b(a(a(b(a(x96))))) -> b(a(b(a(b(x96))))) a(b(a(b(x97)))) -> a(a(b(a(x97)))) a(b(a(b(x97)))) -> a(b(a(b(x97)))) a(b(a(b(x97)))) -> a(a(b(a(x97)))) a(a(b(a(x97)))) -> a(b(a(b(x97)))) b(a(b(a(x98)))) -> b(b(a(b(x98)))) b(a(b(a(x98)))) -> a(b(a(a(x98)))) b(b(a(b(x98)))) -> b(a(b(a(x98)))) a(b(a(a(x98)))) -> b(a(b(a(x98)))) a(b(a(b(a(x99))))) -> a(b(b(a(b(x99))))) a(b(a(b(a(x99))))) -> b(a(b(b(a(x99))))) a(b(b(a(b(x99))))) -> a(b(a(b(a(x99))))) b(a(b(b(a(x99))))) -> a(b(a(b(a(x99))))) b(a(b(a(x100)))) -> b(b(a(b(x100)))) b(a(b(a(x100)))) -> b(a(b(a(x100)))) b(a(b(a(x100)))) -> b(b(a(b(x100)))) b(b(a(b(x100)))) -> b(a(b(a(x100)))) a(b(a(x))) -> b(a(b(x))) a(b(a(x))) -> a(b(a(x))) a(b(a(x))) -> b(a(b(x))) b(a(b(x))) -> a(b(a(x))) a(b(a(b(a(x102))))) -> a(b(b(a(b(x102))))) a(b(a(b(a(x102))))) -> a(b(a(b(a(x102))))) a(b(a(b(a(x102))))) -> a(b(b(a(b(x102))))) a(b(b(a(b(x102))))) -> a(b(a(b(a(x102))))) p() -> b(b(p())) p() -> b(p()) b(p()) -> b(b(p())) b(b(p())) -> b(b(b(p()))) b(p()) -> b(b(b(p()))) b(b(p())) -> b(b(a(p()))) b(p()) -> b(b(a(p()))) p() -> b(b(p())) p() -> a(p()) b(b(p())) -> b(b(a(b(p())))) b(b(a(b(p())))) -> b(a(b(a(p())))) a(p()) -> a(b(p())) a(b(p())) -> a(b(a(a(p())))) a(b(a(a(p())))) -> b(a(b(a(p())))) b(b(p())) -> b(b(a(b(p())))) b(b(a(b(p())))) -> b(a(b(a(p())))) a(p()) -> a(b(a(p()))) a(b(a(p()))) -> a(b(a(a(p())))) a(b(a(a(p())))) -> b(a(b(a(p())))) b(b(p())) -> b(b(a(b(p())))) b(b(a(b(p())))) -> b(a(b(a(p())))) a(p()) -> a(b(a(p()))) a(b(a(p()))) -> b(a(b(p()))) b(a(b(p()))) -> b(a(b(a(p())))) b(b(p())) -> b(b(a(p()))) b(b(a(p()))) -> b(b(a(b(p())))) b(b(a(b(p())))) -> b(a(b(a(p())))) a(p()) -> a(b(p())) a(b(p())) -> a(b(a(a(p())))) a(b(a(a(p())))) -> b(a(b(a(p())))) b(b(p())) -> b(b(a(p()))) b(b(a(p()))) -> b(b(a(b(p())))) b(b(a(b(p())))) -> b(a(b(a(p())))) a(p()) -> a(b(a(p()))) a(b(a(p()))) -> a(b(a(a(p())))) a(b(a(a(p())))) -> b(a(b(a(p())))) b(b(p())) -> b(b(a(p()))) b(b(a(p()))) -> b(b(a(b(p())))) b(b(a(b(p())))) -> b(a(b(a(p())))) a(p()) -> a(b(a(p()))) a(b(a(p()))) -> b(a(b(p()))) b(a(b(p()))) -> b(a(b(a(p())))) b(b(p())) -> b(b(a(b(p())))) b(b(a(b(p())))) -> b(b(a(b(p())))) b(b(a(b(p())))) -> b(a(b(a(p())))) a(p()) -> a(b(p())) a(b(p())) -> a(b(a(a(p())))) a(b(a(a(p())))) -> b(a(b(a(p())))) b(b(p())) -> b(b(a(b(p())))) b(b(a(b(p())))) -> b(b(a(b(p())))) b(b(a(b(p())))) -> b(a(b(a(p())))) a(p()) -> a(b(a(p()))) a(b(a(p()))) -> a(b(a(a(p())))) a(b(a(a(p())))) -> b(a(b(a(p())))) b(b(p())) -> b(b(a(b(p())))) b(b(a(b(p())))) -> b(b(a(b(p())))) b(b(a(b(p())))) -> b(a(b(a(p())))) a(p()) -> a(b(a(p()))) a(b(a(p()))) -> b(a(b(p()))) b(a(b(p()))) -> b(a(b(a(p())))) b(b(p())) -> b(b(a(b(p())))) b(b(a(b(p())))) -> b(a(b(a(p())))) b(a(b(a(p())))) -> b(a(b(a(p())))) a(p()) -> a(b(p())) a(b(p())) -> a(b(a(a(p())))) a(b(a(a(p())))) -> b(a(b(a(p())))) b(b(p())) -> b(b(a(b(p())))) b(b(a(b(p())))) -> b(a(b(a(p())))) b(a(b(a(p())))) -> b(a(b(a(p())))) a(p()) -> a(b(a(p()))) a(b(a(p()))) -> a(b(a(a(p())))) a(b(a(a(p())))) -> b(a(b(a(p())))) b(b(p())) -> b(b(a(b(p())))) b(b(a(b(p())))) -> b(a(b(a(p())))) b(a(b(a(p())))) -> b(a(b(a(p())))) a(p()) -> a(b(a(p()))) a(b(a(p()))) -> b(a(b(p()))) b(a(b(p()))) -> b(a(b(a(p())))) b(b(p())) -> b(b(a(p()))) b(b(a(p()))) -> b(b(a(b(b(p()))))) b(b(a(b(b(p()))))) -> b(a(b(a(b(p()))))) a(p()) -> a(b(a(p()))) a(b(a(p()))) -> b(a(b(p()))) b(a(b(p()))) -> b(a(b(a(b(p()))))) b(b(p())) -> b(b(a(p()))) b(b(a(p()))) -> b(b(a(b(b(p()))))) b(b(a(b(b(p()))))) -> b(a(b(a(b(p()))))) a(p()) -> a(b(a(p()))) a(b(a(p()))) -> a(b(a(a(b(p()))))) a(b(a(a(b(p()))))) -> b(a(b(a(b(p()))))) b(b(p())) -> b(b(a(b(p())))) b(b(a(b(p())))) -> b(b(a(b(b(p()))))) b(b(a(b(b(p()))))) -> b(a(b(a(b(p()))))) a(p()) -> a(b(a(p()))) a(b(a(p()))) -> b(a(b(p()))) b(a(b(p()))) -> b(a(b(a(b(p()))))) b(b(p())) -> b(b(a(b(p())))) b(b(a(b(p())))) -> b(b(a(b(b(p()))))) b(b(a(b(b(p()))))) -> b(a(b(a(b(p()))))) a(p()) -> a(b(a(p()))) a(b(a(p()))) -> a(b(a(a(b(p()))))) a(b(a(a(b(p()))))) -> b(a(b(a(b(p()))))) b(b(p())) -> b(b(a(b(p())))) b(b(a(b(p())))) -> b(a(b(a(p())))) b(a(b(a(p())))) -> b(a(b(a(b(p()))))) a(p()) -> a(b(a(p()))) a(b(a(p()))) -> b(a(b(p()))) b(a(b(p()))) -> b(a(b(a(b(p()))))) b(b(p())) -> b(b(a(b(p())))) b(b(a(b(p())))) -> b(a(b(a(p())))) b(a(b(a(p())))) -> b(a(b(a(b(p()))))) a(p()) -> a(b(a(p()))) a(b(a(p()))) -> a(b(a(a(b(p()))))) a(b(a(a(b(p()))))) -> b(a(b(a(b(p()))))) b(b(p())) -> b(b(a(p()))) b(b(a(p()))) -> b(b(a(b(a(p()))))) b(b(a(b(a(p()))))) -> b(a(b(a(a(p()))))) a(p()) -> a(b(a(p()))) a(b(a(p()))) -> b(a(b(p()))) b(a(b(p()))) -> b(a(b(a(a(p()))))) b(b(p())) -> b(b(a(p()))) b(b(a(p()))) -> b(b(a(b(a(p()))))) b(b(a(b(a(p()))))) -> b(a(b(a(a(p()))))) a(p()) -> a(b(a(p()))) a(b(a(p()))) -> a(b(a(a(a(p()))))) a(b(a(a(a(p()))))) -> b(a(b(a(a(p()))))) b(b(p())) -> b(b(a(b(p())))) b(b(a(b(p())))) -> b(b(a(b(a(p()))))) b(b(a(b(a(p()))))) -> b(a(b(a(a(p()))))) a(p()) -> a(b(a(p()))) a(b(a(p()))) -> b(a(b(p()))) b(a(b(p()))) -> b(a(b(a(a(p()))))) b(b(p())) -> b(b(a(b(p())))) b(b(a(b(p())))) -> b(b(a(b(a(p()))))) b(b(a(b(a(p()))))) -> b(a(b(a(a(p()))))) a(p()) -> a(b(a(p()))) a(b(a(p()))) -> a(b(a(a(a(p()))))) a(b(a(a(a(p()))))) -> b(a(b(a(a(p()))))) b(b(p())) -> b(b(a(b(p())))) b(b(a(b(p())))) -> b(a(b(a(p())))) b(a(b(a(p())))) -> b(a(b(a(a(p()))))) a(p()) -> a(b(a(p()))) a(b(a(p()))) -> b(a(b(p()))) b(a(b(p()))) -> b(a(b(a(a(p()))))) b(b(p())) -> b(b(a(b(p())))) b(b(a(b(p())))) -> b(a(b(a(p())))) b(a(b(a(p())))) -> b(a(b(a(a(p()))))) a(p()) -> a(b(a(p()))) a(b(a(p()))) -> a(b(a(a(a(p()))))) a(b(a(a(a(p()))))) -> b(a(b(a(a(p()))))) b(b(p())) -> b(b(a(b(p())))) b(b(a(b(p())))) -> b(a(b(a(p())))) b(a(b(a(p())))) -> a(b(a(a(p())))) a(p()) -> a(b(p())) a(b(p())) -> a(b(a(a(p())))) b(b(p())) -> b(b(a(b(p())))) b(b(a(b(p())))) -> b(a(b(a(p())))) b(a(b(a(p())))) -> a(b(a(a(p())))) a(p()) -> a(b(a(p()))) a(b(a(p()))) -> a(b(a(a(p())))) b(b(p())) -> b(b(a(b(p())))) b(b(a(b(p())))) -> b(a(b(a(p())))) b(a(b(a(p())))) -> a(b(a(a(p())))) a(p()) -> a(b(p())) a(b(p())) -> a(b(a(p()))) a(b(a(p()))) -> a(b(a(a(p())))) b(b(p())) -> b(b(a(b(p())))) b(b(a(b(p())))) -> b(a(b(a(p())))) b(a(b(a(p())))) -> a(b(a(a(p())))) a(p()) -> a(b(a(p()))) a(b(a(p()))) -> a(b(a(p()))) a(b(a(p()))) -> a(b(a(a(p())))) b(b(p())) -> b(b(a(b(p())))) b(b(a(b(p())))) -> b(a(b(a(p())))) b(a(b(a(p())))) -> a(b(a(a(p())))) a(p()) -> a(b(p())) a(b(p())) -> a(b(a(a(p())))) a(b(a(a(p())))) -> a(b(a(a(p())))) b(b(p())) -> b(b(a(b(p())))) b(b(a(b(p())))) -> b(a(b(a(p())))) b(a(b(a(p())))) -> a(b(a(a(p())))) a(p()) -> a(b(a(p()))) a(b(a(p()))) -> a(b(a(a(p())))) a(b(a(a(p())))) -> a(b(a(a(p())))) p() -> b(b(p())) p() -> b(a(p())) b(b(p())) -> b(b(a(b(p())))) b(a(p())) -> b(a(b(a(p())))) b(a(b(a(p())))) -> b(b(a(b(p())))) b(b(p())) -> b(b(a(p()))) b(b(a(p()))) -> b(b(a(b(p())))) b(a(p())) -> b(a(b(a(p())))) b(a(b(a(p())))) -> b(b(a(b(p())))) b(b(p())) -> b(b(a(b(p())))) b(b(a(b(p())))) -> b(b(a(b(p())))) b(a(p())) -> b(a(b(a(p())))) b(a(b(a(p())))) -> b(b(a(b(p())))) b(b(p())) -> b(b(a(b(p())))) b(b(a(b(p())))) -> b(a(b(a(p())))) b(a(p())) -> b(a(b(a(p())))) b(b(p())) -> b(b(a(b(p())))) b(b(a(b(p())))) -> b(a(b(a(p())))) b(a(p())) -> b(a(b(p()))) b(a(b(p()))) -> b(a(b(a(p())))) b(b(p())) -> b(b(a(b(p())))) b(b(a(b(p())))) -> b(a(b(a(p())))) b(a(p())) -> b(a(b(a(p())))) b(a(b(a(p())))) -> b(a(b(a(p())))) p() -> b(b(p())) p() -> a(b(p())) b(b(p())) -> b(b(a(b(p())))) b(b(a(b(p())))) -> b(a(b(a(p())))) a(b(p())) -> a(b(a(a(p())))) a(b(a(a(p())))) -> b(a(b(a(p())))) p() -> b(b(p())) p() -> a(a(p())) b(b(p())) -> b(b(a(b(p())))) b(b(a(b(p())))) -> b(a(b(a(p())))) b(a(b(a(p())))) -> a(b(a(a(p())))) a(b(a(a(p())))) -> a(b(a(a(b(a(p())))))) a(a(p())) -> a(a(b(a(p())))) a(a(b(a(p())))) -> a(b(a(b(p())))) a(b(a(b(p())))) -> a(b(a(b(a(b(p())))))) a(b(a(b(a(b(p())))))) -> a(b(a(a(b(a(p())))))) b(b(p())) -> b(b(a(b(p())))) b(b(a(b(p())))) -> b(a(b(a(p())))) b(a(b(a(p())))) -> a(b(a(a(p())))) a(b(a(a(p())))) -> a(b(a(a(b(a(p())))))) a(a(p())) -> a(a(b(a(p())))) a(a(b(a(p())))) -> a(a(b(a(a(b(p())))))) a(a(b(a(a(b(p())))))) -> a(b(a(b(a(b(p())))))) a(b(a(b(a(b(p())))))) -> a(b(a(a(b(a(p())))))) b(b(p())) -> b(b(a(b(p())))) b(b(a(b(p())))) -> b(a(b(a(p())))) b(a(b(a(p())))) -> b(a(b(a(b(a(p())))))) b(a(b(a(b(a(p())))))) -> a(b(a(a(b(a(p())))))) a(a(p())) -> a(a(b(a(p())))) a(a(b(a(p())))) -> a(b(a(b(p())))) a(b(a(b(p())))) -> a(b(a(b(a(b(p())))))) a(b(a(b(a(b(p())))))) -> a(b(a(a(b(a(p())))))) b(b(p())) -> b(b(a(b(p())))) b(b(a(b(p())))) -> b(a(b(a(p())))) b(a(b(a(p())))) -> b(a(b(a(b(a(p())))))) b(a(b(a(b(a(p())))))) -> a(b(a(a(b(a(p())))))) a(a(p())) -> a(a(b(a(p())))) a(a(b(a(p())))) -> a(a(b(a(a(b(p())))))) a(a(b(a(a(b(p())))))) -> a(b(a(b(a(b(p())))))) a(b(a(b(a(b(p())))))) -> a(b(a(a(b(a(p())))))) b(b(p())) -> b(b(a(b(p())))) b(b(a(b(p())))) -> b(b(a(b(b(a(p())))))) b(b(a(b(b(a(p())))))) -> b(a(b(a(b(a(p())))))) b(a(b(a(b(a(p())))))) -> a(b(a(a(b(a(p())))))) a(a(p())) -> a(a(b(a(p())))) a(a(b(a(p())))) -> a(b(a(b(p())))) a(b(a(b(p())))) -> a(b(a(b(a(b(p())))))) a(b(a(b(a(b(p())))))) -> a(b(a(a(b(a(p())))))) b(b(p())) -> b(b(a(b(p())))) b(b(a(b(p())))) -> b(b(a(b(b(a(p())))))) b(b(a(b(b(a(p())))))) -> b(a(b(a(b(a(p())))))) b(a(b(a(b(a(p())))))) -> a(b(a(a(b(a(p())))))) a(a(p())) -> a(a(b(a(p())))) a(a(b(a(p())))) -> a(a(b(a(a(b(p())))))) a(a(b(a(a(b(p())))))) -> a(b(a(b(a(b(p())))))) a(b(a(b(a(b(p())))))) -> a(b(a(a(b(a(p())))))) b(b(p())) -> b(b(a(b(p())))) b(b(a(b(p())))) -> b(a(b(a(p())))) b(a(b(a(p())))) -> b(a(b(a(b(a(p())))))) b(a(b(a(b(a(p())))))) -> b(a(b(b(a(b(p())))))) a(a(p())) -> a(a(b(a(p())))) a(a(b(a(p())))) -> a(b(a(b(p())))) a(b(a(b(p())))) -> b(a(b(b(p())))) b(a(b(b(p())))) -> b(a(b(b(a(b(p())))))) b(b(p())) -> b(b(a(b(p())))) b(b(a(b(p())))) -> b(a(b(a(p())))) b(a(b(a(p())))) -> b(a(b(a(b(a(p())))))) b(a(b(a(b(a(p())))))) -> b(a(b(b(a(b(p())))))) a(a(p())) -> a(a(b(a(p())))) a(a(b(a(p())))) -> a(b(a(b(p())))) a(b(a(b(p())))) -> a(b(a(b(a(b(p())))))) a(b(a(b(a(b(p())))))) -> b(a(b(b(a(b(p())))))) b(b(p())) -> b(b(a(b(p())))) b(b(a(b(p())))) -> b(a(b(a(p())))) b(a(b(a(p())))) -> b(a(b(a(b(a(p())))))) b(a(b(a(b(a(p())))))) -> b(a(b(b(a(b(p())))))) a(a(p())) -> a(a(b(a(p())))) a(a(b(a(p())))) -> a(a(b(a(a(b(p())))))) a(a(b(a(a(b(p())))))) -> a(b(a(b(a(b(p())))))) a(b(a(b(a(b(p())))))) -> b(a(b(b(a(b(p())))))) b(b(p())) -> b(b(a(b(p())))) b(b(a(b(p())))) -> b(b(a(b(b(a(p())))))) b(b(a(b(b(a(p())))))) -> b(a(b(a(b(a(p())))))) b(a(b(a(b(a(p())))))) -> b(a(b(b(a(b(p())))))) a(a(p())) -> a(a(b(a(p())))) a(a(b(a(p())))) -> a(b(a(b(p())))) a(b(a(b(p())))) -> b(a(b(b(p())))) b(a(b(b(p())))) -> b(a(b(b(a(b(p())))))) b(b(p())) -> b(b(a(b(p())))) b(b(a(b(p())))) -> b(b(a(b(b(a(p())))))) b(b(a(b(b(a(p())))))) -> b(a(b(a(b(a(p())))))) b(a(b(a(b(a(p())))))) -> b(a(b(b(a(b(p())))))) a(a(p())) -> a(a(b(a(p())))) a(a(b(a(p())))) -> a(b(a(b(p())))) a(b(a(b(p())))) -> a(b(a(b(a(b(p())))))) a(b(a(b(a(b(p())))))) -> b(a(b(b(a(b(p())))))) b(b(p())) -> b(b(a(b(p())))) b(b(a(b(p())))) -> b(b(a(b(b(a(p())))))) b(b(a(b(b(a(p())))))) -> b(a(b(a(b(a(p())))))) b(a(b(a(b(a(p())))))) -> b(a(b(b(a(b(p())))))) a(a(p())) -> a(a(b(a(p())))) a(a(b(a(p())))) -> a(a(b(a(a(b(p())))))) a(a(b(a(a(b(p())))))) -> a(b(a(b(a(b(p())))))) a(b(a(b(a(b(p())))))) -> b(a(b(b(a(b(p())))))) p() -> b(a(p())) p() -> b(p()) b(p()) -> b(a(p())) b(a(p())) -> b(a(b(p()))) b(p()) -> b(a(b(p()))) b(a(p())) -> b(a(a(p()))) b(p()) -> b(a(a(p()))) p() -> b(a(p())) p() -> a(p()) b(a(p())) -> b(a(b(p()))) a(p()) -> a(b(a(p()))) a(b(a(p()))) -> b(a(b(p()))) b(a(p())) -> b(a(b(p()))) b(a(b(p()))) -> b(a(b(p()))) a(p()) -> a(b(a(p()))) a(b(a(p()))) -> b(a(b(p()))) b(a(p())) -> b(a(b(p()))) b(a(b(p()))) -> a(b(a(p()))) a(p()) -> a(b(a(p()))) b(a(p())) -> b(a(b(p()))) b(a(b(p()))) -> a(b(a(p()))) a(p()) -> a(b(p())) a(b(p())) -> a(b(a(p()))) b(a(p())) -> b(a(b(p()))) b(a(b(p()))) -> a(b(a(p()))) a(p()) -> a(b(a(p()))) a(b(a(p()))) -> a(b(a(p()))) b(a(p())) -> b(a(b(b(p())))) b(a(b(b(p())))) -> a(b(a(b(p())))) a(p()) -> a(b(p())) a(b(p())) -> a(b(a(b(p())))) b(a(p())) -> b(a(b(b(p())))) b(a(b(b(p())))) -> a(b(a(b(p())))) a(p()) -> a(b(a(p()))) a(b(a(p()))) -> a(b(a(b(p())))) b(a(p())) -> b(a(b(a(p())))) b(a(b(a(p())))) -> a(b(a(a(p())))) a(p()) -> a(b(p())) a(b(p())) -> a(b(a(a(p())))) b(a(p())) -> b(a(b(a(p())))) b(a(b(a(p())))) -> a(b(a(a(p())))) a(p()) -> a(b(a(p()))) a(b(a(p()))) -> a(b(a(a(p())))) p() -> b(a(p())) p() -> b(b(p())) b(a(p())) -> b(a(b(a(p())))) b(b(p())) -> b(b(a(b(p())))) b(b(a(b(p())))) -> b(a(b(a(p())))) b(a(p())) -> b(a(b(p()))) b(a(b(p()))) -> b(a(b(a(p())))) b(b(p())) -> b(b(a(b(p())))) b(b(a(b(p())))) -> b(a(b(a(p())))) b(a(p())) -> b(a(b(a(p())))) b(a(b(a(p())))) -> b(a(b(a(p())))) b(b(p())) -> b(b(a(b(p())))) b(b(a(b(p())))) -> b(a(b(a(p())))) b(a(p())) -> b(a(b(a(p())))) b(a(b(a(p())))) -> b(b(a(b(p())))) b(b(p())) -> b(b(a(b(p())))) b(a(p())) -> b(a(b(a(p())))) b(a(b(a(p())))) -> b(b(a(b(p())))) b(b(p())) -> b(b(a(p()))) b(b(a(p()))) -> b(b(a(b(p())))) b(a(p())) -> b(a(b(a(p())))) b(a(b(a(p())))) -> b(b(a(b(p())))) b(b(p())) -> b(b(a(b(p())))) b(b(a(b(p())))) -> b(b(a(b(p())))) p() -> b(a(p())) p() -> a(b(p())) b(a(p())) -> b(a(b(p()))) a(b(p())) -> a(b(a(p()))) a(b(a(p()))) -> b(a(b(p()))) b(a(p())) -> b(a(b(p()))) b(a(b(p()))) -> b(a(b(p()))) a(b(p())) -> a(b(a(p()))) a(b(a(p()))) -> b(a(b(p()))) b(a(p())) -> b(a(b(b(p())))) a(b(p())) -> a(b(a(b(p())))) a(b(a(b(p())))) -> b(a(b(b(p())))) b(a(p())) -> b(a(b(p()))) b(a(b(p()))) -> b(a(b(b(p())))) a(b(p())) -> a(b(a(b(p())))) a(b(a(b(p())))) -> b(a(b(b(p())))) b(a(p())) -> b(a(b(b(p())))) b(a(b(b(p())))) -> b(a(b(b(p())))) a(b(p())) -> a(b(a(b(p())))) a(b(a(b(p())))) -> b(a(b(b(p())))) b(a(p())) -> b(a(b(a(p())))) a(b(p())) -> a(b(a(a(p())))) a(b(a(a(p())))) -> b(a(b(a(p())))) b(a(p())) -> b(a(b(p()))) b(a(b(p()))) -> b(a(b(a(p())))) a(b(p())) -> a(b(a(a(p())))) a(b(a(a(p())))) -> b(a(b(a(p())))) b(a(p())) -> b(a(b(a(p())))) b(a(b(a(p())))) -> b(a(b(a(p())))) a(b(p())) -> a(b(a(a(p())))) a(b(a(a(p())))) -> b(a(b(a(p())))) b(a(p())) -> b(a(b(p()))) b(a(b(p()))) -> a(b(a(p()))) a(b(p())) -> a(b(a(p()))) b(a(p())) -> b(a(b(p()))) b(a(b(p()))) -> a(b(a(p()))) a(b(p())) -> a(b(a(p()))) a(b(a(p()))) -> a(b(a(p()))) b(a(p())) -> b(a(b(b(p())))) b(a(b(b(p())))) -> a(b(a(b(p())))) a(b(p())) -> a(b(a(b(p())))) b(a(p())) -> b(a(b(b(p())))) b(a(b(b(p())))) -> a(b(a(b(p())))) a(b(p())) -> a(b(a(p()))) a(b(a(p()))) -> a(b(a(b(p())))) b(a(p())) -> b(a(b(b(p())))) b(a(b(b(p())))) -> a(b(a(b(p())))) a(b(p())) -> a(b(a(b(p())))) a(b(a(b(p())))) -> a(b(a(b(p())))) b(a(p())) -> b(a(b(a(p())))) b(a(b(a(p())))) -> a(b(a(a(p())))) a(b(p())) -> a(b(a(a(p())))) b(a(p())) -> b(a(b(a(p())))) b(a(b(a(p())))) -> a(b(a(a(p())))) a(b(p())) -> a(b(a(p()))) a(b(a(p()))) -> a(b(a(a(p())))) b(a(p())) -> b(a(b(a(p())))) b(a(b(a(p())))) -> a(b(a(a(p())))) a(b(p())) -> a(b(a(a(p())))) a(b(a(a(p())))) -> a(b(a(a(p())))) p() -> b(a(p())) p() -> a(a(p())) b(a(p())) -> b(a(b(b(p())))) b(a(b(b(p())))) -> a(b(a(b(p())))) a(a(p())) -> a(a(b(a(p())))) a(a(b(a(p())))) -> a(b(a(b(p())))) p() -> a(b(p())) p() -> b(p()) a(b(p())) -> a(b(a(p()))) b(p()) -> b(a(b(p()))) b(a(b(p()))) -> a(b(a(p()))) a(b(p())) -> a(b(a(p()))) a(b(a(p()))) -> a(b(a(p()))) b(p()) -> b(a(b(p()))) b(a(b(p()))) -> a(b(a(p()))) a(b(p())) -> a(b(a(p()))) a(b(a(p()))) -> b(a(b(p()))) b(p()) -> b(a(b(p()))) a(b(p())) -> a(b(a(p()))) a(b(a(p()))) -> b(a(b(p()))) b(p()) -> b(a(p())) b(a(p())) -> b(a(b(p()))) a(b(p())) -> a(b(a(p()))) a(b(a(p()))) -> b(a(b(p()))) b(p()) -> b(a(b(p()))) b(a(b(p()))) -> b(a(b(p()))) a(b(p())) -> a(b(a(b(p())))) a(b(a(b(p())))) -> b(a(b(b(p())))) b(p()) -> b(a(p())) b(a(p())) -> b(a(b(b(p())))) a(b(p())) -> a(b(a(b(p())))) a(b(a(b(p())))) -> b(a(b(b(p())))) b(p()) -> b(a(b(p()))) b(a(b(p()))) -> b(a(b(b(p())))) a(b(p())) -> a(b(a(a(p())))) a(b(a(a(p())))) -> b(a(b(a(p())))) b(p()) -> b(a(p())) b(a(p())) -> b(a(b(a(p())))) a(b(p())) -> a(b(a(a(p())))) a(b(a(a(p())))) -> b(a(b(a(p())))) b(p()) -> b(a(b(p()))) b(a(b(p()))) -> b(a(b(a(p())))) p() -> a(b(p())) p() -> a(p()) a(p()) -> a(b(p())) a(b(p())) -> a(b(b(p()))) a(p()) -> a(b(b(p()))) a(b(p())) -> a(b(a(p()))) a(p()) -> a(b(a(p()))) p() -> a(b(p())) p() -> b(b(p())) a(b(p())) -> a(b(a(a(p())))) a(b(a(a(p())))) -> b(a(b(a(p())))) b(b(p())) -> b(b(a(b(p())))) b(b(a(b(p())))) -> b(a(b(a(p())))) p() -> a(b(p())) p() -> b(a(p())) a(b(p())) -> a(b(a(p()))) b(a(p())) -> b(a(b(p()))) b(a(b(p()))) -> a(b(a(p()))) a(b(p())) -> a(b(a(p()))) a(b(a(p()))) -> a(b(a(p()))) b(a(p())) -> b(a(b(p()))) b(a(b(p()))) -> a(b(a(p()))) a(b(p())) -> a(b(a(b(p())))) b(a(p())) -> b(a(b(b(p())))) b(a(b(b(p())))) -> a(b(a(b(p())))) a(b(p())) -> a(b(a(p()))) a(b(a(p()))) -> a(b(a(b(p())))) b(a(p())) -> b(a(b(b(p())))) b(a(b(b(p())))) -> a(b(a(b(p())))) a(b(p())) -> a(b(a(b(p())))) a(b(a(b(p())))) -> a(b(a(b(p())))) b(a(p())) -> b(a(b(b(p())))) b(a(b(b(p())))) -> a(b(a(b(p())))) a(b(p())) -> a(b(a(a(p())))) b(a(p())) -> b(a(b(a(p())))) b(a(b(a(p())))) -> a(b(a(a(p())))) a(b(p())) -> a(b(a(p()))) a(b(a(p()))) -> a(b(a(a(p())))) b(a(p())) -> b(a(b(a(p())))) b(a(b(a(p())))) -> a(b(a(a(p())))) a(b(p())) -> a(b(a(a(p())))) a(b(a(a(p())))) -> a(b(a(a(p())))) b(a(p())) -> b(a(b(a(p())))) b(a(b(a(p())))) -> a(b(a(a(p())))) a(b(p())) -> a(b(a(p()))) a(b(a(p()))) -> b(a(b(p()))) b(a(p())) -> b(a(b(p()))) a(b(p())) -> a(b(a(p()))) a(b(a(p()))) -> b(a(b(p()))) b(a(p())) -> b(a(b(p()))) b(a(b(p()))) -> b(a(b(p()))) a(b(p())) -> a(b(a(b(p())))) a(b(a(b(p())))) -> b(a(b(b(p())))) b(a(p())) -> b(a(b(b(p())))) a(b(p())) -> a(b(a(b(p())))) a(b(a(b(p())))) -> b(a(b(b(p())))) b(a(p())) -> b(a(b(p()))) b(a(b(p()))) -> b(a(b(b(p())))) a(b(p())) -> a(b(a(b(p())))) a(b(a(b(p())))) -> b(a(b(b(p())))) b(a(p())) -> b(a(b(b(p())))) b(a(b(b(p())))) -> b(a(b(b(p())))) a(b(p())) -> a(b(a(a(p())))) a(b(a(a(p())))) -> b(a(b(a(p())))) b(a(p())) -> b(a(b(a(p())))) a(b(p())) -> a(b(a(a(p())))) a(b(a(a(p())))) -> b(a(b(a(p())))) b(a(p())) -> b(a(b(p()))) b(a(b(p()))) -> b(a(b(a(p())))) a(b(p())) -> a(b(a(a(p())))) a(b(a(a(p())))) -> b(a(b(a(p())))) b(a(p())) -> b(a(b(a(p())))) b(a(b(a(p())))) -> b(a(b(a(p())))) p() -> a(b(p())) p() -> a(a(p())) a(b(p())) -> a(b(a(b(p())))) a(a(p())) -> a(a(b(a(p())))) a(a(b(a(p())))) -> a(b(a(b(p())))) a(b(p())) -> a(b(a(p()))) a(b(a(p()))) -> a(b(a(b(p())))) a(a(p())) -> a(a(b(a(p())))) a(a(b(a(p())))) -> a(b(a(b(p())))) a(b(p())) -> a(b(a(b(p())))) a(b(a(b(p())))) -> a(b(a(b(p())))) a(a(p())) -> a(a(b(a(p())))) a(a(b(a(p())))) -> a(b(a(b(p())))) a(b(p())) -> a(b(a(b(p())))) a(b(a(b(p())))) -> a(a(b(a(p())))) a(a(p())) -> a(a(b(a(p())))) a(b(p())) -> a(b(a(b(p())))) a(b(a(b(p())))) -> a(a(b(a(p())))) a(a(p())) -> a(a(b(p()))) a(a(b(p()))) -> a(a(b(a(p())))) a(b(p())) -> a(b(a(b(p())))) a(b(a(b(p())))) -> a(a(b(a(p())))) a(a(p())) -> a(a(b(a(p())))) a(a(b(a(p())))) -> a(a(b(a(p())))) p() -> a(a(p())) p() -> b(p()) a(a(p())) -> a(a(b(a(p())))) a(a(b(a(p())))) -> a(b(a(b(p())))) b(p()) -> b(a(p())) b(a(p())) -> b(a(b(b(p())))) b(a(b(b(p())))) -> a(b(a(b(p())))) a(a(p())) -> a(a(b(a(p())))) a(a(b(a(p())))) -> a(b(a(b(p())))) b(p()) -> b(a(b(p()))) b(a(b(p()))) -> b(a(b(b(p())))) b(a(b(b(p())))) -> a(b(a(b(p())))) a(a(p())) -> a(a(b(a(p())))) a(a(b(a(p())))) -> a(b(a(b(p())))) b(p()) -> b(a(b(p()))) b(a(b(p()))) -> a(b(a(p()))) a(b(a(p()))) -> a(b(a(b(p())))) a(a(p())) -> a(a(b(p()))) a(a(b(p()))) -> a(a(b(a(p())))) a(a(b(a(p())))) -> a(b(a(b(p())))) b(p()) -> b(a(p())) b(a(p())) -> b(a(b(b(p())))) b(a(b(b(p())))) -> a(b(a(b(p())))) a(a(p())) -> a(a(b(p()))) a(a(b(p()))) -> a(a(b(a(p())))) a(a(b(a(p())))) -> a(b(a(b(p())))) b(p()) -> b(a(b(p()))) b(a(b(p()))) -> b(a(b(b(p())))) b(a(b(b(p())))) -> a(b(a(b(p())))) a(a(p())) -> a(a(b(p()))) a(a(b(p()))) -> a(a(b(a(p())))) a(a(b(a(p())))) -> a(b(a(b(p())))) b(p()) -> b(a(b(p()))) b(a(b(p()))) -> a(b(a(p()))) a(b(a(p()))) -> a(b(a(b(p())))) a(a(p())) -> a(a(b(a(p())))) a(a(b(a(p())))) -> a(a(b(a(p())))) a(a(b(a(p())))) -> a(b(a(b(p())))) b(p()) -> b(a(p())) b(a(p())) -> b(a(b(b(p())))) b(a(b(b(p())))) -> a(b(a(b(p())))) a(a(p())) -> a(a(b(a(p())))) a(a(b(a(p())))) -> a(a(b(a(p())))) a(a(b(a(p())))) -> a(b(a(b(p())))) b(p()) -> b(a(b(p()))) b(a(b(p()))) -> b(a(b(b(p())))) b(a(b(b(p())))) -> a(b(a(b(p())))) a(a(p())) -> a(a(b(a(p())))) a(a(b(a(p())))) -> a(a(b(a(p())))) a(a(b(a(p())))) -> a(b(a(b(p())))) b(p()) -> b(a(b(p()))) b(a(b(p()))) -> a(b(a(p()))) a(b(a(p()))) -> a(b(a(b(p())))) a(a(p())) -> a(a(b(a(p())))) a(a(b(a(p())))) -> a(b(a(b(p())))) a(b(a(b(p())))) -> a(b(a(b(p())))) b(p()) -> b(a(p())) b(a(p())) -> b(a(b(b(p())))) b(a(b(b(p())))) -> a(b(a(b(p())))) a(a(p())) -> a(a(b(a(p())))) a(a(b(a(p())))) -> a(b(a(b(p())))) a(b(a(b(p())))) -> a(b(a(b(p())))) b(p()) -> b(a(b(p()))) b(a(b(p()))) -> b(a(b(b(p())))) b(a(b(b(p())))) -> a(b(a(b(p())))) a(a(p())) -> a(a(b(a(p())))) a(a(b(a(p())))) -> a(b(a(b(p())))) a(b(a(b(p())))) -> a(b(a(b(p())))) b(p()) -> b(a(b(p()))) b(a(b(p()))) -> a(b(a(p()))) a(b(a(p()))) -> a(b(a(b(p())))) a(a(p())) -> a(a(b(p()))) a(a(b(p()))) -> a(a(b(a(b(p()))))) a(a(b(a(b(p()))))) -> a(b(a(b(b(p()))))) b(p()) -> b(a(b(p()))) b(a(b(p()))) -> a(b(a(p()))) a(b(a(p()))) -> a(b(a(b(b(p()))))) a(a(p())) -> a(a(b(p()))) a(a(b(p()))) -> a(a(b(a(b(p()))))) a(a(b(a(b(p()))))) -> a(b(a(b(b(p()))))) b(p()) -> b(a(b(p()))) b(a(b(p()))) -> b(a(b(b(b(p()))))) b(a(b(b(b(p()))))) -> a(b(a(b(b(p()))))) a(a(p())) -> a(a(b(a(p())))) a(a(b(a(p())))) -> a(a(b(a(b(p()))))) a(a(b(a(b(p()))))) -> a(b(a(b(b(p()))))) b(p()) -> b(a(b(p()))) b(a(b(p()))) -> a(b(a(p()))) a(b(a(p()))) -> a(b(a(b(b(p()))))) a(a(p())) -> a(a(b(a(p())))) a(a(b(a(p())))) -> a(a(b(a(b(p()))))) a(a(b(a(b(p()))))) -> a(b(a(b(b(p()))))) b(p()) -> b(a(b(p()))) b(a(b(p()))) -> b(a(b(b(b(p()))))) b(a(b(b(b(p()))))) -> a(b(a(b(b(p()))))) a(a(p())) -> a(a(b(a(p())))) a(a(b(a(p())))) -> a(b(a(b(p())))) a(b(a(b(p())))) -> a(b(a(b(b(p()))))) b(p()) -> b(a(b(p()))) b(a(b(p()))) -> a(b(a(p()))) a(b(a(p()))) -> a(b(a(b(b(p()))))) a(a(p())) -> a(a(b(a(p())))) a(a(b(a(p())))) -> a(b(a(b(p())))) a(b(a(b(p())))) -> a(b(a(b(b(p()))))) b(p()) -> b(a(b(p()))) b(a(b(p()))) -> b(a(b(b(b(p()))))) b(a(b(b(b(p()))))) -> a(b(a(b(b(p()))))) a(a(p())) -> a(a(b(p()))) a(a(b(p()))) -> a(a(b(a(a(p()))))) a(a(b(a(a(p()))))) -> a(b(a(b(a(p()))))) b(p()) -> b(a(b(p()))) b(a(b(p()))) -> a(b(a(p()))) a(b(a(p()))) -> a(b(a(b(a(p()))))) a(a(p())) -> a(a(b(p()))) a(a(b(p()))) -> a(a(b(a(a(p()))))) a(a(b(a(a(p()))))) -> a(b(a(b(a(p()))))) b(p()) -> b(a(b(p()))) b(a(b(p()))) -> b(a(b(b(a(p()))))) b(a(b(b(a(p()))))) -> a(b(a(b(a(p()))))) a(a(p())) -> a(a(b(a(p())))) a(a(b(a(p())))) -> a(a(b(a(a(p()))))) a(a(b(a(a(p()))))) -> a(b(a(b(a(p()))))) b(p()) -> b(a(b(p()))) b(a(b(p()))) -> a(b(a(p()))) a(b(a(p()))) -> a(b(a(b(a(p()))))) a(a(p())) -> a(a(b(a(p())))) a(a(b(a(p())))) -> a(a(b(a(a(p()))))) a(a(b(a(a(p()))))) -> a(b(a(b(a(p()))))) b(p()) -> b(a(b(p()))) b(a(b(p()))) -> b(a(b(b(a(p()))))) b(a(b(b(a(p()))))) -> a(b(a(b(a(p()))))) a(a(p())) -> a(a(b(a(p())))) a(a(b(a(p())))) -> a(b(a(b(p())))) a(b(a(b(p())))) -> a(b(a(b(a(p()))))) b(p()) -> b(a(b(p()))) b(a(b(p()))) -> a(b(a(p()))) a(b(a(p()))) -> a(b(a(b(a(p()))))) a(a(p())) -> a(a(b(a(p())))) a(a(b(a(p())))) -> a(b(a(b(p())))) a(b(a(b(p())))) -> a(b(a(b(a(p()))))) b(p()) -> b(a(b(p()))) b(a(b(p()))) -> b(a(b(b(a(p()))))) b(a(b(b(a(p()))))) -> a(b(a(b(a(p()))))) a(a(p())) -> a(a(b(a(p())))) a(a(b(a(p())))) -> a(b(a(b(p())))) a(b(a(b(p())))) -> b(a(b(b(p())))) b(p()) -> b(a(p())) b(a(p())) -> b(a(b(b(p())))) a(a(p())) -> a(a(b(a(p())))) a(a(b(a(p())))) -> a(b(a(b(p())))) a(b(a(b(p())))) -> b(a(b(b(p())))) b(p()) -> b(a(b(p()))) b(a(b(p()))) -> b(a(b(b(p())))) a(a(p())) -> a(a(b(a(p())))) a(a(b(a(p())))) -> a(b(a(b(p())))) a(b(a(b(p())))) -> b(a(b(b(p())))) b(p()) -> b(a(p())) b(a(p())) -> b(a(b(p()))) b(a(b(p()))) -> b(a(b(b(p())))) a(a(p())) -> a(a(b(a(p())))) a(a(b(a(p())))) -> a(b(a(b(p())))) a(b(a(b(p())))) -> b(a(b(b(p())))) b(p()) -> b(a(b(p()))) b(a(b(p()))) -> b(a(b(p()))) b(a(b(p()))) -> b(a(b(b(p())))) a(a(p())) -> a(a(b(a(p())))) a(a(b(a(p())))) -> a(b(a(b(p())))) a(b(a(b(p())))) -> b(a(b(b(p())))) b(p()) -> b(a(p())) b(a(p())) -> b(a(b(b(p())))) b(a(b(b(p())))) -> b(a(b(b(p())))) a(a(p())) -> a(a(b(a(p())))) a(a(b(a(p())))) -> a(b(a(b(p())))) a(b(a(b(p())))) -> b(a(b(b(p())))) b(p()) -> b(a(b(p()))) b(a(b(p()))) -> b(a(b(b(p())))) b(a(b(b(p())))) -> b(a(b(b(p())))) p() -> a(a(p())) p() -> a(p()) a(p()) -> a(a(p())) a(a(p())) -> a(a(b(p()))) a(p()) -> a(a(b(p()))) a(a(p())) -> a(a(a(p()))) a(p()) -> a(a(a(p()))) p() -> a(a(p())) p() -> b(b(p())) a(a(p())) -> a(a(b(a(p())))) a(a(b(a(p())))) -> a(b(a(b(p())))) a(b(a(b(p())))) -> b(a(b(b(p())))) b(a(b(b(p())))) -> b(a(b(b(a(b(p())))))) b(b(p())) -> b(b(a(b(p())))) b(b(a(b(p())))) -> b(a(b(a(p())))) b(a(b(a(p())))) -> b(a(b(a(b(a(p())))))) b(a(b(a(b(a(p())))))) -> b(a(b(b(a(b(p())))))) a(a(p())) -> a(a(b(a(p())))) a(a(b(a(p())))) -> a(b(a(b(p())))) a(b(a(b(p())))) -> b(a(b(b(p())))) b(a(b(b(p())))) -> b(a(b(b(a(b(p())))))) b(b(p())) -> b(b(a(b(p())))) b(b(a(b(p())))) -> b(b(a(b(b(a(p())))))) b(b(a(b(b(a(p())))))) -> b(a(b(a(b(a(p())))))) b(a(b(a(b(a(p())))))) -> b(a(b(b(a(b(p())))))) a(a(p())) -> a(a(b(a(p())))) a(a(b(a(p())))) -> a(b(a(b(p())))) a(b(a(b(p())))) -> a(b(a(b(a(b(p())))))) a(b(a(b(a(b(p())))))) -> b(a(b(b(a(b(p())))))) b(b(p())) -> b(b(a(b(p())))) b(b(a(b(p())))) -> b(a(b(a(p())))) b(a(b(a(p())))) -> b(a(b(a(b(a(p())))))) b(a(b(a(b(a(p())))))) -> b(a(b(b(a(b(p())))))) a(a(p())) -> a(a(b(a(p())))) a(a(b(a(p())))) -> a(b(a(b(p())))) a(b(a(b(p())))) -> a(b(a(b(a(b(p())))))) a(b(a(b(a(b(p())))))) -> b(a(b(b(a(b(p())))))) b(b(p())) -> b(b(a(b(p())))) b(b(a(b(p())))) -> b(b(a(b(b(a(p())))))) b(b(a(b(b(a(p())))))) -> b(a(b(a(b(a(p())))))) b(a(b(a(b(a(p())))))) -> b(a(b(b(a(b(p())))))) a(a(p())) -> a(a(b(a(p())))) a(a(b(a(p())))) -> a(a(b(a(a(b(p())))))) a(a(b(a(a(b(p())))))) -> a(b(a(b(a(b(p())))))) a(b(a(b(a(b(p())))))) -> b(a(b(b(a(b(p())))))) b(b(p())) -> b(b(a(b(p())))) b(b(a(b(p())))) -> b(a(b(a(p())))) b(a(b(a(p())))) -> b(a(b(a(b(a(p())))))) b(a(b(a(b(a(p())))))) -> b(a(b(b(a(b(p())))))) a(a(p())) -> a(a(b(a(p())))) a(a(b(a(p())))) -> a(a(b(a(a(b(p())))))) a(a(b(a(a(b(p())))))) -> a(b(a(b(a(b(p())))))) a(b(a(b(a(b(p())))))) -> b(a(b(b(a(b(p())))))) b(b(p())) -> b(b(a(b(p())))) b(b(a(b(p())))) -> b(b(a(b(b(a(p())))))) b(b(a(b(b(a(p())))))) -> b(a(b(a(b(a(p())))))) b(a(b(a(b(a(p())))))) -> b(a(b(b(a(b(p())))))) a(a(p())) -> a(a(b(a(p())))) a(a(b(a(p())))) -> a(b(a(b(p())))) a(b(a(b(p())))) -> a(b(a(b(a(b(p())))))) a(b(a(b(a(b(p())))))) -> a(b(a(a(b(a(p())))))) b(b(p())) -> b(b(a(b(p())))) b(b(a(b(p())))) -> b(a(b(a(p())))) b(a(b(a(p())))) -> a(b(a(a(p())))) a(b(a(a(p())))) -> a(b(a(a(b(a(p())))))) a(a(p())) -> a(a(b(a(p())))) a(a(b(a(p())))) -> a(b(a(b(p())))) a(b(a(b(p())))) -> a(b(a(b(a(b(p())))))) a(b(a(b(a(b(p())))))) -> a(b(a(a(b(a(p())))))) b(b(p())) -> b(b(a(b(p())))) b(b(a(b(p())))) -> b(a(b(a(p())))) b(a(b(a(p())))) -> b(a(b(a(b(a(p())))))) b(a(b(a(b(a(p())))))) -> a(b(a(a(b(a(p())))))) a(a(p())) -> a(a(b(a(p())))) a(a(b(a(p())))) -> a(b(a(b(p())))) a(b(a(b(p())))) -> a(b(a(b(a(b(p())))))) a(b(a(b(a(b(p())))))) -> a(b(a(a(b(a(p())))))) b(b(p())) -> b(b(a(b(p())))) b(b(a(b(p())))) -> b(b(a(b(b(a(p())))))) b(b(a(b(b(a(p())))))) -> b(a(b(a(b(a(p())))))) b(a(b(a(b(a(p())))))) -> a(b(a(a(b(a(p())))))) a(a(p())) -> a(a(b(a(p())))) a(a(b(a(p())))) -> a(a(b(a(a(b(p())))))) a(a(b(a(a(b(p())))))) -> a(b(a(b(a(b(p())))))) a(b(a(b(a(b(p())))))) -> a(b(a(a(b(a(p())))))) b(b(p())) -> b(b(a(b(p())))) b(b(a(b(p())))) -> b(a(b(a(p())))) b(a(b(a(p())))) -> a(b(a(a(p())))) a(b(a(a(p())))) -> a(b(a(a(b(a(p())))))) a(a(p())) -> a(a(b(a(p())))) a(a(b(a(p())))) -> a(a(b(a(a(b(p())))))) a(a(b(a(a(b(p())))))) -> a(b(a(b(a(b(p())))))) a(b(a(b(a(b(p())))))) -> a(b(a(a(b(a(p())))))) b(b(p())) -> b(b(a(b(p())))) b(b(a(b(p())))) -> b(a(b(a(p())))) b(a(b(a(p())))) -> b(a(b(a(b(a(p())))))) b(a(b(a(b(a(p())))))) -> a(b(a(a(b(a(p())))))) a(a(p())) -> a(a(b(a(p())))) a(a(b(a(p())))) -> a(a(b(a(a(b(p())))))) a(a(b(a(a(b(p())))))) -> a(b(a(b(a(b(p())))))) a(b(a(b(a(b(p())))))) -> a(b(a(a(b(a(p())))))) b(b(p())) -> b(b(a(b(p())))) b(b(a(b(p())))) -> b(b(a(b(b(a(p())))))) b(b(a(b(b(a(p())))))) -> b(a(b(a(b(a(p())))))) b(a(b(a(b(a(p())))))) -> a(b(a(a(b(a(p())))))) p() -> a(a(p())) p() -> b(a(p())) a(a(p())) -> a(a(b(a(p())))) a(a(b(a(p())))) -> a(b(a(b(p())))) b(a(p())) -> b(a(b(b(p())))) b(a(b(b(p())))) -> a(b(a(b(p())))) p() -> a(a(p())) p() -> a(b(p())) a(a(p())) -> a(a(b(a(p())))) a(b(p())) -> a(b(a(b(p())))) a(b(a(b(p())))) -> a(a(b(a(p())))) a(a(p())) -> a(a(b(p()))) a(a(b(p()))) -> a(a(b(a(p())))) a(b(p())) -> a(b(a(b(p())))) a(b(a(b(p())))) -> a(a(b(a(p())))) a(a(p())) -> a(a(b(a(p())))) a(a(b(a(p())))) -> a(a(b(a(p())))) a(b(p())) -> a(b(a(b(p())))) a(b(a(b(p())))) -> a(a(b(a(p())))) a(a(p())) -> a(a(b(a(p())))) a(a(b(a(p())))) -> a(b(a(b(p())))) a(b(p())) -> a(b(a(b(p())))) a(a(p())) -> a(a(b(a(p())))) a(a(b(a(p())))) -> a(b(a(b(p())))) a(b(p())) -> a(b(a(p()))) a(b(a(p()))) -> a(b(a(b(p())))) a(a(p())) -> a(a(b(a(p())))) a(a(b(a(p())))) -> a(b(a(b(p())))) a(b(p())) -> a(b(a(b(p())))) a(b(a(b(p())))) -> a(b(a(b(p())))) b(a(b(x))) -> b(a(b(x))) b(a(b(x))) -> a(b(a(x))) a(b(a(x))) -> b(a(b(x))) b(a(b(x))) -> a(b(a(x))) b(a(b(a(b(x104))))) -> b(a(b(a(b(x104))))) b(a(b(a(b(x104))))) -> a(b(a(a(b(x104))))) a(b(a(a(b(x104))))) -> b(a(b(a(b(x104))))) b(a(b(a(b(x104))))) -> a(b(a(a(b(x104))))) a(b(a(b(x105)))) -> a(b(a(b(x105)))) a(b(a(b(x105)))) -> b(a(b(b(x105)))) b(a(b(b(x105)))) -> a(b(a(b(x105)))) a(b(a(b(x105)))) -> b(a(b(b(x105)))) b(a(b(a(b(x106))))) -> b(a(b(a(b(x106))))) b(a(b(a(b(x106))))) -> b(a(b(a(b(x106))))) a(b(a(b(x107)))) -> a(b(a(b(x107)))) a(b(a(b(x107)))) -> a(b(a(b(x107)))) b(a(b(a(x108)))) -> b(a(b(a(x108)))) b(a(b(a(x108)))) -> a(b(a(a(x108)))) a(b(a(a(x108)))) -> b(a(b(a(x108)))) b(a(b(a(x108)))) -> a(b(a(a(x108)))) a(b(a(x))) -> a(b(a(x))) a(b(a(x))) -> b(a(b(x))) b(a(b(x))) -> a(b(a(x))) a(b(a(x))) -> b(a(b(x))) a(b(a(b(a(x110))))) -> a(b(a(b(a(x110))))) a(b(a(b(a(x110))))) -> b(a(b(b(a(x110))))) b(a(b(b(a(x110))))) -> a(b(a(b(a(x110))))) a(b(a(b(a(x110))))) -> b(a(b(b(a(x110))))) b(a(b(a(x111)))) -> b(a(b(a(x111)))) b(a(b(a(x111)))) -> b(a(b(a(x111)))) a(b(a(b(a(x112))))) -> a(b(a(b(a(x112))))) a(b(a(b(a(x112))))) -> a(b(a(b(a(x112))))) weak: p() -> b(p()) p() -> a(p()) b(a(b(x))) -> a(b(a(x))) a(b(a(x))) -> b(a(b(x))) p() -> b(b(p())) p() -> b(a(p())) p() -> a(b(p())) p() -> a(a(p())) b(a(b(x))) -> b(a(b(x))) a(b(a(x))) -> a(b(a(x))) Shift Processor (ldh) lab=left (force): strict: weak: Rule Labeling Processor: strict: weak: rule labeling (right): p() -> b(p()): 2 p() -> a(p()): 2 b(a(b(x))) -> a(b(a(x))): 0 a(b(a(x))) -> b(a(b(x))): 0 p() -> b(b(p())): 8 p() -> b(a(p())): 2 p() -> a(b(p())): 2 p() -> a(a(p())): 8 b(a(b(x))) -> b(a(b(x))): 0 a(b(a(x))) -> a(b(a(x))): 0 Decreasing Processor: The following diagrams are decreasing: peak: b(p()) <-0|[==1,==2]- p() -1|[==1,==2]-> a(p()) joins (1): b(p()) -6|0[==1,==2]-> b(a(b(p()))) a(p()) -5|0[==1,==2]-> a(b(a(p()))) -3|[==1,>>0]-> b(a(b(p()))) peak: b(p()) <-0|[==1,=>2]- p() -4|[==1,?=8]-> b(b(p())) joins (1): b(p()) -0|0[==1,=>2]-> b(b(p())) peak: b(p()) <-0|[==1,==2]- p() -5|[==1,==2]-> b(a(p())) joins (1): b(p()) -1|0[==1,==2]-> b(a(p())) peak: b(p()) <-0|[==1,==2]- p() -6|[==1,==2]-> a(b(p())) joins (1): b(p()) -6|0[==1,==2]-> b(a(b(p()))) a(b(p())) -1|0,0[==1,==2]-> a(b(a(p()))) -3|[==1,>>0]-> b(a(b(p()))) peak: b(p()) <-0|[==1,=>2]- p() -7|[==1,?=8]-> a(a(p())) joins (1): b(p()) -6|0[==1,=>2]-> b(a(b(p()))) -0|0,0,0[==1,=>2]-> b(a(b(b(p())))) a(a(p())) -5|0,0[==1,=>2]-> a(a(b(a(p())))) -3|0[==1,>>0]-> a(b(a(b(p())))) -3|[==1,>>0]-> b(a(b(b(p())))) peak: a(p()) <-1|[==1,==2]- p() -0|[==1,==2]-> b(p()) joins (1): a(p()) -5|0[==1,==2]-> a(b(a(p()))) b(p()) -6|0[==1,==2]-> b(a(b(p()))) -2|[==1,>>0]-> a(b(a(p()))) peak: a(p()) <-1|[==1,=>2]- p() -4|[==1,?=8]-> b(b(p())) joins (1): a(p()) -5|0[==1,=>2]-> a(b(a(p()))) -1|0,0,0[==1,=>2]-> a(b(a(a(p())))) b(b(p())) -6|0,0[==1,=>2]-> b(b(a(b(p())))) -2|0[==1,>>0]-> b(a(b(a(p())))) -2|[==1,>>0]-> a(b(a(a(p())))) peak: a(p()) <-1|[==1,==2]- p() -5|[==1,==2]-> b(a(p())) joins (1): a(p()) -5|0[==1,==2]-> a(b(a(p()))) b(a(p())) -0|0,0[==1,==2]-> b(a(b(p()))) -2|[==1,>>0]-> a(b(a(p()))) peak: a(p()) <-1|[==1,==2]- p() -6|[==1,==2]-> a(b(p())) joins (1): a(p()) -0|0[==1,==2]-> a(b(p())) peak: a(p()) <-1|[==1,=>2]- p() -7|[==1,?=8]-> a(a(p())) joins (1): a(p()) -1|0[==1,=>2]-> a(a(p())) peak: b(a(a(b(a(x93))))) <-2|0,0[==1,==0]- b(a(b(a(b(x93))))) -2|[==1,==0]-> a(b(a(a(b(x93))))) joins (1): b(a(a(b(a(x93))))) -3|0,0[==1,==0]-> b(a(b(a(b(x93))))) a(b(a(a(b(x93))))) -3|[==1,==0]-> b(a(b(a(b(x93))))) peak: a(a(b(a(x94)))) <-2|0[==1,==0]- a(b(a(b(x94)))) -3|[==1,==0]-> b(a(b(b(x94)))) joins (1): a(a(b(a(x94)))) -3|0[==1,==0]-> a(b(a(b(x94)))) b(a(b(b(x94)))) -2|[==1,==0]-> a(b(a(b(x94)))) peak: a(b(a(x))) <-2|[==1,==0]- b(a(b(x))) -8|[==1,==0]-> b(a(b(x))) joins (1): b(a(b(x))) -2|[==1,==0]-> a(b(a(x))) peak: b(a(a(b(a(x96))))) <-2|0,0[==1,==0]- b(a(b(a(b(x96))))) -8|[==1,==0]-> b(a(b(a(b(x96))))) joins (1): b(a(b(a(b(x96))))) -2|0,0[==1,==0]-> b(a(a(b(a(x96))))) peak: a(a(b(a(x97)))) <-2|0[==1,==0]- a(b(a(b(x97)))) -9|[==1,==0]-> a(b(a(b(x97)))) joins (1): a(b(a(b(x97)))) -2|0[==1,==0]-> a(a(b(a(x97)))) peak: b(b(a(b(x98)))) <-3|0[==1,==0]- b(a(b(a(x98)))) -2|[==1,==0]-> a(b(a(a(x98)))) joins (1): b(b(a(b(x98)))) -2|0[==1,==0]-> b(a(b(a(x98)))) a(b(a(a(x98)))) -3|[==1,==0]-> b(a(b(a(x98)))) peak: a(b(b(a(b(x99))))) <-3|0,0[==1,==0]- a(b(a(b(a(x99))))) -3|[==1,==0]-> b(a(b(b(a(x99))))) joins (1): a(b(b(a(b(x99))))) -2|0,0[==1,==0]-> a(b(a(b(a(x99))))) b(a(b(b(a(x99))))) -2|[==1,==0]-> a(b(a(b(a(x99))))) peak: b(b(a(b(x100)))) <-3|0[==1,==0]- b(a(b(a(x100)))) -8|[==1,==0]-> b(a(b(a(x100)))) joins (1): b(a(b(a(x100)))) -3|0[==1,==0]-> b(b(a(b(x100)))) peak: b(a(b(x))) <-3|[==1,==0]- a(b(a(x))) -9|[==1,==0]-> a(b(a(x))) joins (1): a(b(a(x))) -3|[==1,==0]-> b(a(b(x))) peak: a(b(b(a(b(x102))))) <-3|0,0[==1,==0]- a(b(a(b(a(x102))))) -9| [==1,==0]-> a(b(a(b(a(x102))))) joins (1): a(b(a(b(a(x102))))) -3|0,0[==1,==0]-> a(b(b(a(b(x102))))) peak: b(b(p())) <-4|[==1,=?8]- p() -0|[==1,>=2]-> b(p()) joins (1): b(p()) -0|0[==1,>=2]-> b(b(p())) peak: b(b(p())) <-4|[==1,=?8]- p() -1|[==1,>=2]-> a(p()) joins (1): b(b(p())) -6|0,0[==1,>=2]-> b(b(a(b(p())))) -2|0[==1,>>0]-> b(a(b(a(p())))) a(p()) -5|0[==1,>=2]-> a(b(a(p()))) -1|0,0,0[==1,>=2]-> a(b(a(a(p())))) -3| [==1,>>0]-> b(a(b(a(p())))) peak: b(b(p())) <-4|[==1,=?8]- p() -5|[==1,>=2]-> b(a(p())) joins (1): b(b(p())) -6|0,0[==1,>=2]-> b(b(a(b(p())))) b(a(p())) -5|0,0[==1,>=2]-> b(a(b(a(p())))) -3|0[==1,>>0]-> b(b(a(b(p())))) peak: b(b(p())) <-4|[==1,=?8]- p() -6|[==1,>=2]-> a(b(p())) joins (1): b(b(p())) -6|0,0[==1,>=2]-> b(b(a(b(p())))) -2|0[==1,>>0]-> b(a(b(a(p())))) a(b(p())) -7|0,0[==1,=?8]-> a(b(a(a(p())))) -3|[==1,>>0]-> b(a(b(a(p())))) peak: b(b(p())) <-4|[==1,==8]- p() -7|[==1,==8]-> a(a(p())) joins (1): b(b(p())) -6|0,0[==1,>>2]-> b(b(a(b(p())))) -2|0[==1,>>0]-> b(a(b(a(p())))) -2|[==1,>>0]-> a(b(a(a(p())))) -5|0,0,0,0[ ==1,>>2]-> a(b(a(a(b(a(p())))))) a(a(p())) -5|0,0[==1,>>2]-> a(a(b(a(p())))) -3|0[==1,>>0]-> a(b(a(b(p())))) -6|0,0,0,0[==1,>>2]-> a(b(a(b(a(b(p())))))) -2| 0,0,0[==1,>>0]-> a(b(a(a(b(a(p())))))) peak: b(a(p())) <-5|[==1,==2]- p() -0|[==1,==2]-> b(p()) joins (1): b(p()) -1|0[==1,==2]-> b(a(p())) peak: b(a(p())) <-5|[==1,==2]- p() -1|[==1,==2]-> a(p()) joins (1): b(a(p())) -0|0,0[==1,==2]-> b(a(b(p()))) a(p()) -5|0[==1,==2]-> a(b(a(p()))) -3|[==1,>>0]-> b(a(b(p()))) peak: b(a(p())) <-5|[==1,=>2]- p() -4|[==1,?=8]-> b(b(p())) joins (1): b(a(p())) -5|0,0[==1,=>2]-> b(a(b(a(p())))) b(b(p())) -6|0,0[==1,=>2]-> b(b(a(b(p())))) -2|0[==1,>>0]-> b(a(b(a(p())))) peak: b(a(p())) <-5|[==1,==2]- p() -6|[==1,==2]-> a(b(p())) joins (1): b(a(p())) -0|0,0[==1,==2]-> b(a(b(p()))) a(b(p())) -1|0,0[==1,==2]-> a(b(a(p()))) -3|[==1,>>0]-> b(a(b(p()))) peak: b(a(p())) <-5|[==1,=>2]- p() -7|[==1,?=8]-> a(a(p())) joins (1): b(a(p())) -4|0,0[==1,?=8]-> b(a(b(b(p())))) -2|[==1,>>0]-> a(b(a(b(p())))) a(a(p())) -5|0,0[==1,=>2]-> a(a(b(a(p())))) -3|0[==1,>>0]-> a(b(a(b(p())))) peak: a(b(p())) <-6|[==1,==2]- p() -0|[==1,==2]-> b(p()) joins (1): a(b(p())) -1|0,0[==1,==2]-> a(b(a(p()))) b(p()) -6|0[==1,==2]-> b(a(b(p()))) -2|[==1,>>0]-> a(b(a(p()))) peak: a(b(p())) <-6|[==1,==2]- p() -1|[==1,==2]-> a(p()) joins (1): a(p()) -0|0[==1,==2]-> a(b(p())) peak: a(b(p())) <-6|[==1,=>2]- p() -4|[==1,?=8]-> b(b(p())) joins (1): a(b(p())) -7|0,0[==1,?=8]-> a(b(a(a(p())))) -3|[==1,>>0]-> b(a(b(a(p())))) b(b(p())) -6|0,0[==1,=>2]-> b(b(a(b(p())))) -2|0[==1,>>0]-> b(a(b(a(p())))) peak: a(b(p())) <-6|[==1,==2]- p() -5|[==1,==2]-> b(a(p())) joins (1): a(b(p())) -1|0,0[==1,==2]-> a(b(a(p()))) b(a(p())) -0|0,0[==1,==2]-> b(a(b(p()))) -2|[==1,>>0]-> a(b(a(p()))) peak: a(b(p())) <-6|[==1,=>2]- p() -7|[==1,?=8]-> a(a(p())) joins (1): a(b(p())) -6|0,0[==1,=>2]-> a(b(a(b(p())))) a(a(p())) -5|0,0[==1,=>2]-> a(a(b(a(p())))) -3|0[==1,>>0]-> a(b(a(b(p())))) peak: a(a(p())) <-7|[==1,=?8]- p() -0|[==1,>=2]-> b(p()) joins (1): a(a(p())) -5|0,0[==1,>=2]-> a(a(b(a(p())))) -3|0[==1,>>0]-> a(b(a(b(p())))) b(p()) -6|0[==1,>=2]-> b(a(b(p()))) -0|0,0,0[==1,>=2]-> b(a(b(b(p())))) -2| [==1,>>0]-> a(b(a(b(p())))) peak: a(a(p())) <-7|[==1,=?8]- p() -1|[==1,>=2]-> a(p()) joins (1): a(p()) -1|0[==1,>=2]-> a(a(p())) peak: a(a(p())) <-7|[==1,==8]- p() -4|[==1,==8]-> b(b(p())) joins (1): a(a(p())) -5|0,0[==1,>>2]-> a(a(b(a(p())))) -3|0[==1,>>0]-> a(b(a(b(p())))) -3|[==1,>>0]-> b(a(b(b(p())))) -6|0,0,0,0[ ==1,>>2]-> b(a(b(b(a(b(p())))))) b(b(p())) -6|0,0[==1,>>2]-> b(b(a(b(p())))) -2|0[==1,>>0]-> b(a(b(a(p())))) -5|0,0,0,0[==1,>>2]-> b(a(b(a(b(a(p())))))) -3| 0,0,0[==1,>>0]-> b(a(b(b(a(b(p())))))) peak: a(a(p())) <-7|[==1,=?8]- p() -5|[==1,>=2]-> b(a(p())) joins (1): a(a(p())) -5|0,0[==1,>=2]-> a(a(b(a(p())))) -3|0[==1,>>0]-> a(b(a(b(p())))) b(a(p())) -4|0,0[==1,=?8]-> b(a(b(b(p())))) -2|[==1,>>0]-> a(b(a(b(p())))) peak: a(a(p())) <-7|[==1,=?8]- p() -6|[==1,>=2]-> a(b(p())) joins (1): a(a(p())) -5|0,0[==1,>=2]-> a(a(b(a(p())))) a(b(p())) -6|0,0[==1,>=2]-> a(b(a(b(p())))) -2|0[==1,>>0]-> a(a(b(a(p())))) peak: b(a(b(x))) <-8|[==1,==0]- b(a(b(x))) -2|[==1,==0]-> a(b(a(x))) joins (1): a(b(a(x))) -3|[==1,==0]-> b(a(b(x))) peak: b(a(b(a(b(x104))))) <-8|0,0[==1,==0]- b(a(b(a(b(x104))))) -2| [==1,==0]-> a(b(a(a(b(x104))))) joins (1): a(b(a(a(b(x104))))) -3|[==1,==0]-> b(a(b(a(b(x104))))) peak: a(b(a(b(x105)))) <-8|0[==1,==0]- a(b(a(b(x105)))) -3|[==1,==0]-> b(a(b(b(x105)))) joins (1): b(a(b(b(x105)))) -2|[==1,==0]-> a(b(a(b(x105)))) peak: b(a(b(a(b(x106))))) <-8|0,0[==1,==0]- b(a(b(a(b(x106))))) -8| [==1,==0]-> b(a(b(a(b(x106))))) joins (1): peak: a(b(a(b(x107)))) <-8|0[==1,==0]- a(b(a(b(x107)))) -9|[==1,==0]-> a(b(a(b(x107)))) joins (1): peak: b(a(b(a(x108)))) <-9|0[==1,==0]- b(a(b(a(x108)))) -2|[==1,==0]-> a(b(a(a(x108)))) joins (1): a(b(a(a(x108)))) -3|[==1,==0]-> b(a(b(a(x108)))) peak: a(b(a(x))) <-9|[==1,==0]- a(b(a(x))) -3|[==1,==0]-> b(a(b(x))) joins (1): b(a(b(x))) -2|[==1,==0]-> a(b(a(x))) peak: a(b(a(b(a(x110))))) <-9|0,0[==1,==0]- a(b(a(b(a(x110))))) -3| [==1,==0]-> b(a(b(b(a(x110))))) joins (1): b(a(b(b(a(x110))))) -2|[==1,==0]-> a(b(a(b(a(x110))))) peak: b(a(b(a(x111)))) <-9|0[==1,==0]- b(a(b(a(x111)))) -8|[==1,==0]-> b(a(b(a(x111)))) joins (1): peak: a(b(a(b(a(x112))))) <-9|0,0[==1,==0]- a(b(a(b(a(x112))))) -9| [==1,==0]-> a(b(a(b(a(x112))))) joins (1): Qed