Nuprl Definition : setmemfunc

setmemfunc(x1; s1; x2; s2) ==
  λ%,%1. <λ%5.let x,y = s2 
              in let b,y1 = %5 
                 in let q1,y2 = %1 
                                <2
                                , λi.if i=0
                                     then <(), ()>
                                     else if i - 1=0 then <copath-cons(b;()), ()> else (⋅ (i - 1 - 1))
                                > 
                    in <copath-hd(y2)
                       , seteqtrans() x2 x1 (y copath-hd(y2)) (seteqinv() x1 x2 %) 
                         coW-trans(y1;
                                   λmoves.let u,v = %1 
                                                    let k,g = moves 
                                                    in <(k + 1) + 1
                                                       , λi.if i=0
                                                            then <(), ()>
                                                            else if i - 1=0
                                                                 then <copath-cons(b;()), ()>
                                                                 else let u,v = g (i - 1 - 1) 
                                                                      in <copath-cons(b;u)
                                                                         , copath-cons(copath-hd(y2);v)
                                                                         >
                                                       > 
                                          in <copath-tl(u), copath-tl(v)>)
                       >
         , λ%5.let x,y = s1 
               in let b,y1 = %5 
                  in let u,y2 = %1 
                                <2
                                , λi.if i=0
                                     then <(), ()>
                                     else if i - 1=0 then <(), copath-cons(b;())> else let u,v = ⋅ (i - 1 - 1) in <v, u>
                                > 
                     in <copath-hd(u)
                        , seteqtrans() x1 x2 (y copath-hd(u)) % 
                          coW-trans(y1;
                                    λmoves.let u,v = %1 
                                                     let k,g = moves 
                                                     in <(k + 1) + 1
                                                        , λi.if i=0
                                                             then <(), ()>
                                                             else if i - 1=0
                                                                  then <(), copath-cons(b;())>
                                                                  else let u@0,v = g (i - 1 - 1) 
                                                                       in <copath-cons(copath-hd(u);v)
                                                                          , copath-cons(b;u@0)
                                                                          >
                                                        > 
                                           in <copath-tl(v), copath-tl(u)>)
                        >
         >


Definitions occuring in Statement :  seteqtrans: seteqtrans(),  seteqinv: seteqinv(),  coW-trans: coW-trans(X; Y),  copath-cons: copath-cons(b;x),  copath-tl: copath-tl(x),  copath-hd: copath-hd(p),  copath-nil: (),  it: ⋅,  int_eq: if a=b then c else d,  apply: f a,  lambda: λx.A[x],  spread: spread def,  pair: <a, b>,  subtract: n - m,  add: n + m,  natural_number: $n
Definitions occuring in definition :  it: ⋅,  seteqtrans: seteqtrans(),  seteqinv: seteqinv(),  coW-trans: coW-trans(X; Y),  add: n + m,  copath-hd: copath-hd(p),  copath-tl: copath-tl(x),  spread: spread def,  apply: f a,  lambda: λx.A[x],  int_eq: if a=b then c else d,  subtract: n - m,  natural_number: $n,  pair: <a, b>,  copath-nil: (),  copath-cons: copath-cons(b;x)
Latex:
setmemfunc(x1;  s1;  x2;  s2)  ==
    \mlambda{}\%,\%1.  <\mlambda{}\%5.let  x,y  =  s2 
                            in  let  b,y1  =  \%5 
                                  in  let  q1,y2  =  \%1 
                                                                ɚ
                                                                ,  \mlambda{}i.if  i=0
                                                                          then  <(),  ()>
                                                                          else  if  i  -  1=0
                                                                                    then  <copath-cons(b;()),  ()>
                                                                                    else  (\mcdot{}  (i  -  1  -  1))
                                                                > 
                                        in  <copath-hd(y2)
                                              ,  seteqtrans()  x2  x1  (y  copath-hd(y2))  (seteqinv()  x1  x2  \%) 
                                                  coW-trans(y1;
                                                                      \mlambda{}moves.let  u,v  =
                                                                                      \%1 
                                                                                      let  k,g  =  moves 
                                                                                      in  <(k  +  1)  +  1
                                                                                            ,  \mlambda{}i.if  i=0
                                                                                                      then  <(),  ()>
                                                                                                      else  if  i  -  1=0
                                                                                                                then  <copath-cons(b;()),  ()>
                                                                                                                else  let  u,v  =  g  (i  -  1  -  1) 
                                                                                                                          in  <copath-cons(b;u)
                                                                                                                                ,  copath-cons(copath-hd(y2);v)
                                                                                                                                >
                                                                                            > 
                                                                                    in  <copath-tl(u),  copath-tl(v)>)
                                              >
                  ,  \mlambda{}\%5.let  x,y  =  s1 
                              in  let  b,y1  =  \%5 
                                    in  let  u,y2  =  \%1 
                                                                ɚ
                                                                ,  \mlambda{}i.if  i=0
                                                                          then  <(),  ()>
                                                                          else  if  i  -  1=0
                                                                                    then  <(),  copath-cons(b;())>
                                                                                    else  let  u,v  =  \mcdot{}  (i  -  1  -  1) 
                                                                                              in  <v,  u>
                                                                > 
                                          in  <copath-hd(u)
                                                ,  seteqtrans()  x1  x2  (y  copath-hd(u))  \% 
                                                    coW-trans(y1;
                                                                        \mlambda{}moves.let  u,v  =
                                                                                        \%1 
                                                                                        let  k,g  =  moves 
                                                                                        in  <(k  +  1)  +  1
                                                                                              ,  \mlambda{}i.if  i=0
                                                                                                        then  <(),  ()>
                                                                                                        else  if  i  -  1=0
                                                                                                                  then  <(),  copath-cons(b;())>
                                                                                                                  else  let  u@0,v  =  g  (i  -  1  -  1) 
                                                                                                                            in  <copath-cons(copath-hd(u);v)
                                                                                                                                  ,  copath-cons(b;u@0)
                                                                                                                                  >
                                                                                              > 
                                                                                      in  <copath-tl(v),  copath-tl(u)>)
                                                >
                  >


Date html generated: 2018_07_29-AM-09_51_34
Last ObjectModification: 2018_07_11-PM-00_33_02

Theory : constructive!set!theory


Home Index