proposition: Theorem Infinite_bs : forall (q:states A1) (t:LList acts), Trace A1 q t -> satisfies t (F_Infinite (Atomic (eq b))).
proof: Proof. cofix Infinite_bs. intros q; case q. - intros t Ht; case (from_q0 Ht). intros x [tx [ea| eb]]. + rewrite ea; split. * case (from_q2 tx). intros x0 [[t2| t1] e]; rewrite e; auto with llists. * split. case (from_q2 tx). intros x0 [_ e]; rewrite e; auto with llists. apply Infinite_bs with q2; auto. + rewrite eb; split. * auto with llists. * case (from_q2 tx). intros x0 [_ e]; rewrite e. split. auto with llists. case e; apply Infinite_bs with q2; auto. - intros t Ht; case (from_q1 Ht). intros x [tx e]; rewrite e. split. + case (from_q2 tx). intros x0 [_ e']; rewrite e'; auto with llists. + apply Infinite_bs with q2; auto. - intros t Ht; case (from_q2 Ht). intros x [[t1| t2] e]; rewrite e. split. + auto with llists. + apply Infinite_bs with q2; auto. + split. * auto with llists. * apply Infinite_bs with q1; auto. Qed.
imports: Arith List RelationClasses