$$$top.pvs
top: THEORY
 BEGIN

  IMPORTING abstraction

 END top

$$$mutheorems.pvs
mutheorems[T : TYPE]: THEORY

BEGIN


IMPORTING mucalculus[T], connectives[T]

f,g,h: VAR pred[T]

refl: LEMMA
f <= f

antisym: LEMMA
f <= g AND g <= f IMPLIES f =g

trans: LEMMA
f <= g AND g <= h IMPLIES f <= h

AND_comm: LEMMA
(f AND g) = (g AND f)

AND_assoc: LEMMA
(f AND (g AND h)) = ((f AND g) AND h)

OR_comm: LEMMA
(f OR g) = (g OR f)

OR_assoc: LEMMA
(f OR (g OR h)) = ((f OR g) OR h)

AND_OR_dist: LEMMA
(f AND (g OR h)) = ((f AND g) OR (f AND h))

lem1: LEMMA
(f <= (g AND h)) = ((f <= g) AND (f <= h))

lem2: LEMMA
(f AND g) <= f

lem3: LEMMA
f <= (f OR g)

lem4: LEMMA
(f OR g) <= g IMPLIES f <= g

lem5: LEMMA
((f <= h) AND (g <= h)) = ((f OR g) <= h)

F: VAR pred[pred[T]]
glb_min: THEOREM
member(f,F) IMPLIES glb(F) <= f 

glb_max: THEOREM
(FORALL g: member(g,F) IMPLIES f <= g) IMPLIES
f <= glb(F)

lub_max: THEOREM
member(f,F) IMPLIES f <= lub(F) 

lub_min: THEOREM
(FORALL g: member(g,F) IMPLIES g <= f) IMPLIES
lub(F) <= f

ff: VAR [pred[T]->pred[T]]
lfp_lem1: LEMMA
(ff(f) = f) IMPLIES (lfp(ff) <= f)

lfp_lem2: LEMMA
ismono(ff) IMPLIES FORALL f: ff(f) <= f IMPLIES
		             ff(glb(LAMBDA f: ff(f) <= f)) <= f

lfp_thm: THEOREM
ismono(ff) IMPLIES ff(lfp(ff)) <= lfp(ff)

lfp_thm1: THEOREM
ismono(ff) IMPLIES lfp(ff) <= ff(lfp(ff))

lfp_thm2: THEOREM
ismono(ff) IMPLIES (ff(lfp(ff)) = lfp(ff))

lfp_lem3: LEMMA
ismono(ff) IMPLIES FORALL f: ff(f) <= f IMPLIES
		             lfp(ff) <= f

lfp_is_lfp: THEOREM
ismono(ff) IMPLIES islfp(ff,lfp(ff))

gfp_lem1: LEMMA
 ff(f) = f IMPLIES f <= gfp(ff)

gfp_lem2: LEMMA
  ismono(ff) IMPLIES
  (FORALL f: f <= ff(f)  IMPLIES f <= ff(lub(LAMBDA f: f <= ff(f) )))

gfp_thm1: THEOREM
 ismono(ff) IMPLIES gfp(ff) <= ff(gfp(ff))


gfp_thm: THEOREM
 ismono(ff) IMPLIES ff(gfp(ff)) <= gfp(ff)

gfp_thm2: THEOREM
 ismono(ff) IMPLIES (ff(gfp(ff)) = gfp(ff))

gfp_lem3: LEMMA
ismono(ff) IMPLIES FORALL f: f <= ff(f) IMPLIES
		             f <= gfp(ff)

gfp_is_gfp: THEOREM
ismono(ff) IMPLIES isgfp(ff,gfp(ff))

END mutheorems




$$$mutheorems.prf
(|mutheorems| (|refl| "" (TCC) NIL)
 (|antisym| "" (SKOSIMP)
  (("" (APPLY-EXTENSIONALITY) (("" (TCC) NIL)))))
 (|trans| "" (TCC) NIL)
 (|AND_comm| "" (SKOLEM!)
  (("" (APPLY-EXTENSIONALITY) (("" (TCC) NIL)))))
 (|AND_assoc| "" (SKOLEM!)
  (("" (APPLY-EXTENSIONALITY) (("" (TCC) NIL)))))
 (|OR_comm| "" (SKOLEM!)
  (("" (APPLY-EXTENSIONALITY) (("" (TCC) NIL)))))
 (|OR_assoc| "" (SKOLEM!)
  (("" (APPLY-EXTENSIONALITY) (("" (TCC) NIL)))))
 (|AND_OR_dist| "" (SKOLEM!)
  (("" (APPLY-EXTENSIONALITY) (("" (TCC) NIL)))))
 (|lem1| "" (TCC) NIL) (|lem2| "" (TCC) NIL) (|lem3| "" (TCC) NIL)
 (|lem4| "" (TCC) NIL) (|lem5| "" (TCC) NIL) (|glb_min| "" (TCC) NIL)
 (|glb_max| "" (SKOSIMP)
  (("" (EXPAND "member")
    (("" (EXPAND "<=")
      (("" (EXPAND "glb")
        (("" (SKOLEM!)
          (("" (FLATTEN)
            (("" (SKOLEM!)
              (("" (EXPAND "member")
                (("" (INST -1 "p!1")
                  (("" (FLATTEN)
                    (("" (ASSERT)
                      (("" (INST?)
                        (("" (ASSERT) NIL)))))))))))))))))))))))))
 (|lub_max| "" (TCC) NIL)
 (|lub_min| "" (SKOSIMP)
  (("" (AUTO-REWRITE-THEORY "mucalculus[T]")
    (("" (ASSERT)
      (("" (SKOSIMP)
        (("" (SKOLEM!) (("" (INST?) (("" (TCC) NIL)))))))))))))
 (|lfp_lem1| "" (TCC) NIL)
 (|lfp_lem2| "" (SKOSIMP)
  (("" (EXPAND "ismono")
    (("" (SKOSIMP)
      (("" (LEMMA "glb_min")
        (("" (INST -1 "LAMBDA (f: pred[T]): (ff!1(f) <= f)" "f!1")
          (("" (EXPAND "member")
            ((""
              (INST -2 "glb(LAMBDA (f: pred[T]): (ff!1(f) <= f))"
               "f!1")
              (("" (BDDSIMP)
                (("" (LEMMA "trans")
                  ((""
                    (INST -1
                     "ff!1(glb(LAMBDA (f: pred[T]): (ff!1(f) <= f)))"
                     "ff!1(f!1)" "f!1")
                    (("" (ASSERT) NIL)))))))))))))))))))))
 (|lfp_thm| "" (SKOSIMP)
  (("" (EXPAND "lfp")
    (("" (LEMMA "lfp_lem2")
      (("" (INST?)
        (("" (ASSERT)
          (("" (LEMMA "glb_max")
            (("" (EXPAND "member")
              ((""
                (INST -1 "LAMBDA (f: pred[T]): (ff!1(f) <= f)"
                 "ff!1(glb(LAMBDA (f: pred[T]): (ff!1(f) <= f)))")
                (("" (BETA) (("" (ASSERT) NIL)))))))))))))))))))
 (|lfp_thm1| "" (SKOSIMP)
  (("" (LEMMA "glb_min")
    ((""
      (INST -1 "LAMBDA (f: pred[T]): (ff!1(f) <= f)"
       "ff!1(lfp(ff!1))")
      (("" (EXPAND "member")
        (("" (EXPAND "lfp")
          (("" (LEMMA "lfp_thm")
            (("" (INST?)
              (("" (ASSERT)
                (("" (EXPAND "ismono")
                  (("" (EXPAND "lfp")
                    ((""
                      (INST -2
                       "ff!1(glb(LAMBDA (p: pred[T]): (ff!1(p) <= p)))"
                       "glb(LAMBDA (p: pred[T]): (ff!1(p) <= p))")
                      (("" (ASSERT) NIL)))))))))))))))))))))))
 (|lfp_thm2| "" (SKOLEM!)
  (("" (LEMMA "lfp_thm1")
    (("" (INST?)
      (("" (BDDSIMP)
        (("" (LEMMA "lfp_thm")
          (("" (INST?)
            (("" (BDDSIMP)
              (("" (LEMMA "antisym")
                (("" (INST -1 "ff!1(lfp(ff!1))" "lfp(ff!1)")
                  (("" (ASSERT) NIL)))))))))))))))))))
 (|lfp_lem3| "" (SKOSIMP*)
  (("" (LEMMA "lfp_lem2")
    (("" (INST?)
      (("" (PROP)
        (("" (INST?)
          (("" (REWRITE "lfp_thm2" :DIR RL)
            (("" (EXPAND "lfp") (("" (PROP) NIL)))))))))))))))
 (|lfp_is_lfp| "" (SKOSIMP)
  (("" (EXPAND "islfp")
    (("" (EXPAND "isfix")
      (("" (LEMMA "lfp_thm2")
        (("" (INST?)
          (("" (LEMMA "lfp_lem1")
            (("" (INST?)
              (("" (BDDSIMP)
                (("" (SKOLEM!)
                  (("" (LEMMA "lfp_lem1")
                    (("" (INST -1 "p2!1" "ff!1")
                      NIL)))))))))))))))))))))
 (|gfp_lem1| "" (GRIND) NIL)
 (|gfp_lem2| "" (SKOSIMP*)
  (("" (EXPAND "ismono")
    (("" (LEMMA "lub_max")
      (("" (INST -1 "LAMBDA (f: pred[T]): f <= ff!1(f)" "f!1")
        (("" (EXPAND "member")
          ((""
            (INST -2 "f!1"
             "lub(LAMBDA (f: pred[T]): (f <= ff!1(f)))")
            (("" (PROP)
              (("" (LEMMA "trans")
                ((""
                  (INST -1 "f!1" "ff!1(f!1)"
                   "ff!1(lub(LAMBDA (f: pred[T]): (f <= ff!1(f) )))")
                  (("" (PROP) NIL)))))))))))))))))))
 (|gfp_thm1| "" (SKOSIMP)
  (("" (EXPAND "gfp")
    (("" (LEMMA "gfp_lem2")
      (("" (INST?)
        (("" (ASSERT)
          (("" (INST?)
            (("" (PROP)
              (("" (LEMMA "lub_min")
                (("" (INST?)
                  (("" (EXPAND "member")
                    (("" (HIDE 2 3)
                      (("" (SKOSIMP*)
                        (("" (LEMMA "lub_max")
                          (("" (INST?)
                            ((""
                              (INST?)
                              ((""
                                (EXPAND "member")
                                ((""
                                  (PROP)
                                  ((""
                                    (EXPAND "ismono")
                                    ((""
                                      (INST?)
                                      ((""
                                        (ASSERT)
                                        ((""
                                          (HIDE -1)
                                          ((""
                                            (FORWARD-CHAIN "trans")
                                            NIL)))))))))))))))))))))))))))))))))))))))))))
 (|gfp_thm| "" (SKOSIMP*)
  (("" (LEMMA "lub_max")
    ((""
      (INST -1 "LAMBDA (f: pred[T]): (f <= ff!1(f))"
       "ff!1(gfp(ff!1))")
      (("" (EXPAND "member")
        (("" (EXPAND "gfp")
          (("" (PROP)
            (("" (LEMMA "gfp_thm1")
              (("" (EXPAND "gfp")
                (("" (INST?)
                  (("" (PROP)
                    (("" (EXPAND "ismono")
                      (("" (INST?)
                        (("" (PROP) NIL)))))))))))))))))))))))))
 (|gfp_thm2| "" (SKOSIMP*)
  (("" (LEMMA "gfp_thm")
    (("" (INST?)
      (("" (LEMMA "gfp_thm1")
        (("" (INST?)
          (("" (LEMMA "antisym")
            (("" (INST?) (("" (PROP) NIL)))))))))))))))
 (|gfp_lem3| "" (SKOSIMP*)
  (("" (LEMMA "gfp_lem2")
    (("" (INST?)
      (("" (PROP)
        (("" (INST?)
          (("" (REWRITE "gfp_thm2" :DIR RL)
            (("" (EXPAND "gfp") (("" (PROP) NIL)))))))))))))))
 (|gfp_is_gfp| "" (SKOSIMP*)
  (("" (EXPAND "isgfp")
    (("" (EXPAND "isfix")
      (("" (USE "gfp_thm2")
        (("" (USE "gfp_lem1")
          (("" (PROP)
            (("" (SKOSIMP*)
              (("" (USE "gfp_lem1") (("" (PROP) NIL))))))))))))))))))
$$$more_mucalculus_theorems.pvs
more_mucalculus_theorems[T:TYPE]: THEORY
 %Contains definitions of union and intersection continuity along
 %with proof that the iterated fixpoint of a union-continuous
 %predicate transformer least 

BEGIN

IMPORTING mucalculus[T], mutheorems[T]

q : VAR sequence[PRED[T]]
r, s: VAR T
Q, P, f, g, p,p1,p2: VAR pred[T]
N: VAR [T, T->bool]
predtt: TYPE = [pred[T]->pred[T]]
pp, qq: VAR predtt
setofpred: VAR pred[pred[T]]

%ascending/descending sequences of predicates
ascends?(q): bool = ascends?(q, <=)
descends?(q): bool = descends?(q, <=)

%pp(Uq) = U(pp(q)), q ascending
U_continuous?(pp): bool =
 (FORALL (q: (ascends?)) :
    pp(lub({p | EXISTS (i : nat): p = q(i)})) =
    lub({p | EXISTS (i : nat) : p = pp(q(i))}))

%pp(/\q) = /\pp(q), q descending
I_continuous?(pp) : bool =
 (FORALL (q: (descends?)) :
    pp(glb({p | EXISTS (i : nat): p = q(i)})) =
    glb({p | EXISTS (i : nat) : p = pp(q(i))}))

U_continuity_implies_monotonicity: LEMMA
  U_continuous?(pp) IMPLIES ismono(pp)

I_continuity_implies_monotonicity: LEMMA
  I_continuous?(pp) IMPLIES ismono(pp)

%pp(pp^{i}(p)) = pp^{i+1}(p)
iterate_step: LEMMA
  (FORALL (i:nat): pp(iterate(pp, i)(p)) = iterate(pp, i+1)(p))

%Mu is iterated fixpoint
Mu(pp)(s): bool =   lub({p | (EXISTS (j:nat):  p = iterate(pp, j)(emptyset[T]))})(s)

%For U_continuous pp, iterated fixpoint is the least fixpoint
Mu_mu: LEMMA (FORALL (pp: (U_continuous?)): Mu(pp) = mu(pp))

%remaining lemmas are useful but not hard.
mu_monot: LEMMA
  ismono(pp) AND ismono(qq) AND 
(FORALL p: pp(p) <= qq(p)) IMPLIES mu(pp) <= mu(qq)

