```\$\$\$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))))))))))))))))))))))))))))))))))
```