Nuprl Definition : sbhomout

sbhomout(a;b;c;d;L)
==r if L = Ax then sbcode(a + b;c + d) otherwise let h,t = L 
                                                 in if mtge1(a;b;c;d)
                                                      then eval a' = a - c in
                                                           eval b' = b - d in
                                                             [1 / sbhomout(a';b';c;d;L)]
                                                    if mtge1(c;d;a;b)
                                                      then eval c' = c - a in
                                                           eval d' = d - b in
                                                             [0 / sbhomout(a;b;c';d';L)]
                                                    else let h,t = L 
                                                         in if h=0
                                                               then eval a' = a + b in
                                                                    eval c' = c + d in
                                                                      sbhomout(a';b;c';d;t)
                                                               else eval b' = a + b in
                                                                    eval d' = c + d in
                                                                      sbhomout(a;b';c;d';t)
                                                    fi 
sbhomout(a;b;c;d;L) ==
  fix((λsbhomout,a,b,c,d,L. if L = Ax then sbcode(a + b;c + d) otherwise let h,t = L 
                                                                         in if mtge1(a;b;c;d)
                                                                              then eval a' = a - c in
                                                                                   eval b' = b - d in
                                                                                     [1 / (sbhomout a' b' c d L)]
                                                                            if mtge1(c;d;a;b)
                                                                              then eval c' = c - a in
                                                                                   eval d' = d - b in
                                                                                     [0 / (sbhomout a b c' d' L)]
                                                                            else let h,t = L 
                                                                                 in if h=0
                                                                                       then eval a' = a + b in
                                                                                            eval c' = c + d in
                                                                                              sbhomout a' b c' d t
                                                                                       else eval b' = a + b in
                                                                                            eval d' = c + d in
                                                                                              sbhomout a b' c d' t
                                                                            fi )) 
  a 
  b 
  c 
  d 
  L


Definitions occuring in Statement :  mtge1: mtge1(a;b;c;d),  sbcode: sbcode(m;n),  cons: [a / b],  callbyvalue: callbyvalue,  ifthenelse: if b then t else f fi ,  isaxiom: if z = Ax then a otherwise b,  int_eq: if a=b  then c  else d,  apply: f a,  fix: fix(F),  lambda: λx.A[x],  spread: spread def,  subtract: n - m,  add: n + m,  natural_number: $n
Definitions occuring in definition :  fix: fix(F),  lambda: λx.A[x],  isaxiom: if z = Ax then a otherwise b,  sbcode: sbcode(m;n),  ifthenelse: if b then t else f fi ,  mtge1: mtge1(a;b;c;d),  subtract: n - m,  cons: [a / b],  spread: spread def,  int_eq: if a=b  then c  else d,  natural_number: $n,  callbyvalue: callbyvalue,  add: n + m,  apply: f a
FDL editor aliases :  sbhomout
Latex:
sbhomout(a;b;c;d;L)
==r  if  L  =  Ax  then  sbcode(a  +  b;c  +  d)  otherwise  let  h,t  =  L 
                                                                                                  in  if  mtge1(a;b;c;d)
                                                                                                            then  eval  a'  =  a  -  c  in
                                                                                                                      eval  b'  =  b  -  d  in
                                                                                                                          [1  /  sbhomout(a';b';c;d;L)]
                                                                                                        if  mtge1(c;d;a;b)
                                                                                                            then  eval  c'  =  c  -  a  in
                                                                                                                      eval  d'  =  d  -  b  in
                                                                                                                          [0  /  sbhomout(a;b;c';d';L)]
                                                                                                        else  let  h,t  =  L 
                                                                                                                  in  if  h=0
                                                                                                                              then  eval  a'  =  a  +  b  in
                                                                                                                                        eval  c'  =  c  +  d  in
                                                                                                                                            sbhomout(a';b;c';d;t)
                                                                                                                              else  eval  b'  =  a  +  b  in
                                                                                                                                        eval  d'  =  c  +  d  in
                                                                                                                                            sbhomout(a;b';c;d';t)
                                                                                                        fi 

Latex:
sbhomout(a;b;c;d;L)  ==
    fix((\mlambda{}sbhomout,a,b,c,d,L.  if  L  =  Ax  then  sbcode(a  +  b;c  +  d)
                                                        otherwise  let  h,t  =  L 
                                                                            in  if  mtge1(a;b;c;d)
                                                                                      then  eval  a'  =  a  -  c  in
                                                                                                eval  b'  =  b  -  d  in
                                                                                                    [1  /  (sbhomout  a'  b'  c  d  L)]
                                                                                  if  mtge1(c;d;a;b)
                                                                                      then  eval  c'  =  c  -  a  in
                                                                                                eval  d'  =  d  -  b  in
                                                                                                    [0  /  (sbhomout  a  b  c'  d'  L)]
                                                                                  else  let  h,t  =  L 
                                                                                            in  if  h=0
                                                                                                        then  eval  a'  =  a  +  b  in
                                                                                                                  eval  c'  =  c  +  d  in
                                                                                                                      sbhomout  a'  b  c'  d  t
                                                                                                        else  eval  b'  =  a  +  b  in
                                                                                                                  eval  d'  =  c  +  d  in
                                                                                                                      sbhomout  a  b'  c  d'  t
                                                                                  fi  )) 
    a 
    b 
    c 
    d 
    L


Date html generated: 2016_05_15-PM-10_34_34
Last ObjectModification: 2015_09_23-AM-08_26_49

Theory : rationals


Home Index