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

PVS Bug 633


Synopsis:        dump file
Severity:        serious
Priority:        medium
Responsible:     owre
State:           analyzed
Class:           sw-bug
Arrival-Date:    Fri Nov 30 9:04:32 2001
Originator:      John Rushby
Organization:    csl.sri.com
Release:         PVS 2.4
Environment: 
 System:          
 Architecture: 

Description: 
  This is the undistilled problem.   Load the dumpfile and do prt on
  genlinks.   A few proofs fail (I'm loading the two methods you sent
  earlier in pvs-strategies).  Find the first one that does and study
  the sequent after the final assert.   You'll see that it needs to
  reassociate one of the set expressions (I recall it's the last one).
  Go to cardprops and look at norm_assoc.   You'll see I've trivialised it.
    norm_assoc: SUBLEMMA true % ((r AND s) AND t) = (r AND (s AND t))
  change it back to
    norm_assoc: SUBLEMMA ((r AND s) AND t) = (r AND (s AND t))
  and redo the proof.  You'll see it loops.   It also loops doing the
  associativity the other way.
  
  John
  
  
  $$$pvs-strategies
  ; (load "./manip-package/manip-strategies")
  
  (defstep subtype-tcc ()
    (grind :rewrites ("finite_below") :defs explicit)
  "Modified subtyp-tcc rule to use finite_below"
  "By modified TCC strategy"
  )
  
  (defstep case-replace (formula &optional hide?) 
    (then@ (case formula)
           (replace -1 :hide? hide?))
    "Case splits on a given FORMULA lhs=rhs and replaces lhs by rhs.
  See also CASE, CASE*.  Hides FORMULA when HIDE? is T. "
    "Assuming and applying ~a")
  
  (defstep name-case-replace (A B X)
    (let ((A (pc-typecheck (pc-parse A 'expr)))
          (B (pc-typecheck (pc-parse B 'expr)))
          (eq (make-equality A B)))
      (then@ (case-replace eq :hide? T)(name-replace X B))) 
    "Replace A with B, then name B as X" 
    "Replacing ~a with ~a which is then named ~a")
  
  (defstep set-case-replace (A)
     (spread (case-replace A :hide? t) 
       ((skip) (then (apply-extensionality :hide? t)(grind))))
  "does a replace and tries to discharge subgoal"
  "replacing..."
  )
  
  (defstep set-equality ()
  	 (then (apply-extensionality :hide? t)(grind))
  "Does apply-extensionality and grind to establish equality of sets and functi
 ons"
  "Applying extensionality...")
  
  
  (defmethod match* ((lhs disjunction) (instance disjunction) bind-alist subst)
    (let ((dmatch (call-next-method)))
      (if (eq dmatch 'fail)
  	(match* (collect-disjuncts lhs) (collect-disjuncts instance)
  		bind-alist subst)
  	dmatch)))
  
  (defmethod match* ((lhs conjunction) (instance conjunction) bind-alist subst)
    (let ((cmatch (call-next-method)))
      (if (eq cmatch 'fail)
  	(match* (collect-conjuncts lhs) (collect-conjuncts instance)
  		bind-alist subst)
  	cmatch)))
  
  
  
  $$$genlinks.pvs
  genlinks[n: posnat, T: NONEMPTY_TYPE]: THEORY
  BEGIN
    
    npos: LEMMA n > 0
    node: TYPE+ = below[n] CONTAINING 0
    
    IMPORTING cardprops[node],
      finite_sets@finite_sets_below,
      finite_sets@finite_sets_pred
  
    nodeset: TYPE = finite_set[node]
    vector: TYPE = [node -> T]
    
    x, t, t1, t2: VAR T
  
    E: T
    UnR, R:[T->T]
  
    R_ax: AXIOM UnR(R(t)) = t
    R_E_prop: AXIOM R(t)/=E
    UnR_inv: AXIOM UnR(x)=t => x=R(t)
  
    arbval: T
  
    G, p, q, z: VAR node
    
    r: VAR nat
    
    caucus, ayes, Es, nonEs: VAR nodeset
    
    v: VAR vector
  
    send(r,t,p,q): T
  
    maj(caucus, v): T
    
    OMH(G, r, t, caucus) (p) : RECURSIVE T = 
      IF r = 0
        THEN IF member(G, caucus) AND member(p, caucus) THEN send(0, t, G, p)
        ELSE arbval
        ENDIF
      ELSE IF member(G, caucus) AND member(p, caucus)
          THEN IF p = G
            THEN send(r, t, G, G)
          ELSE
            UnR(maj(remove(G, caucus),
                (LAMBDA q: OMH(q, r - 1, R(send(r, t, G, q)), 
                                 remove(G, caucus))(p))))
          ENDIF
        ELSE arbval
        ENDIF
      ENDIF
     MEASURE r
  
    faults: TYPE = {good, manifest, omission, symmetric, arbitrary}
  
    status(p): faults
    
    ok(p): bool = good?(status(p))
    man(p): bool = manifest?(status(p))
    omit(p): bool = omission?(status(p))
    sym(p): bool = symmetric?(status(p))
    arb(p): bool = arbitrary?(status(p))
  
    perturb(G,t): T
  
    val(G,t,x): bool = 
     CASES status(G) of
        good: x=t,
        manifest: x=E,
        omission: x=t or x=E,
        symmetric: x=perturb(G,t),
        arbitrary: true
      ENDCASES
  
    j:var nat
  
    a, s, o, c, ls, lr, lra, lro: node
  
    okm(q):bool = ok(q) or omit(q)
  
    als(caucus,G,j,t): nat = card({q | member(q,remove(G,caucus)) AND okm(q)
               AND not val(G, t, send(j,t,G,q))})
  
    send_self_ax: axiom not arb(G) => val(G,t,send(r,t,G,G))
  
  % given following, can prove next 4
  
    als_ax_alt: axiom als(caucus,p, j,t) <= ls
  
    als_ax: axiom j>0 => als(caucus,p, j,t) <= ls
  
    ls0: AXIOM ls=0 => ok(q) => val(G, t, send(0,t,G,q))
  
    s_send_ax: AXIOM ls=0 => sym(G) and omit(q) => val(G,t,send(0,t,G,q))
  
    o_rcv_ax0: AXIOM ls=0 => ok(G) and omit(q) => val(G,t,send(0,t,G,q))
  
  
    alr(caucus,v,p): nat = card({q | member(q,caucus) AND ok(q)
                    AND send(0, v(q), q, p) /= v(q)})
    alro(caucus,v,p): nat = card({q | member(q,caucus) AND ok(q)
                    AND send(0, v(q), q, p) = E})
    alra(caucus,v,p): nat = card({q | member(q,caucus) AND ok(q)
                    AND send(0, v(q), q, p) /= v(q)
                    AND send(0, v(q), q, p) /= E})
  
    alr_lim: AXIOM
       alr(caucus, v, p) <= lr and alra(caucus, v, p) <= lra
  
    alr_prop: lemma (forall q: v(q)/=E) =>
          alr(caucus, v, p) = alro(caucus, v, p)+alra(caucus, v, p)
  
    m_send_ax: axiom man(G) and okm(q) => val(G,t,send(0,t,G,q))
  
    o_send_ax: axiom omit(G) and okm(q)  => val(G,t,send(0,t,G,q))
  
    allnodes: nodeset = fullset[node]
    
  
    Q: VAR [T->bool]
  
    hybrid_maj_ax: AXIOM
      (FORALL (x:node): member(x,caucus) and Q(v(x)) => v(x)/=E)
     and
      (FORALL (x, y:node): member(x,caucus) and Q(v(x))
                 and member(y,caucus) and Q(v(y)) => v(x)=v(y) or v(x)=R(E) or 
 v(y)=R(E))
     and
      (EXISTS (ayes, Es): subset?(ayes, caucus) AND
       subset?(Es, caucus) AND
        (FORALL p: member(p, ayes) => Q(v(p))) AND
         (FORALL p:  member(p, Es) => v(p) = E)
          AND 2 * card(ayes) > card(caucus) - card(Es))
       IMPLIES Q(maj(caucus, v))
  
    maj_ext: AXIOM
      FORALL (v1, v2: vector):
        (FORALL p: member(p, caucus) => v1(p) = v2(p))
          IMPLIES maj(caucus, v1) = maj(caucus, v2)
  
    
    aa(caucus): nat = card({q | member(q,caucus) AND arb(q)})
    as(caucus): nat = card({q | member(q,caucus) AND sym(q)})
    am(caucus): nat = card({q | member(q,caucus) AND man(q)})
    ao(caucus): nat = card({q | member(q,caucus) AND omit(q)})
    akm(caucus): nat = card({q | member(q,caucus) AND okm(q)})
  
  
    aoo(caucus,G,j,t,p): nat = card({q | member(q,caucus) AND omit(q)
               AND OMH(q,j,R(send(1+j,t,G,q)),caucus)(p) = E})
  
    A,B,C,D,Z,W: var nodeset
  
    card_u: SUBLEMMA disjoint?(Z,W) IMPLIES
      card({q|A(q) AND (Z(q) or W(q))}) = card({q|A(q) AND
      Z(q)})+card({q|A(q) AND W(q)})
  
    count_status: LEMMA card(A) = 
      card({q|A(q) AND man(q)})
       + card({q|A(q) AND ok(q)})
       + card({q|A(q) AND omit(q)})
       + card({q|A(q) AND arb(q)})
       + card({q|A(q) AND sym(q)})
  
    count_status_alt: LEMMA card(A) = 
      card({q|A(q) AND man(q)})
       + card({q|A(q) AND okm(q)})
       + card({q|A(q) AND arb(q)})
       + card({q|A(q) AND sym(q)})
  
    am_prop: lemma am(remove(G,caucus))<=am(caucus)
    as_prop: lemma as(remove(G,caucus))<=as(caucus)
    aa_prop: lemma aa(remove(G,caucus))<=aa(caucus)
    ao_prop: lemma ao(remove(G,caucus))<=ao(caucus)
  
    c_prop: lemma member(G,caucus) => card(remove(G,caucus)) = card(caucus) -1
  
  validity0: lemma
               ok(p) AND member(p, caucus) AND member(G, caucus)
           AND ls=0 and lr=0 
           IMPLIES val(G, t, OMH(G, 0, t, caucus)(p))
  
  % following uses different proof to prev
  
  validity0o: lemma
               omit(p) AND member(p, caucus) AND member(G, caucus)
           AND ls=0 and lr=0 
           IMPLIES val(G, t, OMH(G, 0, t, caucus)(p))
  
  
  
  %   count_t1: lemma okm(p) and not arb(G) and member(p,remove(G,caucus))
  %     implies
  %         card({q | let x = send(1, t, G, q) in
  %                  member(q, remove(G, caucus)) AND
  %                  val(G, t, x) AND
  %                   OMH(q, 0, R(x), remove(G, caucus))(p) =  R(x)})
  %         >= ax(remove(G,caucus))
  %             - als(caucus,G, 1,t)
  %             - alr(remove(G,caucus),lambda q:R(send(1,t,G,q)),p)
  %             + aox(remove(G,caucus),G, 0,t,p)
  
  
    count_t1a: lemma okm(p) and not arb(G) and member(p,remove(G,caucus))
      implies
          card({q | let x = send(1, t, G, q) in
                   member(q, remove(G, caucus)) AND
                   val(G, t, x) AND
                    OMH(q, 0, R(x), remove(G, caucus))(p) =  R(x)})
          >= 
          card({q | let x = send(1, t, G, q) in
                   member(q, remove(G, caucus)) AND okm(q) AND
                   val(G, t, x)})
           -
          card({q | let x = send(1, t, G, q) in
                   member(q, remove(G, caucus)) AND okm(q) AND
                   val(G, t, x) AND
                    OMH(q, 0, R(x), remove(G, caucus))(p) /=  R(x)})
  
    count_t1b: lemma okm(p) and not arb(G) and member(p,remove(G,caucus))
      implies
          card({q | let x = send(1, t, G, q) in
                   member(q, remove(G, caucus)) AND okm(q) AND
                   val(G, t, x)})
     =
          card({q | member(q, remove(G, caucus)) AND okm(q)})
              - als(caucus,G, 1,t)
  
  
    count_t1c: lemma  okm(p) and not arb(G) and member(p,remove(G,caucus))
      implies
         card({q | let x = send(1, t, G, q) in
                   member(q, remove(G, caucus)) AND okm(q) AND
                   val(G, t, x) AND
                    OMH(q, 0, R(x), remove(G, caucus))(p) /=  R(x)})
            =
        card({q | let x = send(1, t, G, q) in
                   member(q, remove(G, caucus)) AND ok(q) AND
                   val(G, t, x) AND
                    OMH(q, 0, R(x), remove(G, caucus))(p) /=  R(x)})
      +
        card({q | let x = send(1, t, G, q) in
                   member(q, remove(G, caucus)) AND omit(q) AND
                   val(G, t, x) AND
                    OMH(q, 0, R(x), remove(G, caucus))(p) /=  R(x)})
  
    count_t1d: lemma  okm(p) and not arb(G) and member(p,remove(G,caucus))
      implies
        card({q | let x = send(1, t, G, q) in
                   member(q, remove(G, caucus)) AND ok(q) AND
                   val(G, t, x) AND
                    OMH(q, 0, R(x), remove(G, caucus))(p) /=  R(x)})
            <= alr(remove(G,caucus),lambda q:R(send(1,t,G,q)),p) 
  
    count_t1e: lemma  okm(p) and not arb(G) and member(p,remove(G,caucus))
      implies
        card({q | let x = send(1, t, G, q) in
                   member(q, remove(G, caucus)) AND omit(q) AND
                   val(G, t, x) AND
                    OMH(q, 0, R(x), remove(G, caucus))(p) /=  R(x)})
              <= aoo(remove(G,caucus),G, 0,t,p)
  
    count_t1_new: lemma okm(p) and not arb(G) and member(p,remove(G,caucus))
      implies
          card({q | let x = send(1, t, G, q) in
                   member(q, remove(G, caucus)) AND
                   val(G, t, x) AND
                    OMH(q, 0, R(x), remove(G, caucus))(p) =  R(x)})
          >= 
              akm(remove(G,caucus))
              - als(caucus,G, 1,t)
              - alr(remove(G,caucus),lambda q:R(send(1,t,G,q)),p) 
              - aoo(remove(G,caucus),G, 0,t,p)
  
  
  
    count_E1: lemma okm(p) and member(p,remove(G,caucus))
          implies
         card({q | member(q, remove(G, caucus)) AND
                   OMH(q, 0, R(send(1, t, G, q)), remove(G, caucus))(p) = E})
           >= am(remove(G,caucus))
              + aoo(remove(G,caucus),G,0,t,p)
              + alro(remove(G,caucus),lambda q:R(send(1,t,G,q)),p)
  
  validity1: lemma
               NOT arb(G) AND okm(p) AND member(p, caucus)
           AND member(G, caucus)
           AND card(caucus)> 2 * (aa(caucus)+as(caucus)+ls) + am(caucus) + ao(c
 aucus) +lr +lra +1
           IMPLIES val(G, t, OMH(G, 1, t, caucus)(p))
  
  %   count_t: lemma okm(p) and not arb(G) and
  %        (forall q,x: okm(q) and member(q,remove(G,caucus)) implies
  %            val(q, R(x),  OMH(q, j, R(x), remove(G, caucus))(p))) implies
  %         card({q | let x = send(1 + j, t, G, q) in
  %                  member(q, remove(G, caucus)) AND
  %                  val(G, t, x) AND
  %                   OMH(q, j, R(x), remove(G, caucus))(p) =  R(x)})
  %         >= ax(remove(G,caucus))
  %             - als(caucus,G, j+1,t)
  %             + aox(remove(G,caucus),G, j,t,p)
  
    count_ta: lemma okm(p) and not arb(G) and
         (forall q,x: okm(q) and member(q,remove(G,caucus)) implies
             val(q, R(x),  OMH(q, j, R(x), remove(G, caucus))(p))) implies
          card({q | let x = send(1 + j, t, G, q) in
                   member(q, remove(G, caucus)) AND
                   val(G, t, x) AND
                    OMH(q, j, R(x), remove(G, caucus))(p) =  R(x)})
        >=
          card({q | let x = send(1 + j, t, G, q) in
                   member(q, remove(G, caucus)) AND okm(q) AND
                   val(G, t, x)})
         - card({q | let x = send(1 + j, t, G, q) in
                   member(q, remove(G, caucus)) AND okm(q) AND
                   val(G, t, x) AND
                    OMH(q, j, R(x), remove(G, caucus))(p) /=  R(x)})
  
    count_tb: lemma okm(p) and not arb(G) and
         (forall q,x: okm(q) and member(q,remove(G,caucus)) implies
             val(q, R(x),  OMH(q, j, R(x), remove(G, caucus))(p))) implies
          card({q | let x = send(1 + j, t, G, q) in
                   member(q, remove(G, caucus)) AND okm(q) AND
                   val(G, t, x)})
      = card({q | let x = send(1 + j, t, G, q) in
                   member(q, remove(G, caucus)) AND okm(q)})
              - als(caucus,G, j+1,t)
  
    count_tc: lemma okm(p) and not arb(G) and
         (forall q,x: okm(q) and member(q,remove(G,caucus)) implies
             val(q, R(x),  OMH(q, j, R(x), remove(G, caucus))(p))) implies
          card({q | let x = send(1 + j, t, G, q) in
                   member(q, remove(G, caucus)) AND okm(q) AND
                   val(G, t, x) AND
                    OMH(q, j, R(x), remove(G, caucus))(p) /=  R(x)})
      = card({q | let x = send(1 + j, t, G, q) in
                   member(q, remove(G, caucus)) AND ok(q) AND
                   val(G, t, x) AND
                    OMH(q, j, R(x), remove(G, caucus))(p) /=  R(x)})
         + card({q | let x = send(1 + j, t, G, q) in
                   member(q, remove(G, caucus)) AND omit(q) AND
                   val(G, t, x) AND
                    OMH(q, j, R(x), remove(G, caucus))(p) /=  R(x)})
  
    count_td: lemma okm(p) and not arb(G) and
         (forall q,x: okm(q) and member(q,remove(G,caucus)) implies
             val(q, R(x),  OMH(q, j, R(x), remove(G, caucus))(p))) implies
         card({q | let x = send(1 + j, t, G, q) in
                   member(q, remove(G, caucus)) AND ok(q) AND
                   val(G, t, x) AND
                    OMH(q, j, R(x), remove(G, caucus))(p) /=  R(x)})
              =0
  
    count_te: lemma okm(p) and not arb(G) and
         (forall q,x: okm(q) and member(q,remove(G,caucus)) implies
             val(q, R(x),  OMH(q, j, R(x), remove(G, caucus))(p))) implies
         card({q | let x = send(1 + j, t, G, q) in
                   member(q, remove(G, caucus)) AND omit(q) AND
                   val(G, t, x) AND
                    OMH(q, j, R(x), remove(G, caucus))(p) /=  R(x)})
              <= aoo(remove(G,caucus),G, j,t,p)
  
    count_t_new: lemma okm(p) and not arb(G) and
         (forall q,x: okm(q) and member(q,remove(G,caucus)) implies
             val(q, R(x),  OMH(q, j, R(x), remove(G, caucus))(p))) implies
          card({q | let x = send(1 + j, t, G, q) in
                   member(q, remove(G, caucus)) AND
                   val(G, t, x) AND
                    OMH(q, j, R(x), remove(G, caucus))(p) =  R(x)})
          >= akm(remove(G,caucus))
              - als(caucus,G, j+1,t)
              - aoo(remove(G,caucus),G, j,t,p)
  
  
    count_E: lemma okm(p) and
         (forall q, x: man(q) and member(q,remove(G,caucus)) implies
             OMH(q, j, x, remove(G, caucus))(p) =  E) implies
         card({q | member(q, remove(G, caucus)) AND
                   OMH(q, j, R(send(1 + j, t, G, q)), remove(G, caucus))(p) = E
 })
           >= am(remove(G,caucus))
              + aoo(remove(G,caucus),G,j,t,p)
  
  validity: lemma  forall (r:upfrom(1)):
         not arb(G) and
           okm(p) AND member(p, caucus) AND member(G, caucus)
           AND card(caucus)> 2 * (aa(caucus)+as(caucus)+ls) + am(caucus) + ao(c
 aucus) +lr +lra
           + r
             IMPLIES val(G,t,OMH(G, r, t, caucus)(p))
  
  agreement: lemma  
          member(G,caucus) and ok(p) AND member(p, caucus) and ok(q) AND member
 (q, caucus)
           AND card(caucus)> 2 * (aa(caucus)+as(caucus)+ls) + am(caucus) + ao(c
 aucus) +lr +lra
           + r
          and r > aa(caucus) + ao(caucus)+min(1,ls)
             IMPLIES OMH(G, r, t, caucus)(p)=OMH(G, r, t, caucus)(q)
  
  END genlinks
  
  $$$genlinks.prf
  (|genlinks| (|npos| "" (ASSERT) NIL NIL)
   (|node_TCC1| "" (SUBTYPE-TCC) NIL NIL)
   (OMH_TCC1 "" (SUBTYPE-TCC) NIL NIL)
   (OMH_TCC2 "" (TERMINATION-TCC) NIL NIL)
   (|als_TCC1| "" (SUBTYPE-TCC) NIL NIL)
   (|als_ax| "" (SKOSIMP) (("" (USE "als_ax_alt") NIL NIL)) NIL)
   (|ls0| "" (AUTO-REWRITE "finite_below")
    (("" (SKOSIMP)
      (("" (LEMMA "als_ax_alt")
        (("" (INST - "fullset[node]" 0 "G!1" "t!1")
          (("" (EXPAND "als")
            (("" (USE "empty_card[node]")
              (("" (GROUND)
                (("" (HIDE -2 -3)
                  (("" (EXPAND "empty?")
                    (("" (EXPAND "member")
                      (("" (INST - "q!1")
                        (("" (GROUND)
                          (("1" (CASE "G!1=q!1")
                            (("1" (LEMMA "send_self_ax")
                              (("1" (ASSERT)
                                (("1"
                                  (REWRITE -1)
                                  (("1" (ASSERT) NIL NIL)
                                   ("2" (GRIND) NIL NIL))
                                  NIL))
                                NIL))
                              NIL)
                             ("2" (GRIND) NIL NIL))
                            NIL)
                           ("2" (GRIND) NIL NIL))
                          NIL))
                        NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|s_send_ax| "" (AUTO-REWRITE "finite_below")
    (("" (SKOSIMP)
      (("" (LEMMA "als_ax_alt")
        (("" (INST - "fullset[node]" 0 "G!1" "t!1")
          (("" (EXPAND "als")
            (("" (USE "empty_card[node]")
              (("" (GROUND)
                (("" (HIDE -2 -3)
                  (("" (EXPAND "empty?")
                    (("" (EXPAND "member")
                      (("" (INST - "q!1") (("" (GRIND) NIL NIL)) NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|o_rcv_ax0| "" (AUTO-REWRITE "finite_below")
    (("" (SKOSIMP)
      (("" (LEMMA "als_ax_alt")
        (("" (INST - "fullset[node]" 0 "G!1" "t!1")
          (("" (EXPAND "als")
            (("" (USE "empty_card[node]")
              (("" (GROUND)
                (("" (HIDE -2 -3)
                  (("" (EXPAND "empty?")
                    (("" (EXPAND "member")
                      (("" (INST - "q!1") (("" (GRIND) NIL NIL)) NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|alr_TCC1| "" (SUBTYPE-TCC) NIL NIL)
   (|alro_TCC1| "" (SUBTYPE-TCC) NIL NIL)
   (|alra_TCC1| "" (SUBTYPE-TCC) NIL NIL)
   (|alr_prop| "" (AUTO-REWRITE "finite_below" "norm_assoc")
    (("" (SKOSIMP)
      (("" (EXPAND* "alr" "alra" "alro")
        (("" (REWRITE "card_disj_union[node]" :DIR RL)
          (("1" (REWRITE "equal_card")
            (("1" (APPLY-EXTENSIONALITY :HIDE? T)
              (("1" (EXPAND "union")
                (("1" (EXPAND "member")
                  (("1" (BDDSIMP)
                    (("1" (ASSERT) NIL NIL)
                     ("2" (INST?) (("2" (ASSERT) NIL NIL)) NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL)
           ("2" (HIDE 2) (("2" (GRIND) NIL NIL)) NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|allnodes_TCC1| "" (SUBTYPE-TCC) NIL NIL)
   (|aa_TCC1| "" (SUBTYPE-TCC) NIL NIL)
   (|as_TCC1| "" (SUBTYPE-TCC) NIL NIL)
   (|am_TCC1| "" (SUBTYPE-TCC) NIL NIL)
   (|ao_TCC1| "" (SUBTYPE-TCC) NIL NIL)
   (|akm_TCC1| "" (SUBTYPE-TCC) NIL NIL)
   (|aoo_TCC1| "" (SUBTYPE-TCC) NIL NIL)
   (|card_u_TCC1| "" (SUBTYPE-TCC) NIL NIL)
   (|card_u_TCC2| "" (SUBTYPE-TCC) NIL NIL)
   (|card_u_TCC3| "" (SUBTYPE-TCC) NIL NIL)
   (|card_u| "" (AUTO-REWRITE "finite_below")
    (("" (SKOSIMP)
      ((""
        (CASE-REPLACE "card({q | A!1(q) AND (Z!1(q) OR W!1(q))}) =
               card(union({q | A!1(q) AND Z!1(q)},{q | A!1(q) AND W!1(q)}))"
         :HIDE? T)
        (("1" (REWRITE "card_union")
          (("1" (ASSERT)
            (("1"
              (CASE "empty?(intersection({q | A!1(q) AND Z!1(q)}, {q | A!1(q) A
 ND W!1(q)}))")
              (("1" (REWRITE "empty_card") NIL NIL)
               ("2" (HIDE 2) (("2" (GRIND) NIL NIL)) NIL))
              NIL))
            NIL))
          NIL)
         ("2" (HIDE 2)
          (("2" (REWRITE "equal_card[node]")
            (("2" (HIDE 2)
              (("2" (APPLY-EXTENSIONALITY :HIDE? T)
                (("2" (GRIND) NIL NIL)) NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|count_status_TCC1| "" (SUBTYPE-TCC) NIL NIL)
   (|count_status_TCC2| "" (SUBTYPE-TCC) NIL NIL)
   (|count_status_TCC3| "" (SUBTYPE-TCC) NIL NIL)
   (|count_status_TCC4| "" (SUBTYPE-TCC) NIL NIL)
   (|count_status_TCC5| "" (SUBTYPE-TCC) NIL NIL)
   (|count_status| "" (SKOSIMP)
    (("" (AUTO-REWRITE "finite_below")
      ((""
        (CASE-REPLACE
         "card(A!1)=card({q | A!1(q) AND ( man(q) or omit(q) or arb(q) or ok(q)
  or sym(q))})")
        (("1" (HIDE -1)
          (("1" (REWRITE "card_u")
            (("1" (REWRITE "card_u")
              (("1" (REWRITE "card_u")
                (("1" (REWRITE "card_u")
                  (("1" (ASSERT) NIL NIL)
                   ("2" (HIDE 2) (("2" (GRIND) NIL NIL)) NIL))
                  NIL)
                 ("2" (HIDE 2) (("2" (GRIND) NIL NIL)) NIL))
                NIL)
               ("2" (HIDE 2) (("2" (GRIND) NIL NIL)) NIL))
              NIL)
             ("2" (HIDE 2) (("2" (GRIND) NIL NIL)) NIL))
            NIL))
          NIL)
         ("2" (HIDE 2)
          (("2" (REWRITE "equal_card[node]")
            (("2" (APPLY-EXTENSIONALITY :HIDE? T) (("2" (GRIND) NIL NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|count_status_alt_TCC1| "" (SUBTYPE-TCC) NIL NIL)
   (|count_status_alt| "" (SKOSIMP)
    (("" (AUTO-REWRITE "finite_below")
      ((""
        (CASE-REPLACE
         "card(A!1)=card({q | A!1(q) AND ( man(q) or arb(q) or okm(q) or sym(q)
 )})")
        (("1" (HIDE -1)
          (("1" (REWRITE "card_u")
            (("1" (REWRITE "card_u")
              (("1" (REWRITE "card_u")
                (("1" (ASSERT) NIL NIL)
                 ("2" (HIDE 2) (("2" (GRIND) NIL NIL)) NIL))
                NIL)
               ("2" (HIDE 2) (("2" (GRIND) NIL NIL)) NIL))
              NIL)
             ("2" (HIDE 2) (("2" (GRIND) NIL NIL)) NIL))
            NIL))
          NIL)
         ("2" (HIDE 2)
          (("2" (REWRITE "equal_card[node]")
            (("2" (APPLY-EXTENSIONALITY :HIDE? T) (("2" (GRIND) NIL NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|am_prop| "" (AUTO-REWRITE "finite_below" "norm_assoc")
    (("" (SKOSIMP)
      (("" (EXPAND "am")
        (("" (REWRITE "card_subset") (("" (GRIND) NIL NIL)) NIL)) NIL))
      NIL))
    NIL)
   (|as_prop| "" (AUTO-REWRITE "finite_below" "norm_assoc")
    (("" (SKOSIMP)
      (("" (EXPAND "as")
        (("" (REWRITE "card_subset") (("" (GRIND) NIL NIL)) NIL)) NIL))
      NIL))
    NIL)
   (|aa_prop| "" (AUTO-REWRITE "finite_below" "norm_assoc")
    (("" (SKOSIMP)
      (("" (EXPAND "aa")
        (("" (REWRITE "card_subset") (("" (GRIND) NIL NIL)) NIL)) NIL))
      NIL))
    NIL)
   (|ao_prop| "" (AUTO-REWRITE "finite_below" "norm_assoc")
    (("" (SKOSIMP)
      (("" (EXPAND "ao")
        (("" (REWRITE "card_subset") (("" (GRIND) NIL NIL)) NIL)) NIL))
      NIL))
    NIL)
   (|c_prop| "" (SKOSIMP)
    (("" (REWRITE "card_remove[node]") (("" (GRIND) NIL NIL)) NIL)) NIL)
   (|validity0| "" (AUTO-REWRITE "finite_below" "norm_assoc")
    (("" (SKOSIMP)
      (("" (EXPAND "OMH")
        (("" (LIFT-IF) (("" (USE "ls0") (("" (GROUND) NIL NIL)) NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|validity0o| "" (AUTO-REWRITE "finite_below" "norm_assoc")
    (("" (SKOSIMP)
      (("" (EXPAND "val")
        (("" (LIFT-IF)
          (("" (GROUND)
            (("1" (EXPAND "OMH")
              (("1" (CASE-REPLACE "G!1=p!1")
                (("1" (USE "send_self_ax") (("1" (GRIND) NIL NIL)) NIL)
                 ("2" (USE "o_rcv_ax0") (("2" (GRIND) NIL NIL)) NIL))
                NIL))
              NIL)
             ("2" (EXPAND "OMH")
              (("2" (USE "m_send_ax") (("2" (GRIND) NIL NIL)) NIL)) NIL)
             ("3" (EXPAND "OMH")
              (("3" (USE "o_send_ax") (("3" (GRIND) NIL NIL)) NIL)) NIL)
             ("4" (EXPAND "OMH")
              (("4" (USE "s_send_ax") (("4" (GRIND) NIL NIL)) NIL)) NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|count_t1a_TCC1| "" (SUBTYPE-TCC) NIL NIL)
   (|count_t1a_TCC2| "" (SUBTYPE-TCC) NIL NIL)
   (|count_t1a_TCC3| "" (SUBTYPE-TCC) NIL NIL)
   (|count_t1a| "" (AUTO-REWRITE "finite_below" "norm_assoc")
    (("" (SKOSIMP)
      (("" (REWRITE "count_status_alt")
        (("" (BETA *)
          (("" (LEMMA "card_prop")
            ((""
              (INST - "lambda q: member(q, remove(G!1, caucus!1)) AND
                        okm(q) AND val(G!1, t!1, send(1, t!1, G!1, q))"
               "lambda q: OMH(q, 0, R(send(1, t!1, G!1, q)),
                                remove(G!1, caucus!1))
                               (p!1)
                             = R(send(1, t!1, G!1, q))")
              ((""
                (CASE-REPLACE "{q_701: node |
                   (member(q_701, remove(G!1, caucus!1)) AND
                     okm(q_701) AND val(G!1, t!1, send(1, t!1, G!1, q_701)))
                    AND
                    OMH(q_701, 0, R(send(1, t!1, G!1, q_701)),
                        remove(G!1, caucus!1))
                       (p!1)
                     = R(send(1, t!1, G!1, q_701))}=
     {q_685: node |
                   (member(q_685, remove(G!1, caucus!1)) AND
                     (val(G!1, t!1, send(1, t!1, G!1, q_685)) AND
                       (OMH(q_685, 0, R(send(1, t!1, G!1, q_685)),
                            remove(G!1, caucus!1))
                           (p!1)
                         = R(send(1, t!1, G!1, q_685))
                         AND okm(q_685))))}" :HIDE? T)
                (("1" (ASSERT)
                  (("1" (REPLACE -1 :HIDE? T)
                    (("1"
                      (CASE-REPLACE "{q_704: node |
                      (member(q_704, remove(G!1, caucus!1)) AND
                        (okm(q_704) AND
                          (val(G!1, t!1, send(1, t!1, G!1, q_704)) AND
                            NOT OMH(q_704, 0, R(send(1, t!1, G!1, q_704)),
                                    remove(G!1, caucus!1))
                                   (p!1)
                                 = R(send(1, t!1, G!1, q_704)))))}=
       {q |
                       member(q, remove(G!1, caucus!1)) AND
                        okm(q) AND
                         val(G!1, t!1, send(1, t!1, G!1, q)) AND
                          OMH(q, 0, R(send(1, t!1, G!1, q)), remove(G!1, caucus
 !1))
                             (p!1)
                           /= R(send(1, t!1, G!1, q))}" :HIDE? T)
                      (("1" (ASSERT) NIL NIL)
                       ("2" (HIDE 3)
                        (("2" (APPLY-EXTENSIONALITY :HIDE? T)
                          (("2" (GRIND) NIL NIL)) NIL))
                        NIL))
                      NIL))
                    NIL))
                  NIL)
                 ("2" (HIDE -1 3)
                  (("2" (APPLY-EXTENSIONALITY :HIDE? T)
                    (("2" (GRIND) NIL NIL)) NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|count_t1b_TCC1| "" (SUBTYPE-TCC) NIL NIL)
   (|count_t1b| "" (AUTO-REWRITE "finite_below" "norm_assoc")
    (("" (SKOSIMP)
      (("" (BETA *)
        (("" (EXPAND "als")
          (("" (LEMMA "card_prop")
            (("" (ASSERT)
              ((""
                (INST -
                 "lambda q: member(q, remove(G!1, caucus!1)) AND okm(q)"
                 "lambda q: val(G!1, t!1, send(1, t!1, G!1, q))")
                (("" (ASSERT) NIL NIL)) NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|count_t1c_TCC1| "" (SUBTYPE-TCC) NIL NIL)
   (|count_t1c_TCC2| "" (SUBTYPE-TCC) NIL NIL)
   (|count_t1c| "" (AUTO-REWRITE "finite_below" "norm_assoc")
    (("" (SKOSIMP)
      (("" (REWRITE "card_disj_union" :DIR RL)
        (("1" (REWRITE "equal_card")
          (("1" (HIDE 3)
            (("1" (APPLY-EXTENSIONALITY :HIDE? T)
              (("1" (GRIND :EXCLUDE "OMH") NIL NIL)) NIL))
            NIL))
          NIL)
         ("2" (HIDE 3) (("2" (GRIND :EXCLUDE "OMH") NIL NIL)) NIL))
        NIL))
      NIL))
    NIL)
   (|count_t1d| "" (AUTO-REWRITE "finite_below" "norm_assoc")
    (("" (SKOSIMP)
      (("" (EXPAND "alr")
        (("" (REWRITE "card_subset")
          (("" (HIDE 3) (("" (GRIND) NIL NIL)) NIL)) NIL))
        NIL))
      NIL))
    NIL)
   (|count_t1e| "" (AUTO-REWRITE "finite_below" "norm_assoc")
    (("" (SKOSIMP)
      (("" (EXPAND "aoo")
        (("" (REWRITE "card_subset")
          (("" (HIDE 3)
            (("" (EXPAND "subset?")
              (("" (EXPAND "member")
                (("" (SKOSIMP)
                  (("" (GROUND)
                    (("" (EXPAND "OMH")
                      (("" (LIFT-IF)
                        (("" (GROUND)
                          (("1" (USE "o_send_ax")
                            (("1" (EXPAND "val")
                              (("1" (EXPAND "omit")
                                (("1" (ASSERT) NIL NIL)) NIL))
                              NIL))
                            NIL)
                           ("2" (EXPAND "member")
                            (("2" (PROPAX) NIL NIL)) NIL))
                          NIL))
                        NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|count_t1_new| "" (SKOSIMP)
    (("" (BETA *)
      (("" (EXPAND "akm")
        (("" (USE "count_t1a")
          (("" (GROUND)
            (("" (USE "count_t1b")
              (("" (GROUND)
                (("" (REPLACE -1 :HIDE? T)
                  (("" (USE "count_t1c")
                    (("" (GROUND)
                      (("" (REPLACE -1 :HIDE? T)
                        (("" (USE "count_t1d")
                          (("" (GROUND)
                            (("" (USE "count_t1e")
                              (("" (GROUND) NIL NIL)) NIL))
                            NIL))
                          NIL))
                        NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|count_E1_TCC1| "" (SUBTYPE-TCC) NIL NIL)
   (|count_E1| "" (AUTO-REWRITE "finite_below" "norm_assoc")
    (("" (SKOSIMP)
      (("" (REWRITE "count_status")
        ((""
          (CASE-REPLACE " card({q_4826: node |
                                      (member(q_4826, remove(G!1, caucus!1)) AN
 D
                                        (OMH(q_4826, 0, R(send(1, t!1, G!1, q_4
 826)),
                                              remove(G!1, caucus!1))
                                             (p!1)
                                          = E
                                          AND ok(q_4826)))})=
                            alro(remove(G!1,caucus!1), LAMBDA q: R(send(1, t!1,
  G!1, q)), p!1)"
           :HIDE? T)
          (("1"
            (CASE-REPLACE " card({q_4826: node |
                                                    (member(q_4826, remove(G!1,
  caucus!1)) AND
                                                      (OMH(q_4826, 0, R(send(1,
  t!1, G!1, q_4826)),
                                                            remove(G!1, caucus!
 1))
                                                           (p!1)
                                                        = E
                                                        AND man(q_4826)))})=
                                            am(remove(G!1, caucus!1))"
             :HIDE? T)
            (("1"
              (CASE-REPLACE " card({q_4826: node |
                                                                  (member(q_482
 6, remove(G!1, caucus!1)) AND
                                                                    (OMH(q_4826
 , 0, R(send(1, t!1, G!1, q_4826)),
                                                                          remov
 e(G!1, caucus!1))
                                                                         (p!1)
                                                                      = E
                                                                      AND omit(
 q_4826)))})=
                                                           aoo(remove(G!1, cauc
 us!1), G!1, 0, t!1, p!1)"
               :HIDE? T)
              (("1" (ASSERT) NIL NIL)
               ("2" (HIDE 2)
                (("2" (EXPAND "aoo")
                  (("2" (REWRITE "equal_card")
                    (("2" (APPLY-EXTENSIONALITY :HIDE? T)
                      (("2" (GRIND) NIL NIL)) NIL))
                    NIL))
                  NIL))
                NIL))
              NIL)
             ("2" (HIDE 2)
              (("2" (EXPAND "am")
                (("2" (REWRITE "equal_card")
                  (("2" (HIDE 2)
                    (("2" (APPLY-EXTENSIONALITY :HIDE? T)
                      (("2" (BDDSIMP)
                        (("2" (EXPAND "OMH")
                          (("2" (LIFT-IF)
                            (("2" (GROUND)
                              (("2" (USE "m_send_ax")
                                (("2" (GRIND) NIL NIL)) NIL))
                              NIL))
                            NIL))
                          NIL))
                        NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL)
           ("2" (HIDE 2)
            (("2" (EXPAND "alro")
              (("2" (REWRITE "equal_card")
                (("2" (APPLY-EXTENSIONALITY :HIDE? T)
                  (("2" (GRIND) NIL NIL)) NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|validity1| "" (AUTO-REWRITE "finite_below" "norm_assoc")
    (("" (SKOSIMP)
      (("" (EXPAND "OMH")
        (("" (LIFT-IF)
          (("" (GROUND)
            (("1" (USE "send_self_ax") (("1" (GROUND) NIL NIL)) NIL)
             ("2" (LEMMA "hybrid_maj_ax")
              (("2" (INST?)
                (("2" (INST - "lambda t: val(G!1,t!1,UnR(t))")
                  (("2" (ASSERT)
                    (("2" (HIDE 3)
                      (("2" (GROUND)
                        (("1" (SKOSIMP)
                          (("1" (EXPAND "val")
                            (("1" (LIFT-IF)
                              (("1" (GROUND)
                                (("1"
                                  (FORWARD-CHAIN "UnR_inv")
                                  (("1"
                                    (REPLACE -1 :HIDE? T)
                                    (("1"
                                      (USE "R_E_prop")
                                      (("1" (ASSERT) NIL NIL))
                                      NIL))
                                    NIL))
                                  NIL)
                                 ("2"
                                  (FORWARD-CHAIN "UnR_inv")
                                  (("2"
                                    (REPLACE -1 :HIDE? T)
                                    (("2"
                                      (USE "R_E_prop")
                                      (("2" (ASSERT) NIL NIL))
                                      NIL))
                                    NIL))
                                  NIL)
                                 ("3"
                                  (FORWARD-CHAIN "UnR_inv")
                                  (("3"
                                    (REPLACE -1 :HIDE? T)
                                    (("3"
                                      (USE "R_E_prop")
                                      (("3" (ASSERT) NIL NIL))
                                      NIL))
                                    NIL))
                                  NIL)
                                 ("4"
                                  (FORWARD-CHAIN "UnR_inv")
                                  (("4"
                                    (REPLACE -1 :HIDE? T)
                                    (("4"
                                      (USE "R_E_prop")
                                      (("4" (ASSERT) NIL NIL))
                                      NIL))
                                    NIL))
                                  NIL)
                                 ("5"
                                  (FORWARD-CHAIN "UnR_inv")
                                  (("5"
                                    (REPLACE -1 :HIDE? T)
                                    (("5"
                                      (USE "R_E_prop")
                                      (("5" (ASSERT) NIL NIL))
                                      NIL))
                                    NIL))
                                  NIL)
                                 ("6" (GRIND) NIL NIL))
                                NIL))
                              NIL))
                            NIL))
                          NIL)
                         ("2" (SKOSIMP)
                          (("2" (EXPAND "val")
                            (("2" (LIFT-IF)
                              (("2" (GROUND)
                                (("1"
                                  (FORWARD-CHAIN "UnR_inv")
                                  (("1"
                                    (FORWARD-CHAIN "UnR_inv")
                                    (("1" (ASSERT) NIL NIL))
                                    NIL))
                                  NIL)
                                 ("2" (FORWARD-CHAIN "UnR_inv") NIL NIL)
                                 ("3"
                                  (FORWARD-CHAIN "UnR_inv")
                                  (("3"
                                    (FORWARD-CHAIN "UnR_inv")
                                    (("3" (ASSERT) NIL NIL))
                                    NIL))
                                  NIL)
                                 ("4" (FORWARD-CHAIN "UnR_inv") NIL NIL)
                                 ("5"
                                  (FORWARD-CHAIN "UnR_inv")
                                  (("5"
                                    (ASSERT)
                                    (("5"
                                      (FORWARD-CHAIN "UnR_inv")
                                      NIL
                                      NIL))
                                    NIL))
                                  NIL)
                                 ("6" (FORWARD-CHAIN "UnR_inv") NIL NIL)
                                 ("7"
                                  (FORWARD-CHAIN "UnR_inv")
                                  (("7"
                                    (FORWARD-CHAIN "UnR_inv")
                                    (("7" (ASSERT) NIL NIL))
                                    NIL))
                                  NIL)
                                 ("8" (GRIND) NIL NIL))
                                NIL))
                              NIL))
                            NIL))
                          NIL)
                         ("3"
                          (INST +
                           "{q| let t=send(1,t!1,G!1,q) in member(q,remove(G!1,
 caucus!1)) and val(G!1, t!1,t)
                                                                               
                                                                               
                                                                               
                                                                               
                 and OMH(q, 0,R(t),remove(G!1,caucus!1))(p!1)=R(t)}"
                           _)
                          (("3" (GROUND)
                            (("3"
                              (INST + "{q| member(q,remove(G!1,caucus!1))
                                                                               
                                                                          and O
 MH(q, 0,R(send(1,t!1,G!1,q)),remove(G!1,caucus!1))(p!1)=E}")
                              (("3" (GROUND)
                                (("1"
                                  (HIDE -6)
                                  (("1"
                                    (GRIND :EXCLUDE ("OMH"))
                                    NIL
                                    NIL))
                                  NIL)
                                 ("2"
                                  (HIDE -6)
                                  (("2"
                                    (GRIND :EXCLUDE ("OMH"))
                                    NIL
                                    NIL))
                                  NIL)
                                 ("3"
                                  (HIDE -6)
                                  (("3"
                                    (SKOSIMP)
                                    (("3"
                                      (USE "R_ax")
                                      (("3"
                                        (GRIND :EXCLUDE ("OMH"))
                                        NIL
                                        NIL))
                                      NIL))
                                    NIL))
                                  NIL)
                                 ("4"
                                  (SKOSIMP)
                                  (("4"
                                    (EXPAND "member")
                                    (("4" (FLATTEN) NIL NIL))
                                    NIL))
                                  NIL)
                                 ("5"
                                  (LEMMA "count_E1")
                                  (("5"
                                    (INST?)
                                    (("5"
                                      (GROUND)
                                      (("1"
                                        (LEMMA "count_t1_new")
                                        (("1"
                                          (BETA *)
                                          (("1"
                                            (INST?)
                                            (("1"
                                              (GROUND)
                                              (("1"
                                                (ASSERT)
                                                (("1"
                                                  (CASE-REPLACE
                                                   "let x=remove(G!1,caucus!1) 
 in akm(x)=card(x)-aa(x)-as(x)-am(x)")
                                                  (("1"
                                                    (BETA *)
                                                    (("1"
                                                      (EXPAND "akm")
                                                      (("1"
                                                        (REPLACE
  
                                                         -1
                                                         :HIDE?
  
                                                         T)
                                                        (("1"
                                                          (CASE
                                                           "2*(card(remove(G!1,
  caucus!1)) - aa(remove(G!1, caucus!1)) -
          am(remove(G!1, caucus!1))
          - as(remove(G!1, caucus!1))
          -
          alr(remove(G!1, caucus!1), LAMBDA q: R(send(1, t!1, G!1, q)), p!1)
          - als(caucus!1, G!1, 1, t!1)
          - aoo(remove(G!1, caucus!1), G!1, 0, t!1, p!1))
  >
         card(remove(G!1, caucus!1)) -
  (am(remove(G!1, caucus!1)) +
          alro(remove(G!1, caucus!1), LAMBDA q: R(send(1, t!1, G!1, q)), p!1)
          + aoo(remove(G!1, caucus!1), G!1, 0, t!1, p!1))")
                                                          (("1"
                                                            (ASSERT)
                                                            NIL
                                                            NIL)
                                                           ("2"
                                                            (HIDE
                                                             -1
                                                             -2
                                                             2)
                                                            (("2"
                                                              (ASSERT)
                                                              (("2"
                                                                (ASSERT)
                                                                (("2"
                                                                  (CASE
                                                                   "- 2 * alr(r
 emove(G!1,caucus!1), LAMBDA q: R(send(1, t!1, G!1, q)), p!1)
                                                                               
                                                                               
                                                                               
                                                                               
                     + alro(remove(G!1,caucus!1), LAMBDA q: R(send(1, t!1, G!1,
  q)), p!1)
                                                                               
                                                                               
                                                                               
                                                                               
              >= -lr-lra")
                                                                  (("1"
                                                                    (REWRITE
                                                                     "c_prop")
                                                                    (("1"
                                                                      (USE
                                                                       "als_ax"
 )
                                                                      (("1"
                                                                        (ASSERT
 )
                                                                        (("1"
                                                                          (USE
                                                                           "am_
 prop")
                                                                          (("1"
                                                                            (US
 E
                                                                             "a
 o_prop")
                                                                            (("
 1"
                                                                              (
 USE
                                                                               
 "aa_prop")
                                                                              (
 ("1"
                                                                               
  (USE
                                                                               
   "as_prop")
                                                                               
  (("1"
                                                                               
    (CASE
                                                                               
     "aoo(remove(G!1, caucus!1), G!1, 0, t!1, p!1)<=ao(remove(G!1, caucus!1))")
                                                                               
    (("1"
                                                                               
      (ASSERT
                                                                               
       :FLUSH?
                                                                               
       T)
                                                                               
      NIL
                                                                               
      NIL)
                                                                               
     ("2"
                                                                               
      (HIDE
                                                                               
       -6
                                                                               
       -12
                                                                               
       2)
                                                                               
      (("2"
                                                                               
        (EXPAND
                                                                               
         "aoo")
                                                                               
        (("2"
                                                                               
          (EXPAND
                                                                               
           "ao")
                                                                               
          (("2"
                                                                               
            (REWRITE
                                                                               
             "card_subset")
                                                                               
            (("2"
                                                                               
              (HIDE
                                                                               
               2)
                                                                               
              (("2"
                                                                               
                (EXPAND
                                                                               
                 "subset?")
                                                                               
                (("2"
                                                                               
                  (SKOSIMP)
                                                                               
                  (("2"
                                                                               
                    (EXPAND
                                                                               
                     "member")
                                                                               
                    (("2"
                                                                               
                      (GROUND)
                                                                               
                      NIL
                                                                               
                      NIL))
                                                                               
                    NIL))
                                                                               
                  NIL))
                                                                               
                NIL))
                                                                               
              NIL))
                                                                               
            NIL))
                                                                               
          NIL))
                                                                               
        NIL))
                                                                               
      NIL))
                                                                               
    NIL))
                                                                               
  NIL))
                                                                              N
 IL))
                                                                            NIL
 ))
                                                                          NIL))
                                                                        NIL))
                                                                      NIL))
                                                                    NIL)
                                                                   ("2"
                                                                    (GROUND)
                                                                    (("2"
                                                                      (USE
                                                                       "alr_lim
 ")
                                                                      (("2"
                                                                        (GROUND
 )
                                                                        (("2"
                                                                          (USE
                                                                           "R_E
 _prop")
                                                                          (("2"
                                                                            (AS
 SERT)
                                                                            (("
 2"
                                                                              (
 HIDE
                                                                               
 -9
                                                                               
 2)
                                                                              (
 ("2"
                                                                               
  (USE
                                                                               
   "alr_prop")
                                                                               
  (("2"
                                                                               
    (ASSERT)
                                                                               
    (("2"
                                                                               
      (SKOSIMP)
                                                                               
      (("2"
                                                                               
        (USE
                                                                               
         "R_E_prop")
                                                                               
        (("2"
                                                                               
          (ASSERT)
                                                                               
          NIL
                                                                               
          NIL))
                                                                               
        NIL))
                                                                               
      NIL))
                                                                               
    NIL))
                                                                               
  NIL))
                                                                              N
 IL))
                                                                            NIL
 ))
                                                                          NIL))
                                                                        NIL))
                                                                      NIL))
                                                                    NIL))
                                                                  NIL))
                                                                NIL))
                                                              NIL))
                                                            NIL))
                                                          NIL))
                                                        NIL))
                                                      NIL))
                                                    NIL)
                                                   ("2"
                                                    (BETA *)
                                                    (("2"
                                                      (HIDE -1 -2 -8 2)
                                                      (("2"
                                                        (USE
                                                         "count_status_alt")
                                                        (("2"
                                                          (EXPAND*
                                                           "ax"
                                                           "aa"
                                                           "as"
                                                           "am"
                                                           "akm")
                                                          (("2"
                                                            (EXPAND
                                                             "member")
                                                            (("2"
                                                              (ASSERT)
                                                              NIL
                                                              NIL))
                                                            NIL))
                                                          NIL))
                                                        NIL))
                                                      NIL))
                                                    NIL))
                                                  NIL))
                                                NIL)
                                               ("2" (GRIND) NIL NIL))
                                              NIL))
                                            NIL))
                                          NIL))
                                        NIL)
                                       ("2" (GRIND) NIL NIL))
                                      NIL))
                                    NIL))
                                  NIL))
                                NIL))
                              NIL))
                            NIL))
                          NIL))
                        NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|count_ta_TCC1| "" (SUBTYPE-TCC) NIL NIL)
   (|count_ta_TCC2| "" (SUBTYPE-TCC) NIL NIL)
   (|count_ta_TCC3| "" (SUBTYPE-TCC) NIL NIL)
   (|count_ta| "" (AUTO-REWRITE "finite_below" "norm_assoc")
    (("" (SKOSIMP)
      (("" (REWRITE "count_status_alt")
        (("" (BETA *)
          (("" (LEMMA "card_prop")
            ((""
              (INST - "lambda q:member(q, remove(G!1, caucus!1)) AND
                        okm(q) AND val(G!1, t!1, send(1 + j!1, t!1, G!1, q))"
               "lambda q: OMH(q, j!1, R(send(1 + j!1, t!1, G!1, q)),
                               remove(G!1, caucus!1))
                              (p!1)
                            = R(send(1 + j!1, t!1, G!1, q))")
              ((""
                (CASE-REPLACE "{q_3728: node |
                      (member(q_3728, remove(G!1, caucus!1)) AND
                        okm(q_3728) AND
                         val(G!1, t!1, send(1 + j!1, t!1, G!1, q_3728)))
                       AND
                       OMH(q_3728, j!1, R(send(1 + j!1, t!1, G!1, q_3728)),
                           remove(G!1, caucus!1))
                          (p!1)
                        = R(send(1 + j!1, t!1, G!1, q_3728))}=
        {q_3712: node |
                      (member(q_3712, remove(G!1, caucus!1)) AND
                        (val(G!1, t!1, send(1 + j!1, t!1, G!1, q_3712)) AND
                          (OMH(q_3712, j!1, R(send(1 + j!1, t!1, G!1, q_3712)),
                               remove(G!1, caucus!1))
                              (p!1)
                            = R(send(1 + j!1, t!1, G!1, q_3712))
                            AND okm(q_3712))))}" :HIDE? T)
                (("1" (ASSERT)
                  (("1" (REPLACE -1 :HIDE? T)
                    (("1" (ASSERT)
                      (("1"
                        (CASE-REPLACE "{q_3765: node |
                      (member(q_3765, remove(G!1, caucus!1)) AND
                        (okm(q_3765) AND
                          (val(G!1, t!1, send(1 + j!1, t!1, G!1, q_3765)) AND
                            NOT OMH(q_3765, j!1,
                                    R(send(1 + j!1, t!1, G!1, q_3765)),
                                    remove(G!1, caucus!1))
                                   (p!1)
                                 = R(send(1 + j!1, t!1, G!1, q_3765)))))}
       ={q |
                       member(q, remove(G!1, caucus!1)) AND
                        okm(q) AND
                         val(G!1, t!1, send(1 + j!1, t!1, G!1, q)) AND
                          OMH(q, j!1, R(send(1 + j!1, t!1, G!1, q)),
                              remove(G!1, caucus!1))
                             (p!1)
                           /= R(send(1 + j!1, t!1, G!1, q))}" :HIDE? T)
                        (("1" (ASSERT) NIL NIL)
                         ("2" (HIDE 3)
                          (("2" (APPLY-EXTENSIONALITY :HIDE? T)
                            (("2" (GRIND) NIL NIL)) NIL))
                          NIL))
                        NIL))
                      NIL))
                    NIL))
                  NIL)
                 ("2" (HIDE -1 3)
                  (("2" (APPLY-EXTENSIONALITY :HIDE? T)
                    (("2" (GRIND) NIL NIL)) NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|count_tb_TCC1| "" (SUBTYPE-TCC) NIL NIL)
   (|count_tb| "" (AUTO-REWRITE "finite_below" "norm_assoc")
    (("" (SKOSIMP)
      (("" (BETA *)
        (("" (EXPAND "als")
          (("" (LEMMA "card_prop")
            (("" (ASSERT)
              ((""
                (INST -
                 "lambda q: member(q, remove(G!1, caucus!1)) AND okm(q)"
                 "lambda q: val(G!1, t!1, send(1+j!1, t!1, G!1, q))")
                (("" (ASSERT) NIL NIL)) NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|count_tc_TCC1| "" (SUBTYPE-TCC) NIL NIL)
   (|count_tc_TCC2| "" (SUBTYPE-TCC) NIL NIL)
   (|count_tc| "" (AUTO-REWRITE "finite_below" "norm_assoc")
    (("" (SKOSIMP)
      (("" (REWRITE "card_disj_union" :DIR RL)
        (("1" (REWRITE "equal_card")
          (("1" (HIDE 3)
            (("1" (APPLY-EXTENSIONALITY :HIDE? T)
              (("1" (GRIND :EXCLUDE "OMH") NIL NIL)) NIL))
            NIL))
          NIL)
         ("2" (HIDE 3) (("2" (GRIND :EXCLUDE "OMH") NIL NIL)) NIL))
        NIL))
      NIL))
    NIL)
   (|count_td| "" (AUTO-REWRITE "finite_below" "norm_assoc")
    (("" (SKOSIMP)
      (("" (BETA *)
        (("" (LEMMA "empty_card[node]")
          (("" (INST?)
            (("" (GROUND)
              (("" (HIDE 1 4)
                (("" (EXPAND "empty?")
                  (("" (SKOSIMP)
                    (("" (EXPAND "member")
                      (("" (FLATTEN)
                        (("" (INST?)
                          (("" (EXPAND "okm")
                            (("" (GROUND)
                              (("1" (EXPAND "ok")
                                (("1"
                                  (ASSERT)
                                  (("1"
                                    (EXPAND "val")
                                    (("1" (PROPAX) NIL NIL))
                                    NIL))
                                  NIL))
                                NIL)
                               ("2" (GRIND) NIL NIL))
                              NIL))
                            NIL))
                          NIL))
                        NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|count_te| "" (AUTO-REWRITE "finite_below" "norm_assoc")
    (("" (SKOSIMP)
      (("" (EXPAND "aoo")
        (("" (REWRITE "card_subset")
          (("" (HIDE 3)
            (("" (EXPAND "subset?")
              (("" (EXPAND "member")
                (("" (SKOSIMP)
                  (("" (GROUND)
                    (("" (INST?)
                      (("" (EXPAND "okm")
                        (("" (EXPAND "omit")
                          (("" (ASSERT)
                            (("" (EXPAND "val") (("" (PROPAX) NIL NIL))
                              NIL))
                            NIL))
                          NIL))
                        NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|count_t_new| "" (SKOSIMP)
    (("" (USE "count_ta")
      (("" (GROUND)
        (("" (USE "count_tb")
          (("" (GROUND)
            (("" (REPLACE -1 :HIDE? T)
              (("" (USE "count_tc")
                (("" (GROUND)
                  (("" (REPLACE -1 :HIDE? T)
                    (("" (USE "count_td")
                      (("" (GROUND)
                        (("" (REPLACE -1 :HIDE? T)
                          (("" (USE "count_te")
                            (("" (GROUND)
                              (("" (ASSERT)
                                ((""
                                  (EXPAND "akm")
                                  (("" (ASSERT) NIL NIL))
                                  NIL))
                                NIL))
                              NIL))
                            NIL))
                          NIL))
                        NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|count_E_TCC1| "" (SUBTYPE-TCC) NIL NIL)
   (|count_E| "" (AUTO-REWRITE "finite_below" "norm_assoc")
    (("" (SKOSIMP)
      (("" (REWRITE "count_status")
        ((""
          (CASE-REPLACE "card({q_2242: node |
                              (member(q_2242, remove(G!1, caucus!1)) AND
                                (OMH(q_2242, j!1, R(send(1 + j!1, t!1, G!1, q_2
 242)),
                                      remove(G!1, caucus!1))
                                     (p!1)
                                  = E
                                  AND omit(q_2242)))})
                  = aoo(remove(G!1,caucus!1), G!1, j!1, t!1, p!1)" :HIDE?
           T)
          (("1"
            (CASE-REPLACE "card({q_2242: node |
                                  (member(q_2242, remove(G!1, caucus!1)) AND
                                    (OMH(q_2242, j!1, R(send(1 + j!1, t!1, G!1,
  q_2242)),
                                          remove(G!1, caucus!1))
                                         (p!1)
                                      = E
                                      AND man(q_2242)))})
                      = am(remove(G!1,caucus!1))" :HIDE? T)
            (("1" (ASSERT) NIL NIL)
             ("2" (HIDE 2)
              (("2" (EXPAND "am")
                (("2" (REWRITE "equal_card")
                  (("2" (APPLY-EXTENSIONALITY :HIDE? T)
                    (("2" (LAZY-GRIND) NIL NIL)) NIL))
                  NIL))
                NIL))
              NIL))
            NIL)
           ("2" (EXPAND "aoo")
            (("2" (REWRITE "equal_card")
              (("2" (APPLY-EXTENSIONALITY :HIDE? T)
                (("2" (GRIND) NIL NIL)) NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|validity| "" (AUTO-REWRITE "finite_below" "norm_assoc")
    (("" (INDUCT "r")
      (("1" (SKOSIMP)
        (("1" (USE "validity1") (("1" (GRIND) NIL NIL)) NIL)) NIL)
       ("2" (SKOSIMP*)
        (("2" (EXPAND "OMH" +)
          (("2" (LIFT-IF)
            (("2" (GROUND)
              (("1" (USE "send_self_ax") (("1" (ASSERT) NIL NIL)) NIL)
               ("2" (LEMMA "hybrid_maj_ax")
                (("2" (INST?)
                  (("2" (INST - "lambda t: val(G!1,t!1,UnR(t))")
                    (("2" (ASSERT)
                      (("2" (HIDE 3)
                        (("2" (GROUND)
                          (("1" (SKOSIMP)
                            (("1" (EXPAND "val")
                              (("1" (LIFT-IF)
                                (("1"
                                  (GROUND)
                                  (("1"
                                    (FORWARD-CHAIN "UnR_inv")
                                    (("1"
                                      (REPLACE -1 :HIDE? T)
                                      (("1"
                                        (USE "R_E_prop")
                                        (("1" (ASSERT) NIL NIL))
                                        NIL))
                                      NIL))
                                    NIL)
                                   ("2"
                                    (FORWARD-CHAIN "UnR_inv")
                                    (("2"
                                      (REPLACE -1 :HIDE? T)
                                      (("2"
                                        (USE "R_E_prop")
                                        (("2" (ASSERT) NIL NIL))
                                        NIL))
                                      NIL))
                                    NIL)
                                   ("3"
                                    (FORWARD-CHAIN "UnR_inv")
                                    (("3"
                                      (REPLACE -1 :HIDE? T)
                                      (("3"
                                        (USE "R_E_prop")
                                        (("3" (ASSERT) NIL NIL))
                                        NIL))
                                      NIL))
                                    NIL)
                                   ("4"
                                    (FORWARD-CHAIN "UnR_inv")
                                    (("4"
                                      (REPLACE -1 :HIDE? T)
                                      (("4"
                                        (ASSERT)
                                        (("4"
                                          (USE "R_E_prop")
                                          (("4" (ASSERT) NIL NIL))
                                          NIL))
                                        NIL))
                                      NIL))
                                    NIL)
                                   ("5"
                                    (FORWARD-CHAIN "UnR_inv")
                                    (("5"
                                      (REPLACE -1 :HIDE? T)
                                      (("5"
                                        (USE "R_E_prop")
                                        (("5" (ASSERT) NIL NIL))
                                        NIL))
                                      NIL))
                                    NIL)
                                   ("6" (GRIND) NIL NIL))
                                  NIL))
                                NIL))
                              NIL))
                            NIL)
                           ("2" (SKOSIMP)
                            (("2" (HIDE -7 -11)
                              (("2" (EXPAND "val")
                                (("2"
                                  (LIFT-IF)
                                  (("2"
                                    (GROUND)
                                    (("1"
                                      (FORWARD-CHAIN "UnR_inv")
                                      (("1"
                                        (FORWARD-CHAIN "UnR_inv")
                                        (("1" (ASSERT) NIL NIL))
                                        NIL))
                                      NIL)
                                     ("2"
                                      (FORWARD-CHAIN "UnR_inv")
                                      NIL
                                      NIL)
                                     ("3"
                                      (FORWARD-CHAIN "UnR_inv")
                                      (("3"
                                        (FORWARD-CHAIN "UnR_inv")
                                        (("3" (ASSERT) NIL NIL))
                                        NIL))
                                      NIL)
                                     ("4"
                                      (FORWARD-CHAIN "UnR_inv")
                                      NIL
                                      NIL)
                                     ("5"
                                      (FORWARD-CHAIN "UnR_inv")
                                      (("5"
                                        (FORWARD-CHAIN "UnR_inv")
                                        NIL
                                        NIL))
                                      NIL)
                                     ("6"
                                      (FORWARD-CHAIN "UnR_inv")
                                      NIL
                                      NIL)
                                     ("7"
                                      (FORWARD-CHAIN "UnR_inv")
                                      (("7"
                                        (FORWARD-CHAIN "UnR_inv")
                                        (("7" (ASSERT) NIL NIL))
                                        NIL))
                                      NIL)
                                     ("8" (GRIND) NIL NIL))
                                    NIL))
                                  NIL))
                                NIL))
                              NIL))
                            NIL)
                           ("3"
                            (INST +
                             "{q| let t=send(1+jf!1,t!1,G!1,q) in member(q,remo
 ve(G!1,caucus!1)) and val(G!1, t!1,t)
                                                                               
                                                                               
                                                                               
                                            and OMH(q, jf!1,R(t),remove(G!1,cau
 cus!1))(p!1)=R(t)}"
                             _)
                            (("3"
                              (INST + "{q| member(q,remove(G!1,caucus!1))
                                                                               
                                                                               
          and OMH(q, jf!1,R(send(1+jf!1,t!1,G!1,q)),remove(G!1,caucus!1))(p!1)=
 E}")
                              (("3" (GROUND)
                                (("1"
                                  (HIDE -3 -7)
                                  (("1" (GRIND) NIL NIL))
                                  NIL)
                                 ("2"
                                  (HIDE -3 -7)
                                  (("2"
                                    (GRIND :EXCLUDE ("OMH"))
                                    NIL
                                    NIL))
                                  NIL)
                                 ("3"
                                  (SKOSIMP)
                                  (("3"
                                    (EXPAND "member")
                                    (("3"
                                      (FLATTEN)
                                      (("3"
                                        (REPLACE -3)
                                        (("3" (REWRITE "R_ax") NIL NIL))
                                        NIL))
                                      NIL))
                                    NIL))
                                  NIL)
                                 ("4"
                                  (SKOSIMP)
                                  (("4"
                                    (EXPAND "member")
                                    (("4" (GROUND) NIL NIL))
                                    NIL))
                                  NIL)
                                 ("5"
                                  (LEMMA "count_t_new")
                                  (("5"
                                    (ASSERT)
                                    (("5"
                                      (INST?)
                                      (("5"
                                        (LEMMA "count_E")
                                        (("5"
                                          (INST?)
                                          (("5"
                                            (GROUND)
                                            (("1"
                                              (CASE-REPLACE
                                               "let x=remove(G!1,caucus!1) in a
 km(x)=card(x)-aa(x)-as(x)-am(x)")
                                              (("1"
                                                (BETA *)
                                                (("1"
                                                  (REPLACE -1 :HIDE? T)
                                                  (("1"
                                                    (CASE
                                                     "2*(card(remove(G!1, caucu
 s!1)) - aa(remove(G!1, caucus!1)) -
          as(remove(G!1, caucus!1))
          - am(remove(G!1, caucus!1))
          - als(caucus!1, G!1, 1 + jf!1, t!1)
          - aoo(remove(G!1, caucus!1), G!1, jf!1, t!1, p!1))>
         card(remove(G!1, caucus!1)) -
         am(remove(G!1, caucus!1)) -
          aoo(remove(G!1, caucus!1), G!1, jf!1, t!1, p!1)")
                                                    (("1"
                                                      (ASSERT)
                                                      NIL
                                                      NIL)
                                                     ("2"
                                                      (ASSERT)
                                                      (("2"
                                                        (HIDE -1 -2 2)
                                                        (("2"
                                                          (CASE
                                                           "aoo(remove(G!1, cau
 cus!1), G!1, jf!1, t!1, p!1)<=
  ao(remove(G!1, caucus!1))")
                                                          (("1"
                                                            (ASSERT)
                                                            (("1"
                                                              (REWRITE
                                                               "c_prop")
                                                              (("1"
                                                                (USE
                                                                 "als_ax")
                                                                (("1"
                                                                  (USE
                                                                   "am_prop")
                                                                  (("1"
                                                                    (USE
                                                                     "ao_prop")
                                                                    (("1"
                                                                      (USE
                                                                       "aa_prop
 ")
                                                                      (("1"
                                                                        (USE
                                                                         "as_pr
 op")
                                                                        (("1"
                                                                          (PROP
 )
                                                                          (("1"
                                                                            (AS
 SERT
                                                                             :F
 LUSH?
                                                                             T)
                                                                            NIL
                                                                            NIL
 )
                                                                           ("2"
                                                                            (AS
 SERT)
                                                                            NIL
                                                                            NIL
 ))
                                                                          NIL))
                                                                        NIL))
                                                                      NIL))
                                                                    NIL))
                                                                  NIL))
                                                                NIL))
                                                              NIL))
                                                            NIL)
                                                           ("2"
                                                            (HIDE 2)
                                                            (("2"
                                                              (EXPAND
                                                               "aoo")
                                                              (("2"
                                                                (EXPAND
                                                                 "ao")
                                                                (("2"
                                                                  (REWRITE
                                                                   "card_subset
 ")
                                                                  (("2"
                                                                    (HIDE
                                                                     -3
                                                                     -7
                                                                     2)
                                                                    (("2"
                                                                      (GRIND)
                                                                      NIL
                                                                      NIL))
                                                                    NIL))
                                                                  NIL))
                                                                NIL))
                                                              NIL))
                                                            NIL))
                                                          NIL))
                                                        NIL))
                                                      NIL))
                                                    NIL))
                                                  NIL))
                                                NIL)
                                               ("2"
                                                (HIDE -1 -2 -5 -9 2)
                                                (("2"
                                                  (BETA *)
                                                  (("2"
                                                    (USE
                                                     "count_status_alt")
                                                    (("2"
                                                      (EXPAND*
                                                       "akm"
                                                       "aa"
                                                       "as"
                                                       "am"
                                                       "ao")
                                                      (("2"
                                                        (EXPAND "member")
                                                        (("2"
                                                          (ASSERT)
                                                          NIL
                                                          NIL))
                                                        NIL))
                                                      NIL))
                                                    NIL))
                                                  NIL))
                                                NIL))
                                              NIL)
                                             ("2"
                                              (HIDE 2)
                                              (("2"
                                                (SKOSIMP)
                                                (("2"
                                                  (INST?)
                                                  (("2"
                                                    (GROUND)
                                                    (("1"
                                                      (GRIND)
                                                      NIL
                                                      NIL)
                                                     ("2"
                                                      (GRIND)
                                                      NIL
                                                      NIL)
                                                     ("3"
                                                      (USE "aa_prop")
                                                      (("3"
                                                        (USE "am_prop")
                                                        (("3"
                                                          (USE "ao_prop")
                                                          (("3"
                                                            (USE
                                                             "as_prop")
                                                            (("3"
                                                              (REWRITE
                                                               "c_prop")
                                                              (("3"
                                                                (ASSERT
                                                                 :FLUSH?
                                                                 T)
                                                                NIL
                                                                NIL))
                                                              NIL))
                                                            NIL))
                                                          NIL))
                                                        NIL))
                                                      NIL))
                                                    NIL))
                                                  NIL))
                                                NIL))
                                              NIL)
                                             ("3"
                                              (HIDE -1 2)
                                              (("3"
                                                (SKOSIMP)
                                                (("3"
                                                  (INST?)
                                                  (("3"
                                                    (GROUND)
                                                    (("1"
                                                      (HIDE -9)
                                                      (("1"
                                                        (GRIND)
                                                        NIL
                                                        NIL))
                                                      NIL)
                                                     ("2"
                                                      (HIDE -9)
                                                      (("2"
                                                        (GRIND)
                                                        NIL
                                                        NIL))
                                                      NIL)
                                                     ("3"
                                                      (HIDE -8)
                                                      (("3"
                                                        (GRIND)
                                                        NIL
                                                        NIL))
                                                      NIL)
                                                     ("4"
                                                      (USE "as_prop")
                                                      (("4"
                                                        (USE "aa_prop")
                                                        (("4"
                                                          (USE "ao_prop")
                                                          (("4"
                                                            (USE
                                                             "am_prop")
                                                            (("4"
                                                              (REWRITE
                                                               "c_prop")
                                                              (("4"
                                                                (ASSERT
                                                                 :FLUSH?
                                                                 T)
                                                                NIL
                                                                NIL))
                                                              NIL))
                                                            NIL))
                                                          NIL))
                                                        NIL))
                                                      NIL))
                                                    NIL))
                                                  NIL))
                                                NIL))
                                              NIL)
                                             ("4"
                                              (HIDE 1 3)
                                              (("4"
                                                (SKOSIMP)
                                                (("4"
                                                  (INST?)
                                                  (("4"
                                                    (GROUND)
                                                    (("1"
                                                      (HIDE -9)
                                                      (("1"
                                                        (GRIND)
                                                        NIL
                                                        NIL))
                                                      NIL)
                                                     ("2"
                                                      (HIDE -9)
                                                      (("2"
                                                        (GRIND)
                                                        NIL
                                                        NIL))
                                                      NIL)
                                                     ("3"
                                                      (HIDE -8)
                                                      (("3"
                                                        (GRIND)
                                                        NIL
                                                        NIL))
                                                      NIL)
                                                     ("4"
                                                      (USE "am_prop")
                                                      (("4"
                                                        (USE "aa_prop")
                                                        (("4"
                                                          (USE "as_prop")
                                                          (("4"
                                                            (USE
                                                             "ao_prop")
                                                            (("4"
                                                              (REWRITE
                                                               "c_prop")
                                                              (("4"
                                                                (ASSERT
                                                                 :FLUSH?
                                                                 T)
                                                                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)
   (|agreement| "" (INDUCT "r")
    (("1" (SKOSIMP*)
      (("1" (LEMMA "validity0")
        (("1" (INST? :IF-MATCH ALL) (("1" (GROUND) NIL NIL)) NIL)) NIL))
      NIL)
     ("2" (SKOSIMP*)
      (("2" (CASE "arb(G!1) or omit(G!1)")
        (("1" (GROUND)
          (("1" (EXPAND "OMH" +)
            (("1" (LIFT-IF)
              (("1" (LIFT-IF)
                (("1" (GROUND)
                  (("1" (GRIND) NIL NIL) ("2" (GRIND) NIL NIL)
                   ("3" (LEMMA "maj_ext")
                    (("3" (INST? -1 :IF-MATCH ALL)
                      (("3" (INST? -1 :IF-MATCH ALL)
                        (("3" (GROUND)
                          (("3" (HIDE -1 3)
                            (("3" (SKOSIMP)
                              (("3" (INST?)
                                (("3"
                                  (GROUND)
                                  (("1" (GRIND) NIL NIL)
                                   ("2" (GRIND) NIL NIL)
                                   ("3"
                                    (HIDE 2)
                                    (("3"
                                      (REWRITE "c_prop")
                                      (("3"
                                        (USE "am_prop")
                                        (("3"
                                          (USE "ao_prop")
                                          (("3"
                                            (USE "aa_prop")
                                            (("3"
                                              (USE "as_prop")
                                              (("3"
                                                (ASSERT :FLUSH? T)
                                                NIL
                                                NIL))
                                              NIL))
                                            NIL))
                                          NIL))
                                        NIL))
                                      NIL))
                                    NIL)
                                   ("4"
                                    (HIDE 2)
                                    (("4"
                                      (CASE-REPLACE
                                       "aa(remove(G!1, caucus!1))=aa(caucus!1)-
 1")
                                      (("1"
                                        (USE "ao_prop")
                                        (("1"
                                          (ASSERT :FLUSH? T)
                                          NIL
                                          NIL))
                                        NIL)
                                       ("2"
                                        (HIDE -8 -9 2)
                                        (("2"
                                          (EXPAND "aa")
                                          (("2"
                                            (EXPAND "member")
                                            (("2"
                                              (CASE-REPLACE
                                               "{q | remove(G!1, caucus!1)(q) A
 ND arb(q)}=remove(G!1,{q | caucus!1(q) AND arb(q)})"
                                               :HIDE?
                                               T)
                                              (("1"
                                                (LEMMA
                                                 "card_remove[node]")
                                                (("1"
                                                  (AUTO-REWRITE
                                                   "finite_below")
                                                  (("1"
                                                    (INST? :IF-MATCH ALL)
                                                    (("1"
                                                      (REPLACE -7)
                                                      (("1"
                                                        (GRIND)
                                                        NIL
                                                        NIL))
                                                      NIL))
                                                    NIL))
                                                  NIL))
                                                NIL)
                                               ("2"
                                                (APPLY-EXTENSIONALITY
                                                 :HIDE?
                                                 T)
                                                (("2"
                                                  (HIDE -7 2)
                                                  (("2"
                                                    (EXPAND "remove")
                                                    (("2"
                                                      (EXPAND "member")
                                                      (("2"
                                                        (BDDSIMP)
                                                        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" (EXPAND "OMH" +)
            (("2" (LIFT-IF)
              (("2" (LIFT-IF)
                (("2" (GROUND)
                  (("1" (GRIND) NIL NIL) ("2" (GRIND) NIL NIL)
                   ("3" (LEMMA "maj_ext")
                    (("3" (INST? :IF-MATCH ALL)
                      (("3" (INST? :IF-MATCH ALL)
                        (("3" (GROUND)
                          (("3" (HIDE -1 3)
                            (("3" (SKOSIMP)
                              (("3" (INST?)
                                (("3"
                                  (GROUND)
                                  (("1" (GRIND) NIL NIL)
                                   ("2" (GRIND) NIL NIL)
                                   ("3"
                                    (HIDE 2)
                                    (("3"
                                      (REWRITE "c_prop")
                                      (("3"
                                        (USE "am_prop")
                                        (("3"
                                          (USE "ao_prop")
                                          (("3"
                                            (USE "aa_prop")
                                            (("3"
                                              (USE "as_prop")
                                              (("3"
                                                (ASSERT :FLUSH? T)
                                                NIL
                                                NIL))
                                              NIL))
                                            NIL))
                                          NIL))
                                        NIL))
                                      NIL))
                                    NIL)
                                   ("4"
                                    (HIDE 2)
                                    (("4"
                                      (CASE-REPLACE
                                       "ao(remove(G!1, caucus!1))=ao(caucus!1)-
 1")
                                      (("1"
                                        (USE "aa_prop")
                                        (("1" (ASSERT) NIL NIL))
                                        NIL)
                                       ("2"
                                        (HIDE -8 -9 2)
                                        (("2"
                                          (EXPAND "ao")
                                          (("2"
                                            (EXPAND "member")
                                            (("2"
                                              (CASE-REPLACE
                                               "{q | remove(G!1, caucus!1)(q) A
 ND omit(q)}=remove(G!1,{q | caucus!1(q) AND omit(q)})"
                                               :HIDE?
                                               T)
                                              (("1"
                                                (LEMMA
                                                 "card_remove[node]")
                                                (("1"
                                                  (AUTO-REWRITE
                                                   "finite_below")
                                                  (("1"
                                                    (INST? :IF-MATCH ALL)
                                                    (("1"
                                                      (REPLACE -7)
                                                      (("1"
                                                        (GRIND)
                                                        NIL
                                                        NIL))
                                                      NIL))
                                                    NIL))
                                                  NIL))
                                                NIL)
                                               ("2"
                                                (APPLY-EXTENSIONALITY
                                                 :HIDE?
                                                 T)
                                                (("2" (GRIND) NIL NIL))
                                                NIL))
                                              NIL))
                                            NIL))
                                          NIL))
                                        NIL))
                                      NIL))
                                    NIL))
                                  NIL))
                                NIL))
                              NIL))
                            NIL))
                          NIL))
                        NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL)
         ("2" (HIDE -1)
          (("2" (LEMMA "validity")
            (("2" (INST? :IF-MATCH ALL)
              (("2" (EXPAND "okm")
                (("2" (GROUND)
                  (("2" (EXPAND "val")
                    (("2" (LIFT-IF)
                      (("2" (GROUND)
                        (("1" (EXPAND "omit") (("1" (PROPAX) NIL NIL))
                          NIL)
                         ("2" (EXPAND "omit") (("2" (PROPAX) NIL NIL))
                          NIL)
                         ("3" (GRIND) NIL NIL))
                        NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  
  
  $$$cardprops.pvs
  cardprops[T: NONEMPTY_TYPE]: THEORY
  BEGIN
  
    A,B,C,D: VAR finite_set[T]
  
    IMPORTING finite_sets@finite_sets_below,
    finite_sets@finite_sets_pred
  
    r,s,t: VAR bool
  
    norm_assocl: SUBLEMMA (r AND (s AND t)) = ((r AND s) AND t)
    norm_assocr: SUBLEMMA ((r AND s) AND t) = (r AND (s AND t))
    norm_assoclo: SUBLEMMA (r OR (s OR t)) = ((r OR s) OR t)
    norm_assocro: SUBLEMMA ((r OR s) OR t) = (r OR (s OR t))
  
    norm_assoc: SUBLEMMA true % ((r AND s) AND t) = (r AND (s AND t))
  
    union_diff: SUBLEMMA A = union({q:T|A(q) AND B(q)}, {q:T|A(q) AND NOT B(q)}
 )
  
    intersect_empty: SUBLEMMA  intersection(A,B)=emptyset => card(intersection(
 A,B))=0
  
    card_prop: SUBLEMMA card({q:T|A(q) AND B(q)}) = card({q:T|A(q)}) -   card({
 q:T|A(q) AND NOT B(q)})
    card_prop2: SUBLEMMA card({q:T|A(q) AND NOT B(q)}) = card({q:T|A(q)}) - car
 d({q:T|A(q) AND B(q)})
  
    equal_card: SUBLEMMA A=B => card(A)=card(B)
    equal_card_minus: SUBLEMMA A=B => -1*card(A)=-1*card(B)
    equal_card_diff: SUBLEMMA A=B and D=C => card(A)-card(C)=card(B)-card(D)
  
    n: var nat
    similar_card: SUBLEMMA A=B => card(A)<=n => card(B)<=n
  
    supset?(A, B): bool = subset?(B,A)
  
    card_supset     : THEOREM supset?(A,B) IMPLIES card(A) >= card(B)
  
    union_or: SUBLEMMA {q:T| A(q) and (B(q) or C(q)) and D(q)} =
        union({q:T|A(q) AND B(q) and D(q)},{q:T|A(q) AND C(q) and D(q)})
  
  END cardprops
  
  $$$cardprops.prf
  (|cardprops| (|norm_assocl| "" (GRIND) NIL NIL)
   (|norm_assocr| "" (ASSERT) (("" (GRIND) NIL NIL)) NIL)
   (|norm_assoclo| "" (GRIND) NIL NIL)
   (|norm_assocro| "" (GRIND) NIL NIL) (|norm_assoc| "" (GRIND) NIL NIL)
   (|union_diff| "" (SKOSIMP)
    (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (GRIND) NIL NIL)) NIL))
    NIL)
   (|intersect_empty| "" (SKOSIMP)
    (("" (REPLACE -1) (("" (REWRITE "card_emptyset") NIL NIL)) NIL)) NIL)
   (|card_prop_TCC1| "" (SKOSIMP)
    (("" (LEMMA "finite_intersection2[T]")
      (("" (INST - "A!1" "B!1") (("" (GRIND) NIL NIL)) NIL)) NIL))
    NIL)
   (|card_prop_TCC2| "" (SUBTYPE-TCC) NIL NIL)
   (|card_prop_TCC3| "" (SKOSIMP)
    (("" (LEMMA "finite_intersection2[T]")
      (("" (INST - "A!1" "{q:T | not B!1(q)}") (("" (GRIND) NIL NIL))
        NIL))
      NIL))
    NIL)
   (|card_prop| "" (SKOSIMP)
    (("" (LEMMA "card_union[T]")
      ((""
        (INST - "{q:T | A!1(q) AND B!1(q)}"
         "{q:T | A!1(q) AND not B!1(q)}")
        (("1"
          (CASE "empty?(intersection({q:T | A!1(q) AND B!1(q)},
                                                {q:T | A!1(q) AND NOT B!1(q)}))
 ")
          (("1" (REWRITE "empty_card")
            (("1" (REPLACE -1 :HIDE? T)
              (("1"
                (CASE-REPLACE
                 "union({q:T | A!1(q) AND B!1(q)}, {q:T | A!1(q) AND NOT B!1(q)
 })=
                    {q:T | A!1(q)}")
                (("1" (ASSERT) NIL NIL)
                 ("2" (APPLY-EXTENSIONALITY :HIDE? T)
                  (("2" (GRIND) NIL NIL)) NIL))
                NIL))
              NIL)
             ("2" (HIDE -1 -2 2)
              (("2" (LEMMA "finite_intersection2[T]")
                (("2" (INST?)
                  (("2" (LEMMA "finite_intersection2[T]")
                    (("2" (INST - "A!1" "B!1") (("2" (GRIND) NIL NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL)
           ("2" (HIDE -1 -2 2) (("2" (GRIND) NIL NIL)) NIL))
          NIL)
         ("2" (HIDE 2)
          (("2" (LEMMA "finite_intersection2[T]")
            (("2" (INST - "A!1" "{q:T | not B!1(q)}")
              (("2" (GRIND) NIL NIL)) NIL))
            NIL))
          NIL)
         ("3" (HIDE 2)
          (("3" (LEMMA "finite_intersection2[T]")
            (("3" (INST?)
              (("3" (INST - "B!1") (("3" (GRIND) NIL NIL)) NIL)) NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|card_prop2| "" (SKOSIMP)
    (("" (USE "card_prop") (("" (ASSERT) NIL NIL)) NIL)) NIL)
   (|equal_card| "" (GRIND) NIL NIL)
   (|equal_card_minus| "" (GRIND) NIL NIL)
   (|equal_card_diff| "" (GRIND) NIL NIL)
   (|similar_card| "" (SKOSIMP) (("" (GROUND) NIL NIL)) NIL)
   (|card_supset| "" (SKOSIMP)
    (("" (LEMMA "card_subset[T]")
      (("" (INST - "B!1" "A!1")
        (("" (GROUND) (("" (GRIND) NIL NIL)) NIL)) NIL))
      NIL))
    NIL)
   (|union_or| "" (SKOSIMP)
    (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (GRIND) NIL NIL)) NIL))
    NIL))

How-To-Repeat: 

Fix: 
A while back the prettyprinter was modified to use Lamport-style
formatting for conjunctions and disjunctions when there are more than
three subterms.  This works fine, but then cut-and-paste doesn't respect
the parens, so doesn't match.  It was decided that it would be better to
add associativity to tc-eq for conjunction and disjunction rather than
back this out, as it would also simplify certain proofs, and is cheap to
do (unlike commutativity, which would be quite expensive).  match had to
be changed as well.  If (more probably when) I add classes for sums and
products I'll add tc-eq methods for them as well.  This is less important,
since the decision procedures will get these.

With this change, the rewrite is effectively rewriting the term to an
equal term.

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