proposition: Lemma termination : forall x : Z, exists c : Config, legal x c /\ ~ (exists t : transition c, True).
proof: Proof. intro; case (Z_lt_ge_dec x 0); intros. split with (mkconfig x). split. apply legal_x_x. apply blocked; simpl in |- *; omega. split with (mkconfig 0%Z); split. apply fin_O; auto with arith. apply blocked; simpl in |- *; auto with zarith. Qed.
imports: ZArith Omega