NO 0.09/0.18 NO 0.09/0.18 0.09/0.18 Problem: 0.09/0.18 U52(tt()) -> N 0.09/0.18 U64(tt()) -> s(plus(N,M)) 0.09/0.18 U11(tt()) -> U12(isNatKind()) 0.09/0.18 U12(tt()) -> U13(isNatKind()) 0.09/0.18 U13(tt()) -> U14(isNatKind()) 0.09/0.18 U14(tt()) -> U15(isNat()) 0.09/0.18 U15(tt()) -> U16(isNat()) 0.09/0.18 U16(tt()) -> tt() 0.09/0.18 U21(tt()) -> U22(isNatKind()) 0.09/0.18 U22(tt()) -> U23(isNat()) 0.09/0.18 U23(tt()) -> tt() 0.09/0.18 U31(tt()) -> U32(isNatKind()) 0.09/0.18 U32(tt()) -> tt() 0.09/0.18 U41(tt()) -> tt() 0.09/0.18 U51(tt()) -> U52(isNatKind()) 0.09/0.18 U61(tt()) -> U62(isNatKind()) 0.09/0.18 U62(tt()) -> U63(isNat()) 0.09/0.18 U63(tt()) -> U64(isNatKind()) 0.09/0.18 isNat() -> tt() 0.09/0.18 isNat() -> U11(isNatKind()) 0.09/0.18 isNat() -> U21(isNatKind()) 0.09/0.18 isNatKind() -> tt() 0.09/0.18 isNatKind() -> U31(isNatKind()) 0.09/0.18 isNatKind() -> U41(isNatKind()) 0.09/0.18 plus(N,0()) -> U51(isNat()) 0.09/0.18 plus(N,s(M)) -> U61(isNat()) 0.09/0.18 0.09/0.18 Proof: 0.09/0.18 Fresh Variable Processor: loop length: 1 0.09/0.18 terms: 0.09/0.18 U52(tt()) 0.09/0.18 context: [] 0.09/0.18 substitution: 0.09/0.18 N -> U52(tt()) 0.09/0.18 Qed 0.09/0.18 EOF