MAYBE
0.08/0.18	MAYBE
0.08/0.19	
0.08/0.19	Problem:
0.08/0.19	 p(s(N)) -> N
0.08/0.19	 +(N,0()) -> N
0.08/0.19	 +(s(N),s(M)) -> s(s(+(N,M)))
0.08/0.19	 *(N,0()) -> 0()
0.08/0.19	 *(s(N),s(M)) -> s(+(N,+(M,*(N,M))))
0.08/0.19	 gt(0(),M) -> False()
0.08/0.19	 gt(NzN,0()) -> u_4(is_NzNat(NzN))
0.08/0.19	 u_4(True()) -> True()
0.08/0.19	 is_NzNat(0()) -> False()
0.08/0.19	 is_NzNat(s(N)) -> True()
0.08/0.19	 gt(s(N),s(M)) -> gt(N,M)
0.08/0.19	 lt(N,M) -> gt(M,N)
0.08/0.19	 d(0(),N) -> N
0.08/0.19	 d(s(N),s(M)) -> d(N,M)
0.08/0.19	 quot(N,NzM) -> u_11(is_NzNat(NzM),N,NzM)
0.08/0.19	 u_11(True(),N,NzM) -> u_1(gt(N,NzM),N,NzM)
0.08/0.19	 u_1(True(),N,NzM) -> s(quot(d(N,NzM),NzM))
0.08/0.19	 quot(NzM,NzM) -> u_01(is_NzNat(NzM))
0.08/0.19	 u_01(True()) -> s(0())
0.08/0.19	 quot(N,NzM) -> u_21(is_NzNat(NzM),NzM,N)
0.08/0.19	 u_21(True(),NzM,N) -> u_2(gt(NzM,N))
0.08/0.19	 u_2(True()) -> 0()
0.08/0.19	 gcd(0(),N) -> 0()
0.08/0.19	 gcd(NzM,NzM) -> u_02(is_NzNat(NzM),NzM)
0.08/0.19	 u_02(True(),NzM) -> NzM
0.08/0.19	 gcd(NzN,NzM) -> u_31(is_NzNat(NzN),is_NzNat(NzM),NzN,NzM)
0.08/0.19	 u_31(True(),True(),NzN,NzM) -> u_3(gt(NzN,NzM),NzN,NzM)
0.08/0.19	 u_3(True(),NzN,NzM) -> gcd(d(NzN,NzM),NzM)
0.08/0.19	
0.08/0.19	Proof:
0.08/0.19	 Open
0.08/0.19	EOF