Skip to content

Instantly share code, notes, and snippets.

@yoshihiro503

yoshihiro503/rsc_trans.v

Created February 23, 2013 08:21
Show Gist options
  • Save yoshihiro503/5018946 to your computer and use it in GitHub Desktop.
Save yoshihiro503/5018946 to your computer and use it in GitHub Desktop.
Download ZIP
「ソフトウェアの基礎」Rel_J 練習問題 rsc_trans の証明
Raw
rsc_trans.v
(** **** 練習問題:★★, optional(rsc_trans) *)
Theorem rsc_trans :
forall (X:Type) (R: relation X) (x y z : X),
refl_step_closure R x y ->
refl_step_closure R y z ->
refl_step_closure R x z.
Proof.
intros. induction H.
apply H0.
apply rsc_step with y.
apply H.
apply IHrefl_step_closure. apply H0.
Qed.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment