---

Step * of Lemma ancestral-logic-induction-ext

(∀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 ``list_accum map append hd tl`` false (ioid Obid: ancestral-logic-induction)⋅
   THEN All (Fold `spread3`)
   THEN Assert ⌜λF,x,y,L. accumulate (with value q and list item y):
                           let b,c,r = y in 
                           λw.(F b c r (q w))
                          over list:
                            tl(L)
                          with starting value:
                           let a,b,r = hd(L) in 
                           F a b r) ∈ (∀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 Trivial) }

---

Latex:

---

Latex:
(\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

---

Latex:
(NewUseNormalizedExtract  ``list\_accum  map  append  hd  tl``  false  (ioid  Obid:  ancestral-logic-induction
  )\mcdot{}
  THEN  All  (Fold  `spread3`)
  THEN  Assert  \mkleeneopen{}\mlambda{}F,x,y,L.  accumulate  (with  value  q  and  list  item  y):
                                                  let  b,c,r  =  y  in 
                                                  \mlambda{}w.(F  b  c  r  (q  w))
                                                over  list:
                                                    tl(L)
                                                with  starting  value:
                                                  let  a,b,r  =  hd(L)  in 
                                                  F  a  b  r)  \mmember{}  (\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  Trivial)

---

Home Index