nu_mu: LEMMA ismono(pp) IMPLIES
  nu(pp) = NOT mu(LAMBDA p: NOT pp(NOT p))

Pp, Qq : VAR (ismono)

mu_induction: LEMMA
   ismono(pp) AND 
  (FORALL s: pp(Q)(s) IMPLIES Q(s)) IMPLIES
  (FORALL s: mu(pp)(s) IMPLIES Q(s))


END more_mucalculus_theorems



$$$more_mucalculus_theorems.prf
(|more_mucalculus_theorems|
 (|U_continuity_implies_monotonicity| "" (SKOSIMP*)
  (("" (EXPAND "U_continuous?")
    (("" (EXPAND "ismono")
      (("" (SKOSIMP*)
        ((""
          (NAME "QQ"
                "LAMBDA (i:nat): IF i = 0 THEN p1!1 ELSE p2!1 ENDIF")
          ((""
            (CASE "lub({p | EXISTS (i : nat) : p = QQ(i)}) = p2!1")
            (("1" (INST - "QQ")
              (("1" (REPLACE -1)
                (("1" (REPLACE -3)
                  (("1" (EXPAND "<=" +)
                    (("1" (SKOSIMP*)
                      (("1" (EXPAND "lub" +)
                        (("1" (INST + "pp!1(p1!1)")
                          (("1" (PROP)
                            (("1"
                              (EXPAND "member")
                              (("1"
                                (INST + 0)
                                (("1"
                                  (REPLACE -2 :DIR RL)
                                  (("1"
                                    (GROUND)
                                    NIL)))))))))))))))))))))
               ("2" (EXPAND "ascends?")
                (("2" (EXPAND "ascends?")
                  (("2" (EXPAND "preserves")
                    (("2" (SKOSIMP*)
                      (("2" (REPLACE -3 :DIR RL)
                        (("2" (HIDE -2 -3)
                          (("2" (GRIND) NIL)))))))))))))))
             ("2" (ASSERT)
              (("2" (GROUND)
                (("2" (HIDE -2 2)
                  (("2" (EXPAND "lub")
                    (("2" (APPLY-EXTENSIONALITY)
                      (("2" (HIDE 2)
                        (("2" (IFF)
                          (("2" (PROP)
                            (("1"
                              (SKOSIMP)
                              (("1"
                                (EXPAND "<=")
                                (("1"
                                  (INST?)
                                  (("1"
                                    (PROP)
                                    (("1"
                                      (EXPAND "member")
                                      (("1"
                                        (SKOSIMP)
                                        (("1"
                                          (CASE "i!1 = 0")
                                          (("1"
                                            (REPLACE -4 :DIR RL)
                                            (("1" (ASSERT) NIL)))
                                           ("2"
                                            (REPLACE -3 :DIR RL)
                                            (("2"
                                              (GROUND)
                                              NIL)))))))))))))))))
                             ("2"
                              (INST + "p2!1")
                              (("2"
                                (PROP)
                                (("2"
                                  (EXPAND "member")
                                  (("2"
                                    (INST + 2)
                                    (("2"
                                      (REPLACE -2 :DIR RL)
                                      (("2"
                                        (ASSERT)
                                        NIL)))))))))))))))))))))))))))))))))))))))
 (|I_continuity_implies_monotonicity| "" (SKOSIMP*)
  (("" (EXPAND "I_continuous?")
    (("" (EXPAND "ismono")
      (("" (SKOSIMP*)
        ((""
          (NAME "QQ"
                "LAMBDA (i:nat): IF i = 0 THEN p2!1 ELSE p1!1 ENDIF")
          ((""
            (CASE "glb({p | EXISTS (i : nat) : p = QQ(i)}) = p1!1")
            (("1" (INST - "QQ")
              (("1" (REPLACE -1)
                (("1" (REPLACE -3)
                  (("1" (HIDE -1 -3)
                    (("1" (EXPAND "glb")
                      (("1" (EXPAND "<=")
                        (("1" (SKOSIMP*)
                          (("1" (INST -3 "pp!1(p2!1)")
                            (("1"
                              (PROP)
                              (("1"
                                (EXPAND "member")
                                (("1"
                                  (INST + 0)
                                  (("1"
                                    (REPLACE -1 :DIR RL)
                                    (("1"
                                      (BETA)
                                      (("1"
                                        (ASSERT)
                                        NIL)))))))))))))))))))))))))
               ("2" (EXPAND "descends?")
                (("2" (EXPAND "descends?")
                  (("2" (EXPAND "inverts")
                    (("2" (SKOSIMP)
                      (("2" (REPLACE -3 :DIR RL)
                        (("2" (BETA)
                          (("2" (LIFT-IF)
                            (("2"
                              (GROUND)
                              (("1"
                                (EXPAND "<=" 1)
                                (("1" (SKOSIMP*) NIL)))
                               ("2"
                                (LIFT-IF)
                                (("2"
                                  (GROUND)
                                  (("2"
                                    (EXPAND "<=" 2)
                                    (("2"
                                      (SKOSIMP*)
                                      NIL)))))))))))))))))))))))))
             ("2" (HIDE -2 2)
              (("2" (EXPAND "glb")
                (("2" (APPLY-EXTENSIONALITY :HIDE? T)
                  (("2" (IFF)
                    (("2" (PROP)
                      (("1" (INST - "p1!1")
                        (("1" (EXPAND "member")
                          (("1" (PROP)
                            (("1"
                              (INST + 1)
                              (("1"
                                (REPLACE -1 :DIR RL)
                                (("1" (ASSERT) NIL)))))))))))
                       ("2" (SKOSIMP*)
                        (("2" (EXPAND "member")
                          (("2" (SKOSIMP*)
                            (("2"
                              (CASE "i!1 = 0")
                              (("1"
                                (REPLACE -4 :DIR RL)
                                (("1"
                                  (ASSERT)
                                  (("1"
                                    (EXPAND "<=")
                                    (("1"
                                      (INST?)
                                      (("1" (ASSERT) NIL)))))))))
                               ("2"
                                (REPLACE -3 :DIR RL)
                                (("2"
                                  (ASSERT)
                                  NIL)))))))))))))))))))))))))))))))))
 (|iterate_step| "" (INDUCT-AND-REWRITE! "i") NIL)
 (|Mu_mu| "" (SKOSIMP*)
  (("" (CASE "Mu(pp!1) <= mu(pp!1)")
    (("1" (CASE "mu(pp!1) <= Mu(pp!1)")
      (("1" (APPLY-EXTENSIONALITY)
        (("1" (HIDE 2)
          (("1" (EXPAND "<=")
            (("1" (INST?)
              (("1" (INST?) (("1" (IFF) (("1" (PROP) NIL)))))))))))))
       ("2" (HIDE -1 2)
        (("2" (TYPEPRED "pp!1")
          (("2" (FORWARD-CHAIN "U_continuity_implies_monotonicity")
            (("2" (EXPAND "U_continuous?")
              (("2"
                (INST -
                 "(LAMBDA (i:nat): iterate(pp!1, i)(emptyset[T]))")
                (("1"
                  (CASE-REPLACE "lub({p: pred[T] |
            EXISTS (i: nat):
              p
                =
                pp!1((LAMBDA (i: nat):
                        iterate(pp!1, i)(emptyset[T]))(i))}) = 
  lub({p: pred[T] |
               EXISTS (i: nat):
                 p
                   =
                   (LAMBDA (i: nat):
                      iterate(pp!1, i)(emptyset[T]))(i)})")
                  (("1" (HIDE -1)
                    (("1" (FORWARD-CHAIN "lfp_lem1")
                      (("1" (HIDE -3)
                        (("1" (EXPAND "lfp")
                          (("1" (EXPAND "mu")
                            (("1"
                              (EXPAND "Mu")
                              (("1"
                                (CASE-REPLACE
                                 "(LAMBDA (s):
             lub({p: pred[T] |
                 (EXISTS (j: nat): p = iterate(pp!1, j)(emptyset[T]))})(s)) = 
      lub({p: pred[T] |
             EXISTS (i: nat): p = iterate(pp!1, i)(emptyset[T])})")
                                (("1"
                                  (HIDE -1 2)
                                  (("1"
                                    (EXPAND "lfp")
                                    (("1" (PROPAX) NIL)))))
                                 ("2"
                                  (APPLY-EXTENSIONALITY)
                                  NIL)))))))))))))))
                   ("2" (HIDE -2 2)
                    (("2" (EXPAND "lub")
                      (("2" (APPLY-EXTENSIONALITY)
                        (("2" (HIDE 2)
                          (("2" (IFF)
                            (("2"
                              (PROP)
                              (("1"
                                (SKOSIMP*)
                                (("1"
                                  (EXPAND "member")
                                  (("1"
                                    (SKOSIMP*)
                                    (("1"
                                      (INST?)
                                      (("1"
                                        (REWRITE "iterate_step")
                                        (("1"
                                          (PROP)
                                          (("1"
                                            (INST + "i!1 + 1")
                                            (("1"
                                              (ASSERT)
                                              NIL)))))))))))))))
                               ("2"
                                (SKOSIMP*)
                                (("2"
                                  (EXPAND "member")
                                  (("2"
                                    (SKOSIMP*)
                                    (("2"
                                      (INST?)
                                      (("2"
                                        (PROP)
                                        (("2"
                                          (CASE "i!1 = 0")
                                          (("1" (GRIND) NIL)
                                           ("2"
                                            (INST + "i!1 - 1")
                                            (("1"
                                              (REWRITE
                                               "iterate_step")
                                              NIL)
                                             ("2"
                                              (ASSERT)
                                              NIL)))))))))))))))))))))))))))))
                 ("2" (HIDE 2)
                  (("2" (EXPAND "ascends?")
                    (("2" (EXPAND "ascends?")
                      (("2" (EXPAND "preserves")
                        (("2" (INDUCT "x1")
                          (("1" (GRIND) NIL)
                           ("2" (SKOSIMP*)
                            (("2"
                              (SIMPLIFY-WITH-REWRITES :DEFS T)
                              (("2"
                                (SKOSIMP*)
                                (("2"
                                  (INST - "x2!1 - 1")
                                  (("2"
                                    (INST
                                     -
                                     "(iterate(pp!1, j!1)(emptyset[T]))"
                                     "(iterate(pp!1, x2!1 - 1)(emptyset[T]))")
                                    (("2"
                                      (GRIND)
                                      NIL)))))))))))))))))))))))))))))))))
     ("2" (HIDE 2)
      (("2" (EXPAND "Mu")
        (("2" (TYPEPRED "pp!1")
          (("2" (FORWARD-CHAIN "U_continuity_implies_monotonicity")
            (("2" (EXPAND "<=")
              (("2"
                (CASE "(FORALL (i:nat), p: p<= mu(pp!1) IMPLIES iterate(pp!1, i)(p) <= mu(pp!1))")
                (("1" (SKOSIMP*)
                  (("1" (EXPAND "lub")
                    (("1" (SKOSIMP*)
                      (("1" (EXPAND "member")
                        (("1" (SKOSIMP*)
                          (("1" (INST?)
                            (("1"
                              (PROP)
                              (("1"
                                (EXPAND "<=")
                                (("1" (INST?) (("1" (GROUND) NIL)))))
                               ("2"
                                (EXPAND "<=")
                                (("2"
                                  (HIDE -1 -2 -3 2)
                                  (("2"
                                    (GRIND)
                                    NIL)))))))))))))))))))
                 ("2" (HIDE 2)
                  (("2" (INDUCT "i")
                    (("1" (GRIND) NIL)
                     ("2" (SKOSIMP*)
                      (("2" (EXPAND "iterate" +)
                        (("2" (INST?)
                          (("2" (PROP)
                            (("2"
                              (FORWARD-CHAIN "lfp_thm2")
                              (("2"
                                (EXPAND "mu")
                                (("2"
                                  (EXPAND "lfp")
                                  (("2"
                                    (REPLACE -1 1 RL)
                                    (("2"
                                      (EXPAND "ismono")
                                      (("2"
                                        (INST?)
                                        (("2"
                                          (PROP)
                                          NIL)))))))))))))))))))))))))))))))))))))))))
 (|mu_monot| "" (SKOSIMP*)
  (("" (EXPAND "mu")
    (("" (LEMMA "lfp_lem3")
      (("" (INST - "pp!1")
        (("" (PROP)
          (("" (INST - "lfp(qq!1)")
            (("" (REWRITE "lfp_thm2" :DIR RL)
              (("" (INST?)
                (("" (PROP)
                  (("" (LEMMA "lfp_thm2")
                    (("" (INST?)
                      (("" (GROUND) NIL)))))))))))))))))))))))
 (|nu_mu| "" (SKOSIMP*)
  (("" (EXPAND "mu")
    (("" (EXPAND "nu")
      (("" (EXPAND "lfp")
        (("" (APPLY-EXTENSIONALITY)
          (("" (HIDE 2)
            (("" (EXPAND "glb")
              (("" (IFF)
                (("" (PROP)
                  (("1" (EXPAND "NOT")
                    (("1" (EXPAND "gfp")
                      (("1" (EXPAND "lub")
                        (("1" (SKOSIMP*)
                          (("1" (EXPAND "member")
                            (("1"
                              (INST - "NOT gfp(pp!1)")
                              (("1"
                                (PROP)
                                (("1"
                                  (EXPAND "NOT")
                                  (("1"
                                    (EXPAND "gfp")
                                    (("1"
                                      (EXPAND "lub")
                                      (("1"
                                        (INST?)
                                        (("1"
                                          (HIDE -3)
                                          (("1"
                                            (GRIND)
                                            NIL)))))))))))
                                 ("2"
                                  (EXPAND "<=" +)
                                  (("2"
                                    (SKOSIMP*)
                                    (("2"
                                      (EXPAND "NOT")
                                      (("2"
                                        (FORWARD-CHAIN "gfp_thm1")
                                        (("2"
                                          (EXPAND "<=")
                                          (("2"
                                            (INST?)
                                            (("2"
                                              (REPLACE-ETA
                                               "gfp(pp!1)")
                                              (("2"
                                                (PROP)
                                                NIL)))))))))))))))))))))))))))))
                   ("2" (EXPAND "gfp")
                    (("2" (EXPAND "lub")
                      (("2" (EXPAND "NOT")
                        (("2" (SKOSIMP*)
                          (("2"
                            (INST +
                             "NOT lfp(LAMBDA p: NOT pp!1(NOT p))")
                            (("2"
                              (PROP)
                              (("1"
                                (EXPAND "member")
                                (("1"
                                  (LEMMA "lfp_thm")
                                  (("1"
                                    (INST
                                     -
                                     "(LAMBDA p: NOT pp!1(NOT p))")
                                    (("1"
                                      (PROP)
                                      (("1"
                                        (HIDE -2 -3)
                                        (("1"
                                          (EXPAND "<=")
                                          (("1"
                                            (SKOSIMP*)
                                            (("1"
                                              (INST?)
                                              (("1"
                                                (EXPAND "NOT")
                                                (("1"
                                                  (PROP)
                                                  NIL)))))))))))
                                       ("2"
                                        (HIDE -1 2)
                                        (("2"
                                          (EXPAND "ismono")
                                          (("2"
                                            (SKOSIMP*)
                                            (("2"
                                              (INST
                                               -
                                               "NOT p2!1"
                                               "NOT p1!1")
                                              (("2"
                                                (PROP)
                                                (("1"
                                                  (EXPAND "<=")
                                                  (("1"
                                                    (SKOSIMP*)
                                                    (("1"
                                                      (INST?)
                                                      (("1"
                                                        (EXPAND
                                                         "NOT")
                                                        (("1"
                                                          (PROP)
                                                          NIL)))))))))
                                                 ("2"
                                                  (EXPAND "NOT")
                                                  (("2"
                                                    (EXPAND "<=")
                                                    (("2"
                                                      (SKOSIMP*)
                                                      (("2"
                                                        (INST?)
                                                        (("2"
                                                          (PROP)
                                                          NIL)))))))))))))))))))))))))))
                               ("2"
                                (EXPAND "member")
                                (("2"
                                  (EXPAND "NOT" +)
                                  (("2"
                                    (EXPAND "lfp")
                                    (("2"
                                      (EXPAND "glb")
                                      (("2"
                                        (INST?)
                                        (("2"
                                          (EXPAND "member")
                                          (("2"
                                            (PROP)
                                            NIL)))))))))))))))))))))))))))))))))))))))))))
 (|mu_induction| "" (SKOSIMP*)
  (("" (EXPAND "mu")
    (("" (LEMMA "lfp_lem3")
      (("" (EXPAND "<=") (("" (GRIND) NIL))))))))))
