-- Case Analyses

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

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

--> 3) end(s,p10)
mod EICASE3 { pr(ICASE3)
-- Basic predicates
  ops bp1 bp2 : -> Bool
  #define bp1 ::= (p = p10) .
  #define bp2 ::= (q = p10) .
-- Exhaustiveness check
  op check : -> Bool
  eq check = (bp1 and bp2) or (bp1 and not bp2) or 
             (not bp1 and bp2) or (not bp1 and not bp2) .
}
-- Case splitting
mod ICASE3-1 { pr(EICASE3)
  eq bp1 = true .
  eq bp2 = true .
}
--
mod ICASE3-2 { pr(EICASE3)
  eq bp1 = true .
  eq bp2 = false .
}
--
mod ICASE3-3 { pr(EICASE3)
  eq bp1 = false .
  eq bp2 = true .
}
--
mod ICASE3-4 { pr(EICASE3)
  eq bp1 = false .
  eq bp2 = 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 : inv100(init,p,q) .
-- II) Inductive cases
  red in ICASE1-1 : istep100(p,q) .
  red in ICASE1-2 : inv110(s,q) implies istep100(p,q) .
  red in ICASE1-3 : inv110(s,p) implies istep100(p,q) .
  red in ICASE2-1 : istep100(p,q) .
  red in ICASE2-2 : istep100(p,q) .
  red in ICASE2-3 : istep100(p,q) .
  red in ICASE2-4 : istep100(p,q) .
  red in ICASE3-1 : istep100(p,q) .
  red in ICASE3-2 : istep100(p,q) .
  red in ICASE3-3 : istep100(p,q) .
  red in ICASE3-4 : istep100(p,q) .
-- Q.E.D.