proposition: Lemma fold_next2s_correct p ps ss : (forall i, In i (fst (fst (fold_left (next2s p) (snd ps) (fst ps, ss)))) <-> In i (fst (fst ps)) \/ exists f, exists s, In f movel /\ In s (snd ps) /\ i = f s /\ ~In i (snd (fst ps)) /\ is_odd p) /\ (forall i, In i (snd (fst (fold_left (next2s p) (snd ps) (fst ps, ss)))) <-> In i (snd (fst ps)) \/ exists f, exists s, In f movel /\ In s (snd ps) /\ i = f s /\ ~In i (fst (fst ps)) /\ p <> 1%positive) /\ (forall i, In i (snd (fold_left (next2s p) (snd ps) (fst ps, ss))) <-> In i ss \/ exists f, exists s, In f movel /\ In s (snd ps) /\ i = f s /\ ~In i (fst (fst ps)) /\ ~In i (snd (fst ps))).
proof: Proof. destruct ps as (ss1, ss2); simpl fst; simpl snd. generalize ss1 ss; elim ss2; clear ss ss1 ss2; auto. - unfold fold_left, fst, snd. intros ss1 ss; split; [idtac | split]; intros; split; auto. + intros [H1 | H1]; auto. case H1; intros f (i1, (_, (HH, _))); case HH. + intros [H1 | H1]; auto. case H1; intros f (i1, (_, (HH, _))); case HH. + intros [H1 | H1]; auto. case H1; intros f (i1, (_, (HH, _))); case HH. - intros s1 ss2 Hrec ss1 ss. rewrite fold_left_cons. generalize (next2s_correct p (ss1, ss) s1); case next2s; simpl fst; simpl snd; intros (ss3, ss4) ss5 (Hss3, (Hss4, Hss5)). simpl fst in Hss3, Hss4, Hss5; simpl snd in Hss3, Hss4, Hss5. split; [idtac | split]. + intros s; case (Hrec (ss3, ss4) ss5); intros Hr1 (Hr2, Hr3); clear Hrec. apply iff_trans with (1 := Hr1 s); simpl fst; simpl snd; clear Hr1 Hr2 Hr3. split; intros [H1 | H1]. * rewrite Hss3 in H1; case H1; auto. intros (f, (Hf1, (Hf2, Hf3))); subst s; right; exists f; exists s1; auto with datatypes. * case H1; intros f (i, (Hf1, (Hf2, (Hf3, (Hf4, Hf5))))); subst s; right; exists f; exists i; repeat split; auto with datatypes. intros H2; case Hf4. rewrite Hss4; auto. * left; unfold lequiv in Hss3; rewrite Hss3; auto. * case H1; intros f (i, (Hf1, (Hf2, (Hf3, (Hf4, Hf5))))); subst; auto; clear H1. simpl in Hf2; case Hf2; clear Hf2; intros Hf2; subst; auto. -- left; rewrite Hss3; auto. right; exists f; auto. -- generalize (in_states_correct (f i) ss3); case in_states; auto; intros H3. right; exists f; exists i; repeat split; auto. rewrite Hss4. intros [HH | HH]; auto. case H3; rewrite Hss3; auto. case HH; intros f1 (Gf1, (Gf2, (Gf3, Gf4))). right; exists f1; split; auto. + intros s; case (Hrec (ss3, ss4) ss5); intros Hr1 (Hr2, Hr3); clear Hrec. apply iff_trans with (1 := Hr2 s); simpl fst; simpl snd; clear Hr1 Hr2 Hr3. split; intros [H1 | H1]. * rewrite Hss4 in H1; case H1; auto. intros (f, (Hf1, (Hf2, Hf3))); subst s; right; exists f; exists s1; auto with datatypes. * case H1; intros f (i, (Hf1, (Hf2, (Hf3, (Hf4, Hf5))))); subst s; right; exists f; exists i; repeat split; auto with datatypes. intros H2; case Hf4. rewrite Hss3; auto. * left; rewrite Hss4; auto. * case H1; intros f (i, (Hf1, (Hf2, (Hf3, (Hf4, Hf5))))); subst; auto; clear H1. simpl in Hf2; case Hf2; clear Hf2; intros Hf2; subst; auto. -- left; rewrite Hss4; auto. right; exists f; auto. -- generalize (in_states_correct (f i) ss4); case in_states; auto; intros H3. right; exists f; exists i; repeat split; auto. rewrite Hss3. intros [HH | HH]; auto. case H3; rewrite Hss4; auto. case HH; intros f1 (Gf1, (Gf2, (Gf3, Gf4))). right; exists f1; split; auto. + intros s; case (Hrec (ss3, ss4) ss5); intros Hr1 (Hr2, Hr3); clear Hrec. apply iff_trans with (1 := Hr3 s); simpl fst; simpl snd; clear Hr1 Hr2 Hr3. split; intros [H1 | H1]. * rewrite Hss5 in H1; case H1; auto. intros (f, (Hf1, (Hf2, Hf3))); subst s; right; exists f; exists s1; auto with datatypes. * case H1; intros f (i, (Hf1, (Hf2, (Hf3, (Hf4, Hf5))))); subst s; right; exists f; exists i; repeat split; auto with datatypes. -- intros H2; case Hf4. rewrite Hss3; auto. -- intros H2; case Hf5. rewrite Hss4; auto. * left; rewrite Hss5; auto. * case H1; intros f (i, (Hf1, (Hf2, (Hf3, (Hf4, Hf5))))); subst; auto; clear H1. simpl in Hf2; case Hf2; clear Hf2; intros Hf2; subst; auto. -- left; rewrite Hss5; auto. right; exists f; auto. -- generalize (in_states_correct (f i) ss5); case in_states; auto; intros H3. right; exists f; exists i; repeat split; auto. ++ rewrite Hss3. intros [HH | HH]; auto. case H3; rewrite Hss5; auto; clear H3. case HH; intros f1 (Gf1, (Gf2, (Gf3, Gf4))). right; exists f1; split; auto. ++ rewrite Hss4; intros [HH | HH]. ** case Hf5; auto. ** case HH; intros f1 (Gf1, (Gf2, (Gf3, Gf4))). case H3; rewrite Hss5. right; exists f1; auto. Qed.
imports: ZArith List