$$$connectives.pvs
connectives [ T: TYPE ] : THEORY
%This theory contains the Boolean connectives lifted to
%predicates.		
  BEGIN

  f, g: VAR pred[T]
  u,v,w: VAR T

  AND(f,g)(u):bool =  f(u) AND g(u);
  OR(f,g)(u):bool =  f(u) OR g(u)
  NOT(f)(u):bool =  NOT f(u);
  IMPLIES(f,g)(u):bool = f(u) IMPLIES g(u);
  IFF(f,g)(u):bool = f(u) IFF g(u);

  TRUE(u) : bool = TRUE;
  FALSE(u) : bool = FALSE;



  END connectives

$$$mucalculus.pvs
% Defines fixpoints: parent of ctlops theory
mucalculus[T:TYPE]: THEORY

BEGIN

s: VAR T
p,p1,p2: VAR pred[T]
predtt: TYPE = [pred[T]->pred[T]]
pp: VAR predtt
setofpred: VAR pred[pred[T]]

IMPORTING orders[pred[T]]
<=(p1,p2):bool = FORALL s: p1(s) IMPLIES p2(s)

ismono(pp):bool =
    FORALL p1,p2: p1 <= p2 IMPLIES pp(p1) <= pp(p2)

isfix (pp,p):bool = (pp(p) = p)

