Nuprl Definition : find_transitions

find_transitions(f;L) ==
  let h,hs = L 
  in eval b = f h hd(hs) in
     snd(snd(list_accum'(λd,l. let i,b,p,q = d 
                               in if isr(p) ∧b isr(q)
                                  then d
                                  else let a,as = l 
                                       in eval i' = i + 1 in
                                          if null(as)
                                          then eval b' = f a h in
                                               if b ∧b (¬bb')
                                                 then eval q' = if isl(q) then inr 0  else q fi  in
                                                      <i', b', inr i , q'>
                                               if b' ∧b (¬bb)
                                                 then eval p' = if isl(p) then inr 0  else p fi  in
                                                      <i', b', p', inr i >
                                               if isr(p) then <i', b', p, inr 0 >
                                               if isr(q) then <i', b', inr 0 , q>
                                               else <i', b', p, q>
                                               fi 
                                          else eval b' = f a hd(as) in
                                               if b ∧b (¬bb') then <i', b', inr i , q>
                                               if b' ∧b (¬bb) then <i', b', p, inr i >
                                               else <i', b', p, q>
                                               fi 
                                          fi 
                                  fi   ;<1, b, inl ⋅, inl ⋅>;tl(L))))


Definitions occuring in Statement :  list_accum': list_accum'(f;v;L),  hd: hd(l),  null: null(as),  tl: tl(l),  band: p ∧b q,  callbyvalue: callbyvalue,  bnot: ¬bb,  ifthenelse: if b then t else f fi ,  isr: isr(x),  isl: isl(x),  it: ⋅,  spreadn: spread4,  pi2: snd(t),  apply: f a,  lambda: λx.A[x],  spread: spread def,  pair: <a, b>,  inr: inr x ,  inl: inl x,  add: n + m,  natural_number: $n
Definitions occuring in definition :  tl: tl(l),  it: ⋅,  inl: inl x,  pair: <a, b>,  natural_number: $n,  inr: inr x ,  bnot: ¬bb,  band: p ∧b q,  ifthenelse: if b then t else f fi ,  hd: hd(l),  apply: f a,  callbyvalue: callbyvalue,  isr: isr(x),  isl: isl(x),  null: null(as),  add: n + m,  spread: spread def,  spreadn: spread4,  lambda: λx.A[x],  list_accum': list_accum'(f;v;L),  pi2: snd(t)
FDL editor aliases :  find_transitions
Latex:
find\_transitions(f;L)  ==
    let  h,hs  =  L 
    in  eval  b  =  f  h  hd(hs)  in
          snd(snd(list\_accum'(\mlambda{}d,l.  let  i,b,p,q  =  d 
                                                              in  if  isr(p)  \mwedge{}\msubb{}  isr(q)
                                                                    then  d
                                                                    else  let  a,as  =  l 
                                                                              in  eval  i'  =  i  +  1  in
                                                                                    if  null(as)
                                                                                    then  eval  b'  =  f  a  h  in
                                                                                              if  b  \mwedge{}\msubb{}  (\mneg{}\msubb{}b')
                                                                                                  then  eval  q'  =  if  isl(q)  then  inr  0    else  q  fi    in
                                                                                                            <i',  b',  inr  i  ,  q'>
                                                                                              if  b'  \mwedge{}\msubb{}  (\mneg{}\msubb{}b)
                                                                                                  then  eval  p'  =  if  isl(p)  then  inr  0    else  p  fi    in
                                                                                                            <i',  b',  p',  inr  i  >
                                                                                              if  isr(p)  then  <i',  b',  p,  inr  0  >
                                                                                              if  isr(q)  then  <i',  b',  inr  0  ,  q>
                                                                                              else  <i',  b',  p,  q>
                                                                                              fi 
                                                                                    else  eval  b'  =  f  a  hd(as)  in
                                                                                              if  b  \mwedge{}\msubb{}  (\mneg{}\msubb{}b')  then  <i',  b',  inr  i  ,  q>
                                                                                              if  b'  \mwedge{}\msubb{}  (\mneg{}\msubb{}b)  then  <i',  b',  p,  inr  i  >
                                                                                              else  <i',  b',  p,  q>
                                                                                              fi 
                                                                                    fi 
                                                                    fi      ;ə,  b,  inl  \mcdot{},  inl  \mcdot{}>tl(L))))


Date html generated: 2017_04_14-AM-08_48_37
Last ObjectModification: 2017_04_10-PM-11_25_16

Theory : list_0


Home Index