Right now the proof window looks like this:
1 subgoals
Case := "WHILE" : String.string
b : bexp
c : com
IHc : forall st' st : state,
optimize_0plus_com c / st || st' -> c / st || st'
st : state
st' : state
st'' : state
H0 : optimize_0plus_com c / st || st'
IHceval1 : optimize_0plus_com c = optimize_0plus_com (WHILE b DO c END) ->
(WHILE b DO c END) / st || st'
H : beval st (optimize_0plus_bexp b) = true
Heqloopdef : (WHILE optimize_0plus_bexp b DO optimize_0plus_com c END) =
optimize_0plus_com (WHILE b DO c END)
H1 : (WHILE optimize_0plus_bexp b DO optimize_0plus_com c END) / st' || st''
IHceval2 : (WHILE optimize_0plus_bexp b DO optimize_0plus_com c END) =
optimize_0plus_com (WHILE b DO c END) ->
(WHILE b DO c END) / st' || st''
______________________________________(1/1)
(WHILE b DO c END) / st || st''
I feel like this should be provable fairly easily, but I just can't see how to do it. The IHceval hypotheses in the context are close to what I need but they aren't an exact match. Can someone help me out here?