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