proposition: Theorem rac2_length_assignables_correct: forall p, (forall e st st' s, OpRac2.ExpressionStep p e st st' s -> (length st@fr@assignables) = (length st'@fr@assignables)) /\ (forall l st st' s, OpRac2.ListSteps p l st st' s -> (length st@fr@assignables) = (length st'@fr@assignables)) /\ (forall m b st st' s, OpRac2.StatementStep p m b st st' s -> (length st@fr@assignables) = (length st'@fr@assignables)) /\ (forall m b st st' s, OpRac2.BlockStep p m b st st' s -> (length st@fr@assignables) = (length st'@fr@assignables)).
proof: Proof. intro p. apply OpRac2.mutual_ind; intros; simpl in *; subst; trivial. simpl. unfold Assignables.FieldUpdateAction. case isPivot. simpl. rewrite map_length. rewrite H2. assumption. rewrite H2. assumption. simpl. rewrite H1. rewrite H6. simpl in H15. apply eq_add_S. rewrite H15. unfold pop. destruct st_c' @fr @assignables. discriminate H15. trivial. rewrite H1. assumption. rewrite H1. assumption. Qed.
imports: Coq(List)