Nuprl Rule : isaxiomExceptionCases

This rule proved as lemma rule_can_test_exception_cases_true in file rules/rules_cft_exception.v
 at https://github.com/vrahli/NuprlInCoq  

H  ⊢ b ∈ T

  BY isaxiomExceptionCases ()
  
  H  ⊢ is-exception(if Ax then otherwise v)
  x:(t)↓ ⊢ b ∈ T
  x:is-exception(t) ⊢ b ∈ T
  H  ⊢ t ∈ Base



Definitions occuring in rule :  isaxiom: if Ax then otherwise b has-value: (a)↓ is-exception: is-exception(t) equal: t ∈ T member: t ∈ T base: Base axiom: Ax

Latex:
H    \mvdash{}  a  =  b

    BY  isaxiomExceptionCases  x  t  u  v  ()
   
    H    \mvdash{}  is-exception(if  t  =  Ax  then  u  otherwise  v)
    H  x:(t)\mdownarrow{}  \mvdash{}  a  =  b
    H  x:is-exception(t)  \mvdash{}  a  =  b
    H    \mvdash{}  t  \mmember{}  Base



Date html generated: 2019_06_20-PM-04_12_13
Last ObjectModification: 2016_07_08-PM-03_48_54

Theory : rules


Home Index