Step * of Lemma transitive-closure-minimal-ext

[A:Type]. ∀[R,Q:A ⟶ A ⟶ ℙ].  (R =>  Trans(A;x,y.x 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 and list item y):
                                  let a,b,q1 in 
                                  let b',c,r in 
                                  <a, c, trans q1 (F r)>
                                 over list:
                                   tl(L)
                                 with starting value:
                                  let a,b,r hd(L) in 
                                  <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