---

Step * 2 of Lemma member-all-vars-mkterm


1. [opr] : Type
2. f : opr
3. v : varname()
4. u1 : varname() List
5. u2 : term(opr)
6. v1 : bound-term(opr) List
7. ∀L:varname() List
     ((v ∈ accumulate (with value as and list item bt):
            let vs,a = bt 
            in all-vars(a) ⋃ vs ⋃ as
           over list:
             v1
           with starting value:
            L))
     ⇐⇒ (v ∈ L) ∨ (∃bt:bound-term(opr). ((bt ∈ v1) ∧ ((v ∈ fst(bt)) ∨ (v ∈ all-vars(snd(bt)))))))
8. L : varname() List
9. bt : bound-term(opr)
10. (bt ∈ v1)
11. (v ∈ fst(bt)) ∨ (v ∈ all-vars(snd(bt)))
⊢ (v ∈ L) ∨ (∃bt:bound-term(opr). ((bt ∈ [<u1, u2> / v1]) ∧ ((v ∈ fst(bt)) ∨ (v ∈ all-vars(snd(bt))))))
BY
{ ((OrRight THENA Auto) THEN D 0 With ⌜bt⌝  THEN Auto) }

---

Latex:

---

Latex:

1.  [opr]  :  Type
2.  f  :  opr
3.  v  :  varname()
4.  u1  :  varname()  List
5.  u2  :  term(opr)
6.  v1  :  bound-term(opr)  List
7.  \mforall{}L:varname()  List
          ((v  \mmember{}  accumulate  (with  value  as  and  list  item  bt):
                        let  vs,a  =  bt 
                        in  all-vars(a)  \mcup{}  vs  \mcup{}  as
                      over  list:
                          v1
                      with  starting  value:
                        L))
          \mLeftarrow{}{}\mRightarrow{}  (v  \mmember{}  L)  \mvee{}  (\mexists{}bt:bound-term(opr).  ((bt  \mmember{}  v1)  \mwedge{}  ((v  \mmember{}  fst(bt))  \mvee{}  (v  \mmember{}  all-vars(snd(bt)))))))
8.  L  :  varname()  List
9.  bt  :  bound-term(opr)
10.  (bt  \mmember{}  v1)
11.  (v  \mmember{}  fst(bt))  \mvee{}  (v  \mmember{}  all-vars(snd(bt)))
\mvdash{}  (v  \mmember{}  L)
\mvee{}  (\mexists{}bt:bound-term(opr).  ((bt  \mmember{}  [<u1,  u2>  /  v1])  \mwedge{}  ((v  \mmember{}  fst(bt))  \mvee{}  (v  \mmember{}  all-vars(snd(bt))))))


By

---

Latex:
((OrRight  THENA  Auto)  THEN  D  0  With  \mkleeneopen{}bt\mkleeneclose{}    THEN  Auto)

---

Home Index