Nuprl Rule : sqleLambda

H  ⊢ f ~ λx.(f x)

  BY sqleLambda y a ()
     
     x can not occur free in f
  H  ⊢ f ≤ λy.a
  H  ⊢ (f)↓


Definitions occuring in rule :  sqequal: s ~ t,  apply: f a,  sqle: s ≤ t,  lambda: λx.A[x],  has-value: (a)↓,  axiom: Ax
Latex:
H    \mvdash{}  f  \msim{}  \mlambda{}x.(f  x)

    BY  sqleLambda  y  a  ()
         
          x  can  not  occur  free  in  f
    H    \mvdash{}  f  \mleq{}  \mlambda{}y.a
    H    \mvdash{}  (f)\mdownarrow{}


Date html generated: 2019_06_20-PM-04_12_09
Last ObjectModification: 2015_11_25-PM-03_46_59

Theory : rules


Home Index