glb (setofpred):pred[T] =
    LAMBDA s: (FORALL p: member(p,setofpred) IMPLIES  p(s))
				   

% least fixpoint
lfp (pp):pred[T] = glb({p | pp(p) <= p})

mu(pp): pred[T] = lfp(pp)

islfp (pp,p1):bool =
	isfix (pp,p1) AND
	FORALL p2: isfix (pp,p2) IMPLIES p1 <= p2

lub (setofpred):pred[T] = LAMBDA s: EXISTS p: member(p,setofpred) AND p(s)

% greatest fixpoint
gfp (pp):pred[T] = lub({p | p <= (pp(p))})

nu (pp):pred[T] = gfp(pp)

isgfp (pp,p1):bool =
	isfix (pp,p1) AND
	FORALL p2: isfix (pp,p2) IMPLIES p2 <= p1

END mucalculus



$$$ctlops.pvs
ctlops[state : TYPE]: THEORY
  %Basic CTL temporal operators (without fairness)
  %defined in mu-calculus
BEGIN

IMPORTING mucalculus[state], connectives[state]

u,v,w: VAR state
f,g,Q,P,p1,p2: VAR pred[state]
Z: VAR pred[[state, state]]

N: VAR [state, state->bool]

EX(N,f)(u):bool =  (EXISTS v: (f(v) AND N(u, v)))

EG(N,f):pred[state] = nu (LAMBDA Q: (f AND EX(N,Q)))

EU(N,f,g):pred[state] = mu (LAMBDA Q: (g OR (f AND EX(N,Q))))

% Other operator definitions
EF(N,f):pred[state] = EU(N,(LAMBDA u: TRUE),f)
AX(N,f):pred[state] = NOT EX(N, NOT f)
AF(N,f):pred[state] = NOT EG(N, NOT f)
AG(N,f):pred[state] = NOT EF(N, NOT f)
AU(N,f,g):pred[state] = NOT EU(N, NOT g, (NOT f AND NOT g))
		        AND AF(N,g)


END ctlops



fairctlops  [ state : TYPE ]: THEORY
  %Fair versions of CTL operators where
  %fairAG(N, f)(Ff)(s) means f always holds along every N-path
  %from s along which the fairness predicate Ff holds infinitely
  %often.  This is different from the usual linear-time notion of 
  %fairness where the strong form asserts that if an action A is 
  %enabled infinitely often, it is taken infinitely often, and the 
  %weak form asserts that if any action that is continuously enabled 
  %is taken infinitely often.  

  BEGIN
  IMPORTING ctlops[state]
  u,v,w: VAR state
  f,g,Q,P,p1,p2: VAR pred[state]
  N: VAR [state, state->bool]
  Ff: VAR pred[state] % Fair formula

fairEG(N, f)(Ff): pred[state] =
  nu(LAMBDA P: EU(N, f, f AND Ff AND EX(N, P)))

fairAF(N,f)(Ff):pred[state]  = NOT fairEG(N, NOT f)(Ff)

fair?(N,Ff):pred[state] = fairEG(N,LAMBDA u: TRUE)(Ff)

fairEX(N,f)(Ff):pred[state] = EX(N,f AND fair?(N,Ff))

fairEU(N,f,g)(Ff):pred[state] = EU(N,f,g AND fair?(N,Ff))

fairEF(N,f)(Ff):pred[state] = EF(N,f AND fair?(N,Ff))

fairAX(N,f)(Ff):pred[state] = NOT fairEX(N, NOT f)(Ff)

fairAG(N,f)(Ff):pred[state] = NOT fairEF(N,NOT f)(Ff)

fairAU(N,f,g)(Ff):pred[state] =
      NOT fairEU(N,NOT g,NOT f AND NOT g)(Ff)
          AND fairAF(N,g)(Ff)


  END fairctlops


Fairctlops  [ state : TYPE ]: THEORY
  %Fair versions of CTL operators with lists of fairness conditions.
  %FairAG(N,f)(Fflist)(s) means f always holds on every N-path from
  %s along which each predicate in Fflist holds infinitely often.

  BEGIN
  IMPORTING ctlops[state]
  u,v,w: VAR state
  f,g,Q,P,p1,p2: VAR pred[state]
  N: VAR [state, state->bool]
  Fflist, Gflist: VAR list[pred[state]] % Fair formula

