---

Step * 1 1 1 of Lemma free-vars_functionality


1. opr : Type
2. v : {v:varname()| ¬(v = nullvar() ∈ varname())} 
3. varterm(v) ∈ term(opr)
4. v1 : {v:varname()| ¬(v = nullvar() ∈ varname())} 
5. bnds1 : varname() List
6. bnds2 : varname() List
7. ↑same-binding(bnds1;bnds2;v;v1)
⊢ if v ∈b bnds1 then [] else [v] fi  = if v1 ∈b bnds2 then [] else [v1] fi  ∈ (varname() List)
BY
{ ((RepeatFor 2 (MoveToConcl (-1)) THEN ListInd (-1))
   THEN InductionOnList
   THEN (Unfold `same-binding` 0 THEN Reduce 0)
   THEN Try (((D 0 THENM FalseHD (-1)) THEN Auto))
   THEN Try (((D 0 THENM Progress(RW  assert_pushdownC (-1))) THEN Auto))) }

1
1. opr : Type
2. v : {v:varname()| ¬(v = nullvar() ∈ varname())} 
3. varterm(v) ∈ term(opr)
4. v1 : {v:varname()| ¬(v = nullvar() ∈ varname())} 
5. u : varname()
6. v2 : varname() List
7. ∀bnds2:varname() List
     ((↑same-binding(v2;bnds2;v;v1))
     ⇒ (if v ∈b v2 then [] else [v] fi  = if v1 ∈b bnds2 then [] else [v1] fi  ∈ (varname() List)))
8. u1 : varname()
9. v3 : varname() List
10. (↑same-binding([u / v2];v3;v;v1))
⇒ (if v ∈b [u / v2] then [] else [v] fi  = if v1 ∈b v3 then [] else [v1] fi  ∈ (varname() List))
⊢ (↑case eq_var(u;v) of inl(_) => eq_var(u1;v1) | inr(_) => (¬beq_var(u1;v1)) ∧b same-binding(v2;v3;v;v1))
⇒ (if (VarDeq u v) ∨bv ∈b v2 then [] else [v] fi 
   = if (VarDeq u1 v1) ∨bv1 ∈b v3 then [] else [v1] fi 
   ∈ (varname() List))

---

Latex:

---

Latex:

1.  opr  :  Type
2.  v  :  \{v:varname()|  \mneg{}(v  =  nullvar())\} 
3.  varterm(v)  \mmember{}  term(opr)
4.  v1  :  \{v:varname()|  \mneg{}(v  =  nullvar())\} 
5.  bnds1  :  varname()  List
6.  bnds2  :  varname()  List
7.  \muparrow{}same-binding(bnds1;bnds2;v;v1)
\mvdash{}  if  v  \mmember{}\msubb{}  bnds1  then  []  else  [v]  fi    =  if  v1  \mmember{}\msubb{}  bnds2  then  []  else  [v1]  fi 


By

---

Latex:
((RepeatFor  2  (MoveToConcl  (-1))  THEN  ListInd  (-1))
  THEN  InductionOnList
  THEN  (Unfold  `same-binding`  0  THEN  Reduce  0)
  THEN  Try  (((D  0  THENM  FalseHD  (-1))  THEN  Auto))
  THEN  Try  (((D  0  THENM  Progress(RW    assert\_pushdownC  (-1)))  THEN  Auto)))

---

Home Index