Nuprl Rule : callbyvalueTry

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 callbyvalueTry ()
  
  H  ⊢ (t?n:v.c)↓
  x:(t)↓y:(t?n:v.c if n=2 then else ⊥) ⊢ b ∈ T
  m:Base, u:Base, x:(t exception(m; u)), y:(t?n:v.c if n=2 then c[u/v] else (exception(m; u))) ⊢ b ∈ T
  H  ⊢ t ∈ Base
  H  ⊢ n ∈ Base
  v:Base ⊢ c ∈ Base



Definitions occuring in rule :  has-value: (a)↓ bottom: sqequal: t atom_eq: atomeqn def equal: t ∈ T member: t ∈ T base: Base axiom: Ax

Latex:
H    \mvdash{}  a  =  b

    BY  callbyvalueTry  m  u  x  y  t  n  v  c  ()
   
    H    \mvdash{}  (t?n:v.c)\mdownarrow{}
    H  x:(t)\mdownarrow{},  y:(t?n:v.c  \msim{}  if  n=2  n  then  t  else  \mbot{})  \mvdash{}  a  =  b
    H  m:Base,  u:Base,  x:(t  \msim{}  exception(m;  u)),  y:(t?n:v.c  \msim{}  if  n=2  m
                                                                                                                          then  c[u/v]
                                                                                                                          else  (exception(m;  u)))
          \mvdash{}  a  =  b
    H    \mvdash{}  t  \mmember{}  Base
    H    \mvdash{}  n  \mmember{}  Base
    H  v:Base  \mvdash{}  c  \mmember{}  Base



Date html generated: 2019_06_20-PM-04_12_26
Last ObjectModification: 2017_01_24-PM-04_22_21

Theory : rules


Home Index