---

Step * of Lemma transitive-closure-induction-ext

∀[A:Type]. ∀[P:A ⟶ ℙ]. ∀[R:A ⟶ A ⟶ ℙ].
  ((∀x,y:A.  ((x R y) ⇒ P[x] ⇒ P[y])) ⇒ (∀x,y:A.  ((x TC(R) y) ⇒ P[x] ⇒ P[y])))
BY
{ Extract of Obid: transitive-closure-induction
  not unfolding null list_accum hd tl
  finishing with Auto
  normalizes to:
  
  λF,x,y,L,Px. let a,b,r = accumulate (with value x and list item y):
                            let a,b,rx = x in 
                            let b',c,ry = y in 
                            <a, c, λz.(F b c ry (rx z))>
                           over list:
                             tl(L)
                           with starting value:
                            let a,b,r = hd(L) in 
                            <x, b, F x b r>) in 
              r Px }

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[P:A  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[R:A  {}\mrightarrow{}  A  {}\mrightarrow{}  \mBbbP{}].
    ((\mforall{}x,y:A.    ((x  R  y)  {}\mRightarrow{}  P[x]  {}\mRightarrow{}  P[y]))  {}\mRightarrow{}  (\mforall{}x,y:A.    ((x  TC(R)  y)  {}\mRightarrow{}  P[x]  {}\mRightarrow{}  P[y])))


By

---

Latex:
Extract  of  Obid:  transitive-closure-induction
not  unfolding  null  list\_accum  hd  tl
finishing  with  Auto
normalizes  to:

\mlambda{}F,x,y,L,Px.  let  a,b,r  =  accumulate  (with  value  x  and  list  item  y):
                                                    let  a,b,rx  =  x  in 
                                                    let  b',c,ry  =  y  in 
                                                    <a,  c,  \mlambda{}z.(F  b  c  ry  (rx  z))>
                                                  over  list:
                                                      tl(L)
                                                  with  starting  value:
                                                    let  a,b,r  =  hd(L)  in 
                                                    <x,  b,  F  x  b  r>)  in 
                        r  Px

---

Home Index