-- Case Analyses

--> 1) begin(s,p10)
mod EICASE1 { pr(ICASE1)
-- Basic predicates
  op bp1 : -> Bool
  #define bp1 ::= (p = p10) .
-- Exhaustiveness check
  op check : -> Bool
  eq check = bp1 or not bp1 .
}
-- Case splitting
mod ICASE1-1 { pr(EICASE1)
  eq bp1 = true .
}
--
mod ICASE1-2 { pr(EICASE1)
  eq bp1 = false .
}

--> 2) exit(s,p10)
mod EICASE2 { pr(ICASE2)
-- Basic predicates
  op bp1 : -> Bool
  #define bp1 ::= (p = p10) .
-- Exhaustiveness check
  op check : -> Bool
  eq check = bp1 or not bp1 .
}
-- Case splitting
mod ICASE2-1 { pr(EICASE2)
  eq bp1 = true .
}
--
mod ICASE2-2 { pr(EICASE2)
  eq bp1 = false .
}

--> 3) end(s,p10)
mod EICASE3 { pr(ICASE3)
-- Basic predicates
  op bp1 : -> Bool
  #define bp1 ::= (p = p10) .
-- Exhaustiveness check
  op check : -> Bool
  eq check = bp1 or not bp1 .
}
-- Case splitting
mod ICASE3-1 { pr(EICASE3)
  eq bp1 = true .
}
--
mod ICASE3-2 { pr(EICASE3)
  eq bp1 = false .
}

-- Exhaustiveness Check 
  red in EICASE1 : check .
  red in EICASE2 : check .
  red in EICASE3 : check .
-- End of Exhaustiveness Check

-- Proof
-- I) Base case
  red in INV : inv130(init,p) .
-- II) Inductive cases
  red in ICASE1-1 : istep130(p) .
  red in ICASE1-2 : istep130(p) .
  red in ICASE2-1 : inv110(s,p10) implies istep130(p) .
  red in ICASE2-2 : istep130(p) .
  red in ICASE3-1 : istep130(p) .
  red in ICASE3-2 : inv140(s,p,p10) implies istep130(p) .
-- Q.E.D.