mod! BASIC-NAT {
 [Zero NzNat < Nat]
 op 0  : -> Zero
 op s_ : Nat -> NzNat
}
mod! NAT+ {
 pr(BASIC-NAT)
 op _+_ : Nat Nat -> Nat 
 vars M N : Nat
 eq N +   0 = N .
 eq M + s N = s (M + N) . 
}

select NAT+ + EQL 
set trace whole on
red 0 + s 0 = s 0 + 0 .
red s (0 + s 0) .
set trace whole off

mod! NAT-bad {
 pr(BASIC-NAT) 
 op _+_ : Nat Nat -> Nat 

 op _*_ : Nat Nat -> Nat 

 vars M N : Nat
 eq N = N + 0 .
 eq 0 = N * 0 .

}
select NAT-bad
--> Equations in NAT-bad are ignored in the following reduction
red s 0 .
red 0 .

mod! ABC{
 [Elt]
 ops a b c : -> Elt
 eq a = b .
 eq a = c .
}
select ABC + EQL
red b = c .

mod! NAT* {
 pr(NAT+)
 op _*_ : Nat Nat -> Nat
 vars M N : Nat
 eq N *   0 = 0 .
 eq M * s N = M + (M * N). 
}


select NAT*
--> Reduce 3 * 2 (should be 6)
red s s s 0 * s s 0 .

mod! FIRST{
 pr(NAT+)
 op first : Nat -> Nat
 vars X Y Z : Nat
 eq (X + Y) + Z = X +(Y + Z) .
 eq first(X + Y) = X .
}

select FIRST
--> Apply the first equation first
--> start first((0 + s 0) + s s 0) .
start first((0 + s 0) + s s 0) .
--> apply 1 at (1) .
apply 1 at (1) .
--> apply 2 at term .
apply 2 at term .

--> Apply the second equation first
--> start first((0 + s 0) + s s 0) .
start first((0 + s 0) + s s 0) .
--> apply 2 at term .
apply 2 at term .

--> Critical Pair (X+Y, first(X + (Y + Z))) is not joinable
select FIRST + EQL
red X:Nat + Y:Nat = first(X + (Y + Z:Nat)) .



mod! BOOL-NOT{
 [B]
 ops 0 1 : -> B
 op ~_ : B -> B
 var X : B
 eq ~ ~ X = X .
 eq   ~ 0 = 1 .
 eq   ~ 1 = 0 .

}
select BOOL-NOT + EQL
--> All critical pairs are joinable
--> CP (0, ~1) from ~ ~ 0
red 0 = ~ 1 .
--> CP (1, ~0) from ~ ~ 1
red 1 = ~ 0 .
--> CP (~X, ~X) from ~ ~ ~ X
red ~ X:B = ~ X .

mod! NAT++{
 pr(BASIC-NAT)
 op _+_ : Nat Nat -> Nat
 vars M N : Nat
 eq    0 +   N = N .
 eq    N +   0 = N .
 eq  s M +   N = s (M + N) . 
 eq    M + s N = s (M + N) .
}

select NAT++ + EQL
--> All critical pairs are joinable
red 0 = 0 .
red s N:Nat = s (0 + N) .
red s M:Nat = s(M + 0) .


mod! NAT+bad{
 pr(BASIC-NAT)
 op _+_ : Nat Nat -> Nat
 vars M N : Nat
 eq 0 +   N = N .
 eq M + s N = s (M + N) .
}

select NAT+bad 
red s 0 + 0 .

mod! NAT* {
 [Zero NzNat < Nat]
 op 0  : -> Zero
 op s_ : Nat -> NzNat
 ops (_+_) (_*_) : Nat Nat -> Nat
 vars M N : Nat
 eq N +   0 = N .
 eq M + s N = s (M + N) . 
 eq N *   0 = 0 .
 eq M * s N = M + (M * N). 
}

mod! NAT-EVEN{
 pr(BASIC-NAT)
 op even_: Nat -> Bool
 var N : Nat
 eq even 0 = true .
 ceq even(s N) = false if even N .
 ceq even(s N) = true  if not (even N) .
}

select NAT-EVEN
red even (s s 0) .


mod! INFINITE{
 [Elt]
 op f : Elt -> Bool
 var X : Elt
 ceq f(X) = true  if f(X) .
}

--> The following reduction causes "Stack overflow"
--> select INFINITE .
--> red f(X:Elt) .

mod! NAT+ {
 pr(BASIC-NAT)
 op _+_ : Nat Nat -> Nat {assoc comm}
 vars M N : Nat
 eq N +   0 = N .
 eq M + s N = s (M + N) . 
}

select NAT+
--> Some brackets can be omitted.
--> parse 0 + s 0 + s s 0 + s s s 0 .
parse 0 + s 0 + s s 0 + s s s 0 .

mod! BAG{
  [Elt < Bag]
  ops a b c  : -> Elt
  op _ _ : Bag Bag -> Bag { assoc comm }
  op _in_ : Elt Bag -> Bool
  var E : Elt    var B : Bag
  eq E in (E B) = true .
}
select BAG 
set trace on
red c in (a b c) .
set trace off

mod! BAG2{
  [Elt < Bag]
  ops 0 1  : -> Elt
  op _ _ : Bag Bag -> Bag { assoc comm }
  var E : Elt 
  eq (E E) = 0 1 .
}

select BAG2 .
--> The following reduction causes "Stack overflow"
--> red 0 (0 1) .
--> start 0 (0 1) .
start 0 (0 1) .
--> apply 1 at term .
apply 1 at term .
--> apply 1 at term .
apply 1 at term .

mod! BAG3{
  [Elt < Bag]
  ops 0 1  : -> Elt
  op begin-with-zero : Bag -> Bool
  op _ _ : Bag Bag -> Bag { assoc comm }
  var B : Bag 
  eq begin-with-zero(0 B) = true .
  eq begin-with-zero(1 B) = false .
}

select BAG3
--> apply the first equation 
--> start begin-with-zero(0 1) .
start begin-with-zero(0 1) .
--> apply 1 at term .
apply 1 at term .

select BAG3
--> apply the second equation 
--> start begin-with-zero(0 1) .
start begin-with-zero(0 1) .
--> apply 2 at term .

apply 2 at term .