Step * 1 1 1 1 1 1 1 4 of Lemma alpha-rename-equivalent

.....antecedent..... 
1. varname()
2. bnds varname() List
⊢ ∀aaaa:varname(). ∀LLLL:varname() List.
    ((∀F:{v@0:varname()| (v@0 ∈ LLLL)}  ⟶ varname()
        ((v ∈ LLLL)  Inj({v@0:varname()| (v@0 ∈ LLLL)} ;varname();F)  (↑same-binding(map(F;LLLL);LLLL;F v;v))))
     (∀F:{v@0:varname()| (v@0 ∈ [aaaa LLLL])}  ⟶ varname()
          ((v ∈ [aaaa LLLL])
           Inj({v@0:varname()| (v@0 ∈ [aaaa LLLL])} ;varname();F)
           (↑same-binding(map(F;[aaaa LLLL]);[aaaa LLLL];F v;v)))))
BY
(All Thin
   THEN RepeatFor (Intro)
   THEN RenameVar `u' (-2)
   THEN RenameVar `bnds' (-1)
   THEN (Assert bnds ∈ {v:varname()| (v ∈ bnds)}  List BY
               Auto)
   THEN Intros) }

1
1. varname()
2. varname()
3. bnds varname() List
4. bnds ∈ {v:varname()| (v ∈ bnds)}  List
5. ∀F:{v@0:varname()| (v@0 ∈ bnds)}  ⟶ varname()
     ((v ∈ bnds)  Inj({v@0:varname()| (v@0 ∈ bnds)} ;varname();F)  (↑same-binding(map(F;bnds);bnds;F v;v)))
6. {v@0:varname()| (v@0 ∈ [u bnds])}  ⟶ varname()
7. (v ∈ [u bnds])
8. Inj({v@0:varname()| (v@0 ∈ [u bnds])} ;varname();F)
⊢ ↑same-binding(map(F;[u bnds]);[u bnds];F v;v)


Latex:


Latex:
.....antecedent..... 
1.  v  :  varname()
2.  bnds  :  varname()  List
\mvdash{}  \mforall{}aaaa:varname().  \mforall{}LLLL:varname()  List.
        ((\mforall{}F:\{v@0:varname()|  (v@0  \mmember{}  LLLL)\}    {}\mrightarrow{}  varname()
                ((v  \mmember{}  LLLL)
                {}\mRightarrow{}  Inj(\{v@0:varname()|  (v@0  \mmember{}  LLLL)\}  ;varname();F)
                {}\mRightarrow{}  (\muparrow{}same-binding(map(F;LLLL);LLLL;F  v;v))))
        {}\mRightarrow{}  (\mforall{}F:\{v@0:varname()|  (v@0  \mmember{}  [aaaa  /  LLLL])\}    {}\mrightarrow{}  varname()
                    ((v  \mmember{}  [aaaa  /  LLLL])
                    {}\mRightarrow{}  Inj(\{v@0:varname()|  (v@0  \mmember{}  [aaaa  /  LLLL])\}  ;varname();F)
                    {}\mRightarrow{}  (\muparrow{}same-binding(map(F;[aaaa  /  LLLL]);[aaaa  /  LLLL];F  v;v)))))


By


Latex:
(All  Thin
  THEN  RepeatFor  2  (Intro)
  THEN  RenameVar  `u'  (-2)
  THEN  RenameVar  `bnds'  (-1)
  THEN  (Assert  bnds  \mmember{}  \{v:varname()|  (v  \mmember{}  bnds)\}    List  BY
                          Auto)
  THEN  Intros)




Home Index