---

Step * 1 of Lemma es-le-trans2


1. es : EO@i'
2. a : E@i
3. b : E@i
4. c : E@i
5. a ≤loc b @i
6. (b <loc c)@i
⊢ (a <loc c)
BY
{ MaybeNOOP (skip{(\p. let R1 = h 5 p in
                        let R2 = h 6 p in
                         let e = env_of_sequent p in
                          (let ra,a,b = dest_rel_term_without_check R1 in
                                  let rb,b',c = dest_rel_term_without_check R2 in
                                  let rc = compose_rels ra rb in
                                  let xxx = transitivity_cache_lookup (name_of_rel (get_std_rel rc)) in
                                  let (ra',rb',rc'),ttt = hd (tl xxx) in
                                  let kind1,fam1,root1 = identify_rel ra in
                                  let kind2,fam2,root2 = identify_rel ra' in
                                  SeqOnM [(%AddHiddenLabel (name_of_rel rb')%
                                            Assert (mk_integer_term (length xxx)))] p)⋅)⋅}) }

1
1. es : EO@i'
2. a : E@i
3. b : E@i
4. c : E@i
5. a ≤loc b @i
6. (b <loc c)@i
⊢ (a <loc c)

---

Latex:



1.  es  :  EO@i'
2.  a  :  E@i
3.  b  :  E@i
4.  c  :  E@i
5.  a  \mleq{}loc  b  @i
6.  (b  <loc  c)@i
\mvdash{}  (a  <loc  c)


By

MaybeNOOP  (skip\{(\mbackslash{}p. 
                                let  R1  =  h  5  p  in
                                  let  R2  =  h  6  p  in
                                    let  e  =  env\_of\_sequent  p  in
                                      (let  ra,a,b  =  dest\_rel\_term\_without\_check  R1  in
                                                      let  rb,b',c  =  dest\_rel\_term\_without\_check  R2  in
                                                      let  rc  =  compose\_rels  ra  rb  in
                                                      let  xxx  =  transitivity\_cache\_lookup  (name\_of\_rel  (get\_std\_rel  rc))  in
                                                      let  (ra',rb',rc'),ttt  =  hd  (tl  xxx)  in
                                                      let  kind1,fam1,root1  =  identify\_rel  ra  in
                                                      let  kind2,fam2,root2  =  identify\_rel  ra'  in
                                                      SeqOnM  [(\%AddHiddenLabel  (name\_of\_rel  rb')\%
                                                                          Assert  (mk\_integer\_term  (length  xxx)))]  p)\mcdot{})\mcdot{}\})

---

Home Index