proposition: Lemma EquivAssignables_trans: forall p st st' st'', let x := st@fr@assignables in let x' := st'@fr@assignables in let x'' := st''@fr@assignables in EquivAssignables p st st' -> EquivAssignables p st' st'' -> min (length x) (length x'') <= length x' -> EquivAssignables p st st''.
proof: Proof. intros. unfold EquivAssignables in *; replace (FrameAdds.assignables (State.Frame.adds (State.fr st))) with x in * by trivial; replace (FrameAdds.assignables (State.Frame.adds (State.fr st'))) with x' in * by trivial; replace (FrameAdds.assignables (State.Frame.adds (State.fr st''))) with x'' in * by trivial. elim Nat.min_dec with (length x) (length x''); intro. rewrite a in H1. apply min_L in a. generalize H1. generalize a. intros. apply level_le in a0. apply level_le in H2. rewrite <- a0 in |- *. rewrite <- H2 in H. unfold level in H0. case_eq (Nat.compare (length x') (length x'')); intros; rewrite H3 in H0. apply EquivAssignables_ind_truncated with (n := length x) in H0. apply EquivAssignables_ind_trans with (h' := State.h st') (a' := truncate (length x) x'); trivial. apply truncate_1. trivial. rewrite <- truncate_1 in |- *; trivial. apply truncate_1; trivial. apply nat_compare_Eq in H3; trivial. apply EquivAssignables_ind_truncated with (n := length x) in H0. rewrite <- truncate_truncate in H0. apply EquivAssignables_ind_trans with (h' := State.h st') (a' := truncate (length x) x'); trivial. apply truncate_1. trivial. rewrite <- truncate_1 in |- *; trivial. apply truncate_1; trivial. trivial. apply truncate_1. apply nat_compare_lt in H3; auto with *. apply EquivAssignables_ind_truncated with (n := length x) in H0. rewrite <- truncate_truncate in H0. apply EquivAssignables_ind_trans with (h' := State.h st') (a' := truncate (length x) x'); trivial. apply truncate_1. trivial. rewrite <- truncate_1 in |- *; trivial. apply truncate_1; trivial. trivial. symmetry in |- *. apply truncate_1. apply nat_compare_gt in H3; auto with *. rewrite b in H1. apply min_R in b. generalize H1. generalize b. intros. rewrite le_ge in b0. rewrite le_ge in H2. apply level_ge in b0. apply level_ge in H2. rewrite <- b0 in |- *. rewrite <- H2 in H0. unfold level in H. case_eq (Nat.compare (length x) (length x')); intros; rewrite H3 in H. apply EquivAssignables_ind_truncated with (n := length x'') in H. apply EquivAssignables_ind_trans with (h' := State.h st') (a' := truncate (length x'') x'); trivial. repeat rewrite <- truncate_1 in |- *; trivial. symmetry in |- *. apply truncate_1; trivial. apply nat_compare_Eq in H3; trivial. apply EquivAssignables_ind_truncated with (n := length x'') in H. rewrite <- truncate_truncate in H. apply EquivAssignables_ind_trans with (h' := State.h st') (a' := truncate (length x'') x'); trivial. repeat rewrite <- truncate_1 in |- *; trivial. symmetry in |- *. apply truncate_1; trivial. trivial. apply truncate_1. apply nat_compare_lt in H3; auto with *. apply EquivAssignables_ind_truncated with (n := length x'') in H. rewrite <- truncate_truncate in H. apply EquivAssignables_ind_trans with (h' := State.h st') (a' := truncate (length x'') x'); trivial. repeat rewrite <- truncate_1 in |- *; trivial. symmetry in |- *. apply truncate_1. trivial. apply nat_compare_gt in H3; auto with *. symmetry in |- *. apply truncate_1. apply nat_compare_gt in H3; auto with *. Qed.
imports: Coq(List) JML(Stack) Coq(ListSet) Coq(Bool) Coq(ZArith) Coq(Relation_Operators) JML(ListHelpers) Coq(Classical)