MAYBE * Step 1: WeightGap MAYBE + Considered Problem: - Strict TRS: fac(x) -> help(x,0()) help(x,c) -> if(lt(c,x),x,c) if(false(),x,c) -> s(0()) if(true(),x,c) -> times(s(c),help(x,s(c))) lt(x,0()) -> false() lt(0(),s(x)) -> true() lt(s(x),s(y)) -> lt(x,y) - Signature: {fac/1,help/2,if/3,lt/2} / {0/0,false/0,s/1,times/2,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {fac,help,if,lt} and constructors {0,false,s,times,true} + Applied Processor: WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny} + Details: The weightgap principle applies using the following nonconstant growth matrix-interpretation: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(if) = {1}, uargs(times) = {2} Following symbols are considered usable: all TcT has computed the following interpretation: p(0) = [1] p(fac) = [2] x1 + [2] p(false) = [15] p(help) = [2] x1 + [4] p(if) = [1] x1 + [2] x2 + [1] p(lt) = [2] p(s) = [0] p(times) = [1] x1 + [1] x2 + [2] p(true) = [7] Following rules are strictly oriented: help(x,c) = [2] x + [4] > [2] x + [3] = if(lt(c,x),x,c) if(false(),x,c) = [2] x + [16] > [0] = s(0()) if(true(),x,c) = [2] x + [8] > [2] x + [6] = times(s(c),help(x,s(c))) Following rules are (at-least) weakly oriented: fac(x) = [2] x + [2] >= [2] x + [4] = help(x,0()) lt(x,0()) = [2] >= [15] = false() lt(0(),s(x)) = [2] >= [7] = true() lt(s(x),s(y)) = [2] >= [2] = lt(x,y) Further, it can be verified that all rules not oriented are covered by the weightgap condition. * Step 2: WeightGap MAYBE + Considered Problem: - Strict TRS: fac(x) -> help(x,0()) lt(x,0()) -> false() lt(0(),s(x)) -> true() lt(s(x),s(y)) -> lt(x,y) - Weak TRS: help(x,c) -> if(lt(c,x),x,c) if(false(),x,c) -> s(0()) if(true(),x,c) -> times(s(c),help(x,s(c))) - Signature: {fac/1,help/2,if/3,lt/2} / {0/0,false/0,s/1,times/2,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {fac,help,if,lt} and constructors {0,false,s,times,true} + Applied Processor: WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny} + Details: The weightgap principle applies using the following nonconstant growth matrix-interpretation: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(if) = {1}, uargs(times) = {2} Following symbols are considered usable: all TcT has computed the following interpretation: p(0) = [8] p(fac) = [1] x1 + [8] p(false) = [0] p(help) = [1] x1 + [2] x2 + [12] p(if) = [1] x1 + [1] x2 + [2] x3 + [10] p(lt) = [2] p(s) = [1] x1 + [2] p(times) = [1] x2 + [0] p(true) = [6] Following rules are strictly oriented: lt(x,0()) = [2] > [0] = false() Following rules are (at-least) weakly oriented: fac(x) = [1] x + [8] >= [1] x + [28] = help(x,0()) help(x,c) = [2] c + [1] x + [12] >= [2] c + [1] x + [12] = if(lt(c,x),x,c) if(false(),x,c) = [2] c + [1] x + [10] >= [10] = s(0()) if(true(),x,c) = [2] c + [1] x + [16] >= [2] c + [1] x + [16] = times(s(c),help(x,s(c))) lt(0(),s(x)) = [2] >= [6] = true() lt(s(x),s(y)) = [2] >= [2] = lt(x,y) Further, it can be verified that all rules not oriented are covered by the weightgap condition. * Step 3: WeightGap MAYBE + Considered Problem: - Strict TRS: fac(x) -> help(x,0()) lt(0(),s(x)) -> true() lt(s(x),s(y)) -> lt(x,y) - Weak TRS: help(x,c) -> if(lt(c,x),x,c) if(false(),x,c) -> s(0()) if(true(),x,c) -> times(s(c),help(x,s(c))) lt(x,0()) -> false() - Signature: {fac/1,help/2,if/3,lt/2} / {0/0,false/0,s/1,times/2,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {fac,help,if,lt} and constructors {0,false,s,times,true} + Applied Processor: WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny} + Details: The weightgap principle applies using the following nonconstant growth matrix-interpretation: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(if) = {1}, uargs(times) = {2} Following symbols are considered usable: all TcT has computed the following interpretation: p(0) = [0] p(fac) = [9] x1 + [9] p(false) = [2] p(help) = [2] x1 + [4] x2 + [8] p(if) = [1] x1 + [2] x2 + [4] x3 + [1] p(lt) = [2] p(s) = [1] x1 + [1] p(times) = [1] x2 + [2] p(true) = [15] Following rules are strictly oriented: fac(x) = [9] x + [9] > [2] x + [8] = help(x,0()) Following rules are (at-least) weakly oriented: help(x,c) = [4] c + [2] x + [8] >= [4] c + [2] x + [3] = if(lt(c,x),x,c) if(false(),x,c) = [4] c + [2] x + [3] >= [1] = s(0()) if(true(),x,c) = [4] c + [2] x + [16] >= [4] c + [2] x + [14] = times(s(c),help(x,s(c))) lt(x,0()) = [2] >= [2] = false() lt(0(),s(x)) = [2] >= [15] = true() lt(s(x),s(y)) = [2] >= [2] = lt(x,y) Further, it can be verified that all rules not oriented are covered by the weightgap condition. * Step 4: Failure MAYBE + Considered Problem: - Strict TRS: lt(0(),s(x)) -> true() lt(s(x),s(y)) -> lt(x,y) - Weak TRS: fac(x) -> help(x,0()) help(x,c) -> if(lt(c,x),x,c) if(false(),x,c) -> s(0()) if(true(),x,c) -> times(s(c),help(x,s(c))) lt(x,0()) -> false() - Signature: {fac/1,help/2,if/3,lt/2} / {0/0,false/0,s/1,times/2,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {fac,help,if,lt} and constructors {0,false,s,times,true} + Applied Processor: EmptyProcessor + Details: The problem is still open. MAYBE