From fce0354efc424a9b92a46ecb629c554f387a1c3d Mon Sep 17 00:00:00 2001
From: Alejandro Gomez-Londono <alegomez544@gmail.com>
Date: Wed, 16 May 2018 17:25:02 +0200
Subject: [PATCH] Add handy RTC related lemma

---
 projection/proofs/endpointPropsScript.sml | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/projection/proofs/endpointPropsScript.sml b/projection/proofs/endpointPropsScript.sml
index 6560982..085ede5 100644
--- a/projection/proofs/endpointPropsScript.sml
+++ b/projection/proofs/endpointPropsScript.sml
@@ -7,6 +7,10 @@ val RTC_SANDWICH = Q.store_thm("RTC_SANDWICH",
   `!R a b c d. R^* a b /\ R b c /\ R^* c d ==> R^* a d`,
   metis_tac[RTC_RTC,RTC_SINGLE])
 
+val RTC_SPLIT = Q.store_thm("RTC_SPLIT",
+  `∀R x y z. R^* x z ∧ R^* z y ⇒ R^* x y`,
+  metis_tac[RTC_RTC,RTC_SINGLE])
+
 val INDEX_FIND_normalize = Q.store_thm("INDEX_FIND_normalize",
   `!l n. OPTION_MAP SND (INDEX_FIND n f l) = OPTION_MAP SND (INDEX_FIND 0 f l)`,
   Induct_on `l` >> rpt strip_tac >> rw[INDEX_FIND_def]);