-- 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) swap(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) test(s,p10)
mod EICASE3 { pr(ICASE3)
-- Basic predicates
  ops bp1 bp2 : -> Bool
  #define bp1 ::= (p = p10) .
  #define bp2 ::= check(s,p) .
-- Exhaustiveness check
  op check : -> Bool
  eq check = (bp1 and bp2) or (bp1 and not bp2) or not bp1 .
}
-- 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 .
}

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

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

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

-- Proof
-- I) Base case
  red in INV : inv140(init,p) .
-- II) Inductive cases
  red in ICASE1-1 : istep140(p) .
  red in ICASE1-2 : istep140(p) .
  red in ICASE2-1 : istep140(p) .
  red in ICASE2-2 : istep140(p) .
  red in ICASE3-1 : istep140(p) .
  red in ICASE3-2 : istep140(p) .
  red in ICASE3-3 : istep140(p) .
  red in ICASE3-3 : istep140(p) .
  red in ICASE4-1 : istep140(p) .
  red in ICASE4-2 : istep140(p) .
  red in ICASE5-1 : istep140(p) .
  red in ICASE5-2 : istep140(p) .
-- Q.E.D.