Nuprl Definition : rat-cube-face-decider

rat-cube-face-decider(k;c;d) ==
  eval x = k in
  case int_seg_decide(λk.let a,J1 = d k 
                         in let x,x1 = c k 
                            in if qeq(a;x)
                                 then if qeq(x1;J1)
                                      then ifunion(qeq(J1;x); ifunion(qeq(x1;a); inr (λ%.Ax) ))
                                      else ifunion(qeq(J1;x); if qeq(x1;a) then inr (λ%.Ax)  else inl (λ%.Ax) fi )
                                      fi 
                               if qeq(J1;x) then if qeq(x1;J1) then inr (λ%.Ax)  else inl (λ%.Ax) fi 
                               else inl (λ%.Ax)
                               fi ;0;x)
   of inl(%6) =>
   inr let k,%7 = %6 
       in λ%8.Ax 
   | inr(%7) =>
   inl (λk.let a,J1 = d k 
           in let x,x1 = c k 
              in if qeq(a;x)
                   then if qeq(x1;J1)
                        then if qeq(J1;x) then if qeq(x1;a) then inl Ax else inr (inl Ax)  fi 
                             if qeq(x1;a) then inl Ax
                             else inr inr Ax  
                             fi 
                        else ifunion(qeq(J1;x); if qeq(x1;a) then inl Ax else Ax fi )
                        fi 
                 if qeq(J1;x) then if qeq(x1;J1) then inr (inl Ax)  else Ax fi 
                 else Ax
                 fi )


Definitions occuring in Statement :  qeq: qeq(r;s),  int_seg_decide: int_seg_decide(d;i;j),  callbyvalue: callbyvalue,  ifunion: ifunion(b; t),  ifthenelse: if b then t else f fi ,  apply: f a,  lambda: λx.A[x],  spread: spread def,  decide: case b of inl(x) => s[x] | inr(y) => t[y],  inr: inr x ,  inl: inl x,  natural_number: $n,  axiom: Ax
Definitions occuring in definition :  axiom: Ax,  inl: inl x,  inr: inr x ,  qeq: qeq(r;s),  ifthenelse: if b then t else f fi ,  ifunion: ifunion(b; t),  apply: f a,  spread: spread def,  lambda: λx.A[x],  natural_number: $n,  int_seg_decide: int_seg_decide(d;i;j),  decide: case b of inl(x) => s[x] | inr(y) => t[y],  callbyvalue: callbyvalue
FDL editor aliases :  rat-cube-face-decider
Latex:
rat-cube-face-decider(k;c;d)  ==
    eval  x  =  k  in
    case  int\_seg\_decide(\mlambda{}k.let  a,J1  =  d  k 
                                                  in  let  x,x1  =  c  k 
                                                        in  if  qeq(a;x)
                                                                  then  if  qeq(x1;J1)
                                                                            then  ifunion(qeq(J1;x);  ifunion(qeq(x1;a);  inr  (\mlambda{}\%.Ax)  ))
                                                                            else  ifunion(qeq(J1;x);
                                                                                                      if  qeq(x1;a)
                                                                                                      then  inr  (\mlambda{}\%.Ax) 
                                                                                                      else  inl  (\mlambda{}\%.Ax)
                                                                                                      fi  )
                                                                            fi 
                                                              if  qeq(J1;x)
                                                                  then  if  qeq(x1;J1)  then  inr  (\mlambda{}\%.Ax)    else  inl  (\mlambda{}\%.Ax)  fi 
                                                              else  inl  (\mlambda{}\%.Ax)
                                                              fi  ;0;x)
      of  inl(\%6)  =>
      inr  let  k,\%7  =  \%6 
              in  \mlambda{}\%8.Ax 
      |  inr(\%7)  =>
      inl  (\mlambda{}k.let  a,J1  =  d  k 
                      in  let  x,x1  =  c  k 
                            in  if  qeq(a;x)
                                      then  if  qeq(x1;J1)
                                                then  if  qeq(J1;x)  then  if  qeq(x1;a)  then  inl  Ax  else  inr  (inl  Ax)    fi 
                                                          if  qeq(x1;a)  then  inl  Ax
                                                          else  inr  inr  Ax   
                                                          fi 
                                                else  ifunion(qeq(J1;x);  if  qeq(x1;a)  then  inl  Ax  else  Ax  fi  )
                                                fi 
                                  if  qeq(J1;x)  then  if  qeq(x1;J1)  then  inr  (inl  Ax)    else  Ax  fi 
                                  else  Ax
                                  fi  )


Date html generated: 2019_10_29-AM-07_49_51
Last ObjectModification: 2019_10_19-AM-10_38_23

Theory : rationals


Home Index