---

Step * of Lemma TC-ind-ext

∀[Dom:Type]. ∀[B:Dom ─→ ℙ]. ∀[R:Dom ─→ Dom ─→ ℙ].
  ((∀x,y:Dom.  ((R x y) ⇒ (B x) ⇒ (B y))) ⇒ (∀x,y:Dom.  (TC(λa,b.R a b)(x,y) ⇒ (B x) ⇒ (B y))))
BY
{ (NewUseNormalizedExtract ``null list_ind list_accum hd tl`` false (ioid Obid: TC-ind)⋅
   THEN All (Fold `spread3`)
   THEN Assert ⌈λF,x,y,L,z. let a,b,w = accumulate (with value x and list item y):
                                         let a,b,q = x in 
                                         let b',c,r = y in 
                                         <a, c, λz.(F b c r (q z))>
                                        over list:
                                          tl(L)
                                        with starting value:
                                         let a,b,r = hd(L) in 
                                         <x, b, λz.(F x b r z)>) in 
                           w z ∈ ∀[Dom:Type]. ∀[B:Dom ─→ ℙ]. ∀[R:Dom ─→ Dom ─→ ℙ].
                         ((∀x,y:Dom.  ((R x y) ⇒ (B x) ⇒ (B y)))
                         ⇒ (∀x,y:Dom.  (TC(λa,b.R a b)(x,y) ⇒ (B x) ⇒ (B y))))⌉⋅
   THEN Try (Trivial)) }

---

Latex:


\mforall{}[Dom:Type].  \mforall{}[B:Dom  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[R:Dom  {}\mrightarrow{}  Dom  {}\mrightarrow{}  \mBbbP{}].
    ((\mforall{}x,y:Dom.    ((R  x  y)  {}\mRightarrow{}  (B  x)  {}\mRightarrow{}  (B  y)))  {}\mRightarrow{}  (\mforall{}x,y:Dom.    (TC(\mlambda{}a,b.R  a  b)(x,y)  {}\mRightarrow{}  (B  x)  {}\mRightarrow{}  (B  y))))


By

(NewUseNormalizedExtract  ``null  list\_ind  list\_accum  hd  tl``  false  (ioid  Obid:  TC-ind)\mcdot{}
  THEN  All  (Fold  `spread3`)
  THEN  Assert  \mkleeneopen{}\mlambda{}F,x,y,L,z.  let  a,b,w  =  accumulate  (with  value  x  and  list  item  y):
                                                                              let  a,b,q  =  x  in 
                                                                              let  b',c,r  =  y  in 
                                                                              <a,  c,  \mlambda{}z.(F  b  c  r  (q  z))>
                                                                            over  list:
                                                                                tl(L)
                                                                            with  starting  value:
                                                                              let  a,b,r  =  hd(L)  in 
                                                                              <x,  b,  \mlambda{}z.(F  x  b  r  z)>)  in 
                                                  w  z  \mmember{}  \mforall{}[Dom:Type].  \mforall{}[B:Dom  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[R:Dom  {}\mrightarrow{}  Dom  {}\mrightarrow{}  \mBbbP{}].
                                              ((\mforall{}x,y:Dom.    ((R  x  y)  {}\mRightarrow{}  (B  x)  {}\mRightarrow{}  (B  y)))
                                              {}\mRightarrow{}  (\mforall{}x,y:Dom.    (TC(\mlambda{}a,b.R  a  b)(x,y)  {}\mRightarrow{}  (B  x)  {}\mRightarrow{}  (B  y))))\mkleeneclose{}\mcdot{}
  THEN  Try  (Trivial))

---

Home Index