---

Step * 3 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. (v ∈ L)
⊢ (v ∈ all-vars(u2) ⋃ u1 ⋃ L) ∨ (∃bt:bound-term(opr). ((bt ∈ v1) ∧ ((v ∈ fst(bt)) ∨ (v ∈ all-vars(snd(bt))))))
BY
{ (OrLeft THEN Auto THEN RWW "member-union" 0 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.  (v  \mmember{}  L)
\mvdash{}  (v  \mmember{}  all-vars(u2)  \mcup{}  u1  \mcup{}  L)
\mvee{}  (\mexists{}bt:bound-term(opr).  ((bt  \mmember{}  v1)  \mwedge{}  ((v  \mmember{}  fst(bt))  \mvee{}  (v  \mmember{}  all-vars(snd(bt))))))


By

---

Latex:
(OrLeft  THEN  Auto  THEN  RWW  "member-union"  0  THEN  Auto)

---

Home Index