proposition: Lemma exec_forLoop : forall (i i':inst) (b:bExp) (s:state), i = WhileDo b i' -> forLoops (WhileDo b i') -> forall f:forall s:state, exec_or_not s i', exec_or_not s i.
proof: Proof. intros i i' b s heq h' f; apply (well_founded_induction (state_loop_order_wf b i' h') (fun s:state => exec_or_not s i)). intros s0 loop_again. case_eq (evalB s0 b). - intros vb; case vb. + intros heqCond; elim (f s0). * intros s1 Hexeci'; elim (loop_again s1). intros s2 Hexeci; apply (result s0 i s2). rewrite heq. apply execWhileTrue with (s1 := s1); try assumption. rewrite <- heq. apply Hexeci. intros Hnot; apply no_result. rewrite heq; intros s' H; inversion H. rewrite H2 in heqCond. rewrite heqCond in H4. discriminate H4. elim (Hnot s'). rewrite (exec_det s0 s1 s3 i'); try assumption. rewrite heq. assumption. split; assumption. * intros Hnot; apply no_result. rewrite heq; intros s' H; inversion H. rewrite H2 in heqCond; rewrite H4 in heqCond. discriminate. elim (Hnot s2); assumption. + intros heqCond; apply (result s0 i s0). rewrite heq. apply execWhileFalse; assumption. - intros heqCond; apply no_result. rewrite heq. intros s' H; inversion H. rewrite H2 in heqCond. rewrite H4 in heqCond; discriminate heqCond. rewrite H2 in heqCond. discriminate heqCond. Defined.
imports: ZArith Zwf Inverse_Image Wellfounded Extraction