---

Step * of Lemma ancestral-logic-example2-ext

∀x,y:Dom.  (TC(λa,b.TC(λi,j.P i j)(a,b))(x,y) ⇒ TC(λa,b.P a b)(x,y))
BY
{ (NewUseNormalizedExtract ``map list_accum hd tl append`` false (ioid Obid: ancestral-logic-example2)⋅
   THEN All (Fold `spread3`)
   THEN Assert ⌈λx,y,L. accumulate (with value q and list item y):
                         let b,c,r = y in 
                         q @ r
                        over list:
                          tl(L)
                        with starting value:
                         let a,b,r = hd(L) in 
                         r) ∈ ∀x,y:Dom.  (TC(λa,b.TC(λi,j.P i j)(a,b))(x,y) ⇒ TC(λa,b.P a b)(x,y))⌉⋅
   THEN Trivial) }

---

Latex:


\mforall{}x,y:Dom.    (TC(\mlambda{}a,b.TC(\mlambda{}i,j.P  i  j)(a,b))(x,y)  {}\mRightarrow{}  TC(\mlambda{}a,b.P  a  b)(x,y))


By

(NewUseNormalizedExtract  ``map  list\_accum  hd  tl  append``  false  (ioid  Obid:  ancestral-logic-example2)
  \mcdot{}
  THEN  All  (Fold  `spread3`)
  THEN  Assert  \mkleeneopen{}\mlambda{}x,y,L.  accumulate  (with  value  q  and  list  item  y):
                                              let  b,c,r  =  y  in 
                                              q  @  r
                                            over  list:
                                                tl(L)
                                            with  starting  value:
                                              let  a,b,r  =  hd(L)  in 
                                              r)  \mmember{}  \mforall{}x,y:Dom.    (TC(\mlambda{}a,b.TC(\mlambda{}i,j.P  i  j)(a,b))(x,y)  {}\mRightarrow{}  TC(\mlambda{}a,b.P  a  b)(x,y))\mkleeneclose{}\mcdot{}
  THEN  Trivial)

---

Home Index