---

Step * of Lemma member-all-vars-mkterm

No Annotations
∀[opr:Type]
  ∀f:opr. ∀v:varname(). ∀bts:bound-term(opr) List.
    ((v ∈ all-vars(mkterm(f;bts))) ⇐⇒ ∃bt:bound-term(opr). ((bt ∈ bts) ∧ ((v ∈ fst(bt)) ∨ (v ∈ all-vars(snd(bt))))))
BY
{ (Intros
   THEN Unfold  `mkterm` 0
   THEN RW (AddrC [1;2] (UnfoldTopC `all-vars`)) 0
   THEN Reduce 0
   THEN (Enough to prove ∀L:varname() List
                           ((v ∈ accumulate (with value as and list item bt):
                                  let vs,a = bt 
                                  in all-vars(a) ⋃ vs ⋃ as
                                 over list:
                                   bts
                                 with starting value:
                                  L))
                           ⇐⇒ (v ∈ L)
                               ∨ (∃bt:bound-term(opr). ((bt ∈ bts) ∧ ((v ∈ fst(bt)) ∨ (v ∈ all-vars(snd(bt)))))))
          Because (RWO "-1" 0 THEN Auto))
   THEN ListInd (-1)
   THEN Reduce 0
   THEN (((D 0 THENA Auto) THEN RWO "-2" 0 THEN Auto THEN DVar `u' THEN All Reduce THEN SplitOrHyps THEN ExRepD)
   ORELSE ((Auto THEN ExRepD) THEN Auto)
   )) }

1
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 ∈ all-vars(u2) ⋃ u1 ⋃ L)
⊢ (v ∈ L) ∨ (∃bt:bound-term(opr). ((bt ∈ [<u1, u2> / v1]) ∧ ((v ∈ fst(bt)) ∨ (v ∈ all-vars(snd(bt))))))

2
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))))))

3
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))))))

4
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 ∈ [<u1, u2> / v1])
11. (v ∈ fst(bt)) ∨ (v ∈ all-vars(snd(bt)))
⊢ (v ∈ all-vars(u2) ⋃ u1 ⋃ L) ∨ (∃bt:bound-term(opr). ((bt ∈ v1) ∧ ((v ∈ fst(bt)) ∨ (v ∈ all-vars(snd(bt))))))

---

Latex:

---

Latex:
No  Annotations
\mforall{}[opr:Type]
    \mforall{}f:opr.  \mforall{}v:varname().  \mforall{}bts:bound-term(opr)  List.
        ((v  \mmember{}  all-vars(mkterm(f;bts)))
        \mLeftarrow{}{}\mRightarrow{}  \mexists{}bt:bound-term(opr).  ((bt  \mmember{}  bts)  \mwedge{}  ((v  \mmember{}  fst(bt))  \mvee{}  (v  \mmember{}  all-vars(snd(bt))))))


By

---

Latex:
(Intros
  THEN  Unfold    `mkterm`  0
  THEN  RW  (AddrC  [1;2]  (UnfoldTopC  `all-vars`))  0
  THEN  Reduce  0
  THEN  (Enough  to  prove  \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:
                                                                  bts
                                                              with  starting  value:
                                                                L))
                                                  \mLeftarrow{}{}\mRightarrow{}  (v  \mmember{}  L)
                                                          \mvee{}  (\mexists{}bt:bound-term(opr)
                                                                  ((bt  \mmember{}  bts)  \mwedge{}  ((v  \mmember{}  fst(bt))  \mvee{}  (v  \mmember{}  all-vars(snd(bt)))))))
                Because  (RWO  "-1"  0  THEN  Auto))
  THEN  ListInd  (-1)
  THEN  Reduce  0
  THEN  (((D  0  THENA  Auto)
                THEN  RWO  "-2"  0
                THEN  Auto
                THEN  DVar  `u'
                THEN  All  Reduce
                THEN  SplitOrHyps
                THEN  ExRepD)
  ORELSE  ((Auto  THEN  ExRepD)  THEN  Auto)
  ))

---

Home Index