CheckFair(Q, N, f, Fflist): RECURSIVE pred[state] =
  (CASES Fflist OF
   cons(Ff, Gflist):
           EU(N, f, f AND Ff AND
                    EX(N, CheckFair(Q, N, f, Gflist))),
   null : Q
   ENDCASES)
  MEASURE length(Fflist)

FairEG(N, f)(Fflist): pred[state] =
  nu(LAMBDA P: CheckFair(P, N, f, Fflist))

FairAF(N,f)(Fflist):pred[state]  = NOT FairEG(N, NOT f)(Fflist)

Fair?(N,Fflist):pred[state] = FairEG(N,LAMBDA u: TRUE)(Fflist)

FairEX(N,f)(Fflist):pred[state] = EX(N,f AND Fair?(N,Fflist))

FairEU(N,f,g)(Fflist):pred[state] = EU(N,f,g AND Fair?(N,Fflist))

FairEF(N,f)(Fflist):pred[state] = EF(N,f AND Fair?(N,Fflist))

FairAX(N,f)(Fflist):pred[state] = NOT FairEX(N, NOT f)(Fflist)

FairAG(N,f)(Fflist):pred[state] = NOT FairEF(N,NOT f)(Fflist)

FairAU(N,f,g)(Fflist):pred[state] =
      NOT FairEU(N,NOT g,NOT f AND NOT g)(Fflist)
          AND FairAF(N,g)(Fflist)


  END Fairctlops



$$$ctlthms.pvs
ctlthms  [T : TYPE ] : THEORY
%This theory contains some useful theorems about CTL
%operators.  Currently, only the AG operator is considered
%but theorems abot other operators will also be included.

  BEGIN

  IMPORTING ctlops[T], more_mucalculus_theorems[T]

  u,v,w: VAR T
  f,g,Q,P,p1,p2, I: VAR pred[T]
  F, G, Z: VAR pred[[T, T]]

%<= ordering on binary (next-state) predicates
  <=(F, G): bool =
   (FORALL u, v: F(u, v) IMPLIES G(u, v))

%de Morgan law for unary predicates.
     deMorgan: LEMMA ((NOT f) AND (NOT g)) = NOT (f OR g)

%Contraposition for unary predicates.
   contrapose: LEMMA (NOT g) <= (NOT f) = (f <= g)

%AG TRUE always holds.
  AG_true: LEMMA AG(F, (LAMBDA u: TRUE))(v)

%AG is contravariant in next-state argument, and covariant
%in formula argument.  
  AG_variance: LEMMA
      G <= F AND f <= g IMPLIES
      AG(F, f) <= AG(G, g)

%Restricts a next-state relation F to pre/post states
%satisfying an invariant I (write as F/I).
  restrict(F, I)(u, v): bool =
    (I(u) AND I(v) AND F(u, v))

%If AG f holds in F/I and AG I holds in F, then AG f holds in F.
  AG_invariance: LEMMA
     (AG(F, I) AND AG(restrict(F, I), f)) <= AG(F, f)

  END ctlthms

$$$ctlthms.prf
(|ctlthms|
 (|deMorgan| "" (GRIND)
  (("" (EXPAND* "NOT" "AND" "OR")
    (("" (APPLY-EXTENSIONALITY)
      (("" (BDDSIMP) (("" (PROPAX) NIL)))))))))
 (|contrapose| "" (GRIND) NIL)
 (|AG_true| "" (SKOSIMP*)
  (("" (GRIND :EXCLUDE ("lfp"))
    (("" (LEMMA "lfp_lem3")
      (("" (INST?)
        (("" (PROP)
          (("1" (INST - "LAMBDA u: FALSE")
            (("1" (PROP)
              (("1" (EXPAND "<=") (("1" (INST?) NIL)))
               ("2" (BETA)
                (("2" (EXPAND "<=")
                  (("2" (HIDE -1) (("2" (GRIND) NIL)))))))))))
           ("2" (HIDE -1)
            (("2" (GRIND :IF-MATCH NIL)
              (("2" (INST?)
                (("2" (INST?) (("2" (PROP) NIL)))))))))))))))))))
 (|AG_variance| "" (SKOSIMP*)
  (("" (EXPAND "AG")
    (("" (EXPAND "EF")
      (("" (EXPAND "EU")
        (("" (REWRITE "contrapose")
          (("" (EXPAND "mu")
            (("" (LEMMA "lfp_lem3")
              (("" (INST?)
                (("" (PROP)
                  (("1" (INST?)
                    (("1" (PROP)
                      (("1" (BETA)
                        (("1" (HIDE 2)
                          (("1"
                            (NAME-REPLACE "foo" "EX(G!1,
               lfp(LAMBDA (Q: pred[T]):
                     (NOT f!1 OR ((LAMBDA u: TRUE) AND EX(F!1, Q)))))")
                            (("1"
                              (REWRITE "lfp_thm2" :DIR RL)
                              (("1"
                                (REVEAL -1)
                                (("1"
                                  (REPLACE -1 :DIR RL :HIDE? T)
                                  (("1"
                                    (NAME-REPLACE
                                     "bar"
                                     "lfp(LAMBDA (Q: pred[T]):
                     (NOT f!1 OR ((LAMBDA u: TRUE) AND EX(F!1, Q))))")
                                    (("1"
                                      (EXPAND "<=")
                                      (("1"
                                        (SKOSIMP*)
                                        (("1"
                                          (EXPAND "NOT")
                                          (("1"
                                            (EXPAND "OR")
                                            (("1"
                                              (EXPAND "AND")
                                              (("1"
                                                (PROP)
                                                (("1"
                                                  (INST? -3)
                                                  (("1" (PROP) NIL)))
                                                 ("2"
                                                  (EXPAND "EX")
                                                  (("2"
                                                    (SKOSIMP*)
                                                    (("2"
                                                      (INST?)
                                                      (("2"
                                                        (INST? -4)
                                                        (("2"
                                                          (PROP)
                                                          NIL)))))))))))))))))))))))))))
                               ("2"
                                (HIDE 2)
                                (("2"
                                  (EXPAND "ismono")
                                  (("2"
                                    (GRIND :IF-MATCH NIL)
                                    (("2"
                                      (INST? +)
                                      (("2"
                                        (PROP)
                                        (("2"
                                          (INST? -)
                                          (("2"
                                            (PROP)
                                            NIL)))))))))))))))))))))))))
                   ("2" (HIDE 2)
                    (("2" (GRIND :IF-MATCH NIL)
                      (("2" (INST? +)
                        (("2" (PROP)
                          (("2" (INST? -)
                            (("2"
                              (PROP)
                              NIL)))))))))))))))))))))))))))))
 (|AG_invariance| "" (GRIND :IF-MATCH NIL :EXCLUDE ("lfp" "<="))
  (("" (REWRITE "deMorgan")
    (("" (REWRITE "contrapose")
      ((""
        (NAME-REPLACE "LFP1" "lfp(LAMBDA (Q: pred[T]):
                (NOT I!1 OR ((LAMBDA u: TRUE) AND EX(F!1, Q))))")
        ((""
          (NAME-REPLACE "LFP2" "lfp(LAMBDA (Q: pred[T]):
                  (NOT f!1
                       OR ((LAMBDA u: TRUE) AND EX(restrict(F!1, I!1), Q))))")
          (("" (LEMMA "lfp_lem3")
            (("" (INST?)
              (("" (PROP)
                (("1" (INST?)
                  (("1" (PROP)
                    (("1" (HIDE 2)
                      (("1" (BETA)
                        (("1"
                          (NAME-REPLACE "EXF"
                           "EX(F!1, (LFP1 OR LFP2))")
                          (("1" (REVEAL -4 -5)
                            (("1"
                              (REPLACE -1 :DIR RL)
                              (("1"
                                (REPLACE -2 :DIR RL)
                                (("1"
                                  (REWRITE
                                   "lfp_thm2"
                                   :DIR
                                   RL
                                   :TARGET-FNUMS
                                   +)
                                  (("1"
                                    (REPLACE -1 :HIDE? T)
                                    (("1"
                                      (REWRITE
                                       "lfp_thm2"
                                       :DIR
                                       RL
                                       :TARGET-FNUMS
                                       +)
                                      (("1"
                                        (REPLACE -1 :HIDE? T)
                                        (("1"
                                          (REVEAL -1)
                                          (("1"
                                            (REPLACE
                                             -1
                                             :DIR
                                             RL
                                             :HIDE?
                                             T)
                                            (("1"
                                              (GRIND :IF-MATCH NIL)
                                              (("1"
                                                (INST? +)
                                                (("1" (PROP) NIL)))
                                               ("2"
                                                (INST? 2)
                                                (("2"
                                                  (PROP)
                                                  (("2"
                                                    (INST?)
                                                    (("2"
                                                      (PROP)
                                                      (("2"
                                                        (REVEAL -5)
                                                        (("2"
                                                          (REPLACE
                                                           -1
                                                           :DIR
                                                           RL)
                                                          (("2"
                                                            (STOP-REWRITE)
                                                            (("2"
                                                              (REWRITE
                                                               "lfp_thm2"
                                                               :DIR
                                                               RL
                                                               :TARGET-FNUMS
                                                               +)
                                                              (("1"
                                                                (REPLACE
                                                                 -1
                                                                 :HIDE?
                                                                 T)
                                                                (("1"
                                                                  (GRIND
                                                                   :IF-MATCH
                                                                   NIL)
                                                                  NIL)))
                                                               ("2"
                                                                (HIDE
                                                                 -1
                                                                 2)
                                                                (("2"
                                                                  (GRIND
                                                                   :IF-MATCH
                                                                   NIL)
                                                                  (("2"
                                                                    (INST?)
                                                                    (("2"
                                                                      (INST?)
                                                                      (("2"
                                                                        (PROP)
                                                                        NIL)))))))))))))))))))))))))))))))))
                                       ("2"
                                        (HIDE -1 2)
                                        (("2"
                                          (GRIND :IF-MATCH NIL)
                                          (("2"
                                            (INST?)
                                            (("2"
                                              (INST?)
                                              (("2"
                                                (PROP)
                                                NIL)))))))))))))
                                   ("2"
                                    (HIDE -1 -2 2)
                                    (("2"
                                      (GRIND :IF-MATCH NIL)
                                      (("2"
                                        (INST?)
                                        (("2"
                                          (INST?)
                                          (("2"
                                            (PROP)
                                            NIL)))))))))))))))))))))))))))
                 ("2" (HIDE 2)
                  (("2" (GRIND :IF-MATCH NIL)
                    (("2" (INST?)
                      (("2" (INST?)
                        (("2" (PROP) NIL))))))))))))))))))))))))))
