-- Case analyses

-- 1) sdm1(s,p10,q10,r10)
mod EICASE1 { pr(ICASE1)
-- Basic predicates  
  op bp1 : -> Bool
  #define bp1 ::= (r = r10) .
-- 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) sdm2(s,p10,r10,m10)
mod EICASE2 { pr(ICASE2)
-- Basic predicates  
  op bp1 : -> Bool
  #define bp1 ::= (r = r10) .
-- 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) sdm3(s,p10,r10,m10,m20)
mod EICASE3 { pr(ICASE3)
-- Basic predicates  
-- Exhaustiveness check
  op check : -> Bool 
  eq check = true .
}
-- Case splitting
mod ICASE3-1 { pr(EICASE3) }

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

-- 5) fkm12(s,p10,q10,n10)
mod EICASE5 { pr(ICASE5)
-- Basic predicates  
  ops bp1 bp2 bp3 : -> Bool
  #define bp1 ::= (q10 = intruder) .
  #define bp1 ::= r \in ur(s) .
  #define bp1 ::= (n(p,q,r) = n10) .
-- Exhaustiveness check
  op check : -> Bool 
  eq check = bp1 or (not bp1 and bp2) or (not bp1 and not bp2 and not bp3) or
             (not bp1 and not bp2 and bp3) .
}
-- Case splitting
mod ICASE5-1 { pr(EICASE5)
  -- eq bp1 = true .
  eq q10 = intruder .
}
--
mod ICASE5-2 { pr(EICASE5)
  eq bp1 = false .
  eq bp2 = true .
}
--
mod ICASE5-3 { pr(EICASE5)
  eq bp1 = false .
  eq bp2 = false .
  eq bp3 = false .
}
--
mod ICASE5-4 { pr(EICASE5)
  eq bp1 = false .
  eq bp2 = false .
  -- eq bp3 = true .
  eq n(p,q,r) = n10 .
}

-- 6) fkm21(s,p10,q10,e20)
mod EICASE6 { pr(ICASE6)
-- Basic predicates  
-- Exhaustiveness check
  op check : -> Bool 
  eq check = true .
}
-- Case splitting
mod ICASE6-1 { pr(EICASE6) }

-- 7) fkm22(s,p10,q10,n10,n20)
mod EICASE7 { pr(ICASE7)
-- Basic predicates  
-- Exhaustiveness check
  op check : -> Bool 
  eq check = true .
}
-- Case splitting
mod ICASE7-1 { pr(EICASE7) }

-- 8) fkm31(s,p10,q10,e30)
mod EICASE8 { pr(ICASE8)
-- Basic predicates  
-- Exhaustiveness check
  op check : -> Bool 
  eq check = true .
}
-- Case splitting
mod ICASE8-1 { pr(EICASE8) }

-- 9) fkm32(s,p10,q10,n10)
mod EICASE9 { pr(ICASE9)
-- Basic predicates  
-- Exhaustiveness check
  op check : -> Bool 
  eq check = true .
}
-- Case splitting
mod ICASE9-1 { pr(EICASE9) }

-- Exhaustiveness Check 
  red in EICASE1 : check .
  red in EICASE2 : check .
  red in EICASE3 : check .
  red in EICASE4 : check .
  red in EICASE5 : check .
  red in EICASE6 : check .
  red in EICASE7 : check .
  red in EICASE8 : check .
  red in EICASE9 : check .
-- End of Exhaustiveness Check 

-- Proof
-- I) Base case
  red in INV : inv200(init,p,q,r) .
-- II) Inductive cases
  red in ICASE1-1 : istep200(p,q,r) .
  red in ICASE1-2 : istep200(p,q,r) .
  red in ICASE2-1 : istep200(p,q,r) .
  red in ICASE2-2 : istep200(p,q,r) .
  red in ICASE3-1 : istep200(p,q,r) .
  red in ICASE4-1 : istep200(p,q,r) .
  red in ICASE4-2 : istep200(p,q,r) .
  red in ICASE5-1 : istep200(p,q,r) .
  red in ICASE5-2 : istep200(p,q,r) .
  red in ICASE5-3 : istep200(p,q,r) .
  red in ICASE5-4 : inv210(s,p,q,r) implies istep200(p,q,r) .
  red in ICASE6-1 : istep200(p,q,r) .
  red in ICASE7-1 : istep200(p,q,r) .
  red in ICASE8-1 : istep200(p,q,r) .
  red in ICASE9-1 : istep200(p,q,r) .
-- Q.E.D.