# Re: EXPAND and IF-THEN?

```> However, if you're bound and determined to proceed along this path of
> proving everything at once, here's the proof file for the "first"
> case, that avoids the evil pvs halting expansions.  Note, however,
> that in this case, the theorem isn't true, (you end up having to
> show....
>
> 	validCertificate = unknown
>
> which I'm assuming is false) The trick on proving complicated theorems
> about record updates like you have here is to work "outside in."  Then
> when you get to a point where the field is updated, the rest of the
> expansions can be ignored.
>

Bah, A good night's sleep caused me to see the light.  The "first"
case of your proof is valid, I'll append the proof.  I didn't trying
to prove the rest of your theorem.  Primarily because I'm just blindly
proving things, I've no idea how the proof is "supposed" to go.  But
the point is that if you don't expand everything at once, you can push
the theorem through the theorem prover.

Good luck,

John

==============================++======================
John Hoffman, PhD             ||
Secure Computing Corporation  || Sushi is good?
2675 Long Lake Road           ||     Life is good!
Roseville, MN  55124          ||
hoffman@securecomputing.com   ||
Fax  :(612)628-2701           ||  - Origami Sushi Chef
Phone:(612)628-2808           ||
==============================++======================

--------------------

(""
(USE "initialAEGISServices")
(FLATTEN)
(SIMPLIFY)
(SPLIT)
(("1"
(EXPAND "saneBoot")
(EXPAND "getResource")
(EXPAND "executeBootSequence")
(EXPAND "executeService")
(LIFT-IF)
(SPLIT)
(("1"
(FLATTEN)
(HIDE -1)
(REPLACE -6)
(HIDE -1 -2 -3 -4 -5 -6)
(EXPAND "levelZeroBoot")
(LIFT-IF)
(SPLIT)
(("1"
(FLATTEN)
(HIDE -1)
(EXPAND "executeService")
(LIFT-IF)
(SPLIT)
(("1"
(FLATTEN)
(HIDE -1)
(REVEAL -7)
(REPLACE -1)
(HIDE -1)
(EXPAND "levelOneBoot")
(LIFT-IF)
(SPLIT)
(("1"
(FLATTEN)
(HIDE -1)
(EXPAND "executeService")
(LIFT-IF)
(SPLIT)
(("1"
(FLATTEN)
(HIDE -1)
(REVEAL -8)
(REPLACE -1)
(HIDE -1)
(EXPAND "levelTwoBoot")
(LIFT-IF)
(SPLIT)
(("1"
(FLATTEN)
(HIDE -1)
(EXPAND "executeService")
(LIFT-IF)
(SPLIT)
(("1"
(FLATTEN)
(HIDE -1)
(REVEAL -9)
(REPLACE -1)
(HIDE -1)
(EXPAND "levelThreeBoot")
(LIFT-IF)
(SPLIT)
(("1"
(FLATTEN)
(HIDE -1)
(EXPAND "executeService")
(LIFT-IF)
(SPLIT)
(("1"
(FLATTEN)
(HIDE -1)
(REVEAL -10)
(REPLACE -1)
(HIDE -1)
(EXPAND "levelFourBoot")
(LIFT-IF)
(SPLIT)
(("1"
(FLATTEN)
(HIDE -1)
(EXPAND "executeService")
(LIFT-IF)
(SPLIT)
(("1"
(FLATTEN)
(HIDE -1)
(REVEAL -11)
(REPLACE -1)
(HIDE -1)
(EXPAND "levelFiveBoot")
(EXPAND "installAEGISResources")
(EXPAND "installResource")
(ASSERT)
(REVEAL -1 -2 -3 -4 -5 -6 -7 -8 -9 -10)
(SIMPLIFY)
(EXPAND "integrityValid" -4)
(EXPAND "getResource" -4)
(EXPAND "getBootLevelResource" -4)
(EXPAND "installAEGISResources" -4)
(EXPAND "installResource" -4)
(PROPAX))
("2" (POSTPONE))))
("2" (POSTPONE))))
("2" (POSTPONE))))
("2" (POSTPONE))))
("2" (POSTPONE))))
("2" (POSTPONE))))
("2" (POSTPONE))))
("2" (POSTPONE))))
("2" (POSTPONE))))
("2" (POSTPONE))))
("2" (POSTPONE))))
("2" (POSTPONE)) ("3" (POSTPONE)) ("4" (POSTPONE)) ("5" (POSTPONE))))

```