$$$abstraction.pvs
abstraction  [cstate, astate : TYPE ]
		: THEORY
%Contains the main results on correct abstractions for AG
%properties.  good_abstraction? says that abst is a good
%abstraction from concrete program  (satisfying
%invariant I) to an abstract program  for the
%purpose of proving AG(Cprop) from abstract property AG(Aprop)
%if Cinit implies Ainit o abst, C/I implies A o ,
%and I and Aprop o abst implies Cprop.
  BEGIN

   IMPORTING ctlthms

    abst: VAR [cstate -> astate]
    C : VAR PRED[[cstate, cstate]]
    A : VAR PRED[[astate, astate]]
    Cinit, Cprop : VAR PRED[cstate]
    Ainit, Aprop : VAR PRED[astate]
    I : VAR PRED[cstate]


   good_abstraction?(abst, Cinit, C, Cprop, Ainit, A, Aprop, I): bool = 
   ( (FORALL (u : cstate): Cinit(u) IMPLIES  Ainit(abst(u)))
    AND (FORALL (u, v: cstate):  restrict(C, I)(u, v)
          IMPLIES A(abst(u), abst(v)))
    AND (FORALL (u: cstate): I(u) AND Aprop(abst(u)) IMPLIES Cprop(u))
  )

%If A, abst(a) |= AG(Aprop),
%then A o , a |= Aprop o abst
  abstraction_step: LEMMA
  (FORALL (v: cstate):
      AG(A, Aprop)(abst(v))
    IMPLIES
      AG(LAMBDA (u, v: cstate): A(abst(u), abst(v)),
           LAMBDA (u: cstate): Aprop(abst(u)))(v))

% v |= I and C/I, v |= AG(Cprop), then C/I, v |= AG(I /\ Cprop)
%namely v |= I implies C/I, v |= AG(I).  It takes some thought
%to convince oneself that the I(v) antecedent is needed.  
  restrict_AG: LEMMA
      (FORALL (v: cstate):
           I(v) AND
           AG(restrict(C, I), Cprop)(v) IMPLIES
           AG(restrict(C, I), (LAMBDA (u: cstate): I(u) AND Cprop(u)))(v))

%This is the main theorem: it asserts that if abst is a good abstraction,
%the abstract program satisfies Aprop, the concrete program satisfies
%the abstraction invariant I, then the concrete program satisfies Cprop.
  good_abstraction_works: LEMMA
    good_abstraction?(abst, Cinit, C, Cprop, Ainit, A, Aprop, I)
   AND (FORALL (a: astate): Ainit(a) IMPLIES AG(A, Aprop)(a))
   AND (FORALL (u: cstate): Cinit(u) IMPLIES AG(C, I)(u))
   IMPLIES (FORALL (v: cstate): Cinit(v) IMPLIES AG(C, Cprop)(v))

  END abstraction

