Home Intro Announce FAQ Docs Download Mail Status Bugs Users Related FM Tools

PVS Bug 1035


Synopsis:        error when replaying a proof which worked in version 4.0
Severity:        serious
Priority:        medium
Responsible:     owre
State:           open
Class:           sw-bug
Arrival-Date:    Wed Apr 23 12:15:01 -0700 2008
Originator:      Viorel Preoteasa
Release:         PVS 4.1
Organization:    abo.fi
Environment: 
 System:          
 Architecture: 

Description: 
  
  --Apple-Mail-2-870090089
  Content-Type: text/plain;
  	charset=US-ASCII;
  	format=flowed;
  	delsp=yes
  Content-Transfer-Encoding: 7bit
  
  PVS version: 4.1
  OS: OS X Leopard
  
  When I replay a old proof I get the following error:
  
  Rerunning step: (use "fixpoint_induct")
  Error: the assertion
          (subsetp (freevars preds)
                   (union (freevars ex) *bound-variables*)
            :key #'declaration)
          failed.
     [condition type: simple-error]
  
  The error occurs when proving the last lemma from the attached theory.
  
  The same holds if I try (lemma "fixpoint_induct") (inst?) (inst -  
  "....")
  
  Attached is the theory file and the proof file which generate this  
  error.
  
  Best regards,
  
  Viorel Preoteasa
  
  
  --Apple-Mail-2-870090089
  Content-Disposition: attachment;
  	filename=complete-lattice.pvs
  Content-Type: application/octet-stream;
  	x-unix-mode=0644;
  	name="complete-lattice.pvs"
  Content-Transfer-Encoding: 7bit
  
  po[A: type+]: theory
  begin
      importing orders[A]
      po: type = (partial_order?)
  
  
      le: var [A, A -> bool]
  
      p: var pred[A]
      x, y: var A
  
      lb?(le)(p)(x): bool = forall (y:(p)): le(x, y)
  
      ub?(le)(p)(x): bool = forall (y:(p)): le(y, x)
  
      glb?(le)(p)(x): bool =
        lb?(le)(p)(x) and forall y: lb?(le)(p)(y) => le(y, x)
  
      lub?(le)(p)(x): bool =
        ub?(le)(p)(x) and forall y: ub?(le)(p)(y) => le(x, y)
  
      bottom?(le)(x): bool = forall y: le(x, y)
  
      top?(le)(x): bool = forall y: le(y, x)
  
      ; <= : var po
  
      unique_glb: judgement glb?(<=)(p) has_type (unique?[A])
  
      unique_lub: judgement lub?(<=)(p) has_type (unique?[A])
  
      unique_lub_rw: lemma forall (a, b: (lub?(<=)(p))): a = b
  
      unique_bottom: judgement bottom?(<=) has_type (unique?[A])
  
      unique_top: judgement top?(<=) has_type (unique?[A])
  
  
      top_lub: lemma lub?(<=)(fullset)(x) => top?(<=)(x)
  
      top_glb: lemma glb?(<=)(emptyset)(x) => top?(<=)(x)
  
      bottom_lub: lemma lub?(<=)(emptyset)(x) => bottom?(<=)(x)
  
      bottom_glb: lemma glb?(<=)(fullset)(x) => bottom?(<=)(x)
  
      exists_glb?(<=): bool = forall p: exists x: (glb?(<=)(p)(x))
  
      exists_lub?(<=): bool = forall p: exists x: (lub?(<=)(p)(x))
  
      exists_bottom?(<=): bool = exists x: (bottom?(<=)(x))
  
      exists_top?(<=): bool = exists x: (top?(<=)(x))
  
      glb_lub: judgement (exists_glb?) subtype_of (exists_lub?)
      
      lub_glb: judgement (exists_lub?) subtype_of (exists_glb?)
  
      bottom_is_lub: judgement (exists_lub?) subtype_of (exists_bottom?)
  
      top_is_lub: judgement (exists_lub?) subtype_of (exists_top?)
  
  end po
  
  family[I: type, T: type+]: theory
    begin
      op: var [set[T] -> T]
      f: var [I -> T]
      x: var T
      i: var I
      family(op)(f): T = op({x | exists i: x = f(i)})
  
    end family
  
  cl[L: type+]: theory
    begin
      importing po[L]
  
      less: var [L, L -> bool]
  
      cl?(less): bool = 
            partial_order?(less) and 
            exists_glb?(less) and  
            exists_lub?(less) and 
            exists_bottom?(less) and 
            exists_top?(less)
  
      cl: type = (cl?)
  
      cl_is_po: judgement cl subtype_of po
  
      lub_is_cl: judgement (exists_lub?) subtype_of cl
  
      <=: var cl
  
      p: var pred[L]
  
      glb(<=, p): type+ = (glb?(<=)(p))
  
      lub(<=, p): type+ = (lub?(<=)(p))
  
      top(<=): type+ = (top?(<=))
  
      bottom(<=): type+ = (bottom?(<=))
  
  
      inf(<=)(p): glb(<=, p)
  
      sup(<=)(p): lub(<=, p)
  
      bottom(<=): bottom(<=)
      
      top(<=): top(<=)
  
      x, y, z, a: var L
  
      inf_lemma: lemma (forall x: p(x) => a <= x) and 
           (forall x: (forall y: p(y) => x <= y) => x <= a) => a = inf(<=)(p)
  
      transitivity: lemma x <= y and y <= z => x <= z
  
    end cl
  
  cl_lift[T: type+, L: type+]: theory
    begin
      importing cl
  
      importing family[T, L]
  
      <=: var cl[L]
  
      f, g: var [T -> L]
  
      x: var T
  
      lift(<=): cl[[T -> L]] = lambda f, g: forall x: f(x) <= g(x)
  
      op: var [set[L] -> L] 
  
      X: var set[[T -> L]]
  
      a: var L
  
      lift(op)(X): [T -> L] = lambda x: op(lambda a: exists f: X(f) and a = f(x
 ))
  
  
      lift_inf: lemma lift(inf(<=)) = inf(lift(<=))
  
      lift_sup: lemma lift(sup(<=)) = sup(lift(<=))
  
    end cl_lift
  
  monotonic[L1: type+, L2: type+]: theory
    begin
      importing cl
  
      x, y: var L1
      f: var [L1 -> L2]
  
      monotonic?(<=: cl[L1])(<=: cl[L2])(f): bool = forall x, y: x <= y => f(x)
  <= f(y);
  
      monotonic(lesseq1: cl[L1], lesseq2: cl[L2]): type+ = (monotonic?(lesseq1)
 (lesseq2)) 
            containing (lambda x: bottom(lesseq2))
  
      ; <=: var cl[L1]
  
      le: var cl[L2]
  
      A: var pred[L1]
  
      monotonic_inf: lemma monotonic?(<=)(le)(f) => le(f(inf(<=)(A)), inf(le)(i
 mage(f, A)))
  
    end monotonic
  
  fixpoint[L: type+]: theory
    begin
      importing monotonic[L, L]
      importing cl[L]
      
      <=: var cl
  
      x, y: var L
  
      f: var [L -> L]
  
      monotonic?(<=)(f): bool = monotonic?(<=)(<=)(f)
  
      monotonic(<=): type+ = (monotonic?(<=))
  
      fixpoint?(f)(x): bool = f(x) = x
  
      fixpoint(f): type = (fixpoint?(f))
  
      lfp?(<=)(f)(x): bool =  fixpoint?(f)(x) and (forall y:  fixpoint?(f)(y) =
 > x <= y)
  
      lfp?(<=, f)(x): bool = lfp?(<=)(f)(x)
  
      unique_lfp: judgement lfp?(<=)(f) has_type (unique?[L])
  
      knaster_tarski: theorem monotonic?(<=)(f) => exists x:  lfp?(<=)(f)(x)
  
      mu(<=)(f: monotonic(<=)): (lfp?(<=)(f)) = epsilon(lfp?(<=)(f))
  
      mu_fixpoint: judgement mu(<=)(f:  monotonic(<=)) has_type fixpoint(f)
   
    end fixpoint
  
  fixpoint_induct[W: type+, <: (well_founded?[W]), L: type+]: theory
    begin
      importing fixpoint[L]
      importing family[W, L];
      
      <=: var cl
  
      p: var [W -> L]
  
      v, w: var W
  
      x, y, z: var L
  
      f: var [L -> L]
  
  
      below(<=)(p)(w): L = sup(<=)({x | exists v: (v < w) and x = p(v)})
  
      sup(<=)(p): L      = sup(<=)({x | exists v: x = p(v)})
  
      X: var set[L]
  
      fixpoint_induct: lemma  forall (f: monotonic(<=)), (x: fixpoint(f)):
           (forall w: p(w) <= f(below(<=)(p)(w))) => (sup(<=)(p) <= x)
  
      fixpoint_induct1: lemma  forall (f: monotonic(<=)):
           (forall w: p(w) <= f(below(<=)(p)(w))) => (sup(<=)(p) <= mu(<=)(f))
  
    end fixpoint_induct
  
  
  
  --Apple-Mail-2-870090089
  Content-Disposition: attachment;
  	filename=complete-lattice.prf
  Content-Type: application/octet-stream;
  	x-unix-mode=0644;
  	name="complete-lattice.prf"
  Content-Transfer-Encoding: 7bit
  
  (po
   (unique_glb 0
    (unique_glb-1 nil 3252993907 3311852817
     ("" (skosimp*)
      (("" (typepred "lesseqp!1")
        (("" (expand "unique?")
          (("" (skosimp*)
            (("" (expand "glb?")
              (("" (ground)
                (("" (inst -3 "y!1")
                  (("" (inst -5 "x!1") (("" (grind) nil nil)) nil)) nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil)
     proved
     ((po type-eq-decl nil po nil)
      (partial_order? const-decl "bool" orders nil)
      (pred type-eq-decl nil defined_types nil)
      (A formal-nonempty-type-decl nil po nil)
      (NOT const-decl "[bool -> bool]" booleans nil)
      (bool nonempty-type-eq-decl nil booleans nil)
      (boolean nonempty-type-decl nil booleans nil)
      (reflexive? const-decl "bool" relations nil)
      (transitive? const-decl "bool" relations nil)
      (preorder? const-decl "bool" orders nil)
      (antisymmetric? const-decl "bool" relations nil)
      (lb? const-decl "bool" po nil) (glb? const-decl "bool" po nil)
      (unique? const-decl "bool" exists1 nil))
     432 290 t shostak))
   (unique_lub 0
    (unique_lub-1 nil 3252994101 3311852818
     ("" (skosimp*)
      (("" (expand "unique?")
        (("" (skosimp*)
          (("" (expand "lub?")
            (("" (ground)
              (("" (typepred "lesseqp!1")
                (("" (inst -3 "y!1")
                  (("" (inst -5 "x!1") (("" (grind) nil nil)) nil)) nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil)
     proved
     ((unique? const-decl "bool" exists1 nil)
      (lub? const-decl "bool" po nil) (po type-eq-decl nil po nil)
      (partial_order? const-decl "bool" orders nil)
      (pred type-eq-decl nil defined_types nil)
      (A formal-nonempty-type-decl nil po nil)
      (NOT const-decl "[bool -> bool]" booleans nil)
      (bool nonempty-type-eq-decl nil booleans nil)
      (boolean nonempty-type-decl nil booleans nil)
      (reflexive? const-decl "bool" relations nil)
      (transitive? const-decl "bool" relations nil)
      (preorder? const-decl "bool" orders nil)
      (antisymmetric? const-decl "bool" relations nil)
      (ub? const-decl "bool" po nil))
     351 270 t shostak))
   (unique_lub_rw 0
    (unique_lub_rw-1 nil 3311852829 3311852880
     ("" (skosimp*)
      (("" (typepred "a!1" "b!1")
        (("" (use "unique_lub")
          (("" (expand "unique?")
            (("" (inst?) (("" (assert) nil nil)) nil)) nil))
          nil))
        nil))
      nil)
     proved
     ((po type-eq-decl nil po nil)
      (partial_order? const-decl "bool" orders nil)
      (lub? const-decl "bool" po nil)
      (pred type-eq-decl nil defined_types nil)
      (A formal-nonempty-type-decl nil po nil)
      (NOT const-decl "[bool -> bool]" booleans nil)
      (bool nonempty-type-eq-decl nil booleans nil)
      (boolean nonempty-type-decl nil booleans nil)
      (unique? const-decl "bool" exists1 nil)
      (unique_lub judgement-tcc nil po nil))
     51117 820 t shostak))
   (unique_bottom 0
    (unique_bottom-1 nil 3252994416 3311852818
     ("" (skosimp*)
      (("" (expand "unique?")
        (("" (skosimp*)
          (("" (expand "bottom?")
            (("" (inst -1 "y!1")
              (("" (inst -2 "x!1")
                (("" (typepred "lesseqp!1") (("" (grind) nil nil)) nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil)
     proved
     ((unique? const-decl "bool" exists1 nil)
      (bottom? const-decl "bool" po nil)
      (reflexive? const-decl "bool" relations nil)
      (transitive? const-decl "bool" relations nil)
      (preorder? const-decl "bool" orders nil)
      (antisymmetric? const-decl "bool" relations nil)
      (boolean nonempty-type-decl nil booleans nil)
      (bool nonempty-type-eq-decl nil booleans nil)
      (NOT const-decl "[bool -> bool]" booleans nil)
      (pred type-eq-decl nil defined_types nil)
      (partial_order? const-decl "bool" orders nil)
      (po type-eq-decl nil po nil)
      (A formal-nonempty-type-decl nil po nil))
     261 210 t shostak))
   (unique_top 0
    (unique_top-1 nil 3252994296 3311852818
     ("" (skosimp*)
      (("" (typepred "lesseqp!1")
        (("" (expand "unique?")
          (("" (skosimp*)
            (("" (expand "top?")
              (("" (inst -2 "y!1")
                (("" (inst -3 "x!1") (("" (grind) nil nil)) nil)) nil))
              nil))
            nil))
          nil))
        nil))
      nil)
     proved
     ((po type-eq-decl nil po nil)
      (partial_order? const-decl "bool" orders nil)
      (pred type-eq-decl nil defined_types nil)
      (A formal-nonempty-type-decl nil po nil)
      (NOT const-decl "[bool -> bool]" booleans nil)
      (bool nonempty-type-eq-decl nil booleans nil)
      (boolean nonempty-type-decl nil booleans nil)
      (reflexive? const-decl "bool" relations nil)
      (transitive? const-decl "bool" relations nil)
      (preorder? const-decl "bool" orders nil)
      (antisymmetric? const-decl "bool" relations nil)
      (top? const-decl "bool" po nil)
      (unique? const-decl "bool" exists1 nil))
     284 210 t shostak))
   (top_lub 0
    (top_lub-1 nil 3252995112 3310370906
     ("" (skosimp*)
      (("" (expand "top?")
        (("" (skosimp*)
          (("" (expand "lub?")
            (("" (skosimp*) (("" (hide -2) (("" (grind) nil nil)) nil))
              nil))
            nil))
          nil))
        nil))
      nil)
     unfinished
     ((top? const-decl "bool" po nil) (lub? const-decl "bool" po nil)
      (set type-eq-decl nil sets nil)
      (bool nonempty-type-eq-decl nil booleans nil)
      (boolean nonempty-type-decl nil booleans nil)
      (A formal-nonempty-type-decl nil po nil)
      (ub? const-decl "bool" po nil) (fullset const-decl "set" sets nil))
     126 90 t shostak))
   (top_glb 0
    (top_glb-1 nil 3252995215 3310370906
     ("" (skosimp*)
      (("" (expand "glb?")
        (("" (ground)
          (("" (expand "top?")
            (("" (skosimp*) (("" (hide -1) (("" (grind) nil nil)) nil))
              nil))
            nil))
          nil))
        nil))
      nil)
     unfinished
     ((glb? const-decl "bool" po nil) (top? const-decl "bool" po nil)
      (A formal-nonempty-type-decl nil po nil)
      (emptyset const-decl "set" sets nil)
      (set type-eq-decl nil sets nil)
      (NOT const-decl "[bool -> bool]" booleans nil)
      (bool nonempty-type-eq-decl nil booleans nil)
      (boolean nonempty-type-decl nil booleans nil)
      (lb? const-decl "bool" po nil))
     193 100 t shostak))
   (bottom_lub 0
    (bottom_lub-1 nil 3252995438 3310370906
     ("" (skosimp*)
      (("" (expand "lub?")
        (("" (ground)
          (("" (hide -1)
            (("" (expand "bottom?")
              (("" (skosimp*) (("" (grind) nil nil)) nil)) nil))
            nil))
          nil))
        nil))
      nil)
     unfinished
     ((lub? const-decl "bool" po nil)
      (A formal-nonempty-type-decl nil po nil)
      (emptyset const-decl "set" sets nil)
      (set type-eq-decl nil sets nil)
      (NOT const-decl "[bool -> bool]" booleans nil)
      (bool nonempty-type-eq-decl nil booleans nil)
      (boolean nonempty-type-decl nil booleans nil)
      (ub? const-decl "bool" po nil) (bottom? const-decl "bool" po nil))
     196 120 t shostak))
   (bottom_glb 0
    (bottom_glb-1 nil 3252995485 3310370906
     ("" (skosimp*)
      (("" (expand "bottom?")
        (("" (skosimp*)
          (("" (expand "glb?")
            (("" (ground) (("" (hide -2) (("" (grind) nil nil)) nil))
              nil))
            nil))
          nil))
        nil))
      nil)
     unfinished
     ((bottom? const-decl "bool" po nil) (glb? const-decl "bool" po nil)
      (set type-eq-decl nil sets nil)
      (bool nonempty-type-eq-decl nil booleans nil)
      (boolean nonempty-type-decl nil booleans nil)
      (A formal-nonempty-type-decl nil po nil)
      (lb? const-decl "bool" po nil) (fullset const-decl "set" sets nil))
     129 90 t shostak))
   (glb_lub 0
    (glb_lub-1 nil 3253001642 3311852819
     ("" (skosimp*)
      (("" (typepred "x!1")
        (("" (expand "exists_lub?")
          (("" (expand "exists_glb?")
            (("" (skosimp*)
              (("" (expand "exists1")
                (("" (inst -2 "ub?(x!1)(p!1)")
                  (("" (skosimp*)
                    (("" (inst 1 "x!2")
                      (("" (expand "lub?")
                        (("" (ground)
                          (("1" (grind) nil nil)
                           ("2" (skosimp*)
                            (("2" (expand "glb?")
                              (("2" (ground) (("2" (grind) nil nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil)
     proved
     ((exists_glb? const-decl "bool" po nil) (po type-eq-decl nil po nil)
      (partial_order? const-decl "bool" orders nil)
      (pred type-eq-decl nil defined_types nil)
      (A formal-nonempty-type-decl nil po nil)
      (NOT const-decl "[bool -> bool]" booleans nil)
      (bool nonempty-type-eq-decl nil booleans nil)
      (boolean nonempty-type-decl nil booleans nil)
      (ub? const-decl "bool" po nil) (glb? const-decl "bool" po nil)
      (lb? const-decl "bool" po nil)
      (antisymmetric? const-decl "bool" relations nil)
      (preorder? const-decl "bool" orders nil)
      (transitive? const-decl "bool" relations nil)
      (reflexive? const-decl "bool" relations nil)
      (p!1 skolem-const-decl "pred[A]" po nil)
      (x!2 skolem-const-decl "A" po nil) (lub? const-decl "bool" po nil)
      (exists_lub? const-decl "bool" po nil))
     725 600 t shostak))
   (lub_glb 0
    (lub_glb-1 nil 3253005048 3311852820
     ("" (skosimp*)
      (("" (typepred "x!1")
        (("" (expand "exists_glb?")
          (("" (expand "exists_lub?")
            (("" (skosimp*)
              (("" (expand "exists1")
                (("" (inst -2 "lb?(x!1)(p!1)")
                  (("" (skosimp*)
                    (("" (inst?)
                      (("" (expand "glb?")
                        (("" (ground)
                          (("1" (grind) nil nil)
                           ("2" (skosimp*)
                            (("2" (expand "lub?")
                              (("2" (ground) (("2" (grind) nil nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil)
     proved
     ((exists_lub? const-decl "bool" po nil) (po type-eq-decl nil po nil)
      (partial_order? const-decl "bool" orders nil)
      (pred type-eq-decl nil defined_types nil)
      (A formal-nonempty-type-decl nil po nil)
      (NOT const-decl "[bool -> bool]" booleans nil)
      (bool nonempty-type-eq-decl nil booleans nil)
      (boolean nonempty-type-decl nil booleans nil)
      (lb? const-decl "bool" po nil) (lub? const-decl "bool" po nil)
      (ub? const-decl "bool" po nil)
      (antisymmetric? const-decl "bool" relations nil)
      (preorder? const-decl "bool" orders nil)
      (transitive? const-decl "bool" relations nil)
      (reflexive? const-decl "bool" relations nil)
      (p!1 skolem-const-decl "pred[A]" po nil)
      (x!2 skolem-const-decl "A" po nil) (glb? const-decl "bool" po nil)
      (exists_glb? const-decl "bool" po nil))
     715 600 t shostak))
   (bottom_is_lub 0
    (bottom_is_lub-1 nil 3253005436 3311852820
     ("" (skosimp*)
      (("" (typepred "x!1")
        (("" (expand "exists_bottom?")
          (("" (expand "exists1")
            (("" (expand "exists_lub?")
              (("" (expand "exists1")
                (("" (use "bottom_lub")
                  (("" (inst?)
                    (("" (skosimp*)
                      (("" (inst?)
                        (("" (inst?) (("" (ground) nil nil)) nil)) nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil)
     proved
     ((exists_lub? const-decl "bool" po nil) (po type-eq-decl nil po nil)
      (partial_order? const-decl "bool" orders nil)
      (pred type-eq-decl nil defined_types nil)
      (A formal-nonempty-type-decl nil po nil)
      (NOT const-decl "[bool -> bool]" booleans nil)
      (bool nonempty-type-eq-decl nil booleans nil)
      (boolean nonempty-type-decl nil booleans nil)
      (emptyset const-decl "set" sets nil)
      (set type-eq-decl nil sets nil)
      (bottom_lub formula-decl nil po nil)
      (exists_bottom? const-decl "bool" po nil))
     122 90 t shostak))
   (top_is_lub 0
    (top_is_lub-1 nil 3253006246 3311852820
     ("" (skosimp*)
      (("" (typepred "x!1")
        (("" (expand "exists_lub?")
          (("" (expand "exists_top?")
            (("" (expand "exists1")
              (("" (use "top_lub")
                (("" (inst?)
                  (("" (skosimp*)
                    (("" (inst?)
                      (("" (inst?) (("" (ground) nil nil)) nil)) nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil)
     proved
     ((exists_lub? const-decl "bool" po nil) (po type-eq-decl nil po nil)
      (partial_order? const-decl "bool" orders nil)
      (pred type-eq-decl nil defined_types nil)
      (A formal-nonempty-type-decl nil po nil)
      (NOT const-decl "[bool -> bool]" booleans nil)
      (bool nonempty-type-eq-decl nil booleans nil)
      (boolean nonempty-type-decl nil booleans nil)
      (exists_top? const-decl "bool" po nil)
      (fullset const-decl "set" sets nil) (set type-eq-decl nil sets nil)
      (top_lub formula-decl nil po nil))
     119 90 t shostak)))
  (family)
  (cl
   (cl_is_po 0
    (cl_is_po-1 nil 3309946424 3311852820 ("" (judgement-tcc) nil nil)
     proved
     ((boolean nonempty-type-decl nil booleans nil)
      (bool nonempty-type-eq-decl nil booleans nil)
      (NOT const-decl "[bool -> bool]" booleans nil)
      (cl? const-decl "bool" cl nil) (cl type-eq-decl nil cl nil)
      (lb? const-decl "bool" po nil) (glb? const-decl "bool" po nil)
      (exists_glb? const-decl "bool" po nil)
      (ub? const-decl "bool" po nil) (lub? const-decl "bool" po nil)
      (exists_lub? const-decl "bool" po nil)
      (bottom? const-decl "bool" po nil)
      (exists_bottom? const-decl "bool" po nil)
      (top? const-decl "bool" po nil)
      (exists_top? const-decl "bool" po nil)
      (reflexive? const-decl "bool" relations nil)
      (transitive? const-decl "bool" relations nil)
      (L formal-nonempty-type-decl nil cl nil)
      (preorder? const-decl "bool" orders nil)
      (antisymmetric? const-decl "bool" relations nil)
      (partial_order? const-decl "bool" orders nil))
     259 250 nil nil))
   (lub_is_cl 0
    (lub_is_cl-1 nil 3253263457 3311852820
     ("" (skosimp*)
      (("" (typepred "x!1")
        (("" (expand "cl?")
          (("" (use "top_is_lub")
            (("" (use "bottom_is_lub")
              (("" (use "lub_glb") (("" (assert) nil nil)) nil)) nil))
            nil))
          nil))
        nil))
      nil)
     proved
     ((exists_lub? const-decl "bool" po nil) (po type-eq-decl nil po nil)
      (partial_order? const-decl "bool" orders nil)
      (pred type-eq-decl nil defined_types nil)
      (L formal-nonempty-type-decl nil cl nil)
      (NOT const-decl "[bool -> bool]" booleans nil)
      (bool nonempty-type-eq-decl nil booleans nil)
      (boolean nonempty-type-decl nil booleans nil)
      (top_is_lub judgement-tcc nil po nil)
      (lub_glb judgement-tcc nil po nil)
      (bottom_is_lub judgement-tcc nil po nil)
      (cl? const-decl "bool" cl nil))
     111 80 t shostak))
   (glb_TCC1 0
    (glb_TCC1-1 nil 3309951485 3311852820
     ("" (skosimp*)
      (("" (typepred "lesseqp!1")
        (("" (expand "cl?")
          (("" (ground)
            (("" (expand "exists_glb?")
              (("" (inst -2 "p!1")
                (("" (skosimp*) (("" (inst?) nil nil)) nil)) nil))
              nil))
            nil))
          nil))
        nil))
      nil)
     proved
     ((cl type-eq-decl nil cl nil) (cl? const-decl "bool" cl nil)
      (L formal-nonempty-type-decl nil cl nil)
      (NOT const-decl "[bool -> bool]" booleans nil)
      (bool nonempty-type-eq-decl nil booleans nil)
      (boolean nonempty-type-decl nil booleans nil)
      (pred type-eq-decl nil defined_types nil)
      (lesseqp!1 skolem-const-decl "cl" cl nil)
      (p!1 skolem-const-decl "pred[L]" cl nil)
      (x!1 skolem-const-decl "L" cl nil) (glb? const-decl "bool" po nil)
      (exists_glb? const-decl "bool" po nil))
     96 60 t nil))
   (lub_TCC1 0
    (lub_TCC1-1 nil 3309951485 3311852821
     ("" (skosimp*)
      (("" (typepred "lesseqp!1")
        (("" (expand "cl?")
          (("" (ground)
            (("" (expand "exists_lub?")
              (("" (inst -3 "p!1")
                (("" (skosimp*) (("" (inst?) nil nil)) nil)) nil))
              nil))
            nil))
          nil))
        nil))
      nil)
     proved
     ((cl type-eq-decl nil cl nil) (cl? const-decl "bool" cl nil)
      (L formal-nonempty-type-decl nil cl nil)
      (NOT const-decl "[bool -> bool]" booleans nil)
      (bool nonempty-type-eq-decl nil booleans nil)
      (boolean nonempty-type-decl nil booleans nil)
      (pred type-eq-decl nil defined_types nil)
      (lesseqp!1 skolem-const-decl "cl" cl nil)
      (p!1 skolem-const-decl "pred[L]" cl nil)
      (x!1 skolem-const-decl "L" cl nil) (lub? const-decl "bool" po nil)
      (exists_lub? const-decl "bool" po nil))
     96 60 t nil))
   (top_TCC1 0
    (top_TCC1-1 nil 3253007257 3311852821
     ("" (skosimp*)
      (("" (typepred "lesseqp!1")
        (("" (expand "cl?")
          (("" (expand "exists_top?")
            (("" (ground) (("" (skosimp*) (("" (inst?) nil nil)) nil))
              nil))
            nil))
          nil))
        nil))
      nil)
     proved
     ((cl type-eq-decl nil cl nil) (cl? const-decl "bool" cl nil)
      (L formal-nonempty-type-decl nil cl nil)
      (NOT const-decl "[bool -> bool]" booleans nil)
      (bool nonempty-type-eq-decl nil booleans nil)
      (boolean nonempty-type-decl nil booleans nil)
      (exists_top? const-decl "bool" po nil)
      (top? const-decl "bool" po nil) (x!1 skolem-const-decl "L" cl nil)
      (lesseqp!1 skolem-const-decl "cl" cl nil))
     59 50 t shostak))
   (bottom_TCC1 0
    (bottom_TCC1-1 nil 3253007256 3311852821
     ("" (skosimp*)
      (("" (typepred "lesseqp!1")
        (("" (expand "cl?")
          (("" (expand "exists_bottom?")
            (("" (ground) (("" (skosimp*) (("" (inst?) nil nil)) nil))
              nil))
            nil))
          nil))
        nil))
      nil)
     proved
     ((cl type-eq-decl nil cl nil) (cl? const-decl "bool" cl nil)
      (L formal-nonempty-type-decl nil cl nil)
      (NOT const-decl "[bool -> bool]" booleans nil)
      (bool nonempty-type-eq-decl nil booleans nil)
      (boolean nonempty-type-decl nil booleans nil)
      (exists_bottom? const-decl "bool" po nil)
      (bottom? const-decl "bool" po nil)
      (x!1 skolem-const-decl "L" cl nil)
      (lesseqp!1 skolem-const-decl "cl" cl nil))
     95 60 t shostak))
   (inf_lemma 0
    (inf_lemma-1 nil 3310298832 3310371104
     ("" (skosimp*)
      (("" (use "unique_glb")
        (("" (expand "unique?")
          (("" (inst?)
            (("" (ground)
              (("" (hide 2)
                (("" (expand "glb?")
                  (("" (expand "lb?")
                    (("" (ground)
                      (("1" (skosimp*)
                        (("1" (typepred "y!1")
                          (("1" (inst?) (("1" (assert) nil nil)) nil))
                          nil))
                        nil)
                       ("2" (skosimp*)
                        (("2" (hide -2)
                          (("2" (copy -2)
                            (("2" (hide -3)
                              (("2" (inst?)
                                (("2"
                                  (ground)
                                  (("2"
                                    (skosimp*)
                                    (("2" (inst?) nil nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil)
     unfinished
     ((unique_glb judgement-tcc nil po nil)
      (L formal-nonempty-type-decl nil cl nil)
      (cl type-eq-decl nil cl nil) (cl? const-decl "bool" cl nil)
      (po type-eq-decl nil po nil)
      (partial_order? const-decl "bool" orders nil)
      (pred type-eq-decl nil defined_types nil)
      (bool nonempty-type-eq-decl nil booleans nil)
      (boolean nonempty-type-decl nil booleans nil)
      (inf const-decl "glb(<=, p)" cl nil)
      (glb nonempty-type-eq-decl nil cl nil)
      (glb? const-decl "bool" po nil) (lb? const-decl "bool" po nil)
      (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
      (NOT const-decl "[bool -> bool]" booleans nil)
      (unique? const-decl "bool" exists1 nil))
     303 180 t shostak))
   (transitivity 0
    (transitivity-1 nil 3310374252 3310374322
     ("" (skosimp*)
      (("" (typepred "lesseqp!1")
        (("" (expand "cl?")
          (("" (expand "partial_order?")
            (("" (expand "preorder?")
              (("" (expand "transitive?")
                (("" (ground)
                  (("" (inst - "x!1" "y!1" "z!1") (("" (assert) nil nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil)
     unfinished
     ((cl type-eq-decl nil cl nil) (cl? const-decl "bool" cl nil)
      (L formal-nonempty-type-decl nil cl nil)
      (NOT const-decl "[bool -> bool]" booleans nil)
      (bool nonempty-type-eq-decl nil booleans nil)
      (boolean nonempty-type-decl nil booleans nil)
      (partial_order? const-decl "bool" orders nil)
      (transitive? const-decl "bool" relations nil)
      (preorder? const-decl "bool" orders nil))
     70697 1620 t shostak)))
  (cl_lift
   (lift_TCC1 0
    (lift_TCC1-1 nil 3253213839 3311852822
     ("" (skosimp*)
      (("" (rewrite "lub_is_cl")
        (("" (hide 2)
          (("" (typepred "lesseqp!1")
            (("" (ground)
              (("1" (expand "cl?")
                (("1" (ground)
                  (("1" (hide -2 -3 -4 -5)
                    (("1" (expand "partial_order?")
                      (("1" (expand "preorder?")
                        (("1" (expand "reflexive?")
                          (("1" (expand "antisymmetric?")
                            (("1" (expand "transitive?")
                              (("1" (ground)
                                (("1"
                                  (skosimp*)
                                  (("1" (grind) nil nil))
                                  nil)
                                 ("2"
                                  (skosimp*)
                                  (("2"
                                    (hide -3 -5)
                                    (("2"
                                      (inst?)
                                      (("2"
                                        (inst?)
                                        (("2"
                                          (inst
                                           -3
                                           "x!1(x!2)"
                                           "y!1(x!2)"
                                           "z!1(x!2)")
                                          (("2" (assert) nil nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil)
                                 ("3"
                                  (hide -1 -2)
                                  (("3"
                                    (skosimp*)
                                    (("3"
                                      (decompose-equality)
                                      (("3"
                                        (inst?)
                                        (("3"
                                          (inst?)
                                          (("3"
                                            (inst?)
                                            (("3" (assert) nil nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil)
               ("2" (hide -)
                (("2" (expand "exists_lub?")
                  (("2" (skosimp*)
                    (("2"
                      (inst 1
                       "lambda (t:T): sup(lesseqp!1)({ x: L |  exists (y: [T->L
 ]): p!1(y) and x = y(t) })")
                      (("2" (expand "lub?")
                        (("2" (ground)
                          (("1" (expand "ub?")
                            (("1" (skosimp*)
                              (("1"
                                (typepred "sup(lesseqp!1)
                     ({x: L | EXISTS (y: [T -> L]): p!1(y) AND x = y(x!1)})")
                                (("1"
                                  (expand "lub?")
                                  (("1"
                                    (ground)
                                    (("1"
                                      (hide -2)
                                      (("1"
                                        (expand "ub?")
                                        (("1"
                                          (inst?)
                                          (("1"
                                            (typepred "y!1")
                                            (("1" (inst?) nil nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil)
                           ("2" (skosimp*)
                            (("2"
                              (typepred "sup(lesseqp!1)
                     ({x: L | EXISTS (y: [T -> L]): p!1(y) AND x = y(x!1)})")
                              (("2" (expand "lub?")
                                (("2"
                                  (ground)
                                  (("2"
                                    (hide -1)
                                    (("2"
                                      (inst?)
                                      (("2"
                                        (ground)
                                        (("2"
                                          (hide 2)
                                          (("2"
                                            (expand "ub?")
                                            (("2"
                                              (skosimp*)
                                              (("2"
                                                (typepred "y!2")
                                                (("2"
                                                  (skosimp*)
                                                  (("2"
                                                    (inst?)
                                                    (("2"
                                                      (assert)
                                                      nil
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil)
     proved
     ((AND const-decl "[bool, bool -> bool]" booleans nil)
      (lub_is_cl judgement-tcc nil cl nil)
      (boolean nonempty-type-decl nil booleans nil)
      (bool nonempty-type-eq-decl nil booleans nil)
      (pred type-eq-decl nil defined_types nil)
      (partial_order? const-decl "bool" orders nil)
      (po type-eq-decl nil po nil) (exists_lub? const-decl "bool" po nil)
      (cl? const-decl "bool" cl nil) (cl type-eq-decl nil cl nil)
      (T formal-nonempty-type-decl nil cl_lift nil)
      (L formal-nonempty-type-decl nil cl_lift nil)
      (NOT const-decl "[bool -> bool]" booleans nil)
      (y!3 skolem-const-decl "[T -> L]" cl_lift nil)
      (ub? const-decl "bool" po nil)
      (x!1 skolem-const-decl "T" cl_lift nil)
      (y!1 skolem-const-decl "(p!1)" cl_lift nil)
      (p!1 skolem-const-decl "pred[[T -> L]]" cl_lift nil)
      (lub? const-decl "bool" po nil)
      (lub nonempty-type-eq-decl nil cl nil)
      (sup const-decl "lub(<=, p)" cl nil)
      (= const-decl "[T, T -> boolean]" equalities nil)
      (preorder? const-decl "bool" orders nil)
      (antisymmetric? const-decl "bool" relations nil)
      (transitive? const-decl "bool" relations nil)
      (reflexive? const-decl "bool" relations nil))
     898 710 t shostak))
   (lift_inf 0
    (lift_inf-1 nil 3253871899 3310371106
     ("" (skosimp*)
      (("" (use "unique_glb[[T->L]]")
        ((""
          (case "forall (x: set[[T->L]]):glb?(lift(lesseqp!1))(x)(lift(inf(less
 eqp!1))(x))")
          (("1" (decompose-equality 1)
            (("1" (inst?)
              (("1" (inst?)
                (("1" (expand "unique?")
                  (("1" (inst?)
                    (("1" (typepred "inf(lift(lesseqp!1))(x!1)")
                      (("1" (assert) nil nil)) nil))
                    nil))
                  nil))
                nil))
              nil))
            nil)
           ("2" (hide 2)
            (("2" (skosimp*)
              (("2" (hide -1)
                (("2" (expand "lift")
                  (("2" (expand "glb?")
                    (("2" (ground)
                      (("1" (expand "lb?")
                        (("1" (skosimp*)
                          (("1"
                            (typepred
                             "inf(lesseqp!1)(LAMBDA a: EXISTS f: x!1(f) AND a =
  f(x!2))")
                            (("1" (grind) nil nil)) nil))
                          nil))
                        nil)
                       ("2" (skosimp*)
                        (("2"
                          (typepred
                           "inf(lesseqp!1)(LAMBDA a: EXISTS f: x!1(f) AND a = f
 (x!2))")
                          (("2" (expand "glb?")
                            (("2" (ground)
                              (("2" (hide -1)
                                (("2"
                                  (inst -1 "y!1(x!2)")
                                  (("2"
                                    (ground)
                                    (("2"
                                      (hide 2)
                                      (("2"
                                        (expand "lb?")
                                        (("2"
                                          (skosimp*)
                                          (("2"
                                            (typepred "y!2")
                                            (("2"
                                              (skosimp*)
                                              (("2"
                                                (inst?)
                                                (("2" (assert) nil nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil)
     unfinished
     ((unique_glb judgement-tcc nil po nil)
      (T formal-nonempty-type-decl nil cl_lift nil)
      (L formal-nonempty-type-decl nil cl_lift nil)
      (lift const-decl "cl[[T -> L]]" cl_lift nil)
      (cl type-eq-decl nil cl nil) (cl? const-decl "bool" cl nil)
      (po type-eq-decl nil po nil)
      (partial_order? const-decl "bool" orders nil)
      (pred type-eq-decl nil defined_types nil)
      (bool nonempty-type-eq-decl nil booleans nil)
      (boolean nonempty-type-decl nil booleans nil)
      (lb? const-decl "bool" po nil)
      (AND const-decl "[bool, bool -> bool]" booleans nil)
      (= const-decl "[T, T -> boolean]" equalities nil)
      (NOT const-decl "[bool -> bool]" booleans nil)
      (unique? const-decl "bool" exists1 nil)
      (set type-eq-decl nil sets nil) (glb? const-decl "bool" po nil)
      (lift const-decl "[T -> L]" cl_lift nil)
      (glb nonempty-type-eq-decl nil cl nil)
      (inf const-decl "glb(<=, p)" cl nil))
     943 600 t shostak))
   (lift_sup 0
    (lift_sup-1 nil 3253872804 3310371107
     ("" (skosimp*)
      (("" (use "unique_lub[[T -> L]]")
        ((""
          (case "forall (x: set[[T->L]]):lub?(lift(lesseqp!1))(x)(lift(sup(less
 eqp!1))(x))")
          (("1" (decompose-equality 1)
            (("1" (inst?)
              (("1" (inst?)
                (("1" (expand "unique?")
                  (("1" (inst?)
                    (("1" (typepred "sup(lift(lesseqp!1))(x!1)")
                      (("1" (assert) nil nil)) nil))
                    nil))
                  nil))
                nil))
              nil))
            nil)
           ("2" (hide -1 2)
            (("2" (skosimp*)
              (("2" (expand "lift")
                (("2" (expand "lub?")
                  (("2" (ground)
                    (("1" (expand "ub?")
                      (("1" (skosimp*)
                        (("1"
                          (typepred
                           "sup(lesseqp!1)(LAMBDA a: EXISTS f: x!1(f) AND a = f
 (x!2))")
                          (("1" (grind) nil nil)) nil))
                        nil))
                      nil)
                     ("2" (skosimp*)
                      (("2"
                        (typepred
                         "sup(lesseqp!1)(LAMBDA a: EXISTS f: x!1(f) AND a = f(x
 !2))")
                        (("2" (expand "lub?")
                          (("2" (ground)
                            (("2" (hide -1)
                              (("2" (inst -1 "y!1(x!2)")
                                (("2"
                                  (ground)
                                  (("2"
                                    (hide 2)
                                    (("2"
                                      (expand "ub?")
                                      (("2"
                                        (skosimp*)
                                        (("2"
                                          (typepred "y!2")
                                          (("2"
                                            (skosimp*)
                                            (("2"
                                              (inst?)
                                              (("2" (assert) nil nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil)
     unfinished
     ((unique_lub judgement-tcc nil po nil)
      (T formal-nonempty-type-decl nil cl_lift nil)
      (L formal-nonempty-type-decl nil cl_lift nil)
      (lift const-decl "cl[[T -> L]]" cl_lift nil)
      (cl type-eq-decl nil cl nil) (cl? const-decl "bool" cl nil)
      (po type-eq-decl nil po nil)
      (partial_order? const-decl "bool" orders nil)
      (pred type-eq-decl nil defined_types nil)
      (bool nonempty-type-eq-decl nil booleans nil)
      (boolean nonempty-type-decl nil booleans nil)
      (= const-decl "[T, T -> boolean]" equalities nil)
      (AND const-decl "[bool, bool -> bool]" booleans nil)
      (ub? const-decl "bool" po nil)
      (NOT const-decl "[bool -> bool]" booleans nil)
      (unique? const-decl "bool" exists1 nil)
      (set type-eq-decl nil sets nil) (lub? const-decl "bool" po nil)
      (lift const-decl "[T -> L]" cl_lift nil)
      (lub nonempty-type-eq-decl nil cl nil)
      (sup const-decl "lub(<=, p)" cl nil))
     898 600 t shostak)))
  (monotonic
   (monotonic_TCC1 0
    (monotonic_TCC1-1 nil 3310294392 3311852823
     ("" (existence-tcc) (("" (postpone) nil nil)) nil) proved
     ((boolean nonempty-type-decl nil booleans nil)
      (bool nonempty-type-eq-decl nil booleans nil)
      (NOT const-decl "[bool -> bool]" booleans nil)
      (L1 formal-nonempty-type-decl nil monotonic nil)
      (cl? const-decl "bool" cl nil) (cl type-eq-decl nil cl nil)
      (L2 formal-nonempty-type-decl nil monotonic nil)
      (exists_top? const-decl "bool" po nil)
      (top? const-decl "bool" po nil)
      (exists_bottom? const-decl "bool" po nil)
      (bottom? const-decl "bool" po nil)
      (exists_lub? const-decl "bool" po nil)
      (lub? const-decl "bool" po nil) (ub? const-decl "bool" po nil)
      (exists_glb? const-decl "bool" po nil)
      (glb? const-decl "bool" po nil) (lb? const-decl "bool" po nil)
      (partial_order? const-decl "bool" orders nil)
      (antisymmetric? const-decl "bool" relations nil)
      (preorder? const-decl "bool" orders nil)
      (transitive? const-decl "bool" relations nil)
      (reflexive? const-decl "bool" relations nil)
      (bottom nonempty-type-eq-decl nil cl nil)
      (bottom const-decl "bottom(<=)" cl nil)
      (monotonic? const-decl "bool" monotonic nil))
     1444 1230 t nil))
   (monotonic_inf 0
    (monotonic_inf-1 nil 3253182604 3310371109
     ("" (skosimp*)
      (("" (typepred "inf(le!1)(image(f!1, A!1))")
        (("" (expand "glb?")
          (("" (ground)
            (("" (hide -1)
              (("" (inst?)
                (("" (ground)
                  (("" (expand "monotonic?")
                    (("" (hide 2)
                      (("" (expand "lb?")
                        (("" (skosimp*)
                          (("" (inst?)
                            (("" (typepred "y!1")
                              (("" (expand "image")
                                ((""
                                  (skosimp*)
                                  ((""
                                    (inst?)
                                    ((""
                                      (ground)
                                      ((""
                                        (hide -1 2)
                                        ((""
                                          (typepred "x!1")
                                          ((""
                                            (typepred
                                             "inf(lesseqp!1)(A!1)")
                                            ((""
                                              (expand "glb?")
                                              ((""
                                                (skosimp*)
                                                ((""
                                                  (hide -2)
                                                  (("" (grind) nil nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil)
     unfinished
     ((inf const-decl "glb(<=, p)" cl nil)
      (glb nonempty-type-eq-decl nil cl nil)
      (set type-eq-decl nil sets nil)
      (L1 formal-nonempty-type-decl nil monotonic nil)
      (cl type-eq-decl nil cl nil) (cl? const-decl "bool" cl nil)
      (glb? const-decl "bool" po nil)
      (pred type-eq-decl nil defined_types nil)
      (L2 formal-nonempty-type-decl nil monotonic nil)
      (NOT const-decl "[bool -> bool]" booleans nil)
      (bool nonempty-type-eq-decl nil booleans nil)
      (boolean nonempty-type-decl nil booleans nil)
      (monotonic? const-decl "bool" monotonic nil)
      (lb? const-decl "bool" po nil))
     412 240 t shostak)))
  (fixpoint
   (monotonic_TCC1 0
    (monotonic_TCC1-1 nil 3253209796 3311852823
     ("" (skosimp*)
      (("" (inst 1 "lambda (a:L): a") (("" (grind) nil nil)) nil)) nil)
     proved
     ((L formal-nonempty-type-decl nil fixpoint nil)
      (boolean nonempty-type-decl nil booleans nil)
      (bool nonempty-type-eq-decl nil booleans nil)
      (cl? const-decl "bool" cl nil) (cl type-eq-decl nil cl nil)
      (monotonic? const-decl "bool" fixpoint nil)
      (lesseqp!1 skolem-const-decl "cl[L]" fixpoint nil)
      (monotonic? const-decl "bool" monotonic nil))
     254 210 t shostak))
   (unique_lfp 0
    (unique_lfp-1 nil 3253261615 3311852824
     ("" (skosimp*)
      (("" (expand "unique?")
        (("" (skosimp*)
          (("" (expand "lfp?")
            (("" (ground)
              (("" (inst -2 "y!1")
                (("" (inst -4 "x!1")
                  (("" (ground)
                    (("" (hide -3 -4)
                      (("" (typepred "lesseqp!1")
                        (("" (hide -2) (("" (grind) nil nil)) nil)) nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil)
     proved
     ((unique? const-decl "bool" exists1 nil)
      (lfp? const-decl "bool" fixpoint nil)
      (L formal-nonempty-type-decl nil fixpoint nil)
      (cl type-eq-decl nil cl nil) (cl? const-decl "bool" cl nil)
      (NOT const-decl "[bool -> bool]" booleans nil)
      (bool nonempty-type-eq-decl nil booleans nil)
      (boolean nonempty-type-decl nil booleans nil)
      (exists_top? const-decl "bool" po nil)
      (top? const-decl "bool" po nil)
      (exists_bottom? const-decl "bool" po nil)
      (bottom? const-decl "bool" po nil)
      (exists_lub? const-decl "bool" po nil)
      (lub? const-decl "bool" po nil) (ub? const-decl "bool" po nil)
      (exists_glb? const-decl "bool" po nil)
      (glb? const-decl "bool" po nil) (lb? const-decl "bool" po nil)
      (partial_order? const-decl "bool" orders nil)
      (antisymmetric? const-decl "bool" relations nil)
      (preorder? const-decl "bool" orders nil)
      (transitive? const-decl "bool" relations nil)
      (reflexive? const-decl "bool" relations nil))
     639 500 t shostak))
   (knaster_tarski 0
    (knaster_tarski-2 nil 3310371030 3310371111
     ("" (skosimp*)
      (("" (inst 1 "inf(lesseqp!1)(lambda x: lesseqp!1(f!1(x), x))")
        (("" (expand "lfp?")
          (("" (ground)
            (("1" (expand "fixpoint?")
              (("1" (typepred "lesseqp!1")
                (("1" (expand "cl?")
                  (("1" (expand "partial_order?")
                    (("1" (ground)
                      (("1" (expand "antisymmetric?")
                        (("1" (inst?)
                          (("1"
                            (case "lesseqp!1(f!1(inf(lesseqp!1)(LAMBDA x: lesse
 qp!1(f!1(x), x))),
                           inf(lesseqp!1)(LAMBDA x: lesseqp!1(f!1(x), x)))")
                            (("1" (ground)
                              (("1" (hide 2)
                                (("1"
                                  (expand "monotonic?")
                                  (("1"
                                    (expand "monotonic?")
                                    (("1"
                                      (inst
                                       -7
                                       "f!1(inf(lesseqp!1)(LAMBDA x: lesseqp!1(
 f!1(x), x)))"
                                       "inf(lesseqp!1)(LAMBDA x: lesseqp!1(f!1(
 x), x))")
                                      (("1"
                                        (ground)
                                        (("1"
                                          (typepred
                                           "inf(lesseqp!1)(LAMBDA x: lesseqp!1(
 f!1(x), x))")
                                          (("1"
                                            (expand "glb?")
                                            (("1"
                                              (ground)
                                              (("1"
                                                (expand "lb?")
                                                (("1" (inst?) nil nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil)
                             ("2" (hide 2)
                              (("2"
                                (typepred
                                 "inf(lesseqp!1)(LAMBDA x: lesseqp!1(f!1(x), x)
 )")
                                (("2"
                                  (expand "glb?")
                                  (("2"
                                    (hide -3)
                                    (("2"
                                      (ground)
                                      (("2"
                                        (inst?)
                                        (("2"
                                          (ground)
                                          (("2"
                                            (hide 2)
                                            (("2"
                                              (expand "lb?")
                                              (("2"
                                                (skosimp*)
                                                (("2"
                                                  (typepred "y!1")
                                                  (("2"
                                                    (expand "preorder?")
                                                    (("2"
                                                      (expand
                                                       "transitive?")
                                                      (("2"
                                                        (ground)
                                                        (("2"
                                                          (inst
                                                           -
                                                           "f!1(inf(lesseqp!1)(
 LAMBDA x: lesseqp!1(f!1(x), x)))"
                                                           "f!1(y!1)"
                                                           "y!1")
                                                          (("2"
                                                            (ground)
                                                            (("2"
                                                              (hide 2)
                                                              (("2"
                                                                (expand
                                                                 "monotonic?")
                                                                (("2"
                                                                  (expand
                                                                   "monotonic?"
 )
                                                                  (("2"
                                                                    (inst?)
                                                                    (("2"
                                                                      (ground)
                                                                      (("2"
                                                                        (hide
                                                                         2)
                                                                        (("2"
                                                                          (inst
 ?)
                                                                          nil
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil)
             ("2" (skosimp*)
              (("2"
                (typepred
                 "inf(lesseqp!1)(LAMBDA x: lesseqp!1(f!1(x), x))")
                (("2" (expand "glb?")
                  (("2" (ground)
                    (("2" (expand "lb?")
                      (("2" (inst?)
                        (("2" (hide 2)
                          (("2" (expand "fixpoint?")
                            (("2" (typepred "lesseqp!1")
                              (("2" (expand "cl?")
                                (("2"
                                  (ground)
                                  (("2"
                                    (expand "partial_order?")
                                    (("2"
                                      (expand "preorder?")
                                      (("2"
                                        (expand "reflexive?")
                                        (("2"
                                          (ground)
                                          (("2"
                                            (inst?)
                                            (("2" (assert) nil nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil)
     unfinished
     ((L formal-nonempty-type-decl nil fixpoint nil)
      (boolean nonempty-type-decl nil booleans nil)
      (bool nonempty-type-eq-decl nil booleans nil)
      (cl? const-decl "bool" cl nil) (cl type-eq-decl nil cl nil)
      (pred type-eq-decl nil defined_types nil)
      (glb? const-decl "bool" po nil)
      (glb nonempty-type-eq-decl nil cl nil)
      (inf const-decl "glb(<=, p)" cl nil)
      (NOT const-decl "[bool -> bool]" booleans nil)
      (partial_order? const-decl "bool" orders nil)
      (antisymmetric? const-decl "bool" relations nil)
      (monotonic? const-decl "bool" monotonic nil)
      (lb? const-decl "bool" po nil)
      (monotonic? const-decl "bool" fixpoint nil)
      (preorder? const-decl "bool" orders nil)
      (transitive? const-decl "bool" relations nil)
      (fixpoint? const-decl "bool" fixpoint nil)
      (reflexive? const-decl "bool" relations nil))
     996 610 nil nil)
    (knaster_tarski-1 nil 3253184787 3310370918
     ("" (skosimp*)
      (("" (inst 1 "inf(lesseqp!1)(lambda x: lesseqp!1(f!1(x), x))")
        ((""
          (name-replace "a"
           "(inf(lesseqp!1)(LAMBDA x: lesseqp!1(f!1(x), x)))")
          (("" (reveal -1)
            (("" (name-replace "X" "LAMBDA x: lesseqp!1(f!1(x), x)")
              (("" (reveal -1)
                (("" (expand "lfp?")
                  (("" (ground)
                    (("1" (expand "fixpoint?")
                      (("1" (case "not lesseqp!1(f!1(a), a)")
                        (("1" (hide 2)
                          (("1" (use "monotonic_inf")
                            (("1" (expand "monotonic?" -4)
                              (("1" (ground)
                                (("1"
                                  (typepred "lesseqp!1")
                                  (("1"
                                    (replace -5)
                                    (("1"
                                      (case
                                       "lesseqp!1(inf(lesseqp!1)(image(f!1, X))
 , a)")
                                      (("1"
                                        (hide -3 -5 -6 -7)
                                        (("1"
                                          (expand "partial_order?")
                                          (("1"
                                            (expand "preorder?")
                                            (("1"
                                              (expand "transitive?")
                                              (("1"
                                                (ground)
                                                (("1"
                                                  (hide -2 -4)
                                                  (("1"
                                                    (inst
                                                     -2
                                                     "f!1(a)"
                                                     "inf(lesseqp!1)(image(f!1,
  X))"
                                                     "a")
                                                    (("1"
                                                      (ground)
                                                      nil
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil)
                                       ("2"
                                        (hide 2)
                                        (("2"
                                          (typepred "inf(lesseqp!1)(X)")
                                          (("2"
                                            (expand "glb?")
                                            (("2"
                                              (ground)
                                              (("2"
                                                (hide -1)
                                                (("2"
                                                  (replace -6)
                                                  (("2"
                                                    (inst?)
                                                    (("2"
                                                      (ground)
                                                      (("2"
                                                        (hide 2)
                                                        (("2"
                                                          (expand "lb?")
                                                          (("2"
                                                            (skosimp*)
                                                            (("2"
                                                              (typepred
                                                               "y!1")
                                                              (("2"
                                                                (use
                                                                 "inf_less")
                                                                (("2"
                                                                  (ground)
                                                                  (("2"
                                                                    (inst
                                                                     1
                                                                     "f!1(y!1)"
 )
                                                                    (("1"
                                                                      (hide
                                                                       -2
                                                                       -3
                                                                       -4
                                                                       -6
                                                                       -7
                                                                       2)
                                                                      (("1"
                                                                        (decomp
 ose-equality
                                                                         -2)
                                                                        (("1"
                                                                          (inst
 ?)
                                                                          (("1"
                                                                            (gr
 ound)
                                                                            nil
                                                                            nil
 ))
                                                                          nil))
                                                                        nil))
                                                                      nil)
                                                                     ("2"
                                                                      (hide
                                                                       -2
                                                                       -3
                                                                       -4
                                                                       -6
                                                                       -7
                                                                       2)
                                                                      (("2"
                                                                        (expand
                                                                         "image
 ")
                                                                        (("2"
                                                                          (inst
 ?)
                                                                          nil
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil)
                         ("2" (case "not lesseqp!1(a, f!1(a))")
                          (("1" (hide 2)
                            (("1" (typepred "inf(lesseqp!1)(X)")
                              (("1" (expand "glb?")
                                (("1"
                                  (ground)
                                  (("1"
                                    (hide -2)
                                    (("1"
                                      (expand "lb?")
                                      (("1"
                                        (inst -1 "f!1(a)")
                                        (("1" (assert) nil nil)
                                         ("2"
                                          (decompose-equality -2)
                                          (("2"
                                            (hide 2)
                                            (("2"
                                              (inst -1 "f!1(a)")
                                              (("2"
                                                (iff)
                                                (("2"
                                                  (ground)
                                                  (("2"
                                                    (hide 1 3)
                                                    (("2"
                                                      (hide -2)
                                                      (("2"
                                                        (expand
                                                         "monotonic?")
                                                        (("2"
                                                          (expand
                                                           "monotonic?")
                                                          (("2"
                                                            (inst?)
                                                            (("2"
                                                              (ground)
                                                              nil
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil)
                           ("2" (hide -3 -4 -5)
                            (("2" (typepred "lesseqp!1")
                              (("2" (hide -2) (("2" (grind) nil nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil)
                     ("2" (skosimp*)
                      (("2" (expand "fixpoint?")
                        (("2" (reveal -2)
                          (("2" (replace -3)
                            (("2" (decompose-equality -3)
                              (("2" (inst?)
                                (("2"
                                  (iff)
                                  (("2"
                                    (ground)
                                    (("1"
                                      (typepred "inf(lesseqp!1)(X)")
                                      (("1"
                                        (replace -4)
                                        (("1"
                                          (expand "glb?")
                                          (("1"
                                            (ground)
                                            (("1"
                                              (hide -2)
                                              (("1"
                                                (expand "lb?")
                                                (("1" (inst?) nil nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil)
                                     ("2"
                                      (hide -1 -3 -4 1 3)
                                      (("2"
                                        (typepred " lesseqp!1")
                                        (("2"
                                          (hide -2)
                                          (("2" (grind) nil nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil)
     unfinished
     ((L formal-nonempty-type-decl nil fixpoint nil)
      (boolean nonempty-type-decl nil booleans nil)
      (bool nonempty-type-eq-decl nil booleans nil)
      (pred type-eq-decl nil defined_types nil)
      (partial_order? const-decl "bool" orders nil)
      (po type-eq-decl nil po nil) (cl? const-decl "bool" cl nil)
      (glb? const-decl "bool" po nil)
      (inf const-decl "glb(<=, p)" cl nil)
      (NOT const-decl "[bool -> bool]" booleans nil)
      (monotonic_inf formula-decl nil monotonic nil)
      (lb? const-decl "bool" po nil)
      (preorder? const-decl "bool" orders nil)
      (transitive? const-decl "bool" relations nil)
      (set type-eq-decl nil sets nil)
      (monotonic? const-decl "bool" fixpoint nil)
      (antisymmetric? const-decl "bool" relations nil)
      (reflexive? const-decl "bool" relations nil)
      (monotonic? const-decl "bool" monotonic nil)
      (fixpoint? const-decl "bool" fixpoint nil)
      (= const-decl "[T, T -> boolean]" equalities nil))
     2164 1470 t shostak))
   (mu_TCC1 0
    (mu_TCC1-1 nil 3253261876 3311852824
     ("" (skosimp*)
      (("" (typepred "f!1")
        (("" (use "knaster_tarski")
          (("" (assert)
            (("" (skosimp*)
              (("" (use "epsilon_ax[L]") (("" (ground) nil nil)) nil))
              nil))
            nil))
          nil))
        nil))
      nil)
     proved
     ((monotonic nonempty-type-eq-decl nil fixpoint nil)
      (monotonic? const-decl "bool" fixpoint nil)
      (cl type-eq-decl nil cl nil) (cl? const-decl "bool" cl nil)
      (L formal-nonempty-type-decl nil fixpoint nil)
      (NOT const-decl "[bool -> bool]" booleans nil)
      (bool nonempty-type-eq-decl nil booleans nil)
      (boolean nonempty-type-decl nil booleans nil)
      (epsilon_ax formula-decl nil epsilons nil)
      (pred type-eq-decl nil defined_types nil)
      (lfp? const-decl "bool" fixpoint nil)
      (knaster_tarski formula-decl nil fixpoint nil))
     115 80 t shostak))
   (mu_fixpoint 0
    (mu_fixpoint-1 nil 3253262888 3311852824
     ("" (skosimp*)
      (("" (typepred "mu(lesseqp!1)(f!1)") (("" (grind) nil nil)) nil))
      nil)
     proved
     ((mu const-decl "(lfp?(<=)(f))" fixpoint nil)
      (monotonic nonempty-type-eq-decl nil fixpoint nil)
      (monotonic? const-decl "bool" fixpoint nil)
      (lfp? const-decl "bool" fixpoint nil) (cl type-eq-decl nil cl nil)
      (cl? const-decl "bool" cl nil)
      (L formal-nonempty-type-decl nil fixpoint nil)
      (NOT const-decl "[bool -> bool]" booleans nil)
      (bool nonempty-type-eq-decl nil booleans nil)
      (boolean nonempty-type-decl nil booleans nil)
      (fixpoint? const-decl "bool" fixpoint nil))
     255 210 t shostak)))
  (fixpoint_induct
   (fixpoint_induct 0
    (fixpoint_induct-1 nil 3253210097 3310374239
     ("" (skosimp*)
      (("" (expand "sup")
        (("" (typepred "sup(lesseqp!1)({x | EXISTS v: x = p!1(v)})")
          (("" (expand "lub?")
            (("" (ground)
              (("" (hide -1)
                (("" (inst?)
                  (("" (ground)
                    (("" (hide 2)
                      (("" (expand "ub?")
                        ((""
                          (case "(FORALL (y: ({x | EXISTS v: x = p!1(v)})): les
 seqp!1(y, x!1)) = 
  (forall v: lesseqp!1(p!1(v), x!1))")
                          (("1" (replace -1)
                            (("1" (hide -1)
                              (("1" (use "wf_induction[W, <]")
                                (("1"
                                  (ground)
                                  (("1"
                                    (hide 2)
                                    (("1"
                                      (skosimp*)
                                      (("1"
                                        (inst? -2)
                                        (("1"
                                          (lemma "transitivity")
                                          (("1"
                                            (inst?)
                                            (("1"
                                              (inst
                                               -1
                                               "f!1(below(lesseqp!1)(p!1)(x!2))
 ")
                                              (("1"
                                                (ground)
                                                (("1"
                                                  (hide -2 2)
                                                  (("1"
                                                    (expand "below")
                                                    (("1"
                                                      (typepred "x!1")
                                                      (("1"
                                                        (expand
                                                         "fixpoint?")
                                                        (("1"
                                                          (replace
  
                                                           -1
                                                           (1)
  
                                                           rl)
                                                          (("1"
                                                            (hide -1)
                                                            (("1"
                                                              (typepred
                                                               "f!1")
                                                              (("1"
                                                                (expand
                                                                 "monotonic?")
                                                                (("1"
                                                                  (expand
                                                                   "monotonic?"
 )
                                                                  (("1"
                                                                    (inst?)
                                                                    (("1"
                                                                      (ground)
                                                                      (("1"
                                                                        (hide
                                                                         2)
                                                                        (("1"
                                                                          (type
 pred
                                                                           "sup
 (lesseqp!1)({x | EXISTS v: (v < x!2) AND x = p!1(v)})")
                                                                          (("1"
                                                                            (ex
 pand
                                                                             "l
 ub?")
                                                                            (("
 1"
                                                                              (
 ground)
                                                                              (
 ("1"
                                                                               
  (hide
                                                                               
   -1)
                                                                               
  (("1"
                                                                               
    (inst?)
                                                                               
    (("1"
                                                                               
      (ground)
                                                                               
      (("1"
                                                                               
        (hide
                                                                               
         2)
                                                                               
        (("1"
                                                                               
          (expand
                                                                               
           "ub?")
                                                                               
          (("1"
                                                                               
            (skosimp*)
                                                                               
            (("1"
                                                                               
              (typepred
                                                                               
               "y!1")
                                                                               
              (("1"
                                                                               
                (skosimp*)
                                                                               
                (("1"
                                                                               
                  (inst?)
                                                                               
                  (("1"
                                                                               
                    (assert)
                                                                               
                    nil
                                                                               
                    nil))
                                                                               
                  nil))
                                                                               
                nil))
                                                                               
              nil))
                                                                               
            nil))
                                                                               
          nil))
                                                                               
        nil))
                                                                               
      nil))
                                                                               
    nil))
                                                                               
  nil))
                                                                              n
 il))
                                                                            nil
 ))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil)
                           ("2" (hide - 2)
                            (("2" (iff)
                              (("2" (ground)
                                (("1"
                                  (skosimp*)
                                  (("1"
                                    (inst?)
                                    (("1" (inst?) nil nil))
                                    nil))
                                  nil)
                                 ("2"
                                  (skosimp*)
                                  (("2"
                                    (typepred "y!1")
                                    (("2"
                                      (skosimp*)
                                      (("2"
                                        (inst?)
                                        (("2" (assert) nil nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil)
     unfinished
     ((sup const-decl "lub(<=, p)" cl nil)
      (lub nonempty-type-eq-decl nil cl nil)
      (= const-decl "[T, T -> boolean]" equalities nil)
      (W formal-nonempty-type-decl nil fixpoint_induct nil)
      (cl type-eq-decl nil cl nil) (cl? const-decl "bool" cl nil)
      (lub? const-decl "bool" po nil)
      (pred type-eq-decl nil defined_types nil)
      (L formal-nonempty-type-decl nil fixpoint_induct nil)
      (NOT const-decl "[bool -> bool]" booleans nil)
      (bool nonempty-type-eq-decl nil booleans nil)
      (boolean nonempty-type-decl nil booleans nil)
      (fixpoint type-eq-decl nil fixpoint nil)
      (monotonic nonempty-type-eq-decl nil fixpoint nil)
      (monotonic? const-decl "bool" fixpoint nil)
      (fixpoint? const-decl "bool" fixpoint nil)
      (transitivity formula-decl nil cl nil)
      (below const-decl "L" fixpoint_induct nil)
      (monotonic? const-decl "bool" monotonic nil)
      (AND const-decl "[bool, bool -> bool]" booleans nil)
      (wf_induction formula-decl nil wf_induction nil)
      (well_founded? const-decl "bool" orders nil)
      (< formal-const-decl "(well_founded?[W])" fixpoint_induct nil) nil
      nil (ub? const-decl "bool" po nil)
      (sup const-decl "L" fixpoint_induct nil))
     271803 5900 t shostak))
   (fixpoint_induct1 0
    (fixpoint_induct1-1 nil 3253262337 3310370921
     ("" (skosimp*)
      (("" (use "fixpoint_induct")
        (("1" (assert) nil nil) ("2" (use "mu_fixpoint") nil nil)) nil))
      nil)
     unfinished
     ((fixpoint_induct formula-decl nil fixpoint_induct nil)
      (monotonic nonempty-type-eq-decl nil fixpoint nil)
      (monotonic? const-decl "bool" fixpoint nil)
      (W formal-nonempty-type-decl nil fixpoint_induct nil)
      (cl type-eq-decl nil cl nil) (cl? const-decl "bool" cl nil)
      (bool nonempty-type-eq-decl nil booleans nil)
      (boolean nonempty-type-decl nil booleans nil)
      (L formal-nonempty-type-decl nil fixpoint_induct nil)
      (fixpoint type-eq-decl nil fixpoint nil)
      (fixpoint? const-decl "bool" fixpoint nil)
      (mu const-decl "(lfp?(<=)(f))" fixpoint nil)
      (mu_fixpoint judgement-tcc nil fixpoint nil))
     193 110 t shostak)))
  
  
  --Apple-Mail-2-870090089--

How-To-Repeat: 

Fix: 
Home Intro Announce FAQ Docs Download Mail Status Bugs Users Related FM Tools