Step * of Lemma ancestral-logic-example2-ext

x,y:Dom.  (TC(λa,b.TC(λi,j.P j)(a,b))(x,y)  TC(λa,b.P 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 and list item y):
                         let b,c,r in 
                         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 j)(a,b))(x,y)  TC(λa,b.P 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