app/willard/test1

   1 Input:
   2 let
   3    F={x: x in S | ((forall y in U.((y > x) or(x = x))) and(x /= 0))}
   4 in
   5    F
   6 end
   7
   8    let
   9       F={x: x in S | ((forall y in U.((y > x) or(x = x))) and(x /= 0))}
  10    in
  11       F
  12    end
  13
  14
  15 [Renaming phase]
  16
  17    let
  18       F={x: x in S | ((forall y in U.((y > x) or(x = x))) and(x /= 0))}
  19    in
  20       F
  21    end
  22
  23
  24 [DNF construction and simplification phase]
  25
  26 {x: x in S | ((nonempty U) and(x /= 0))}
  27
  28 [Constructing the query graph]
  29
  30 [Query Graph]
  31 {x: x in S | ((nonempty U) and(x /= 0))}
  32
  33 [Quantifier elimination phase]
  34
  35 if(nonempty U) then{x: x in S | (x /= 0)} else {}
  36
  37 [Disjunction removal phase]
  38
  39 if(nonempty U) then{x: x in S | (x /= 0)} else {}
  40
  41 [Conjunctive query decomposition phase]
  42
  43 [Query Graph]
  44 if(nonempty U) then{x: x in S | (x /= 0)} else {}
  45
  46 [Projection recognition phase]
  47
  48 if(nonempty U) then{x: x in S | (x /= 0)} else {}
  49
  50 [Simple find/count query decomposition phase]
  51
  52 Output:
  53 if(nonempty U) then{x: x in S | (x /= 0)} else {}