(NAME_PREFIX Examples.esc3.valid)
(BG_PUSH
(AND
(< 1000000 |INTEGER.LAST|)
(< |INTEGER.FIRST| -1000000)
(DISTINCT |Test54.T.TYPECODE| |Test54.U.TYPECODE| |Test54.V.TYPECODE| |MUTEX.TYPECODE| |TEXT.TYPECODE| |REFANY.TYPECODE| |ROOT.TYPECODE| |NULL.TYPECODE|)
(DISTINCT RETURN EXIT)
(EQ |BOOLEAN.FALSE| |@false|)
(EQ |BOOLEAN.TRUE| |@true|)
(EQ (SUBSET VIRGIN VIRGIN) |@true|)
(EQ (SUBSET ALLOCATED ALLOCATED) |@true|)
(FORALL (v dum) (IMPLIES (EQ (|Is$INTEGER| v dum) |@true|) (AND (>= v |INTEGER.FIRST|) (<= v |INTEGER.LAST|))))
(EQ (SUBTYPE1 |ROOT.TYPECODE| |REFANY.TYPECODE|) |@true|)
(EQ (SUBTYPE1 |MUTEX.TYPECODE| |ROOT.TYPECODE|) |@true|)
(< |INTEGER.FIRST| 0)
(> |INTEGER.LAST| 0)
(NOT (EQ (MEMBER |$NIL| LL) |@true|))
(EQ (|Is$VDCL| |$NIL| VIRGIN) |@true|)
(EQ (|Is$DCL| |$NIL| ALLOCATED) |@true|)
(NEQ |@true| |@false|)
(EQ (|Is$VIRGIN_TYPE| VIRGIN |@DUMMY|) |@true|)
(FORALL (q dummy1) (IMPLIES (EQ (|Is$VIRGIN_TYPE| q dummy1) |@true|) (FORALL (i) (EQ (|Is$BOOLEAN| (select q i |@SPECIAL|) dummy1) |@true|))))
(FORALL (map) (PATS (|Is$VIRGIN_TYPE| map |@DUMMY|)) (IMPLIES (EQ (|Is$VIRGIN_TYPE| map |@DUMMY|) |@true|) (FORALL (ind val) (PATS (store map ind val)) (IMPLIES (EQ (|Is$BOOLEAN| val |@DUMMY|) |@true|) (EQ (|Is$VIRGIN_TYPE| (store map ind val) |@DUMMY|) |@true|)))))
(FORALL (|q$1| dummy) (IMPLIES (EQ (|Is$BOOLEAN| |q$1| dummy) |@true|) (AND (<= 0 (ORD |q$1|)) (< (ORD |q$1|) 2) (EQ (TYPECODE |q$1| |@DUMMY|) |BOOLEAN.TYPECODE|) (OR (EQ |q$1| |BOOLEAN.FALSE|) (EQ |q$1| |BOOLEAN.TRUE|)))))
(FORALL (|q$2| |dummy$1|) (IMPLIES (EQ (|Is$BOOLEAN| |q$2| |dummy$1|) |@true|) (EQ (|Is$ORDINAL| |q$2| |@DUMMY|) |@true|)))
(FORALL (|q$3| |dummy$2|) (IMPLIES (EQ (|Is$CHAR| |q$3| |dummy$2|) |@true|) (AND (<= 0 (ORD |q$3|)) (< (ORD |q$3|) 256) (EQ (TYPECODE |q$3| |@DUMMY|) |CHAR.TYPECODE|))))
(FORALL (|q$4| |dummy$3|) (IMPLIES (EQ (|Is$CHAR| |q$4| |dummy$3|) |@true|) (EQ (|Is$ORDINAL| |q$4| |@DUMMY|) |@true|)))
(EQ (SUBTYPE |NULL.TYPECODE| |TEXT.TYPECODE|) |@true|)
(FORALL (|q$5|) (PATS (|Is$TEXT| |q$5| |@DUMMY|)) (IMPLIES (EQ (|Is$TEXT| |q$5| |@DUMMY|) |@true|) (EQ (SUBTYPE (TYPECODE |q$5| |@DUMMY|) |TEXT.TYPECODE|) |@true|)))
(FORALL (|q$6|) (PATS (SUBTYPE (TYPECODE |q$6| |@DUMMY|) |TEXT.TYPECODE|)) (IMPLIES (EQ (SUBTYPE (TYPECODE |q$6| |@DUMMY|) |TEXT.TYPECODE|) |@true|) (EQ (|Is$TEXT| |q$6| |@DUMMY|) |@true|)))
(FORALL (|q$7|) (PATS (|Is$CARDINAL| |q$7| |@DUMMY|)) (IMPLIES (EQ (|Is$CARDINAL| |q$7| |@DUMMY|) |@true|) (AND (<= 0 |q$7|) (<= |q$7| |INTEGER.LAST|) (EQ (|Is$INTEGER| |q$7| |@DUMMY|) |@true|))))
(FORALL (|q$8|) (PATS (|Is$MATHINT| |q$8| |@DUMMY|)) (IMPLIES (AND (<= 0 |q$8|) (<= |q$8| |INTEGER.LAST|) (EQ (|Is$MATHINT| |q$8| |@DUMMY|) |@true|)) (EQ (|Is$CARDINAL| |q$8| |@DUMMY|) |@true|)))
(FORALL (|q$9|) (PATS (|Is$CARDINAL| |q$9| |@DUMMY|)) (IMPLIES (EQ (|Is$CARDINAL| |q$9| |@DUMMY|) |@true|) (EQ (|Is$ORDINAL| |q$9| |@DUMMY|) |@true|)))
(EQ (SUBTYPE |NULL.TYPECODE| |MUTEX.TYPECODE|) |@true|)
(FORALL (|q$10|) (PATS (|Is$MUTEX| |q$10| |@DUMMY|)) (IMPLIES (EQ (|Is$MUTEX| |q$10| |@DUMMY|) |@true|) (EQ (SUBTYPE (TYPECODE |q$10| |@DUMMY|) |MUTEX.TYPECODE|) |@true|)))
(FORALL (|q$11|) (PATS (SUBTYPE (TYPECODE |q$11| |@DUMMY|) |MUTEX.TYPECODE|)) (IMPLIES (EQ (SUBTYPE (TYPECODE |q$11| |@DUMMY|) |MUTEX.TYPECODE|) |@true|) (EQ (|Is$MUTEX| |q$11| |@DUMMY|) |@true|)))
(FORALL (|q$12|) (PATS (|Is$MUTEX| |q$12| |@DUMMY|)) (IMPLIES (EQ (|Is$MUTEX| |q$12| |@DUMMY|) |@true|) (EQ (|Is$ROOT| |q$12| |@DUMMY|) |@true|)))
(EQ (SUBTYPE |NULL.TYPECODE| |REFANY.TYPECODE|) |@true|)
(FORALL (|q$13|) (PATS (|Is$REFANY| |q$13| |@DUMMY|)) (IMPLIES (EQ (|Is$REFANY| |q$13| |@DUMMY|) |@true|) (EQ (SUBTYPE (TYPECODE |q$13| |@DUMMY|) |REFANY.TYPECODE|) |@true|)))
(FORALL (|q$14|) (PATS (SUBTYPE (TYPECODE |q$14| |@DUMMY|) |REFANY.TYPECODE|)) (IMPLIES (EQ (SUBTYPE (TYPECODE |q$14| |@DUMMY|) |REFANY.TYPECODE|) |@true|) (EQ (|Is$REFANY| |q$14| |@DUMMY|) |@true|)))
(FORALL (|RESIDUE.Text.Value'| |RESIDUE.Text.Value| |i$1|) (PATS (MPAT (select (|FUNC.Text.Value| |RESIDUE.Text.Value|) |i$1| |@ARRAY|) (select (|FUNC.Text.Value| |RESIDUE.Text.Value'|) |i$1| |@ARRAY|))) (IMPLIES (AND (EQ (|Is$TEXT| |i$1| |@DUMMY|) |@true|) (EQ (select |RESIDUE.Text.Value| |i$1| |@ARRAY|) (select |RESIDUE.Text.Value'| |i$1| |@ARRAY|))) (EQ (select (|FUNC.Text.Value| |RESIDUE.Text.Value|) |i$1| |@ARRAY|) (select (|FUNC.Text.Value| |RESIDUE.Text.Value'|) |i$1| |@ARRAY|))))
(EQ (SUBTYPE |NULL.TYPECODE| |Test54.V.TYPECODE|) |@true|)
(FORALL (|q$15|) (PATS (|Is$Test54.V| |q$15| |@DUMMY|)) (IMPLIES (EQ (|Is$Test54.V| |q$15| |@DUMMY|) |@true|) (EQ (SUBTYPE (TYPECODE |q$15| |@DUMMY|) |Test54.V.TYPECODE|) |@true|)))
(FORALL (|q$16|) (PATS (SUBTYPE (TYPECODE |q$16| |@DUMMY|) |Test54.V.TYPECODE|)) (IMPLIES (EQ (SUBTYPE (TYPECODE |q$16| |@DUMMY|) |Test54.V.TYPECODE|) |@true|) (EQ (|Is$Test54.V| |q$16| |@DUMMY|) |@true|)))
(EQ (|Is$Test54.V.i$MAP| |Test54.V.i| |@DUMMY|) |@true|)
(FORALL (ofm) (IMPLIES (EQ (|Is$Test54.V.i$MAP| ofm |@DUMMY|) |@true|) (FORALL (|q$17|) (EQ (|Is$INTEGER| (select ofm |q$17| |@OBJECT|) |@DUMMY|) |@true|))))
(EQ (SUBTYPE1 |Test54.V.TYPECODE| |ROOT.TYPECODE|) |@true|)
(FORALL (|q$18|) (PATS (|Is$Test54.V| |q$18| |@DUMMY|)) (IMPLIES (EQ (|Is$Test54.V| |q$18| |@DUMMY|) |@true|) (EQ (|Is$ROOT| |q$18| |@DUMMY|) |@true|)))
(FORALL (s) (IMPLIES (NOT (EQ (select ALLOCATED s |@SPECIAL|) |@true|)) (EQ (select |Test54.U.v| s |@OBJECT|) |$NIL|)))
(EQ (SUBTYPE |NULL.TYPECODE| |Test54.U.TYPECODE|) |@true|)
(FORALL (|q$19|) (PATS (|Is$Test54.U| |q$19| |@DUMMY|)) (IMPLIES (EQ (|Is$Test54.U| |q$19| |@DUMMY|) |@true|) (EQ (SUBTYPE (TYPECODE |q$19| |@DUMMY|) |Test54.U.TYPECODE|) |@true|)))
(FORALL (|q$20|) (PATS (SUBTYPE (TYPECODE |q$20| |@DUMMY|) |Test54.U.TYPECODE|)) (IMPLIES (EQ (SUBTYPE (TYPECODE |q$20| |@DUMMY|) |Test54.U.TYPECODE|) |@true|) (EQ (|Is$Test54.U| |q$20| |@DUMMY|) |@true|)))
(EQ (|Is$Test54.U.v$MAP| |Test54.U.v| |@DUMMY|) |@true|)
(FORALL (|ofm$1|) (IMPLIES (EQ (|Is$Test54.U.v$MAP| |ofm$1| |@DUMMY|) |@true|) (FORALL (|q$21|) (EQ (|Is$Test54.V| (select |ofm$1| |q$21| |@OBJECT|) |@DUMMY|) |@true|))))
(FORALL (m |q$22|) (PATS (MPAT (|Is$Test54.U| |q$22| |@DUMMY|) (|Is$Test54.U.v$MAP| m |@DUMMY|))) (IMPLIES (AND (EQ (|Is$Test54.U.v$MAP| m |@DUMMY|) |@true|) (EQ (|Is$Test54.U| |q$22| |@DUMMY|) |@true|)) (FORALL (al) (PATS (MPAT (|Is$DCL| |q$22| al) (select m |q$22| |@OBJECT|))) (IMPLIES (EQ (|Is$DCL| |q$22| al) |@true|) (EQ (|Is$DCL| (select m |q$22| |@OBJECT|) al) |@true|)))))
(FORALL (|m$1|) (PATS (|Is$Test54.U.v$MAP| |m$1| |@DUMMY|)) (IMPLIES (EQ (|Is$Test54.U.v$MAP| |m$1| |@DUMMY|) |@true|) (FORALL (r |VIRGIN$1|) (PATS (select |VIRGIN$1| (select |m$1| r |@OBJECT|) |@SPECIAL|)) (IMPLIES (AND (EQ (|Is$Test54.U| r |@DUMMY|) |@true|) (EQ (|Is$VDCL| r |VIRGIN$1|) |@true|)) (NOT (EQ (select |VIRGIN$1| (select |m$1| r |@OBJECT|) |@SPECIAL|) |@true|))))))
(EQ (SUBTYPE1 |Test54.U.TYPECODE| |ROOT.TYPECODE|) |@true|)
(FORALL (|q$23|) (PATS (|Is$Test54.U| |q$23| |@DUMMY|)) (IMPLIES (EQ (|Is$Test54.U| |q$23| |@DUMMY|) |@true|) (EQ (|Is$ROOT| |q$23| |@DUMMY|) |@true|)))
(EQ (SUBTYPE |NULL.TYPECODE| |Test54.T.TYPECODE|) |@true|)
(FORALL (|q$24|) (PATS (|Is$Test54.T| |q$24| |@DUMMY|)) (IMPLIES (EQ (|Is$Test54.T| |q$24| |@DUMMY|) |@true|) (EQ (SUBTYPE (TYPECODE |q$24| |@DUMMY|) |Test54.T.TYPECODE|) |@true|)))
(FORALL (|q$25|) (PATS (SUBTYPE (TYPECODE |q$25| |@DUMMY|) |Test54.T.TYPECODE|)) (IMPLIES (EQ (SUBTYPE (TYPECODE |q$25| |@DUMMY|) |Test54.T.TYPECODE|) |@true|) (EQ (|Is$Test54.T| |q$25| |@DUMMY|) |@true|)))
(FORALL (|q$26|) (PATS (|Is$Test54.T| |q$26| |@DUMMY|)) (IMPLIES (EQ (|Is$Test54.T| |q$26| |@DUMMY|) |@true|) (EQ (|Is$ROOT| |q$26| |@DUMMY|) |@true|)))
)
)

