-- 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 (bp1 and not bp2) or 
             (not bp1 and bp2) or (not bp1 and not bp2) .
}
-- Case splitting
mod ICASE1-1 { pr(EICASE1)
  eq bp1 = true .
  eq bp2 = true .
}
--
mod ICASE1-2 { pr(EICASE1)
  eq bp1 = true .
  eq bp2 = false .
}
--
mod ICASE1-3 { pr(EICASE1)
  eq bp1 = false .
  eq bp2 = true .
}
--
mod ICASE1-4 { pr(EICASE1)
  eq bp1 = false .
  eq bp2 = false .
}

--> 2) swap(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) test(s,p10)
mod EICASE3 { pr(ICASE3)
-- Basic predicates
  ops bp1 bp2 bp3 : -> Bool
  #define bp1 ::= (p = p10) .
  #define bp2 ::= (q = p10) .
  #define bp3 ::= check(s,p10) .
-- Exhaustiveness check
  op check : -> Bool
  eq check = (bp1 and bp2 and bp3) or (bp1 and bp2 and not bp3) or 
             (bp1 and not bp2 and bp3) or (bp1 and not bp2 and not bp3) or 
             (not bp1 and bp2) or (not bp1 and not bp2) .
}
-- Case splitting
mod ICASE3-1 { pr(EICASE3)
  eq bp1 = true .
  -- eq bp2 = true .
  eq q = p10 .
  --
  eq bp3 = true .
}
--
mod ICASE3-2 { pr(EICASE3)
  eq bp1 = true .
  -- eq bp2 = true .
  eq q = p10 .
  --
  eq bp3 = false .
}
--
mod ICASE3-3 { pr(EICASE3)
  -- eq bp1 = true .
  eq p = p10 .
  --
  eq bp2 = false .
  eq bp3 = true .
}
--
mod ICASE3-4 { pr(EICASE3)
  -- eq bp1 = true .
  eq p = p10 .
  --
  eq bp2 = false .
  eq bp3 = false .
}
--
mod ICASE3-5 { pr(EICASE3)
  eq bp1 = false .
  -- eq bp2 = true .
  eq q = p10 .
}
--
mod ICASE3-6 { pr(EICASE3)
  eq bp1 = false .
  eq bp2 = false .
}

--> 4) exit(s,p10)
mod EICASE4 { pr(ICASE4)
-- 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 ICASE4-1 { pr(EICASE4)
  eq bp1 = true .
  eq bp2 = true .
}
--
mod ICASE4-2 { pr(EICASE4)
  eq bp1 = true .
  eq bp2 = false .
}
--
mod ICASE4-3 { pr(EICASE4)
  eq bp1 = false .
  -- eq bp2 = true .
  eq q = p10 .
}
--
mod ICASE4-4 { pr(EICASE4)
  eq bp1 = false .
  eq bp2 = false .
}

--> 5) end(s,p10)
mod EICASE5 { pr(ICASE5)
-- 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 ICASE5-1 { pr(EICASE5)
  eq bp1 = true .
  eq bp2 = true .
}
--
mod ICASE5-2 { pr(EICASE5)
  eq bp1 = true .
  eq bp2 = false .
}
--
mod ICASE5-3 { pr(EICASE5)
  eq bp1 = false .
  eq bp2 = true .
}
--
mod ICASE5-4 { pr(EICASE5)
  eq bp1 = false .
  eq bp2 = 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 : inv170(init,p,q) .
-- II) Inductive cases
  red in ICASE1-1 : istep170(p,q) .
  red in ICASE1-2 : istep170(p,q) .
  red in ICASE1-3 : istep170(p,q) .
  red in ICASE1-4 : istep170(p,q) .
  red in ICASE2-1 : istep170(p,q) .
  red in ICASE2-2 : istep170(p,q) .
  red in ICASE2-3 : inv180(s,p) implies istep170(p,q) .
  red in ICASE2-4 : istep170(p,q) .
  red in ICASE3-1 : istep170(p,q) .
  red in ICASE3-2 : istep170(p,q) .
  red in ICASE3-3 : istep170(p,q) .
  red in ICASE3-4 : istep170(p,q) .
  red in ICASE3-5 : istep170(p,q) .
  red in ICASE3-6 : istep170(p,q) .
  red in ICASE4-1 : istep170(p,q) .
  red in ICASE4-2 : inv110(s,p10,q) implies istep170(p,q) .
  red in ICASE4-3 : istep170(p,q) .
  red in ICASE4-4 : istep170(p,q) .
  red in ICASE5-1 : istep170(p,q) .
  red in ICASE5-2 : istep170(p,q) .
  red in ICASE5-3 : istep170(p,q) .
  red in ICASE5-4 : istep170(p,q) .
-- Q.E.D.