YES Problem: app(app(and(),true()),true()) -> true() app(app(and(),x),false()) -> false() app(app(and(),false()),y) -> false() app(app(or(),true()),y) -> true() app(app(or(),x),true()) -> true() app(app(or(),false()),false()) -> false() app(app(forall(),p),nil()) -> true() app(app(forall(),p),app(app(cons(),x),xs)) -> app(app(and(),app(p,x)),app(app(forall(),p),xs)) app(app(forsome(),p),nil()) -> false() app(app(forsome(),p),app(app(cons(),x),xs)) -> app(app(or(),app(p,x)),app(app(forsome(),p),xs)) Proof: DP Processor: DPs: app#(app(forall(),p),app(app(cons(),x),xs)) -> app#(app(forall(),p),xs) app#(app(forall(),p),app(app(cons(),x),xs)) -> app#(p,x) app#(app(forall(),p),app(app(cons(),x),xs)) -> app#(and(),app(p,x)) app#(app(forall(),p),app(app(cons(),x),xs)) -> app#(app(and(),app(p,x)),app(app(forall(),p),xs)) app#(app(forsome(),p),app(app(cons(),x),xs)) -> app#(app(forsome(),p),xs) app#(app(forsome(),p),app(app(cons(),x),xs)) -> app#(p,x) app#(app(forsome(),p),app(app(cons(),x),xs)) -> app#(or(),app(p,x)) app#(app(forsome(),p),app(app(cons(),x),xs)) -> app#(app(or(),app(p,x)),app(app(forsome(),p),xs)) TRS: app(app(and(),true()),true()) -> true() app(app(and(),x),false()) -> false() app(app(and(),false()),y) -> false() app(app(or(),true()),y) -> true() app(app(or(),x),true()) -> true() app(app(or(),false()),false()) -> false() app(app(forall(),p),nil()) -> true() app(app(forall(),p),app(app(cons(),x),xs)) -> app(app(and(),app(p,x)),app(app(forall(),p),xs)) app(app(forsome(),p),nil()) -> false() app(app(forsome(),p),app(app(cons(),x),xs)) -> app(app(or(),app(p,x)),app(app(forsome(),p),xs)) ADG Processor: DPs: app#(app(forall(),p),app(app(cons(),x),xs)) -> app#(app(forall(),p),xs) app#(app(forall(),p),app(app(cons(),x),xs)) -> app#(p,x) app#(app(forall(),p),app(app(cons(),x),xs)) -> app#(and(),app(p,x)) app#(app(forall(),p),app(app(cons(),x),xs)) -> app#(app(and(),app(p,x)),app(app(forall(),p),xs)) app#(app(forsome(),p),app(app(cons(),x),xs)) -> app#(app(forsome(),p),xs) app#(app(forsome(),p),app(app(cons(),x),xs)) -> app#(p,x) app#(app(forsome(),p),app(app(cons(),x),xs)) -> app#(or(),app(p,x)) app#(app(forsome(),p),app(app(cons(),x),xs)) -> app#(app(or(),app(p,x)),app(app(forsome(),p),xs)) TRS: app(app(and(),true()),true()) -> true() app(app(and(),x),false()) -> false() app(app(and(),false()),y) -> false() app(app(or(),true()),y) -> true() app(app(or(),x),true()) -> true() app(app(or(),false()),false()) -> false() app(app(forall(),p),nil()) -> true() app(app(forall(),p),app(app(cons(),x),xs)) -> app(app(and(),app(p,x)),app(app(forall(),p),xs)) app(app(forsome(),p),nil()) -> false() app(app(forsome(),p),app(app(cons(),x),xs)) -> app(app(or(),app(p,x)),app(app(forsome(),p),xs)) graph: app#(app(forsome(),p),app(app(cons(),x),xs)) -> app#(app(forsome(),p),xs) -> app#(app(forsome(),p),app(app(cons(),x),xs)) -> app#(app(forsome(),p),xs) app#(app(forsome(),p),app(app(cons(),x),xs)) -> app#(app(forsome(),p),xs) -> app#(app(forsome(),p),app(app(cons(),x),xs)) -> app#(p,x) app#(app(forsome(),p),app(app(cons(),x),xs)) -> app#(app(forsome(),p),xs) -> app#(app(forsome(),p),app(app(cons(),x),xs)) -> app#(or(),app(p,x)) app#(app(forsome(),p),app(app(cons(),x),xs)) -> app#(app(forsome(),p),xs) -> app#(app(forsome(),p),app(app(cons(),x),xs)) -> app#(app(or(),app(p,x)),app(app(forsome(),p),xs)) app#(app(forsome(),p),app(app(cons(),x),xs)) -> app#(p,x) -> app#(app(forall(),p),app(app(cons(),x),xs)) -> app#(app(forall(),p),xs) app#(app(forsome(),p),app(app(cons(),x),xs)) -> app#(p,x) -> app#(app(forall(),p),app(app(cons(),x),xs)) -> app#(p,x) app#(app(forsome(),p),app(app(cons(),x),xs)) -> app#(p,x) -> app#(app(forall(),p),app(app(cons(),x),xs)) -> app#(and(),app(p,x)) app#(app(forsome(),p),app(app(cons(),x),xs)) -> app#(p,x) -> app#(app(forall(),p),app(app(cons(),x),xs)) -> app#(app(and(),app(p,x)),app(app(forall(),p),xs)) app#(app(forsome(),p),app(app(cons(),x),xs)) -> app#(p,x) -> app#(app(forsome(),p),app(app(cons(),x),xs)) -> app#(app(forsome(),p),xs) app#(app(forsome(),p),app(app(cons(),x),xs)) -> app#(p,x) -> app#(app(forsome(),p),app(app(cons(),x),xs)) -> app#(p,x) app#(app(forsome(),p),app(app(cons(),x),xs)) -> app#(p,x) -> app#(app(forsome(),p),app(app(cons(),x),xs)) -> app#(or(),app(p,x)) app#(app(forsome(),p),app(app(cons(),x),xs)) -> app#(p,x) -> app#(app(forsome(),p),app(app(cons(),x),xs)) -> app#(app(or(),app(p,x)),app(app(forsome(),p),xs)) app#(app(forall(),p),app(app(cons(),x),xs)) -> app#(app(forall(),p),xs) -> app#(app(forall(),p),app(app(cons(),x),xs)) -> app#(app(forall(),p),xs) app#(app(forall(),p),app(app(cons(),x),xs)) -> app#(app(forall(),p),xs) -> app#(app(forall(),p),app(app(cons(),x),xs)) -> app#(p,x) app#(app(forall(),p),app(app(cons(),x),xs)) -> app#(app(forall(),p),xs) -> app#(app(forall(),p),app(app(cons(),x),xs)) -> app#(and(),app(p,x)) app#(app(forall(),p),app(app(cons(),x),xs)) -> app#(app(forall(),p),xs) -> app#(app(forall(),p),app(app(cons(),x),xs)) -> app#(app(and(),app(p,x)),app(app(forall(),p),xs)) app#(app(forall(),p),app(app(cons(),x),xs)) -> app#(p,x) -> app#(app(forall(),p),app(app(cons(),x),xs)) -> app#(app(forall(),p),xs) app#(app(forall(),p),app(app(cons(),x),xs)) -> app#(p,x) -> app#(app(forall(),p),app(app(cons(),x),xs)) -> app#(p,x) app#(app(forall(),p),app(app(cons(),x),xs)) -> app#(p,x) -> app#(app(forall(),p),app(app(cons(),x),xs)) -> app#(and(),app(p,x)) app#(app(forall(),p),app(app(cons(),x),xs)) -> app#(p,x) -> app#(app(forall(),p),app(app(cons(),x),xs)) -> app#(app(and(),app(p,x)),app(app(forall(),p),xs)) app#(app(forall(),p),app(app(cons(),x),xs)) -> app#(p,x) -> app#(app(forsome(),p),app(app(cons(),x),xs)) -> app#(app(forsome(),p),xs) app#(app(forall(),p),app(app(cons(),x),xs)) -> app#(p,x) -> app#(app(forsome(),p),app(app(cons(),x),xs)) -> app#(p,x) app#(app(forall(),p),app(app(cons(),x),xs)) -> app#(p,x) -> app#(app(forsome(),p),app(app(cons(),x),xs)) -> app#(or(),app(p,x)) app#(app(forall(),p),app(app(cons(),x),xs)) -> app#(p,x) -> app#(app(forsome(),p),app(app(cons(),x),xs)) -> app#(app(or(),app(p,x)),app(app(forsome(),p),xs)) Restore Modifier: DPs: app#(app(forall(),p),app(app(cons(),x),xs)) -> app#(app(forall(),p),xs) app#(app(forall(),p),app(app(cons(),x),xs)) -> app#(p,x) app#(app(forall(),p),app(app(cons(),x),xs)) -> app#(and(),app(p,x)) app#(app(forall(),p),app(app(cons(),x),xs)) -> app#(app(and(),app(p,x)),app(app(forall(),p),xs)) app#(app(forsome(),p),app(app(cons(),x),xs)) -> app#(app(forsome(),p),xs) app#(app(forsome(),p),app(app(cons(),x),xs)) -> app#(p,x) app#(app(forsome(),p),app(app(cons(),x),xs)) -> app#(or(),app(p,x)) app#(app(forsome(),p),app(app(cons(),x),xs)) -> app#(app(or(),app(p,x)),app(app(forsome(),p),xs)) TRS: app(app(and(),true()),true()) -> true() app(app(and(),x),false()) -> false() app(app(and(),false()),y) -> false() app(app(or(),true()),y) -> true() app(app(or(),x),true()) -> true() app(app(or(),false()),false()) -> false() app(app(forall(),p),nil()) -> true() app(app(forall(),p),app(app(cons(),x),xs)) -> app(app(and(),app(p,x)),app(app(forall(),p),xs)) app(app(forsome(),p),nil()) -> false() app(app(forsome(),p),app(app(cons(),x),xs)) -> app(app(or(),app(p,x)),app(app(forsome(),p),xs)) SCC Processor: #sccs: 1 #rules: 4 #arcs: 24/64 DPs: app#(app(forsome(),p),app(app(cons(),x),xs)) -> app#(app(forsome(),p),xs) app#(app(forsome(),p),app(app(cons(),x),xs)) -> app#(p,x) app#(app(forall(),p),app(app(cons(),x),xs)) -> app#(p,x) app#(app(forall(),p),app(app(cons(),x),xs)) -> app#(app(forall(),p),xs) TRS: app(app(and(),true()),true()) -> true() app(app(and(),x),false()) -> false() app(app(and(),false()),y) -> false() app(app(or(),true()),y) -> true() app(app(or(),x),true()) -> true() app(app(or(),false()),false()) -> false() app(app(forall(),p),nil()) -> true() app(app(forall(),p),app(app(cons(),x),xs)) -> app(app(and(),app(p,x)),app(app(forall(),p),xs)) app(app(forsome(),p),nil()) -> false() app(app(forsome(),p),app(app(cons(),x),xs)) -> app(app(or(),app(p,x)),app(app(forsome(),p),xs)) Matrix Interpretation Processor: dimension: 1 interpretation: [app#](x0, x1) = x0, [forsome] = 0, [cons] = 0, [nil] = 0, [forall] = 0, [or] = 0, [false] = 0, [app](x0, x1) = x1 + 1, [true] = 0, [and] = 0 orientation: app#(app(forsome(),p),app(app(cons(),x),xs)) = p + 1 >= p + 1 = app#(app(forsome(),p),xs) app#(app(forsome(),p),app(app(cons(),x),xs)) = p + 1 >= p = app#(p,x) app#(app(forall(),p),app(app(cons(),x),xs)) = p + 1 >= p = app#(p,x) app#(app(forall(),p),app(app(cons(),x),xs)) = p + 1 >= p + 1 = app#(app(forall(),p),xs) app(app(and(),true()),true()) = 1 >= 0 = true() app(app(and(),x),false()) = 1 >= 0 = false() app(app(and(),false()),y) = y + 1 >= 0 = false() app(app(or(),true()),y) = y + 1 >= 0 = true() app(app(or(),x),true()) = 1 >= 0 = true() app(app(or(),false()),false()) = 1 >= 0 = false() app(app(forall(),p),nil()) = 1 >= 0 = true() app(app(forall(),p),app(app(cons(),x),xs)) = xs + 2 >= xs + 2 = app(app(and(),app(p,x)),app(app(forall(),p),xs)) app(app(forsome(),p),nil()) = 1 >= 0 = false() app(app(forsome(),p),app(app(cons(),x),xs)) = xs + 2 >= xs + 2 = app(app(or(),app(p,x)),app(app(forsome(),p),xs)) problem: DPs: app#(app(forsome(),p),app(app(cons(),x),xs)) -> app#(app(forsome(),p),xs) app#(app(forall(),p),app(app(cons(),x),xs)) -> app#(app(forall(),p),xs) TRS: app(app(and(),true()),true()) -> true() app(app(and(),x),false()) -> false() app(app(and(),false()),y) -> false() app(app(or(),true()),y) -> true() app(app(or(),x),true()) -> true() app(app(or(),false()),false()) -> false() app(app(forall(),p),nil()) -> true() app(app(forall(),p),app(app(cons(),x),xs)) -> app(app(and(),app(p,x)),app(app(forall(),p),xs)) app(app(forsome(),p),nil()) -> false() app(app(forsome(),p),app(app(cons(),x),xs)) -> app(app(or(),app(p,x)),app(app(forsome(),p),xs)) Matrix Interpretation Processor: dimension: 1 interpretation: [app#](x0, x1) = x1 + 1, [forsome] = 0, [cons] = 0, [nil] = 0, [forall] = 0, [or] = 0, [false] = 1, [app](x0, x1) = x1 + 1, [true] = 0, [and] = 0 orientation: app#(app(forsome(),p),app(app(cons(),x),xs)) = xs + 2 >= xs + 1 = app#(app(forsome(),p),xs) app#(app(forall(),p),app(app(cons(),x),xs)) = xs + 2 >= xs + 1 = app#(app(forall(),p),xs) app(app(and(),true()),true()) = 1 >= 0 = true() app(app(and(),x),false()) = 2 >= 1 = false() app(app(and(),false()),y) = y + 1 >= 1 = false() app(app(or(),true()),y) = y + 1 >= 0 = true() app(app(or(),x),true()) = 1 >= 0 = true() app(app(or(),false()),false()) = 2 >= 1 = false() app(app(forall(),p),nil()) = 1 >= 0 = true() app(app(forall(),p),app(app(cons(),x),xs)) = xs + 2 >= xs + 2 = app(app(and(),app(p,x)),app(app(forall(),p),xs)) app(app(forsome(),p),nil()) = 1 >= 1 = false() app(app(forsome(),p),app(app(cons(),x),xs)) = xs + 2 >= xs + 2 = app(app(or(),app(p,x)),app(app(forsome(),p),xs)) problem: DPs: TRS: app(app(and(),true()),true()) -> true() app(app(and(),x),false()) -> false() app(app(and(),false()),y) -> false() app(app(or(),true()),y) -> true() app(app(or(),x),true()) -> true() app(app(or(),false()),false()) -> false() app(app(forall(),p),nil()) -> true() app(app(forall(),p),app(app(cons(),x),xs)) -> app(app(and(),app(p,x)),app(app(forall(),p),xs)) app(app(forsome(),p),nil()) -> false() app(app(forsome(),p),app(app(cons(),x),xs)) -> app(app(or(),app(p,x)),app(app(forsome(),p),xs)) Qed