(IMPLIES
 (NEQ |v$1| |$NIL|)
 (FORALL
     (|Test54.U.v`| |v`| |ALLOCATED`| |LL`| |VIRGIN`|)
   (IMPLIES
    (AND (EQ (|Is$Test54.V| |v$1| |@DUMMY|) |@true|) (EQ (|Is$DCL| |v$1| ALLOCATED) |@true|) (EQ (|Is$VDCL| |v$1| VIRGIN) |@true|))
    (FORALL
	(res)
      (FORALL
	  (|res$1|)
	(IMPLIES
	 (EQ (|Is$Test54.U| (NEW ALLOCATED LL VIRGIN |Test54.U.TYPECODE| |POS$37$11|) |@DUMMY|) |@true|)
	 (FORALL (sss)
	   (IMPLIES
	    (NOT (EQ 
		  (select 
		   (store ALLOCATED
			  (NEW ALLOCATED LL VIRGIN |Test54.U.TYPECODE| |POS$37$11|)
			  |@true|)
		   sss |@SPECIAL|)
		  |@true|))
	    (EQ 
	     (select (store |Test54.U.v| (NEW ALLOCATED LL VIRGIN |Test54.U.TYPECODE| |POS$37$11|) |v$1|) sss |@OBJECT|)
	     |$NIL|)
	    ))))))))
(BG_POP)


;; Exposed a 64-bit dependency.
(BG_PUSH
(AND
(< 1000000 |INTEGER.LAST|)
(< |INTEGER.FIRST| -1000000)
(DISTINCT |TextWriter.T.TYPECODE| |TYPE@39.TYPECODE| |Writer.T.TYPECODE| |Thread.SizedClosure.TYPECODE| |Thread.Closure.TYPECODE| |Thread.Condition.TYPECODE| |Thread.T.TYPECODE| |MUTEX.TYPECODE| |TEXT.TYPECODE| |REFANY.TYPECODE| |ROOT.TYPECODE| |NULL.TYPECODE|)
(DISTINCT |Writer.Failure| |Thread.Alerted| RETURN EXIT)
(FORALL (m1 m2) (NOPATS (|Is$MUTEX| m1 |@DUMMY|) (|Is$MUTEX| m2 |@DUMMY|)) (IMPLIES (AND (EQ (|Is$MUTEX| m2 |@DUMMY|) |@true|) (EQ (|Is$MUTEX| m1 |@DUMMY|) |@true|)) (IMPLIES (AND (NOT (EQ (|Thread.MaxLL| m1) |@true|)) (EQ (|Thread.MaxLL| m2) |@true|) (NEQ m1 |$NIL|) (NEQ m2 |$NIL|)) (EQ (MUT_LT m1 m2) |@true|))))
(EQ |BOOLEAN.FALSE| |@false|)
(EQ |BOOLEAN.TRUE| |@true|)
(EQ (SUBSET VIRGIN VIRGIN) |@true|)
(EQ (SUBSET ALLOCATED ALLOCATED) |@true|)
(FORALL (v dum) (IMPLIES (EQ (|Is$INTEGER| v dum) |@true|) (AND (>= v |INTEGER.FIRST|) (<= v |INTEGER.LAST|))))
(EQ (SUBTYPE1 |ROOT.TYPECODE| |REFANY.TYPECODE|) |@true|)
(EQ (SUBTYPE1 |MUTEX.TYPECODE| |ROOT.TYPECODE|) |@true|)
(< |INTEGER.FIRST| 0)
(> |INTEGER.LAST| 0)
(NOT (EQ (MEMBER |$NIL| LL) |@true|))
(EQ (|Is$VDCL| |$NIL| VIRGIN) |@true|)
(EQ (|Is$DCL| |$NIL| ALLOCATED) |@true|)
(NEQ |@true| |@false|)
(EQ (|Is$VIRGIN_TYPE| VIRGIN |@DUMMY|) |@true|)
(FORALL (q dummy1) (IMPLIES (EQ (|Is$VIRGIN_TYPE| q dummy1) |@true|) (FORALL (i) (EQ (|Is$BOOLEAN| (select q i |@SPECIAL|) dummy1) |@true|))))
(FORALL (map) (PATS (|Is$VIRGIN_TYPE| map |@DUMMY|)) (IMPLIES (EQ (|Is$VIRGIN_TYPE| map |@DUMMY|) |@true|) (FORALL (ind val) (PATS (store map ind val)) (IMPLIES (EQ (|Is$BOOLEAN| val |@DUMMY|) |@true|) (EQ (|Is$VIRGIN_TYPE| (store map ind val) |@DUMMY|) |@true|)))))
(FORALL (|q$1| dummy) (IMPLIES (EQ (|Is$BOOLEAN| |q$1| dummy) |@true|) (AND (<= 0 (ORD |q$1|)) (< (ORD |q$1|) 2) (EQ (TYPECODE |q$1| |@DUMMY|) |BOOLEAN.TYPECODE|) (OR (EQ |q$1| |BOOLEAN.FALSE|) (EQ |q$1| |BOOLEAN.TRUE|)))))
(FORALL (|q$2| |dummy$1|) (IMPLIES (EQ (|Is$BOOLEAN| |q$2| |dummy$1|) |@true|) (EQ (|Is$ORDINAL| |q$2| |@DUMMY|) |@true|)))
(FORALL (|q$3| |dummy$2|) (IMPLIES (EQ (|Is$CHAR| |q$3| |dummy$2|) |@true|) (AND (<= 0 (ORD |q$3|)) (< (ORD |q$3|) 256) (EQ (TYPECODE |q$3| |@DUMMY|) |CHAR.TYPECODE|))))
(FORALL (|q$4| |dummy$3|) (IMPLIES (EQ (|Is$CHAR| |q$4| |dummy$3|) |@true|) (EQ (|Is$ORDINAL| |q$4| |@DUMMY|) |@true|)))
(EQ (SUBTYPE |NULL.TYPECODE| |TEXT.TYPECODE|) |@true|)
(FORALL (|q$5|) (PATS (|Is$TEXT| |q$5| |@DUMMY|)) (IMPLIES (EQ (|Is$TEXT| |q$5| |@DUMMY|) |@true|) (EQ (SUBTYPE (TYPECODE |q$5| |@DUMMY|) |TEXT.TYPECODE|) |@true|)))
(FORALL (|q$6|) (PATS (SUBTYPE (TYPECODE |q$6| |@DUMMY|) |TEXT.TYPECODE|)) (IMPLIES (EQ (SUBTYPE (TYPECODE |q$6| |@DUMMY|) |TEXT.TYPECODE|) |@true|) (EQ (|Is$TEXT| |q$6| |@DUMMY|) |@true|)))
(FORALL (|q$7|) (PATS (|Is$CARDINAL| |q$7| |@DUMMY|)) (IMPLIES (EQ (|Is$CARDINAL| |q$7| |@DUMMY|) |@true|) (AND (<= 0 |q$7|) (<= |q$7| |INTEGER.LAST|) (EQ (|Is$INTEGER| |q$7| |@DUMMY|) |@true|))))
(FORALL (|q$8|) (PATS (|Is$MATHINT| |q$8| |@DUMMY|)) (IMPLIES (AND (<= 0 |q$8|) (<= |q$8| |INTEGER.LAST|) (EQ (|Is$MATHINT| |q$8| |@DUMMY|) |@true|)) (EQ (|Is$CARDINAL| |q$8| |@DUMMY|) |@true|)))
(FORALL (|q$9|) (PATS (|Is$CARDINAL| |q$9| |@DUMMY|)) (IMPLIES (EQ (|Is$CARDINAL| |q$9| |@DUMMY|) |@true|) (EQ (|Is$ORDINAL| |q$9| |@DUMMY|) |@true|)))
(EQ (SUBTYPE |NULL.TYPECODE| |MUTEX.TYPECODE|) |@true|)
(FORALL (|q$10|) (PATS (|Is$MUTEX| |q$10| |@DUMMY|)) (IMPLIES (EQ (|Is$MUTEX| |q$10| |@DUMMY|) |@true|) (EQ (SUBTYPE (TYPECODE |q$10| |@DUMMY|) |MUTEX.TYPECODE|) |@true|)))
(FORALL (|q$11|) (PATS (SUBTYPE (TYPECODE |q$11| |@DUMMY|) |MUTEX.TYPECODE|)) (IMPLIES (EQ (SUBTYPE (TYPECODE |q$11| |@DUMMY|) |MUTEX.TYPECODE|) |@true|) (EQ (|Is$MUTEX| |q$11| |@DUMMY|) |@true|)))
(FORALL (|q$12|) (PATS (|Is$MUTEX| |q$12| |@DUMMY|)) (IMPLIES (EQ (|Is$MUTEX| |q$12| |@DUMMY|) |@true|) (EQ (|Is$ROOT| |q$12| |@DUMMY|) |@true|)))
(EQ (SUBTYPE |NULL.TYPECODE| |REFANY.TYPECODE|) |@true|)
(FORALL (|q$13|) (PATS (|Is$REFANY| |q$13| |@DUMMY|)) (IMPLIES (EQ (|Is$REFANY| |q$13| |@DUMMY|) |@true|) (EQ (SUBTYPE (TYPECODE |q$13| |@DUMMY|) |REFANY.TYPECODE|) |@true|)))
(FORALL (|q$14|) (PATS (SUBTYPE (TYPECODE |q$14| |@DUMMY|) |REFANY.TYPECODE|)) (IMPLIES (EQ (SUBTYPE (TYPECODE |q$14| |@DUMMY|) |REFANY.TYPECODE|) |@true|) (EQ (|Is$REFANY| |q$14| |@DUMMY|) |@true|)))
(FORALL (|RESIDUE.Text.Value'| |RESIDUE.Text.Value| |i$1|) (PATS (MPAT (select (|FUNC.Text.Value| |RESIDUE.Text.Value|) |i$1| |@ARRAY|) (select (|FUNC.Text.Value| |RESIDUE.Text.Value'|) |i$1| |@ARRAY|))) (IMPLIES (AND (EQ (|Is$TEXT| |i$1| |@DUMMY|) |@true|) (EQ (select |RESIDUE.Text.Value| |i$1| |@ARRAY|) (select |RESIDUE.Text.Value'| |i$1| |@ARRAY|))) (EQ (select (|FUNC.Text.Value| |RESIDUE.Text.Value|) |i$1| |@ARRAY|) (select (|FUNC.Text.Value| |RESIDUE.Text.Value'|) |i$1| |@ARRAY|))))
(FORALL (|RESIDUE.Writer.state'| |RESIDUE.Writer.state| |i$2|) (PATS (MPAT (select (|FUNC.Writer.state| |RESIDUE.Writer.state|) |i$2| |@OBJECT|) (select (|FUNC.Writer.state| |RESIDUE.Writer.state'|) |i$2| |@OBJECT|))) (IMPLIES (AND (EQ (|Is$Writer.T| |i$2| |@DUMMY|) |@true|) (EQ (select |RESIDUE.Writer.state| |i$2| |@OBJECT|) (select |RESIDUE.Writer.state'| |i$2| |@OBJECT|))) (EQ (select (|FUNC.Writer.state| |RESIDUE.Writer.state|) |i$2| |@OBJECT|) (select (|FUNC.Writer.state| |RESIDUE.Writer.state'|) |i$2| |@OBJECT|))))
(FORALL (|RESIDUE.Writer.valid'| |RESIDUE.Writer.valid| |i$3|) (PATS (MPAT (select (|FUNC.Writer.valid| |RESIDUE.Writer.valid|) |i$3| |@OBJECT|) (select (|FUNC.Writer.valid| |RESIDUE.Writer.valid'|) |i$3| |@OBJECT|))) (IMPLIES (AND (EQ (|Is$Writer.T| |i$3| |@DUMMY|) |@true|) (EQ (select |RESIDUE.Writer.valid| |i$3| |@OBJECT|) (select |RESIDUE.Writer.valid'| |i$3| |@OBJECT|))) (EQ (select (|FUNC.Writer.valid| |RESIDUE.Writer.valid|) |i$3| |@OBJECT|) (select (|FUNC.Writer.valid| |RESIDUE.Writer.valid'|) |i$3| |@OBJECT|))))
(EQ (SUBTYPE |NULL.TYPECODE| |Thread.T.TYPECODE|) |@true|)
(FORALL (|q$15|) (PATS (|Is$Thread.T| |q$15| |@DUMMY|)) (IMPLIES (EQ (|Is$Thread.T| |q$15| |@DUMMY|) |@true|) (EQ (SUBTYPE (TYPECODE |q$15| |@DUMMY|) |Thread.T.TYPECODE|) |@true|)))
(FORALL (|q$16|) (PATS (SUBTYPE (TYPECODE |q$16| |@DUMMY|) |Thread.T.TYPECODE|)) (IMPLIES (EQ (SUBTYPE (TYPECODE |q$16| |@DUMMY|) |Thread.T.TYPECODE|) |@true|) (EQ (|Is$Thread.T| |q$16| |@DUMMY|) |@true|)))
(FORALL (|q$17|) (PATS (|Is$Thread.T| |q$17| |@DUMMY|)) (IMPLIES (EQ (|Is$Thread.T| |q$17| |@DUMMY|) |@true|) (EQ (|Is$ROOT| |q$17| |@DUMMY|) |@true|)))
(EQ (SUBTYPE |NULL.TYPECODE| |Thread.Condition.TYPECODE|) |@true|)
(FORALL (|q$18|) (PATS (|Is$Thread.Condition| |q$18| |@DUMMY|)) (IMPLIES (EQ (|Is$Thread.Condition| |q$18| |@DUMMY|) |@true|) (EQ (SUBTYPE (TYPECODE |q$18| |@DUMMY|) |Thread.Condition.TYPECODE|) |@true|)))
(FORALL (|q$19|) (PATS (SUBTYPE (TYPECODE |q$19| |@DUMMY|) |Thread.Condition.TYPECODE|)) (IMPLIES (EQ (SUBTYPE (TYPECODE |q$19| |@DUMMY|) |Thread.Condition.TYPECODE|) |@true|) (EQ (|Is$Thread.Condition| |q$19| |@DUMMY|) |@true|)))
(FORALL (|q$20|) (PATS (|Is$Thread.Condition| |q$20| |@DUMMY|)) (IMPLIES (EQ (|Is$Thread.Condition| |q$20| |@DUMMY|) |@true|) (EQ (|Is$ROOT| |q$20| |@DUMMY|) |@true|)))
(EQ (SUBTYPE |NULL.TYPECODE| |Thread.Closure.TYPECODE|) |@true|)
(FORALL (|q$21|) (PATS (|Is$Thread.Closure| |q$21| |@DUMMY|)) (IMPLIES (EQ (|Is$Thread.Closure| |q$21| |@DUMMY|) |@true|) (EQ (SUBTYPE (TYPECODE |q$21| |@DUMMY|) |Thread.Closure.TYPECODE|) |@true|)))
(FORALL (|q$22|) (PATS (SUBTYPE (TYPECODE |q$22| |@DUMMY|) |Thread.Closure.TYPECODE|)) (IMPLIES (EQ (SUBTYPE (TYPECODE |q$22| |@DUMMY|) |Thread.Closure.TYPECODE|) |@true|) (EQ (|Is$Thread.Closure| |q$22| |@DUMMY|) |@true|)))
(EQ (SUBTYPE1 |Thread.Closure.TYPECODE| |ROOT.TYPECODE|) |@true|)
(FORALL (|q$23|) (PATS (|Is$Thread.Closure| |q$23| |@DUMMY|)) (IMPLIES (EQ (|Is$Thread.Closure| |q$23| |@DUMMY|) |@true|) (EQ (|Is$ROOT| |q$23| |@DUMMY|) |@true|)))
(FORALL (s) (IMPLIES (NOT (EQ (select ALLOCATED s |@SPECIAL|) |@true|)) (EQ (select |Thread.SizedClosure.stackSize| s |@OBJECT|) 0)))
(EQ (|Is$INTEGER| 0 |@DUMMY|) |@true|)
(EQ (SUBTYPE |NULL.TYPECODE| |Thread.SizedClosure.TYPECODE|) |@true|)
(FORALL (|q$24|) (PATS (|Is$Thread.SizedClosure| |q$24| |@DUMMY|)) (IMPLIES (EQ (|Is$Thread.SizedClosure| |q$24| |@DUMMY|) |@true|) (EQ (SUBTYPE (TYPECODE |q$24| |@DUMMY|) |Thread.SizedClosure.TYPECODE|) |@true|)))
(FORALL (|q$25|) (PATS (SUBTYPE (TYPECODE |q$25| |@DUMMY|) |Thread.SizedClosure.TYPECODE|)) (IMPLIES (EQ (SUBTYPE (TYPECODE |q$25| |@DUMMY|) |Thread.SizedClosure.TYPECODE|) |@true|) (EQ (|Is$Thread.SizedClosure| |q$25| |@DUMMY|) |@true|)))
(EQ (|Is$Thread.SizedClosure.stackSize$MAP| |Thread.SizedClosure.stackSize| |@DUMMY|) |@true|)
(FORALL (ofm) (IMPLIES (EQ (|Is$Thread.SizedClosure.stackSize$MAP| ofm |@DUMMY|) |@true|) (FORALL (|q$26|) (EQ (|Is$CARDINAL| (select ofm |q$26| |@OBJECT|) |@DUMMY|) |@true|))))
(EQ (SUBTYPE1 |Thread.SizedClosure.TYPECODE| |Thread.Closure.TYPECODE|) |@true|)
(FORALL (|q$27|) (PATS (|Is$Thread.SizedClosure| |q$27| |@DUMMY|)) (IMPLIES (EQ (|Is$Thread.SizedClosure| |q$27| |@DUMMY|) |@true|) (EQ (|Is$Thread.Closure| |q$27| |@DUMMY|) |@true|)))
(EQ (SUBTYPE |NULL.TYPECODE| |Writer.T.TYPECODE|) |@true|)
(FORALL (|q$28|) (PATS (|Is$Writer.T| |q$28| |@DUMMY|)) (IMPLIES (EQ (|Is$Writer.T| |q$28| |@DUMMY|) |@true|) (EQ (SUBTYPE (TYPECODE |q$28| |@DUMMY|) |Writer.T.TYPECODE|) |@true|)))
(FORALL (|q$29|) (PATS (SUBTYPE (TYPECODE |q$29| |@DUMMY|) |Writer.T.TYPECODE|)) (IMPLIES (EQ (SUBTYPE (TYPECODE |q$29| |@DUMMY|) |Writer.T.TYPECODE|) |@true|) (EQ (|Is$Writer.T| |q$29| |@DUMMY|) |@true|)))
(FORALL (|q$30|) (PATS (|Is$Writer.T| |q$30| |@DUMMY|)) (IMPLIES (EQ (|Is$Writer.T| |q$30| |@DUMMY|) |@true|) (EQ (|Is$MUTEX| |q$30| |@DUMMY|) |@true|)))
(FORALL (|q$31| |dummy1$1|) (IMPLIES (EQ (|Is$TYPE@54| |q$31| |dummy1$1|) |@true|) (FORALL (|i$4|) (EQ (|Is$CHAR| (select |q$31| |i$4| |@ARRAY|) |dummy1$1|) |@true|))))
(FORALL (|map$1| start num) (PATS (|Is$TYPE@54| (SUBARRAY |map$1| start num) |@DUMMY|)) (IMPLIES (EQ (|Is$TYPE@54| |map$1| |@DUMMY|) |@true|) (EQ (|Is$TYPE@54| (SUBARRAY |map$1| start num) |@DUMMY|) |@true|)))
(FORALL (|map$2|) (PATS (|Is$TYPE@54| |map$2| |@DUMMY|)) (IMPLIES (EQ (|Is$TYPE@54| |map$2| |@DUMMY|) |@true|) (FORALL (|start$1| |num$1| map2) (PATS (storeSub |map$2| |start$1| |num$1| map2)) (IMPLIES (EQ (|Is$TYPE@54| map2 |@DUMMY|) |@true|) (EQ (|Is$TYPE@54| (storeSub |map$2| |start$1| |num$1| map2) |@DUMMY|) |@true|)))))
(FORALL (|map$3|) (PATS (|Is$TYPE@54| |map$3| |@DUMMY|)) (IMPLIES (EQ (|Is$TYPE@54| |map$3| |@DUMMY|) |@true|) (FORALL (|ind$1| |val$1|) (PATS (store |map$3| |ind$1| |val$1|)) (IMPLIES (EQ (|Is$CHAR| |val$1| |@DUMMY|) |@true|) (EQ (|Is$TYPE@54| (store |map$3| |ind$1| |val$1|) |@DUMMY|) |@true|)))))
(EQ (|Is$TEXT| |Writer.EOL| |@DUMMY|) |@true|)
(EQ (|Is$DCL| |Writer.EOL| ALLOCATED) |@true|)
(EQ (|Is$VDCL| |Writer.EOL| VIRGIN) |@true|)
(NOT (EQ (select VIRGIN |Writer.EOL| |@SPECIAL|) |@true|))
(EQ (SUBTYPE |Writer.T.TYPECODE| |MUTEX.TYPECODE|) |@true|)
(EQ (SUBTYPE |NULL.TYPECODE| |TYPE@39.TYPECODE|) |@true|)
(FORALL (|q$32|) (PATS (|Is$TYPE@39| |q$32| |@DUMMY|)) (IMPLIES (EQ (|Is$TYPE@39| |q$32| |@DUMMY|) |@true|) (EQ (SUBTYPE (TYPECODE |q$32| |@DUMMY|) |TYPE@39.TYPECODE|) |@true|)))
(FORALL (|q$33|) (PATS (SUBTYPE (TYPECODE |q$33| |@DUMMY|) |TYPE@39.TYPECODE|)) (IMPLIES (EQ (SUBTYPE (TYPECODE |q$33| |@DUMMY|) |TYPE@39.TYPECODE|) |@true|) (EQ (|Is$TYPE@39| |q$33| |@DUMMY|) |@true|)))
(EQ (SUBTYPE1 |TYPE@39.TYPECODE| |Writer.T.TYPECODE|) |@true|)
(FORALL (|q$34|) (PATS (|Is$TYPE@39| |q$34| |@DUMMY|)) (IMPLIES (EQ (|Is$TYPE@39| |q$34| |@DUMMY|) |@true|) (EQ (|Is$Writer.T| |q$34| |@DUMMY|) |@true|)))
(EQ (SUBTYPE |NULL.TYPECODE| |TextWriter.T.TYPECODE|) |@true|)
(FORALL (|q$35|) (PATS (|Is$TextWriter.T| |q$35| |@DUMMY|)) (IMPLIES (EQ (|Is$TextWriter.T| |q$35| |@DUMMY|) |@true|) (EQ (SUBTYPE (TYPECODE |q$35| |@DUMMY|) |TextWriter.T.TYPECODE|) |@true|)))
(FORALL (|q$36|) (PATS (SUBTYPE (TYPECODE |q$36| |@DUMMY|) |TextWriter.T.TYPECODE|)) (IMPLIES (EQ (SUBTYPE (TYPECODE |q$36| |@DUMMY|) |TextWriter.T.TYPECODE|) |@true|) (EQ (|Is$TextWriter.T| |q$36| |@DUMMY|) |@true|)))
(FORALL (|q$37|) (PATS (|Is$TextWriter.T| |q$37| |@DUMMY|)) (IMPLIES (EQ (|Is$TextWriter.T| |q$37| |@DUMMY|) |@true|) (EQ (|Is$TYPE@39| |q$37| |@DUMMY|) |@true|)))
(EQ (SUBTYPE |TextWriter.T.TYPECODE| |TYPE@39.TYPECODE|) |@true|)
(FORALL (|q$38| |dummy1$2|) (IMPLIES (EQ (|Is$TYPE@58| |q$38| |dummy1$2|) |@true|) (FORALL (|i$5|) (EQ (|Is$INTEGER| (select |q$38| |i$5| |@ARRAY|) |dummy1$2|) |@true|))))
(FORALL (|map$4| |start$2| |num$2|) (PATS (|Is$TYPE@58| (SUBARRAY |map$4| |start$2| |num$2|) |@DUMMY|)) (IMPLIES (EQ (|Is$TYPE@58| |map$4| |@DUMMY|) |@true|) (EQ (|Is$TYPE@58| (SUBARRAY |map$4| |start$2| |num$2|) |@DUMMY|) |@true|)))
(FORALL (|map$5|) (PATS (|Is$TYPE@58| |map$5| |@DUMMY|)) (IMPLIES (EQ (|Is$TYPE@58| |map$5| |@DUMMY|) |@true|) (FORALL (|start$3| |num$3| |map2$1|) (PATS (storeSub |map$5| |start$3| |num$3| |map2$1|)) (IMPLIES (EQ (|Is$TYPE@58| |map2$1| |@DUMMY|) |@true|) (EQ (|Is$TYPE@58| (storeSub |map$5| |start$3| |num$3| |map2$1|) |@DUMMY|) |@true|)))))
(FORALL (|map$6|) (PATS (|Is$TYPE@58| |map$6| |@DUMMY|)) (IMPLIES (EQ (|Is$TYPE@58| |map$6| |@DUMMY|) |@true|) (FORALL (|ind$2| |val$2|) (PATS (store |map$6| |ind$2| |val$2|)) (IMPLIES (EQ (|Is$INTEGER| |val$2| |@DUMMY|) |@true|) (EQ (|Is$TYPE@58| (store |map$6| |ind$2| |val$2|) |@DUMMY|) |@true|)))))
)
)

;; XXX non UTVPI
TRUE
;(FORALL (|RESIDUE.Writer.valid`| |RESIDUE.Text.Value`| |RESIDUE.Writer.state`| |a`| |ALLOCATED`| |LL`| |VIRGIN`|) (OR (NOT (EQ (|Is$TYPE@58| a |@DUMMY|) |@true|)) (FORALL (wr) (IMPLIES (AND (EQ (|Is$TextWriter.T| wr |@DUMMY|) |@true|) (EQ (|Is$DCL| wr ALLOCATED) |@true|) (EQ (|Is$VDCL| wr VIRGIN) |@true|)) (FORALL (res) (FORALL (|res$1|) (IMPLIES (EQ (|Is$TextWriter.T| (NEW ALLOCATED LL VIRGIN |TextWriter.T.TYPECODE| |POS$7$12|) |@DUMMY|) |@true|) (AND (LBL |ERROR.deref.7.29| (NEQ (NEW ALLOCATED LL VIRGIN |TextWriter.T.TYPECODE| |POS$7$12|) |$NIL|)) (FORALL (|EXCEPTION.code| |RES(TextWriter.init@7.29)| self |ALLOCATED$1| |ALLOCATED'| |RESIDUE.Writer.state$2| |RESIDUE.Writer.state'$1| |RESIDUE.Writer.valid$2| |RESIDUE.Writer.valid'$1|) (AND (LBL |ERROR.pre.7.29| TRUE) (IMPLIES (AND (IMPLIES (EQ |EXCEPTION.code| RETURN) (AND (EQ (select (|FUNC.Writer.valid| |RESIDUE.Writer.valid'$1|) (NEW ALLOCATED LL VIRGIN |TextWriter.T.TYPECODE| |POS$7$12|) |@OBJECT|) |@true|) (EQ (NEW ALLOCATED LL VIRGIN |TextWriter.T.TYPECODE| |POS$7$12|) |RES(TextWriter.init@7.29)|))) (EQ |EXCEPTION.code| RETURN) (FORALL (s0) (PATS (select (|FUNC.Writer.valid| |RESIDUE.Writer.valid$1|) s0 |@OBJECT|) (select (|FUNC.Writer.valid| |RESIDUE.Writer.valid'$1|) s0 |@OBJECT|)) (IMPLIES (AND (EQ (|Is$Writer.T| s0 |@DUMMY|) |@true|) (EQ (|Is$DCL| s0 (store ALLOCATED (NEW ALLOCATED LL VIRGIN |TextWriter.T.TYPECODE| |POS$7$12|) |@true|)) |@true|) (EQ (|Is$VDCL| s0 VIRGIN) |@true|) (NEQ s0 |$NIL|)) (OR (EQ (select (|FUNC.Writer.valid| |RESIDUE.Writer.valid$1|) s0 |@OBJECT|) (select (|FUNC.Writer.valid| |RESIDUE.Writer.valid'$1|) s0 |@OBJECT|)) (EQ s0 (NEW ALLOCATED LL VIRGIN |TextWriter.T.TYPECODE| |POS$7$12|))))) (FORALL (|s0$1|) (PATS (select (|FUNC.Writer.state| |RESIDUE.Writer.state$1|) |s0$1| |@OBJECT|) (select (|FUNC.Writer.state| |RESIDUE.Writer.state'$1|) |s0$1| |@OBJECT|)) (IMPLIES (AND (EQ (|Is$Writer.T| |s0$1| |@DUMMY|) |@true|) (EQ (|Is$DCL| |s0$1| (store ALLOCATED (NEW ALLOCATED LL VIRGIN |TextWriter.T.TYPECODE| |POS$7$12|) |@true|)) |@true|) (EQ (|Is$VDCL| |s0$1| VIRGIN) |@true|) (NEQ |s0$1| |$NIL|)) (OR (EQ (select (|FUNC.Writer.state| |RESIDUE.Writer.state$1|) |s0$1| |@OBJECT|) (select (|FUNC.Writer.state| |RESIDUE.Writer.state'$1|) |s0$1| |@OBJECT|)) (EQ |s0$1| (NEW ALLOCATED LL VIRGIN |TextWriter.T.TYPECODE| |POS$7$12|))))) (EQ |RESIDUE.Writer.valid'$1| (store |RESIDUE.Writer.valid$1| (NEW ALLOCATED LL VIRGIN |TextWriter.T.TYPECODE| |POS$7$12|) (select |RESIDUE.Writer.valid'$1| (NEW ALLOCATED LL VIRGIN |TextWriter.T.TYPECODE| |POS$7$12|) |@OBJECT|))) (EQ (select |RESIDUE.Writer.valid'$1| |$NIL| |@OBJECT|) (select |RESIDUE.Writer.valid$1| |$NIL| |@OBJECT|)) (EQ |RESIDUE.Writer.state'$1| (store |RESIDUE.Writer.state$1| (NEW ALLOCATED LL VIRGIN |TextWriter.T.TYPECODE| |POS$7$12|) (select |RESIDUE.Writer.state'$1| (NEW ALLOCATED LL VIRGIN |TextWriter.T.TYPECODE| |POS$7$12|) |@OBJECT|))) (EQ (select |RESIDUE.Writer.state'$1| |$NIL| |@OBJECT|) (select |RESIDUE.Writer.state$1| |$NIL| |@OBJECT|)) (EQ (SUBSET (store ALLOCATED (NEW ALLOCATED LL VIRGIN |TextWriter.T.TYPECODE| |POS$7$12|) |@true|) |ALLOCATED'|) |@true|) TRUE (EQ (|Is$NULL| |RESIDUE.Writer.state'$1| |@DUMMY|) |@true|) (EQ (|Is$NULL| |RESIDUE.Writer.valid'$1| |@DUMMY|) |@true|) (EQ (|Is$TextWriter.T| |RES(TextWriter.init@7.29)| |@DUMMY|) |@true|) (EQ (|Is$DCL| |RES(TextWriter.init@7.29)| |ALLOCATED'|) |@true|) (EQ (|Is$VDCL| |RES(TextWriter.init@7.29)| VIRGIN) |@true|)) (AND (FORALL (|i$6|) (OR (NOT (<= 0 (- (NUMBER (ADDR a) 0) 1))) (FORALL (|ALLOCATED$2|) (LBL |ERROR.loop-init.8.4| (AND (<= 0 0) (<= 0 (+ (- (NUMBER (ADDR a) 0) 1) 1))))))) (FORALL (|i$6|) (OR (NOT (<= 0 (- (NUMBER (ADDR a) 0) 1))) (FORALL (|ALLOCATED$2|) (OR (NOT (<= 0 (- (NUMBER (ADDR a) 0) 1))) (FORALL (|res$2|) (AND (LBL |ERROR.index.9.26| (AND (<= 0 0) (< 0 (NUMBER (ADDR a) 0)))) (FORALL (|EXCEPTION.code$1| |wr$1| |i$7| |ALLOCATED$3| |ALLOCATED'$1| |RESIDUE.Writer.state$3| |RESIDUE.Writer.state'$2|) (AND (LBL |ERROR.pre.9.12| (EQ (select (|FUNC.Writer.valid| |RESIDUE.Writer.valid'$1|) |RES(TextWriter.init@7.29)| |@OBJECT|) |@true|)) (IMPLIES (AND (OR (EQ |EXCEPTION.code$1| RETURN) (EQ |EXCEPTION.code$1| |Writer.Failure|) (EQ |EXCEPTION.code$1| |Thread.Alerted|)) (FORALL (|s0$2|) (PATS (select (|FUNC.Writer.state| |RESIDUE.Writer.state'$1|) |s0$2| |@OBJECT|) (select (|FUNC.Writer.state| |RESIDUE.Writer.state'$2|) |s0$2| |@OBJECT|)) (IMPLIES (AND (EQ (|Is$Writer.T| |s0$2| |@DUMMY|) |@true|) (EQ (|Is$DCL| |s0$2| |ALLOCATED'|) |@true|) (EQ (|Is$VDCL| |s0$2| VIRGIN) |@true|) (NEQ |s0$2| |$NIL|)) (OR (EQ (select (|FUNC.Writer.state| |RESIDUE.Writer.state'$1|) |s0$2| |@OBJECT|) (select (|FUNC.Writer.state| |RESIDUE.Writer.state'$2|) |s0$2| |@OBJECT|)) (EQ |s0$2| |RES(TextWriter.init@7.29)|)))) (EQ |RESIDUE.Writer.state'$2| (store |RESIDUE.Writer.state'$1| |RES(TextWriter.init@7.29)| (select |RESIDUE.Writer.state'$2| |RES(TextWriter.init@7.29)| |@OBJECT|))) (EQ (select |RESIDUE.Writer.state'$2| |$NIL| |@OBJECT|) (select |RESIDUE.Writer.state'$1| |$NIL| |@OBJECT|)) (EQ (SUBSET |ALLOCATED'| |ALLOCATED'$1|) |@true|) TRUE (EQ (|Is$NULL| |RESIDUE.Writer.state'$2| |@DUMMY|) |@true|)) (AND (OR (NOT (EQ |EXCEPTION.code$1| RETURN)) (FORALL (|res$3|) (FORALL (|res$4|) (OR (NOT (AND (NEQ |res$4| |$NIL|) (EQ (select |ALLOCATED'$1| |res$4| |@SPECIAL|) |@true|) (EQ (|Is$TEXT| |res$4| |@DUMMY|) |@true|) (EQ (NUMBER (select (|FUNC.Text.Value| |RESIDUE.Text.Value$1|) |res$4| |@ARRAY|) 0) 2) (EQ (select (select (|FUNC.Text.Value| |RESIDUE.Text.Value$1|) |res$4| |@ARRAY|) 0 |@ARRAY|) (VAL 92 |CHAR.TYPECODE|)) (EQ (select (select (|FUNC.Text.Value| |RESIDUE.Text.Value$1|) |res$4| |@ARRAY|) 1 |@ARRAY|) (VAL 110 |CHAR.TYPECODE|)))) (FORALL (|EXCEPTION.code$2| |wr$2| t |ALLOCATED$4| |ALLOCATED'$2| |RESIDUE.Writer.state$4| |RESIDUE.Writer.state'$3|) (AND (LBL |ERROR.pre.10.12| (AND (EQ (select (|FUNC.Writer.valid| |RESIDUE.Writer.valid'$1|) |RES(TextWriter.init@7.29)| |@OBJECT|) |@true|) (NEQ |res$4| |$NIL|))) (IMPLIES (AND (OR (EQ |EXCEPTION.code$2| RETURN) (EQ |EXCEPTION.code$2| |Writer.Failure|) (EQ |EXCEPTION.code$2| |Thread.Alerted|)) (FORALL (|s0$3|) (PATS (select (|FUNC.Writer.state| |RESIDUE.Writer.state'$2|) |s0$3| |@OBJECT|) (select (|FUNC.Writer.state| |RESIDUE.Writer.state'$3|) |s0$3| |@OBJECT|)) (IMPLIES (AND (EQ (|Is$Writer.T| |s0$3| |@DUMMY|) |@true|) (EQ (|Is$DCL| |s0$3| |ALLOCATED'$1|) |@true|) (EQ (|Is$VDCL| |s0$3| VIRGIN) |@true|) (NEQ |s0$3| |$NIL|)) (OR (EQ (select (|FUNC.Writer.state| |RESIDUE.Writer.state'$2|) |s0$3| |@OBJECT|) (select (|FUNC.Writer.state| |RESIDUE.Writer.state'$3|) |s0$3| |@OBJECT|)) (EQ |s0$3| |RES(TextWriter.init@7.29)|)))) (EQ |RESIDUE.Writer.state'$3| (store |RESIDUE.Writer.state'$2| |RES(TextWriter.init@7.29)| (select |RESIDUE.Writer.state'$3| |RES(TextWriter.init@7.29)| |@OBJECT|))) (EQ (select |RESIDUE.Writer.state'$3| |$NIL| |@OBJECT|) (select |RESIDUE.Writer.state'$2| |$NIL| |@OBJECT|)) (EQ (SUBSET |ALLOCATED'$1| |ALLOCATED'$2|) |@true|) TRUE (EQ (|Is$NULL| |RESIDUE.Writer.state'$3| |@DUMMY|) |@true|)) (AND (OR (NOT (EQ |EXCEPTION.code$2| RETURN)) (<= (+ 0 1) (- (NUMBER (ADDR a) 0) 1)) (FORALL (|res$5|) (FORALL (|EXCEPTION.code$3| |RES(TextWriter.ToText@12.21)| |wr$3| |ALLOCATED$5| |ALLOCATED'$3| |RESIDUE.Writer.state$5| |RESIDUE.Writer.state'$4|) (AND (LBL |ERROR.pre.12.21| (EQ (select (|FUNC.Writer.valid| |RESIDUE.Writer.valid'$1|) |RES(TextWriter.init@7.29)| |@OBJECT|) |@true|)) (IMPLIES (AND (EQ |EXCEPTION.code$3| RETURN) (FORALL (|s0$4|) (PATS (select (|FUNC.Writer.state| |RESIDUE.Writer.state'$3|) |s0$4| |@OBJECT|) (select (|FUNC.Writer.state| |RESIDUE.Writer.state'$4|) |s0$4| |@OBJECT|)) (IMPLIES (AND (EQ (|Is$Writer.T| |s0$4| |@DUMMY|) |@true|) (EQ (|Is$DCL| |s0$4| |ALLOCATED'$2|) |@true|) (EQ (|Is$VDCL| |s0$4| VIRGIN) |@true|) (NEQ |s0$4| |$NIL|)) (OR (EQ (select (|FUNC.Writer.state| |RESIDUE.Writer.state'$3|) |s0$4| |@OBJECT|) (select (|FUNC.Writer.state| |RESIDUE.Writer.state'$4|) |s0$4| |@OBJECT|)) (EQ |s0$4| |RES(TextWriter.init@7.29)|)))) (EQ |RESIDUE.Writer.state'$4| (store |RESIDUE.Writer.state'$3| |RES(TextWriter.init@7.29)| (select |RESIDUE.Writer.state'$4| |RES(TextWriter.init@7.29)| |@OBJECT|))) (EQ (select |RESIDUE.Writer.state'$4| |$NIL| |@OBJECT|) (select |RESIDUE.Writer.state'$3| |$NIL| |@OBJECT|)) (EQ (SUBSET |ALLOCATED'$2| |ALLOCATED'$3|) |@true|) TRUE (EQ (|Is$NULL| |RESIDUE.Writer.state'$4| |@DUMMY|) |@true|) (EQ (|Is$TEXT| |RES(TextWriter.ToText@12.21)| |@DUMMY|) |@true|) (EQ (|Is$DCL| |RES(TextWriter.ToText@12.21)| |ALLOCATED'$3|) |@true|) (EQ (|Is$VDCL| |RES(TextWriter.ToText@12.21)| VIRGIN) |@true|)) (AND (LBL |ERROR.post.5.0.RAISES| (OR (EQ RETURN RETURN) (EQ RETURN |Writer.Failure|) (EQ RETURN |Thread.Alerted|))) (LBL |ERROR.inv.5.0| TRUE) (LBL |ERROR.mod.5.10.RESIDUE.Writer.state| (FORALL (|s0$5|) (PATS (select |RESIDUE.Writer.state'$4| |s0$5| |@OBJECT|) (select |RESIDUE.Writer.state$1| |s0$5| |@OBJECT|)) (IMPLIES (AND (EQ (|Is$Writer.T| |s0$5| |@DUMMY|) |@true|) (EQ (|Is$DCL| |s0$5| ALLOCATED) |@true|) (EQ (|Is$VDCL| |s0$5| VIRGIN) |@true|) (NEQ |s0$5| |$NIL|)) (EQ (select |RESIDUE.Writer.state$1| |s0$5| |@OBJECT|) (select |RESIDUE.Writer.state'$4| |s0$5| |@OBJECT|))))) (LBL |ERROR.mod.5.10.Writer.state| (FORALL (|s0$6|) (PATS (select (|FUNC.Writer.state| |RESIDUE.Writer.state'$4|) |s0$6| |@OBJECT|) (select (|FUNC.Writer.state| |RESIDUE.Writer.state$1|) |s0$6| |@OBJECT|)) (IMPLIES (AND (EQ (|Is$Writer.T| |s0$6| |@DUMMY|) |@true|) (EQ (|Is$DCL| |s0$6| ALLOCATED) |@true|) (EQ (|Is$VDCL| |s0$6| VIRGIN) |@true|) (NEQ |s0$6| |$NIL|)) (EQ (select (|FUNC.Writer.state| |RESIDUE.Writer.state$1|) |s0$6| |@OBJECT|) (select (|FUNC.Writer.state| |RESIDUE.Writer.state'$4|) |s0$6| |@OBJECT|))))) (LBL |ERROR.mod.5.10.RESIDUE.Writer.valid| (FORALL (|s0$7|) (PATS (select |RESIDUE.Writer.valid'$1| |s0$7| |@OBJECT|) (select |RESIDUE.Writer.valid$1| |s0$7| |@OBJECT|)) (IMPLIES (AND (EQ (|Is$Writer.T| |s0$7| |@DUMMY|) |@true|) (EQ (|Is$DCL| |s0$7| ALLOCATED) |@true|) (EQ (|Is$VDCL| |s0$7| VIRGIN) |@true|) (NEQ |s0$7| |$NIL|)) (EQ (select |RESIDUE.Writer.valid$1| |s0$7| |@OBJECT|) (select |RESIDUE.Writer.valid'$1| |s0$7| |@OBJECT|))))) (LBL |ERROR.mod.5.10.Writer.valid| (FORALL (|s0$8|) (PATS (select (|FUNC.Writer.valid| |RESIDUE.Writer.valid'$1|) |s0$8| |@OBJECT|) (select (|FUNC.Writer.valid| |RESIDUE.Writer.valid$1|) |s0$8| |@OBJECT|)) (IMPLIES (AND (EQ (|Is$Writer.T| |s0$8| |@DUMMY|) |@true|) (EQ (|Is$DCL| |s0$8| ALLOCATED) |@true|) (EQ (|Is$VDCL| |s0$8| VIRGIN) |@true|) (NEQ |s0$8| |$NIL|)) (EQ (select (|FUNC.Writer.valid| |RESIDUE.Writer.valid$1|) |s0$8| |@OBJECT|) (select (|FUNC.Writer.valid| |RESIDUE.Writer.valid'$1|) |s0$8| |@OBJECT|))))))))))) (OR (EQ |EXCEPTION.code$2| RETURN) (EQ |EXCEPTION.code$2| EXIT) (AND (LBL |ERROR.post.5.0.RAISES| (OR (EQ |EXCEPTION.code$2| RETURN) (EQ |EXCEPTION.code$2| |Writer.Failure|) (EQ |EXCEPTION.code$2| |Thread.Alerted|))) (LBL |ERROR.inv.5.0| TRUE) (LBL |ERROR.mod.5.10.RESIDUE.Writer.state| (FORALL (|s0$5|) (PATS (select |RESIDUE.Writer.state'$3| |s0$5| |@OBJECT|) (select |RESIDUE.Writer.state$1| |s0$5| |@OBJECT|)) (IMPLIES (AND (EQ (|Is$Writer.T| |s0$5| |@DUMMY|) |@true|) (EQ (|Is$DCL| |s0$5| ALLOCATED) |@true|) (EQ (|Is$VDCL| |s0$5| VIRGIN) |@true|) (NEQ |s0$5| |$NIL|)) (EQ (select |RESIDUE.Writer.state$1| |s0$5| |@OBJECT|) (select |RESIDUE.Writer.state'$3| |s0$5| |@OBJECT|))))) (LBL |ERROR.mod.5.10.Writer.state| (FORALL (|s0$6|) (PATS (select (|FUNC.Writer.state| |RESIDUE.Writer.state'$3|) |s0$6| |@OBJECT|) (select (|FUNC.Writer.state| |RESIDUE.Writer.state$1|) |s0$6| |@OBJECT|)) (IMPLIES (AND (EQ (|Is$Writer.T| |s0$6| |@DUMMY|) |@true|) (EQ (|Is$DCL| |s0$6| ALLOCATED) |@true|) (EQ (|Is$VDCL| |s0$6| VIRGIN) |@true|) (NEQ |s0$6| |$NIL|)) (EQ (select (|FUNC.Writer.state| |RESIDUE.Writer.state$1|) |s0$6| |@OBJECT|) (select (|FUNC.Writer.state| |RESIDUE.Writer.state'$3|) |s0$6| |@OBJECT|))))) (LBL |ERROR.mod.5.10.RESIDUE.Writer.valid| (FORALL (|s0$7|) (PATS (select |RESIDUE.Writer.valid'$1| |s0$7| |@OBJECT|) (select |RESIDUE.Writer.valid$1| |s0$7| |@OBJECT|)) (IMPLIES (AND (EQ (|Is$Writer.T| |s0$7| |@DUMMY|) |@true|) (EQ (|Is$DCL| |s0$7| ALLOCATED) |@true|) (EQ (|Is$VDCL| |s0$7| VIRGIN) |@true|) (NEQ |s0$7| |$NIL|)) (EQ (select |RESIDUE.Writer.valid$1| |s0$7| |@OBJECT|) (select |RESIDUE.Writer.valid'$1| |s0$7| |@OBJECT|))))) (LBL |ERROR.mod.5.10.Writer.valid| (FORALL (|s0$8|) (PATS (select (|FUNC.Writer.valid| |RESIDUE.Writer.valid'$1|) |s0$8| |@OBJECT|) (select (|FUNC.Writer.valid| |RESIDUE.Writer.valid$1|) |s0$8| |@OBJECT|)) (IMPLIES (AND (EQ (|Is$Writer.T| |s0$8| |@DUMMY|) |@true|) (EQ (|Is$DCL| |s0$8| ALLOCATED) |@true|) (EQ (|Is$VDCL| |s0$8| VIRGIN) |@true|) (NEQ |s0$8| |$NIL|)) (EQ (select (|FUNC.Writer.valid| |RESIDUE.Writer.valid$1|) |s0$8| |@OBJECT|) (select (|FUNC.Writer.valid| |RESIDUE.Writer.valid'$1|) |s0$8| |@OBJECT|))))))))))))))) (OR (EQ |EXCEPTION.code$1| RETURN) (EQ |EXCEPTION.code$1| EXIT) (AND (LBL |ERROR.post.5.0.RAISES| (OR (EQ |EXCEPTION.code$1| RETURN) (EQ |EXCEPTION.code$1| |Writer.Failure|) (EQ |EXCEPTION.code$1| |Thread.Alerted|))) (LBL |ERROR.inv.5.0| TRUE) (LBL |ERROR.mod.5.10.RESIDUE.Writer.state| (FORALL (|s0$5|) (PATS (select |RESIDUE.Writer.state'$2| |s0$5| |@OBJECT|) (select |RESIDUE.Writer.state$1| |s0$5| |@OBJECT|)) (IMPLIES (AND (EQ (|Is$Writer.T| |s0$5| |@DUMMY|) |@true|) (EQ (|Is$DCL| |s0$5| ALLOCATED) |@true|) (EQ (|Is$VDCL| |s0$5| VIRGIN) |@true|) (NEQ |s0$5| |$NIL|)) (EQ (select |RESIDUE.Writer.state$1| |s0$5| |@OBJECT|) (select |RESIDUE.Writer.state'$2| |s0$5| |@OBJECT|))))) (LBL |ERROR.mod.5.10.Writer.state| (FORALL (|s0$6|) (PATS (select (|FUNC.Writer.state| |RESIDUE.Writer.state'$2|) |s0$6| |@OBJECT|) (select (|FUNC.Writer.state| |RESIDUE.Writer.state$1|) |s0$6| |@OBJECT|)) (IMPLIES (AND (EQ (|Is$Writer.T| |s0$6| |@DUMMY|) |@true|) (EQ (|Is$DCL| |s0$6| ALLOCATED) |@true|) (EQ (|Is$VDCL| |s0$6| VIRGIN) |@true|) (NEQ |s0$6| |$NIL|)) (EQ (select (|FUNC.Writer.state| |RESIDUE.Writer.state$1|) |s0$6| |@OBJECT|) (select (|FUNC.Writer.state| |RESIDUE.Writer.state'$2|) |s0$6| |@OBJECT|))))) (LBL |ERROR.mod.5.10.RESIDUE.Writer.valid| (FORALL (|s0$7|) (PATS (select |RESIDUE.Writer.valid'$1| |s0$7| |@OBJECT|) (select |RESIDUE.Writer.valid$1| |s0$7| |@OBJECT|)) (IMPLIES (AND (EQ (|Is$Writer.T| |s0$7| |@DUMMY|) |@true|) (EQ (|Is$DCL| |s0$7| ALLOCATED) |@true|) (EQ (|Is$VDCL| |s0$7| VIRGIN) |@true|) (NEQ |s0$7| |$NIL|)) (EQ (select |RESIDUE.Writer.valid$1| |s0$7| |@OBJECT|) (select |RESIDUE.Writer.valid'$1| |s0$7| |@OBJECT|))))) (LBL |ERROR.mod.5.10.Writer.valid| (FORALL (|s0$8|) (PATS (select (|FUNC.Writer.valid| |RESIDUE.Writer.valid'$1|) |s0$8| |@OBJECT|) (select (|FUNC.Writer.valid| |RESIDUE.Writer.valid$1|) |s0$8| |@OBJECT|)) (IMPLIES (AND (EQ (|Is$Writer.T| |s0$8| |@DUMMY|) |@true|) (EQ (|Is$DCL| |s0$8| ALLOCATED) |@true|) (EQ (|Is$VDCL| |s0$8| VIRGIN) |@true|) (NEQ |s0$8| |$NIL|)) (EQ (select (|FUNC.Writer.valid| |RESIDUE.Writer.valid$1|) |s0$8| |@OBJECT|) (select (|FUNC.Writer.valid| |RESIDUE.Writer.valid'$1|) |s0$8| |@OBJECT|))))))))))))))))) (FORALL (|i$6|) (OR (<= 0 (- (NUMBER (ADDR a) 0) 1)) (FORALL (|res$5|) (FORALL (|EXCEPTION.code$3| |RES(TextWriter.ToText@12.21)| |wr$3| |ALLOCATED$5| |ALLOCATED'$3| |RESIDUE.Writer.state$5| |RESIDUE.Writer.state'$4|) (AND (LBL |ERROR.pre.12.21| (EQ (select (|FUNC.Writer.valid| |RESIDUE.Writer.valid'$1|) |RES(TextWriter.init@7.29)| |@OBJECT|) |@true|)) (IMPLIES (AND (EQ |EXCEPTION.code$3| RETURN) (FORALL (|s0$4|) (PATS (select (|FUNC.Writer.state| |RESIDUE.Writer.state'$1|) |s0$4| |@OBJECT|) (select (|FUNC.Writer.state| |RESIDUE.Writer.state'$4|) |s0$4| |@OBJECT|)) (IMPLIES (AND (EQ (|Is$Writer.T| |s0$4| |@DUMMY|) |@true|) (EQ (|Is$DCL| |s0$4| |ALLOCATED'|) |@true|) (EQ (|Is$VDCL| |s0$4| VIRGIN) |@true|) (NEQ |s0$4| |$NIL|)) (OR (EQ (select (|FUNC.Writer.state| |RESIDUE.Writer.state'$1|) |s0$4| |@OBJECT|) (select (|FUNC.Writer.state| |RESIDUE.Writer.state'$4|) |s0$4| |@OBJECT|)) (EQ |s0$4| |RES(TextWriter.init@7.29)|)))) (EQ |RESIDUE.Writer.state'$4| (store |RESIDUE.Writer.state'$1| |RES(TextWriter.init@7.29)| (select |RESIDUE.Writer.state'$4| |RES(TextWriter.init@7.29)| |@OBJECT|))) (EQ (select |RESIDUE.Writer.state'$4| |$NIL| |@OBJECT|) (select |RESIDUE.Writer.state'$1| |$NIL| |@OBJECT|)) (EQ (SUBSET |ALLOCATED'| |ALLOCATED'$3|) |@true|) TRUE (EQ (|Is$NULL| |RESIDUE.Writer.state'$4| |@DUMMY|) |@true|) (EQ (|Is$TEXT| |RES(TextWriter.ToText@12.21)| |@DUMMY|) |@true|) (EQ (|Is$DCL| |RES(TextWriter.ToText@12.21)| |ALLOCATED'$3|) |@true|) (EQ (|Is$VDCL| |RES(TextWriter.ToText@12.21)| VIRGIN) |@true|)) (AND (LBL |ERROR.post.5.0.RAISES| (OR (EQ RETURN RETURN) (EQ RETURN |Writer.Failure|) (EQ RETURN |Thread.Alerted|))) (LBL |ERROR.inv.5.0| TRUE) (LBL |ERROR.mod.5.10.RESIDUE.Writer.state| (FORALL (|s0$5|) (PATS (select |RESIDUE.Writer.state'$4| |s0$5| |@OBJECT|) (select |RESIDUE.Writer.state$1| |s0$5| |@OBJECT|)) (IMPLIES (AND (EQ (|Is$Writer.T| |s0$5| |@DUMMY|) |@true|) (EQ (|Is$DCL| |s0$5| ALLOCATED) |@true|) (EQ (|Is$VDCL| |s0$5| VIRGIN) |@true|) (NEQ |s0$5| |$NIL|)) (EQ (select |RESIDUE.Writer.state$1| |s0$5| |@OBJECT|) (select |RESIDUE.Writer.state'$4| |s0$5| |@OBJECT|))))) (LBL |ERROR.mod.5.10.Writer.state| (FORALL (|s0$6|) (PATS (select (|FUNC.Writer.state| |RESIDUE.Writer.state'$4|) |s0$6| |@OBJECT|) (select (|FUNC.Writer.state| |RESIDUE.Writer.state$1|) |s0$6| |@OBJECT|)) (IMPLIES (AND (EQ (|Is$Writer.T| |s0$6| |@DUMMY|) |@true|) (EQ (|Is$DCL| |s0$6| ALLOCATED) |@true|) (EQ (|Is$VDCL| |s0$6| VIRGIN) |@true|) (NEQ |s0$6| |$NIL|)) (EQ (select (|FUNC.Writer.state| |RESIDUE.Writer.state$1|) |s0$6| |@OBJECT|) (select (|FUNC.Writer.state| |RESIDUE.Writer.state'$4|) |s0$6| |@OBJECT|))))) (LBL |ERROR.mod.5.10.RESIDUE.Writer.valid| (FORALL (|s0$7|) (PATS (select |RESIDUE.Writer.valid'$1| |s0$7| |@OBJECT|) (select |RESIDUE.Writer.valid$1| |s0$7| |@OBJECT|)) (IMPLIES (AND (EQ (|Is$Writer.T| |s0$7| |@DUMMY|) |@true|) (EQ (|Is$DCL| |s0$7| ALLOCATED) |@true|) (EQ (|Is$VDCL| |s0$7| VIRGIN) |@true|) (NEQ |s0$7| |$NIL|)) (EQ (select |RESIDUE.Writer.valid$1| |s0$7| |@OBJECT|) (select |RESIDUE.Writer.valid'$1| |s0$7| |@OBJECT|))))) (LBL |ERROR.mod.5.10.Writer.valid| (FORALL (|s0$8|) (PATS (select (|FUNC.Writer.valid| |RESIDUE.Writer.valid'$1|) |s0$8| |@OBJECT|) (select (|FUNC.Writer.valid| |RESIDUE.Writer.valid$1|) |s0$8| |@OBJECT|)) (IMPLIES (AND (EQ (|Is$Writer.T| |s0$8| |@DUMMY|) |@true|) (EQ (|Is$DCL| |s0$8| ALLOCATED) |@true|) (EQ (|Is$VDCL| |s0$8| VIRGIN) |@true|) (NEQ |s0$8| |$NIL|)) (EQ (select (|FUNC.Writer.valid| |RESIDUE.Writer.valid$1|) |s0$8| |@OBJECT|) (select (|FUNC.Writer.valid| |RESIDUE.Writer.valid'$1|) |s0$8| |@OBJECT|))))))))))))))))))))))))
(BG_POP)