Nuprl Rule : callbyvalueApplyCases
This rule proved as lemma rule_callbyvalue_apply_cases_true in file rules/rules_apply_callbyvalue.v
 at https://github.com/vrahli/NuprlInCoq  
H  ⊢ (f ~ λx.(f x)) ∨ (⋂x:Base. ⋂z:(x)↓.  if x is an integer then True else f x ≤ ⊥) ext islambda(f)
  BY callbyvalueApplyCases a ()
     
     x ≠ z 
     x,z can not occur free in f
  H  ⊢ 0 ≤ eval f a; 0
  H  ⊢ f ∈ Base
Definitions occuring in rule : 
or: P ∨ Q
, 
sqequal: s ~ t
, 
lambda: λx.A[x]
, 
isect: ⋂x:A. B[x]
, 
has-value: (a)↓
, 
isint: isint def, 
true: True
, 
bottom: ⊥
, 
islambda: if z is lambda then a otherwise b
, 
btrue: tt
, 
bfalse: ff
, 
sqle: s ≤ t
, 
callbyvalue: callbyvalue, 
apply: f a
, 
natural_number: $n
, 
member: t ∈ T
, 
base: Base
, 
axiom: Ax
Latex:
H    \mvdash{}  (f  \msim{}  \mlambda{}x.(f  x))  \mvee{}  (\mcap{}x:Base.  \mcap{}z:(x)\mdownarrow{}.    if  x  is  an  integer  then  True  else  f  x  \mleq{}  \mbot{})  ext  islambda(f)
    BY  callbyvalueApplyCases  a  ()
         
          x  \mneq{}  z 
          x,z  can  not  occur  free  in  f
    H    \mvdash{}  0  \mleq{}  eval  f  a;  0
    H    \mvdash{}  f  \mmember{}  Base
Date html generated:
2019_06_20-PM-04_12_09
Last ObjectModification:
2016_07_08-PM-03_49_05
Theory : rules
Home
Index