Nuprl Rule : decideExceptionCases

This rule proved as lemma rule_decide_exception_cases_true in file rules/rules_decide_exception.v
 at https://github.com/vrahli/NuprlInCoq  
H  ⊢ a = b ∈ T

  BY decideExceptionCases x t y.u z.v ()
  
  H  ⊢ is-exception(case t of inl(y) => u | inr(z) => v)
  H x:(t ∈ Top + Top) ⊢ a = b ∈ T
  H x:is-exception(t) ⊢ a = b ∈ T
  H  ⊢ t ∈ Base


Definitions occuring in rule :  decide: case b of inl(x) => s[x] | inr(y) => t[y],  union: left + right,  top: Top,  is-exception: is-exception(t),  equal: s = t ∈ T,  member: t ∈ T,  base: Base,  axiom: Ax
Latex:
H    \mvdash{}  a  =  b

    BY  decideExceptionCases  x  t  y.u  z.v  ()
   
    H    \mvdash{}  is-exception(case  t  of  inl(y)  =>  u  |  inr(z)  =>  v)
    H  x:(t  \mmember{}  Top  +  Top)  \mvdash{}  a  =  b
    H  x:is-exception(t)  \mvdash{}  a  =  b
    H    \mvdash{}  t  \mmember{}  Base


Date html generated: 2019_06_20-PM-04_11_49
Last ObjectModification: 2016_07_08-PM-03_49_01

Theory : rules


Home Index