Re: [Hol-info] transitive closure

Note that any relation A satisfying !u v z. A u v /\ A u z ==> (u = z) must be a subset of the identity relation. Specialise the above with x, y, y and you get A x y /\ A x y ==> x = y Michael On 30/05/14 02:39, David Sanan wrote: > Hi all, > I am trying to prove this simple property over

Re: [Hol-info] transitive closure

Hi David, I think you could prove your goal with METIS_TAC[EQ_TC_SETS]. (Or even METIS_TAC[TC_RULES].) Alternatively, you could do STRIP_TAC THEN MATCH_MP EQ_TC_SETS and simplification would probably take it from there. Ramana On Thu, May 29, 2014 at 5:39 PM, David Sanan wrote: > Hi all, > I

[Hol-info] transitive closure

Hi all, I am trying to prove this simple property over the transition closure of a relation Next, which is defined used Hol_reln, ((TC (Next h l)) x y) /\ ((TC (Next h l)) x x) /\ (!u v z.((Next h l) u v) /\ ((Next h l) u z) ==> u=z) ==> (((TC (Next h l)) x)=((TC (Next h l)) y)) For that

[Hol-info] Workshop "Human-Oriented Formal Methods" @SEFM 2014

[Apologies if you receive multiple copies of this message] *CALL FOR PAPERS* *HOFM 2014: Human-Oriented Formal Methods Workshop * *co-located to SEFM*, 12th International Conference on Software Engineering and Formal Methods (Grenoble, France) http://hofm2014.w

[Hol-info] First Call for Papers: FSEN 2015

Our apologies if you have received multiple copies.   ## FIRST CALL FOR PAPERS   Sixth International Conference on Fundamentals of Software Engineering 2015 Theory and Practice (FSEN '15) http