$$$abstraction.prf
(|abstraction|
 (|abstraction_step| "" (SKOSIMP*)
  (("" (EXPAND "AG")
    (("" (EXPAND "EF")
      (("" (EXPAND "EU")
        (("" (EXPAND "NOT")
          (("" (EXPAND "mu")
            (("" (LEMMA "lfp_lem3[cstate]")
              (("" (INST?)
                (("" (PROP)
                  (("1"
                    (INST -
                     "LAMBDA (u : cstate): lfp(LAMBDA (Q: pred[astate]):
           ((LAMBDA (a: astate): NOT Aprop!1(a))
                OR ((LAMBDA (a : astate): TRUE) AND EX(A!1, Q))))(abst!1(u))")
                    (("1" (PROP)
                      (("1" (EXPAND "<=")
                        (("1" (INST?) (("1" (PROP) NIL)))))
                       ("2" (HIDE -1 2)
                        (("2" (BETA)
                          (("2"
                            (NAME-REPLACE "EXP"
                             "EX(LAMBDA (u, v: cstate): A!1(abst!1(u), abst!1(v)),
               LAMBDA (u: cstate):
                 lfp(LAMBDA (Q: pred[astate]):
                       ((LAMBDA (a: astate): NOT Aprop!1(a))
                            OR
                          ((LAMBDA (a: astate): TRUE)
                               AND EX(A!1, Q))))(abst!1(u)))")
                            (("2"
                              (REWRITE "lfp_thm2" :DIR RL)
                              (("1"
                                (REVEAL -1)
                                (("1"
                                  (REPLACE -1 :DIR RL)
                                  (("1"
                                    (HIDE -1)
                                    (("1"
                                      (NAME-REPLACE
                                       "LFP"
                                       "lfp(LAMBDA (Q: pred[astate]):
                       ((LAMBDA (a: astate): NOT Aprop!1(a))
                            OR
                          ((LAMBDA (a: astate): TRUE)
                               AND EX(A!1, Q))))")
                                      (("1"
                                        (EXPAND "<=")
                                        (("1"
                                          (GRIND :IF-MATCH NIL)
                                          (("1"
                                            (INST?)
                                            (("1"
                                              (PROP)
                                              NIL)))))))))))))))
                               ("2"
                                (HIDE 2)
                                (("2"
                                  (GRIND :IF-MATCH NIL)
                                  (("2"
                                    (INST?)
                                    (("2"
                                      (INST?)
                                      (("2"
                                        (PROP)
                                        NIL)))))))))))))))))))))
                   ("2" (HIDE -1 2)
                    (("2" (GRIND :IF-MATCH NIL)
                      (("2" (INST?)
                        (("2" (INST?)
                          (("2" (PROP) NIL)))))))))))))))))))))))))))
 (|restrict_AG| "" (SKOSIMP*)
  (("" (EXPAND "AG")
    (("" (EXPAND "EF")
      (("" (EXPAND "EU")
        (("" (EXPAND "NOT")
          (("" (EXPAND "mu")
            (("" (LEMMA "lfp_lem3[cstate]")
              (("" (INST? :WHERE -)
                (("" (PROP)
                  (("1"
                    (NAME-REPLACE "LFP2"
                     "lfp(LAMBDA (Q: pred[cstate]):
                     (LAMBDA (u: cstate): NOT Cprop!1(u))
                          OR
                        ((LAMBDA (u : cstate): TRUE)
                             AND EX(restrict(C!1, I!1), Q)))")
                    (("1" (INST - "(NOT I!1) OR LFP2")
                      (("1" (BETA)
                        (("1" (PROP)
                          (("1" (EXPAND "<=")
                            (("1"
                              (INST?)
                              (("1"
                                (PROP)
                                (("1"
                                  (HIDE -3)
                                  (("1" (GRIND) NIL)))))))))
                           ("2" (HIDE -2 2)
                            (("2"
                              (EXPAND "<=")
                              (("2"
                                (SKOSIMP*)
                                (("2"
                                  (REVEAL -3)
                                  (("2"
                                    (REPLACE -1 + :DIR RL)
                                    (("2"
                                      (REWRITE
                                       "lfp_thm2"
                                       :TARGET-FNUMS
                                       +
                                       :DIR
                                       RL)
                                      (("1"
                                        (REPLACE -1 :HIDE? T)
                                        (("1"
                                          (GRIND :IF-MATCH NIL)
                                          (("1"
                                            (INST?)
                                            (("1" (PROP) NIL)))))))
                                       ("2"
                                        (HIDE -1 -2 -3 2)
                                        (("2"
                                          (GRIND :IF-MATCH NIL)
                                          (("2"
                                            (INST?)
                                            (("2"
                                              (INST?)
                                              (("2"
                                                (PROP)
                                                NIL)))))))))))))))))))))))))))))
                   ("2" (HIDE -1 -2 2)
                    (("2" (GRIND :IF-MATCH NIL)
                      (("2" (INST?)
                        (("2" (INST?)
                          (("2" (PROP) NIL)))))))))))))))))))))))))))
 (|good_abstraction_works| "" (SKOSIMP*)
  (("" (INST? -3)
    (("" (PROP)
      (("" (LEMMA "AG_invariance[cstate]")
        (("" (INST - "C!1" "I!1" "Cprop!1")
          (("" (EXPAND "<=")
            (("" (INST?)
              (("" (PROP)
                (("" (EXPAND "AND")
                  (("" (PROP)
                    (("" (LEMMA "AG_variance[cstate]")
                      ((""
                        (INST -
                         "restrict(LAMBDA (u, v: cstate): A!1(abst!1(u), abst!1(v)), I!1)"
                         "restrict(C!1, I!1)"
                         "LAMBDA (u: cstate): I!1(u) AND Aprop!1(abst!1(u))"
                         "Cprop!1")
                        (("" (PROP)
                          (("1" (EXPAND "<=")
                            (("1"
                              (INST?)
                              (("1"
                                (PROP)
                                (("1"
                                  (REWRITE "restrict_AG")
                                  (("1"
                                    (HIDE -2 -3 -4 2 3 4)
                                    (("1"
                                      (GRIND
                                       :IF-MATCH
                                       NIL
                                       :EXCLUDE
                                       "lfp")
                                      (("1"
                                        (REWRITE "lfp_thm2" :DIR RL)
                                        (("1"
                                          (GRIND
                                           :IF-MATCH
                                           NIL
                                           :EXCLUDE
                                           ("lfp" EX))
                                          NIL)
                                         ("2"
                                          (HIDE 2 3)
                                          (("2"
                                            (GRIND :IF-MATCH NIL)
                                            (("2"
                                              (INST?)
                                              (("2"
                                                (INST?)
                                                (("2"
                                                  (PROP)
                                                  NIL)))))))))))))))
                                   ("2"
                                    (LEMMA "AG_variance[cstate]")
                                    (("2"
                                      (INST
                                       -
                                       "(LAMBDA (u, v: cstate): A!1(abst!1(u), abst!1(v)))"
                                       "restrict(LAMBDA (u, v: cstate): A!1(abst!1(u), abst!1(v)), I!1)"
                                       "LAMBDA (u: cstate): Aprop!1(abst!1(u))"
                                       "LAMBDA (u: cstate): Aprop!1(abst!1(u))")
                                      (("2"
                                        (PROP)
                                        (("1"
                                          (EXPAND "<=")
                                          (("1"
                                            (INST?)
                                            (("1"
                                              (PROP)
                                              (("1"
                                                (REWRITE
                                                 "abstraction_step")
                                                (("1"
                                                  (INST?)
                                                  (("1"
                                                    (PROP)
                                                    (("1"
                                                      (EXPAND
                                                       "good_abstraction?")
                                                      (("1"
                                                        (FLATTEN)
                                                        (("1"
                                                          (INST? -2)
                                                          (("1"
                                                            (PROP)
                                                            NIL)))))))))))))))))))
                                         ("2"
                                          (HIDE 2 3 4)
                                          (("2"
                                            (EXPAND "<=")
                                            (("2"
                                              (EXPAND "restrict")
                                              (("2"
                                                (SKOSIMP*)
                                                NIL)))))))
                                         ("3"
                                          (HIDE 2 3 4)
                                          (("3"
                                            (EXPAND "<=")
                                            (("3"
                                              (SKOSIMP*)
                                              NIL)))))))))))))))))))
                           ("2" (HIDE 2 3)
                            (("2"
                              (EXPAND "good_abstraction?")
                              (("2"
                                (FLATTEN)
                                (("2"
                                  (EXPAND "<=")
                                  (("2"
                                    (SKOSIMP*)
                                    (("2"
                                      (INST? -4)
                                      (("2"
                                        (PROP)
                                        (("2"
                                          (EXPAND "restrict")
                                          (("2"
                                            (PROP)
                                            NIL)))))))))))))))))
                           ("3" (EXPAND "good_abstraction?")
                            (("3"
                              (FLATTEN)
                              (("3"
                                (EXPAND "<=")
                                (("3"
                                  (PROPAX)
                                  NIL))))))))))))))))))))))))))))))))))