---

Step * 1 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. 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))
BY
{ ((Unfold `var-deq` 0 THEN Reduce 0 THEN Fold `var-deq` 0)
   THEN (BoolCase ⌜eq_var(u;v)⌝⋅ THENA Auto)
   THEN BoolCase ⌜eq_var(u1;v1)⌝⋅
   THEN Auto) }

---

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.  u  :  varname()
6.  v2  :  varname()  List
7.  \mforall{}bnds2:varname()  List
          ((\muparrow{}same-binding(v2;bnds2;v;v1))
          {}\mRightarrow{}  (if  v  \mmember{}\msubb{}  v2  then  []  else  [v]  fi    =  if  v1  \mmember{}\msubb{}  bnds2  then  []  else  [v1]  fi  ))
8.  u1  :  varname()
9.  v3  :  varname()  List
10.  (\muparrow{}same-binding([u  /  v2];v3;v;v1))
{}\mRightarrow{}  (if  v  \mmember{}\msubb{}  [u  /  v2]  then  []  else  [v]  fi    =  if  v1  \mmember{}\msubb{}  v3  then  []  else  [v1]  fi  )
\mvdash{}  (\muparrow{}case  eq\_var(u;v)
  of  inl($_{}$)  =>
  eq\_var(u1;v1)
  |  inr($_{}$)  =>
  (\mneg{}\msubb{}eq\_var(u1;v1))  \mwedge{}\msubb{}  same-binding(v2;v3;v;v1))
{}\mRightarrow{}  (if  (VarDeq  u  v)  \mvee{}\msubb{}v  \mmember{}\msubb{}  v2  then  []  else  [v]  fi 
      =  if  (VarDeq  u1  v1)  \mvee{}\msubb{}v1  \mmember{}\msubb{}  v3  then  []  else  [v1]  fi  )


By

---

Latex:
((Unfold  `var-deq`  0  THEN  Reduce  0  THEN  Fold  `var-deq`  0)
  THEN  (BoolCase  \mkleeneopen{}eq\_var(u;v)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  BoolCase  \mkleeneopen{}eq\_var(u1;v1)\mkleeneclose{}\mcdot{}
  THEN  Auto)

---

Home Index