Nuprl Definition : ml-gcd-reduce-eq-constraints

ml-gcd-reduce-eq-constraints(sat;LL) ==
  ml-accum-abort(λL,Ls. let h.t = L 
                        in if null(t)
                           then if (h =z 0) then inl [L / Ls] else inr ⋅  fi 
                           else let g = ml-absval(ml-gcd-list(t)) in
                                    if 1 <z g
                                    then if (h rem g =z 0) then inl [ml-map(λx.(x ÷ g);L) / Ls] else inr ⋅  fi 
                                    else inl [L / Ls]
                                    fi 
                           fi ;inl sat;LL)


Definitions occuring in Statement :  ml-accum-abort: ml-accum-abort(f;sofar;L),  ml-absval: ml-absval(x),  ml-gcd-list: ml-gcd-list(L),  ml-map: ml-map(f;l),  spreadcons: spreadcons,  null: null(as),  cons: [a / b],  ifthenelse: if b then t else f fi ,  lt_int: i <z j,  eq_int: (i =z j),  let: let,  it: ⋅,  lambda: λx.A[x],  inr: inr x ,  inl: inl x,  remainder: n rem m,  divide: n ÷ m,  natural_number: $n
Definitions occuring in definition :  ml-accum-abort: ml-accum-abort(f;sofar;L),  spreadcons: spreadcons,  null: null(as),  let: let,  ml-absval: ml-absval(x),  ml-gcd-list: ml-gcd-list(L),  lt_int: i <z j,  ifthenelse: if b then t else f fi ,  eq_int: (i =z j),  remainder: n rem m,  natural_number: $n,  ml-map: ml-map(f;l),  lambda: λx.A[x],  divide: n ÷ m,  inr: inr x ,  it: ⋅,  cons: [a / b],  inl: inl x
FDL editor aliases :  ml-gcd-reduce-eq-constraints
Latex:
ml-gcd-reduce-eq-constraints(sat;LL)  ==
    ml-accum-abort(\mlambda{}L,Ls.  let  h.t  =  L 
                                                in  if  null(t)
                                                      then  if  (h  =\msubz{}  0)  then  inl  [L  /  Ls]  else  inr  \mcdot{}    fi 
                                                      else  let  g  =  ml-absval(ml-gcd-list(t))  in
                                                                        if  1  <z  g
                                                                        then  if  (h  rem  g  =\msubz{}  0)
                                                                                  then  inl  [ml-map(\mlambda{}x.(x  \mdiv{}  g);L)  /  Ls]
                                                                                  else  inr  \mcdot{} 
                                                                                  fi 
                                                                        else  inl  [L  /  Ls]
                                                                        fi 
                                                      fi  ;inl  sat;LL)


Date html generated: 2017_09_29-PM-05_57_19
Last ObjectModification: 2017_05_22-PM-02_30_36

Theory : omega


Home Index