---

Step * of Lemma transitive-closure-minimal-ext

∀[A:Type]. ∀[R,Q:A ⟶ A ⟶ ℙ].  (R => Q ⇒ Trans(A;x,y.x Q y) ⇒ TC(R) => Q)
BY
{ xxxExtract of Obid: transitive-closure-minimal
     not unfolding  map list_accum hd tl
     finishing with Auto
     normalizes to:
     
     λF,trans,x,y,L. let a,b,w = accumulate (with value x and list item y):
                                  let a,b,q1 = x in 
                                  let b',c,r = y in 
                                  <a, c, trans a b c q1 (F b c r)>
                                 over list:
                                   tl(L)
                                 with starting value:
                                  let a,b,r = hd(L) in 
                                  <x, b, F x b r>) in 
                    wxxx }

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[R,Q:A  {}\mrightarrow{}  A  {}\mrightarrow{}  \mBbbP{}].    (R  =>  Q  {}\mRightarrow{}  Trans(A;x,y.x  Q  y)  {}\mRightarrow{}  TC(R)  =>  Q)


By

---

Latex:
xxxExtract  of  Obid:  transitive-closure-minimal
      not  unfolding    map  list\_accum  hd  tl
      finishing  with  Auto
      normalizes  to:
     
      \mlambda{}F,trans,x,y,L.  let  a,b,w  =  accumulate  (with  value  x  and  list  item  y):
                                                                let  a,b,q1  =  x  in 
                                                                let  b',c,r  =  y  in 
                                                                <a,  c,  trans  a  b  c  q1  (F  b  c  r)>
                                                              over  list:
                                                                  tl(L)
                                                              with  starting  value:
                                                                let  a,b,r  =  hd(L)  in 
                                                                <x,  b,  F  x  b  r>)  in 
                                    wxxx

---

Home Index