---

Step * of Lemma term_accum_mkterm_lemma

No Annotations
∀p,bts,f,M,varcase,Q:Top.
  (term-accum(mkterm(f;bts) with p)
   a,b,c,d.Q[a;b;c;d]
   varterm(x) with p ⇒ varcase[p;x]
   mkterm(f,bts) with p ⇒ trs.M[p;f;bts;trs] ~ let trs = accumulate (with value d and list item bt):
                                                           let p' = Q[p;f;fst(bt);d] in
                                                               d
                                                               @ [<snd(bt)
                                                                  , p'
                                                                  , term-accum(snd(bt) with p')
                                                                    a,b,c,d.Q[a;b;c;d]
                                                                    varterm(x) with p ⇒ varcase[p;x]
                                                                    mkterm(f,bts) with p ⇒ trs.M[p;f;bts;trs]>]
                                                          over list:
                                                            bts
                                                          with starting value:
                                                           []) in
                                                    M[p;f;bts;trs])
BY
{ ((Intros THEN RW (AddrC [1] (TagC (mk_tag_term 4))) 0)
   THEN Reduce 0
   THEN Auto
   THEN (RW (AddrC [2] (TagC (mk_tag_term 3))) 0 THEN Reduce 0)
   THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}p,bts,f,M,varcase,Q:Top.
    (term-accum(mkterm(f;bts)  with  p)
      a,b,c,d.Q[a;b;c;d]
      varterm(x)  with  p  {}\mRightarrow{}  varcase[p;x]
      mkterm(f,bts)  with  p  {}\mRightarrow{}  trs.M[p;f;bts;trs] 
    \msim{}  let  trs  =  accumulate  (with  value  d  and  list  item  bt):
                              let  p'  =  Q[p;f;fst(bt);d]  in
                                      d
                                      @  [<snd(bt)
                                            ,  p'
                                            ,  term-accum(snd(bt)  with  p')
                                                a,b,c,d.Q[a;b;c;d]
                                                varterm(x)  with  p  {}\mRightarrow{}  varcase[p;x]
                                                mkterm(f,bts)  with  p  {}\mRightarrow{}  trs.M[p;f;bts;trs]>]
                            over  list:
                                bts
                            with  starting  value:
                              [])  in
                M[p;f;bts;trs])


By

---

Latex:
((Intros  THEN  RW  (AddrC  [1]  (TagC  (mk\_tag\_term  4)))  0)
  THEN  Reduce  0
  THEN  Auto
  THEN  (RW  (AddrC  [2]  (TagC  (mk\_tag\_term  3)))  0  THEN  Reduce  0)
  THEN  Auto)

---

Home Index