Nuprl Definition : transMoves

transMoves(X;Y;moves) ==
  if (||moves|| =z 0)
  then <seq-nil(), seq-nil()>
  else let a,b = transMoves(X;Y;seq-truncate(moves;||moves|| - 2)) 
       in let x,z1 = if (||moves|| =z 2) then <(), ()> else X a fi  
          in let z2,y = if (||moves|| =z 2) then <(), ()> else Y b fi  
             in let u,v = moves[||moves|| - 1] 
                in if copath-length(x) <z copath-length(u)
                   then let M1 = seq-add(seq-add(a;<x, z1>);<u, z1>) in
                         let M2 = seq-add(seq-add(b;<z2, y>);<snd((X M1)), y>) in
                         <M1, M2>
                   else let M2 = seq-add(seq-add(b;<z2, y>);<z2, v>) in
                         let M1 = seq-add(seq-add(a;<x, z1>);<x, fst((Y M2))>) in
                         <M1, M2>
                   fi 
  fi 


Definitions occuring in Statement :  copath-nil: (),  copath-length: copath-length(p),  seq-add: seq-add(s;x),  seq-nil: seq-nil(),  seq-truncate: seq-truncate(s;n),  seq-item: s[i],  seq-len: ||s||,  ifthenelse: if b then t else f fi ,  lt_int: i <z j,  eq_int: (i =z j),  let: let,  pi1: fst(t),  pi2: snd(t),  apply: f a,  spread: spread def,  pair: <a, b>,  subtract: n - m,  natural_number: $n
Definitions occuring in definition :  seq-nil: seq-nil(),  seq-truncate: seq-truncate(s;n),  eq_int: (i =z j),  copath-nil: (),  spread: spread def,  seq-item: s[i],  subtract: n - m,  seq-len: ||s||,  natural_number: $n,  ifthenelse: if b then t else f fi ,  lt_int: i <z j,  copath-length: copath-length(p),  pi2: snd(t),  let: let,  seq-add: seq-add(s;x),  pi1: fst(t),  apply: f a,  pair: <a, b>
FDL editor aliases :  transMoves
Latex:
transMoves(X;Y;moves)  ==
    if  (||moves||  =\msubz{}  0)
    then  <seq-nil(),  seq-nil()>
    else  let  a,b  =  transMoves(X;Y;seq-truncate(moves;||moves||  -  2)) 
              in  let  x,z1  =  if  (||moves||  =\msubz{}  2)  then  <(),  ()>  else  X  a  fi   
                    in  let  z2,y  =  if  (||moves||  =\msubz{}  2)  then  <(),  ()>  else  Y  b  fi   
                          in  let  u,v  =  moves[||moves||  -  1] 
                                in  if  copath-length(x)  <z  copath-length(u)
                                      then  let  M1  =  seq-add(seq-add(a;<x,  z1>);<u,  z1>)  in
                                                  let  M2  =  seq-add(seq-add(b;<z2,  y>);<snd((X  M1)),  y>)  in
                                                  <M1,  M2>
                                      else  let  M2  =  seq-add(seq-add(b;<z2,  y>);<z2,  v>)  in
                                                  let  M1  =  seq-add(seq-add(a;<x,  z1>);<x,  fst((Y  M2))>)  in
                                                  <M1,  M2>
                                      fi 
    fi 


Date html generated: 2019_06_20-PM-01_06_58
Last ObjectModification: 2019_01_02-PM-01_34_59

Theory : co-recursion-2


Home Index