proposition: Theorem state_loop_order_wf : forall (b:bExp) (i:inst), forLoops (WhileDo b i) -> well_founded (state_loop_order i b).
proof: Proof. intros b i h; inversion h. apply wf_incl with (fun s1 s2:state => Zwf 0 (extract_option (evalA s1 variant) 0%Z) (extract_option (evalA s2 variant) 0%Z)). unfold Relation_Definitions.inclusion in |- *. unfold state_loop_order in |- *; intros x y [H3 H4]. apply H1. apply H3. apply H4. apply (wf_inverse_image state Z (Zwf 0) (fun s:state => extract_option (evalA s variant) 0%Z) (Zwf_well_founded 0)). Qed.
imports: ZArith Zwf Inverse_Image Wellfounded Extraction