---

Step * of Lemma ancestral-logic-example1-ext

(∀x,y:Dom.  ((P x y) ⇒ (Q x y))) ⇒ (∀x,y:Dom.  (TC(λa,b.P a b)(x,y) ⇒ TC(λa,b.Q a b)(x,y)))
BY
{ NormalizeExtract{100:n, list_accum hd tl append:t}(Obid: ancestral-logic-example1;
                                                     λF,x,y,L. accumulate (with value q and list item y):
                                                                let b,c,r = y in 
                                                                q @ [<b, c, F b c r>]
                                                               over list:
                                                                 tl(L)
                                                               with starting value:
                                                                let a,b,r = hd(L) in 
                                                                [<a, b, F a b r>]);
                                                     (RepUR ``cons nil it`` 0⋅ THEN Trivial)) }

---

Latex:


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


By

NormalizeExtract\{100:n,  list\_accum  hd  tl  append:t\}
    (Obid:  ancestral-logic-example1;
      \mlambda{}F,x,y,L.  accumulate  (with  value  q  and  list  item  y):
                            let  b,c,r  =  y  in 
                            q  @  [<b,  c,  F  b  c  r>]
                          over  list:
                              tl(L)
                          with  starting  value:
                            let  a,b,r  =  hd(L)  in 
                            [<a,  b,  F  a  b  r>]);
      (RepUR  ``cons  nil  it``  0\mcdot{}  THEN  Trivial))

---

Home Index