MAYBE Problem: app(nil(),xs) -> nil() app(cons(x,xs),ys) -> cons(x,app(xs,ys)) rev(nil()) -> nil() rev(cons(x,xs)) -> append(xs,rev(cons(x,nil()))) shuffle(nil()) -> nil() shuffle(cons(x,xs)) -> cons(x,shuffle(rev(xs))) Proof: Complexity Transformation Processor: strict: app(nil(),xs) -> nil() app(cons(x,xs),ys) -> cons(x,app(xs,ys)) rev(nil()) -> nil() rev(cons(x,xs)) -> append(xs,rev(cons(x,nil()))) shuffle(nil()) -> nil() shuffle(cons(x,xs)) -> cons(x,shuffle(rev(xs))) weak: Matrix Interpretation Processor: dimension: 1 max_matrix: 1 interpretation: [shuffle](x0) = x0, [append](x0, x1) = x0 + x1, [rev](x0) = x0, [cons](x0, x1) = x0 + x1, [app](x0, x1) = x0 + x1 + 1, [nil] = 0 orientation: app(nil(),xs) = xs + 1 >= 0 = nil() app(cons(x,xs),ys) = x + xs + ys + 1 >= x + xs + ys + 1 = cons(x,app(xs,ys)) rev(nil()) = 0 >= 0 = nil() rev(cons(x,xs)) = x + xs >= x + xs = append(xs,rev(cons(x,nil()))) shuffle(nil()) = 0 >= 0 = nil() shuffle(cons(x,xs)) = x + xs >= x + xs = cons(x,shuffle(rev(xs))) problem: strict: app(cons(x,xs),ys) -> cons(x,app(xs,ys)) rev(nil()) -> nil() rev(cons(x,xs)) -> append(xs,rev(cons(x,nil()))) shuffle(nil()) -> nil() shuffle(cons(x,xs)) -> cons(x,shuffle(rev(xs))) weak: app(nil(),xs) -> nil() Matrix Interpretation Processor: dimension: 1 max_matrix: 1 interpretation: [shuffle](x0) = x0 + 1, [append](x0, x1) = x0 + x1, [rev](x0) = x0, [cons](x0, x1) = x0 + x1, [app](x0, x1) = x0 + x1, [nil] = 0 orientation: app(cons(x,xs),ys) = x + xs + ys >= x + xs + ys = cons(x,app(xs,ys)) rev(nil()) = 0 >= 0 = nil() rev(cons(x,xs)) = x + xs >= x + xs = append(xs,rev(cons(x,nil()))) shuffle(nil()) = 1 >= 0 = nil() shuffle(cons(x,xs)) = x + xs + 1 >= x + xs + 1 = cons(x,shuffle(rev(xs))) app(nil(),xs) = xs >= 0 = nil() problem: strict: app(cons(x,xs),ys) -> cons(x,app(xs,ys)) rev(nil()) -> nil() rev(cons(x,xs)) -> append(xs,rev(cons(x,nil()))) shuffle(cons(x,xs)) -> cons(x,shuffle(rev(xs))) weak: shuffle(nil()) -> nil() app(nil(),xs) -> nil() Matrix Interpretation Processor: dimension: 1 max_matrix: 1 interpretation: [shuffle](x0) = x0 + 1, [append](x0, x1) = x0 + x1 + 1, [rev](x0) = x0 + 1, [cons](x0, x1) = x0 + x1, [app](x0, x1) = x0 + x1, [nil] = 1 orientation: app(cons(x,xs),ys) = x + xs + ys >= x + xs + ys = cons(x,app(xs,ys)) rev(nil()) = 2 >= 1 = nil() rev(cons(x,xs)) = x + xs + 1 >= x + xs + 3 = append(xs,rev(cons(x,nil()))) shuffle(cons(x,xs)) = x + xs + 1 >= x + xs + 2 = cons(x,shuffle(rev(xs))) shuffle(nil()) = 2 >= 1 = nil() app(nil(),xs) = xs + 1 >= 1 = nil() problem: strict: app(cons(x,xs),ys) -> cons(x,app(xs,ys)) rev(cons(x,xs)) -> append(xs,rev(cons(x,nil()))) shuffle(cons(x,xs)) -> cons(x,shuffle(rev(xs))) weak: rev(nil()) -> nil() shuffle(nil()) -> nil() app(nil(),xs) -> nil() Matrix Interpretation Processor: dimension: 2 max_matrix: [1 1] [0 1] interpretation: [1 1] [1] [shuffle](x0) = [0 1]x0 + [0], [1 0] [1 0] [append](x0, x1) = [0 0]x0 + [0 0]x1, [1 0] [rev](x0) = [0 0]x0, [1 0] [1 0] [1] [cons](x0, x1) = [0 0]x0 + [0 0]x1 + [1], [1 0] [app](x0, x1) = x0 + [0 0]x1, [0] [nil] = [0] orientation: [1 0] [1 0] [1 0] [1] [1 0] [1 0] [1 0] [1] app(cons(x,xs),ys) = [0 0]x + [0 0]xs + [0 0]ys + [1] >= [0 0]x + [0 0]xs + [0 0]ys + [1] = cons(x,app(xs,ys)) [1 0] [1 0] [1] [1 0] [1 0] [1] rev(cons(x,xs)) = [0 0]x + [0 0]xs + [0] >= [0 0]x + [0 0]xs + [0] = append(xs,rev(cons(x,nil()))) [1 0] [1 0] [3] [1 0] [1 0] [2] shuffle(cons(x,xs)) = [0 0]x + [0 0]xs + [1] >= [0 0]x + [0 0]xs + [1] = cons(x,shuffle(rev(xs))) [0] [0] rev(nil()) = [0] >= [0] = nil() [1] [0] shuffle(nil()) = [0] >= [0] = nil() [1 0] [0] app(nil(),xs) = [0 0]xs >= [0] = nil() problem: strict: app(cons(x,xs),ys) -> cons(x,app(xs,ys)) rev(cons(x,xs)) -> append(xs,rev(cons(x,nil()))) weak: shuffle(cons(x,xs)) -> cons(x,shuffle(rev(xs))) rev(nil()) -> nil() shuffle(nil()) -> nil() app(nil(),xs) -> nil() Matrix Interpretation Processor: dimension: 2 max_matrix: [1 1] [0 1] interpretation: [1 1] [shuffle](x0) = [0 1]x0, [1 0] [1 0] [append](x0, x1) = [0 0]x0 + [0 0]x1, [1 1] [rev](x0) = [0 0]x0, [1 1] [0] [cons](x0, x1) = [0 0]x0 + x1 + [1], [1 1] [1 1] [app](x0, x1) = [0 1]x0 + [0 0]x1, [0] [nil] = [0] orientation: [1 1] [1 1] [1 1] [1] [1 1] [1 1] [1 1] [0] app(cons(x,xs),ys) = [0 0]x + [0 1]xs + [0 0]ys + [1] >= [0 0]x + [0 1]xs + [0 0]ys + [1] = cons(x,app(xs,ys)) [1 1] [1 1] [1] [1 1] [1 0] [1] rev(cons(x,xs)) = [0 0]x + [0 0]xs + [0] >= [0 0]x + [0 0]xs + [0] = append(xs,rev(cons(x,nil()))) [1 1] [1 1] [1] [1 1] [1 1] [0] shuffle(cons(x,xs)) = [0 0]x + [0 1]xs + [1] >= [0 0]x + [0 0]xs + [1] = cons(x,shuffle(rev(xs))) [0] [0] rev(nil()) = [0] >= [0] = nil() [0] [0] shuffle(nil()) = [0] >= [0] = nil() [1 1] [0] app(nil(),xs) = [0 0]xs >= [0] = nil() problem: strict: rev(cons(x,xs)) -> append(xs,rev(cons(x,nil()))) weak: app(cons(x,xs),ys) -> cons(x,app(xs,ys)) shuffle(cons(x,xs)) -> cons(x,shuffle(rev(xs))) rev(nil()) -> nil() shuffle(nil()) -> nil() app(nil(),xs) -> nil() Open