NO 0.07/0.19 NO 0.18/0.20 0.18/0.20 Problem: 0.18/0.20 U104(tt()) -> plus(x(N,M),N) 0.18/0.20 U72(tt()) -> N 0.18/0.20 U84(tt()) -> s(plus(N,M)) 0.18/0.20 U101(tt()) -> U102(isNatKind()) 0.18/0.20 U102(tt()) -> U103(isNat()) 0.18/0.20 U103(tt()) -> U104(isNatKind()) 0.18/0.20 U11(tt()) -> U12(isNatKind()) 0.18/0.20 U12(tt()) -> U13(isNatKind()) 0.18/0.20 U13(tt()) -> U14(isNatKind()) 0.18/0.20 U14(tt()) -> U15(isNat()) 0.18/0.20 U15(tt()) -> U16(isNat()) 0.18/0.20 U16(tt()) -> tt() 0.18/0.20 U21(tt()) -> U22(isNatKind()) 0.18/0.20 U22(tt()) -> U23(isNat()) 0.18/0.20 U23(tt()) -> tt() 0.18/0.20 U31(tt()) -> U32(isNatKind()) 0.18/0.20 U32(tt()) -> U33(isNatKind()) 0.18/0.20 U33(tt()) -> U34(isNatKind()) 0.18/0.20 U34(tt()) -> U35(isNat()) 0.18/0.20 U35(tt()) -> U36(isNat()) 0.18/0.20 U36(tt()) -> tt() 0.18/0.20 U41(tt()) -> U42(isNatKind()) 0.18/0.20 U42(tt()) -> tt() 0.18/0.20 U51(tt()) -> tt() 0.18/0.20 U61(tt()) -> U62(isNatKind()) 0.18/0.20 U62(tt()) -> tt() 0.18/0.20 U71(tt()) -> U72(isNatKind()) 0.18/0.20 U81(tt()) -> U82(isNatKind()) 0.18/0.20 U82(tt()) -> U83(isNat()) 0.18/0.20 U83(tt()) -> U84(isNatKind()) 0.18/0.20 U91(tt()) -> U92(isNatKind()) 0.18/0.20 U92(tt()) -> 0() 0.18/0.20 isNat() -> tt() 0.18/0.20 isNat() -> U11(isNatKind()) 0.18/0.20 isNat() -> U21(isNatKind()) 0.18/0.20 isNat() -> U31(isNatKind()) 0.18/0.20 isNatKind() -> tt() 0.18/0.20 isNatKind() -> U41(isNatKind()) 0.18/0.20 isNatKind() -> U51(isNatKind()) 0.18/0.20 isNatKind() -> U61(isNatKind()) 0.18/0.20 plus(N,0()) -> U71(isNat()) 0.18/0.20 plus(N,s(M)) -> U81(isNat()) 0.18/0.20 x(N,0()) -> U91(isNat()) 0.18/0.20 x(N,s(M)) -> U101(isNat()) 0.18/0.20 0.18/0.20 Proof: 0.18/0.20 Fresh Variable Processor: 0.18/0.20 loop length: 1 0.18/0.20 terms: 0.18/0.20 U104(tt()) 0.18/0.20 context: plus(x([],M),U104(tt())) 0.18/0.20 substitution: 0.18/0.20 N -> U104(tt()) 0.18/0.20 Qed 0.18/0.20 EOF