/home/nowonder/forschung/aprove/TPDB05/TRS/Cime/maude2.trs

The program

(COMMENT

  encoding of Maude program:

  fmod PEANO-NAT is
    sorts Nat NzNat .
    subsorts NzNat < Nat .
    op 0 : -> Nat .
    ops 1 2 3 4 5 6 7 : -> NzNat .
    op s_ : Nat -> NzNat .
    op p_ : NzNat -> Nat .
    op _+_ : Nat Nat -> Nat [comm] .
    op _*_ : Nat Nat -> Nat [comm] .
    op _*_ : NzNat NzNat -> NzNat [comm] .
    op _>_ : Nat Nat -> Bool .
    op _<_ : Nat Nat -> Bool .
    op d : Nat Nat -> Nat [comm] .
    op quot : Nat NzNat -> Nat .
    op gcd : Nat Nat -> Nat [comm] .
    op gcd : NzNat NzNat -> NzNat [comm] .
    vars N M : Nat .  
    vars N' M' : NzNat .
    eq p s N = N .
    eq N + 0 = N .
    eq (s N) + (s M) = s s (N + M) .
    eq N * 0 = 0 .
    eq (s N) * (s M) = s (N + (M + (N * M))) .
    eq 0 > M = false .
    eq N' > 0 = true .
    eq s N > s M = N > M .
    eq N < M = M > N .
    eq d(0,N) = N .
    eq d(s N, s M) = d(N,M) .
    ceq quot(N,M') = s quot(d(N,M'),M') if N > M' .
    eq quot(M',M') = s 0 .
    ceq quot(N,M') = 0 if M' > N .
    eq gcd(0,N) = 0 .
    eq gcd(N',N') = N' .
    ceq gcd(N',M') =  gcd(d(N',M'),M') if N' > M' .
    eq 1 = s 0 .
    eq 2 = s s 0 .
    eq 3 = s s s 0 .
    eq 4 = s s s s 0 .
    eq 5 = s s s s s 0 .
    eq 6 = s s s s s s 0 .
    eq 7 = s s s s s s s 0 .
   endfm
)

(VAR N M NzN NzM)
(RULES
  p(s(N)) -> N
  +(N,0) -> N
  +(s(N),s(M)) -> s(s(+(N,M)))
  *(N,0) -> 0
  *(s(N),s(M)) -> s(+(N,+(M,*(N,M))))

  gt(0,M) -> False
  gt(NzN,0) -> u_4(is_NzNat(NzN))
  u_4(True) ->  True 
  is_NzNat(0) -> False
  is_NzNat(s(N)) -> True

  gt(s(N),s(M)) -> gt(N,M)

  lt(N,M) -> gt(M,N)
  d(0,N) -> N
  d(s(N),s(M)) -> d(N,M)

  quot(N,NzM) -> u_11(is_NzNat(NzM),N,NzM)
  u_11(True,N,NzM) -> u_1(gt(N,NzM),N,NzM)
  u_1(True,N,NzM) -> s(quot(d(N,NzM),NzM))

  quot(NzM,NzM) -> u_01(is_NzNat(NzM))
  u_01(True) -> s(0)

  quot(N, NzM) -> u_21(is_NzNat(NzM),NzM,N)
  u_21(True,NzM,N) -> u_2(gt(NzM,N))
  u_2(True) -> 0

  gcd(0,N) -> 0
  gcd(NzM,NzM) -> u_02(is_NzNat(NzM),NzM)
  u_02(True,NzM) -> NzM

  gcd(NzN,NzM) -> u_31(is_NzNat(NzN),is_NzNat(NzM),NzN,NzM)
  u_31(True,True,NzN,NzM) -> u_3(gt(NzN,NzM),NzN,NzM)
  u_3(True,NzN,NzM) -> gcd(d(NzN,NzM),NzM) 
)

Submit to AProVE Web Frontend

Edit in AProVE Web Frontend