Nuprl Lemma : st_exp_ind_wf

[X:{j}]. [x:st_exp{i:l}()]. [var:name:Atom  X]. [const:val:st-constant{i:l}  X]. [ap:fun:st_exp{i:l}()
                                                                                                arg:st_exp{i:l}()
                                                                                                rec1:X
                                                                                                rec2:X
                                                                                                X].
[lambda:bound:Atom  type:SimpleType  body:st_exp{i:l}()  rec1:X  X].
  (st_exp_ind(x)
   var(name)=>var[name]
   const(val)=>const[val]
   fun(arg)=>rec1,rec2.ap[fun;arg;rec1;rec2]
   bound:type.body=>rec1.lambda[bound;type;body;rec1]  X)


Proof not projected

Error : references
\mforall{}[X:\mBbbU{}\{j\}].  \mforall{}[x:st\_exp\{i:l\}()].  \mforall{}[var:name:Atom  {}\mrightarrow{}  X].  \mforall{}[const:val:st-constant\{i:l\}  {}\mrightarrow{}  X].
\mforall{}[ap:fun:st\_exp\{i:l\}()  {}\mrightarrow{}  arg:st\_exp\{i:l\}()  {}\mrightarrow{}  rec1:X  {}\mrightarrow{}  rec2:X  {}\mrightarrow{}  X].
\mforall{}[lambda:bound:Atom  {}\mrightarrow{}  type:SimpleType  {}\mrightarrow{}  body:st\_exp\{i:l\}()  {}\mrightarrow{}  rec1:X  {}\mrightarrow{}  X].
    (st\_exp\_ind(x)
      var(name)=>var[name]
      const(val)=>const[val]
      fun(arg)=>rec1,rec2.ap[fun;arg;rec1;rec2]
      \mlambda{}bound:type.body=>rec1.lambda[bound;type;body;rec1]  \mmember{}  X)


Date html generated: 2012_02_20-PM-07_50_49
Last ObjectModification: 2011_02_04-AM-11_57_01

Home Index