Nuprl Definition : mrec_ind

mrec_ind(L;h;x) ==
  let i,x1 
  in letrec r(i)=λx.(h (fst(x)) (snd(x)) 
                     let L' case apply-alist(AtomDeq;L;i)
                               of inl(L2) =>
                               case apply-alist(AtomDeq;L2;fst(x)) of inl(as) => as inr(_) => Ax
                               inr(_) =>
                               Ax in
                         λ L'[j]
                             of inl(x@0) =>
                             case x@0 of inl(x1) => x1 snd(x).j inr(y) => λi@0.(r snd(x).j[i@0])
                             inr(y) =>
                             Ax) in

Definitions occuring in Statement :  select-tuple: x.n apply-alist: apply-alist(eq;L;x) select: L[n] length: ||as|| atom-deq: AtomDeq genrec-ap: genrec-ap let: let pi1: fst(t) pi2: snd(t) apply: a lambda: λx.A[x] spread: spread def decide: case of inl(x) => s[x] inr(y) => t[y] axiom: Ax
Definitions occuring in definition :  spread: spread def genrec-ap: genrec-ap let: let apply-alist: apply-alist(eq;L;x) atom-deq: AtomDeq pi1: fst(t) decide: case of inl(x) => s[x] inr(y) => t[y] lambda: λx.A[x] apply: a select: L[n] select-tuple: x.n length: ||as|| pi2: snd(t) axiom: Ax
FDL editor aliases :  mrec_ind

mrec\_ind(L;h;x)  ==
    let  i,x1  =  x 
    in  letrec  r(i)=\mlambda{}x.(h  i  (fst(x))  (snd(x)) 
                                          let  L'  =  case  apply-alist(AtomDeq;L;i)
                                                              of  inl(L2)  =>
                                                              case  apply-alist(AtomDeq;L2;fst(x))  of  inl(as)  =>  as  |  inr($_\000C{}$)  =>  Ax
                                                              |  inr($_{}$)  =>
                                                              Ax  in
                                                  \mlambda{}  L'[j]
                                                          of  inl(x@0)  =>
                                                          case  x@0
                                                            of  inl(x1)  =>
                                                            r  x1  snd(x).j
                                                            |  inr(y)  =>
                                                            \mlambda{}i@0.(r  y  snd(x).j[i@0])
                                                          |  inr(y)  =>
                                                          Ax)  in

Date html generated: 2019_06_20-PM-02_16_21
Last ObjectModification: 2019_02_28-PM-06_07_55

Theory : tuples

Home Index