Proof of Nuprl Lemma : alpha-rename-binders-disjoint

Step * 1 3 2 1 of Lemma alpha-rename-binders-disjoint

1. [opr] : Type
2. L : varname() List
3. bts : bound-term(opr) List
4. ∀bt:bound-term(opr)
     ((bt ∈ bts)
     ⇒ (∀bnds:varname() List. ∀f:{v:varname()| (v ∈ bnds @ all-vars(snd(bt)))}  ⟶ varname().
           ((∀x:{v:varname()| (v ∈ bnds @ all-vars(snd(bt)))}
               ((((f x) = nullvar() ∈ varname()) ⇒ (x = nullvar() ∈ varname())) ∧ (¬(f x ∈ L))))
           ⇒ binders-disjoint(opr;L;alpha-rename-aux(f;bnds;snd(bt))))))
5. f : opr
6. bnds : varname() List
7. f@0 : {v:varname()| (v ∈ bnds @ all-vars(mkterm(f;bts)))}  ⟶ varname()
8. ∀x:{v:varname()| (v ∈ bnds @ all-vars(mkterm(f;bts)))}
     ((((f@0 x) = nullvar() ∈ varname()) ⇒ (x = nullvar() ∈ varname())) ∧ (¬(f@0 x ∈ L)))
9. bts ∈ {bt:varname() List × term(opr)| (bt ∈ bts)}  List
10. λbt.let vs,a = bt

        in <map(f@0;vs), alpha-rename-aux(f@0;rev(vs) + bnds;a)> ∈ {bt:varname() List × term(opr)| (bt ∈ bts)}  ⟶ bound\000C-term(opr)

⊢ (∀bt∈map(λbt.let vs,a = bt

               in <map(f@0;vs), alpha-rename-aux(f@0;rev(vs) + bnds;a)>;bts).l_disjoint(varname();fst(bt);L)

      ∧ binders-disjoint(opr;L;snd(bt)))
BY
{ ((RWO "l_all_map" 0 THENA Auto)
   THEN (D 0 THENA Auto)
   THEN ((InstHyp [⌜bts[i]⌝] 4⋅ THENA Auto) THEN MoveToConcl (-1))
   THEN (GenConclTerm ⌜bts[i]⌝⋅ THENA Auto)
   THEN Thin (-1)
   THEN D -1
   THEN D -2
   THEN Reduce 0
   THEN (D 0 THENA Auto)
   THEN D 0) }

1
1. [opr] : Type
2. L : varname() List
3. bts : bound-term(opr) List
4. ∀bt:bound-term(opr)
     ((bt ∈ bts)
     ⇒ (∀bnds:varname() List. ∀f:{v:varname()| (v ∈ bnds @ all-vars(snd(bt)))}  ⟶ varname().
           ((∀x:{v:varname()| (v ∈ bnds @ all-vars(snd(bt)))}
               ((((f x) = nullvar() ∈ varname()) ⇒ (x = nullvar() ∈ varname())) ∧ (¬(f x ∈ L))))
           ⇒ binders-disjoint(opr;L;alpha-rename-aux(f;bnds;snd(bt))))))
5. f : opr
6. bnds : varname() List
7. f@0 : {v:varname()| (v ∈ bnds @ all-vars(mkterm(f;bts)))}  ⟶ varname()
8. ∀x:{v:varname()| (v ∈ bnds @ all-vars(mkterm(f;bts)))}
     ((((f@0 x) = nullvar() ∈ varname()) ⇒ (x = nullvar() ∈ varname())) ∧ (¬(f@0 x ∈ L)))
9. bts ∈ {bt:varname() List × term(opr)| (bt ∈ bts)}  List
10. λbt.let vs,a = bt

        in <map(f@0;vs), alpha-rename-aux(f@0;rev(vs) + bnds;a)> ∈ {bt:varname() List × term(opr)| (bt ∈ bts)}  ⟶ bound\000C-term(opr)

11. i : ℕ||bts||
12. v1 : varname() List
13. v2 : term(opr)
14. [%5] : (<v1, v2> ∈ bts)
15. ∀bnds:varname() List. ∀f:{v@0:varname()| (v@0 ∈ bnds @ all-vars(v2))}  ⟶ varname().
      ((∀x:{v@0:varname()| (v@0 ∈ bnds @ all-vars(v2))}
          ((((f x) = nullvar() ∈ varname()) ⇒ (x = nullvar() ∈ varname())) ∧ (¬(f x ∈ L))))
      ⇒ binders-disjoint(opr;L;alpha-rename-aux(f;bnds;v2)))
⊢ l_disjoint(varname();map(f@0;v1);L)

2
1. [opr] : Type
2. L : varname() List
3. bts : bound-term(opr) List
4. ∀bt:bound-term(opr)
     ((bt ∈ bts)
     ⇒ (∀bnds:varname() List. ∀f:{v:varname()| (v ∈ bnds @ all-vars(snd(bt)))}  ⟶ varname().
           ((∀x:{v:varname()| (v ∈ bnds @ all-vars(snd(bt)))}
               ((((f x) = nullvar() ∈ varname()) ⇒ (x = nullvar() ∈ varname())) ∧ (¬(f x ∈ L))))
           ⇒ binders-disjoint(opr;L;alpha-rename-aux(f;bnds;snd(bt))))))
5. f : opr
6. bnds : varname() List
7. f@0 : {v:varname()| (v ∈ bnds @ all-vars(mkterm(f;bts)))}  ⟶ varname()
8. ∀x:{v:varname()| (v ∈ bnds @ all-vars(mkterm(f;bts)))}
     ((((f@0 x) = nullvar() ∈ varname()) ⇒ (x = nullvar() ∈ varname())) ∧ (¬(f@0 x ∈ L)))
9. bts ∈ {bt:varname() List × term(opr)| (bt ∈ bts)}  List
10. λbt.let vs,a = bt

        in <map(f@0;vs), alpha-rename-aux(f@0;rev(vs) + bnds;a)> ∈ {bt:varname() List × term(opr)| (bt ∈ bts)}  ⟶ bound\000C-term(opr)

Latex:

Latex:
1. [opr] : Type 2. L : varname() List 3. bts : bound-term(opr) List 4. \mforall{}bt:bound-term(opr) ((bt \mmember{} bts) {}\mRightarrow{} (\mforall{}bnds:varname() List. \mforall{}f:\{v:varname()| (v \mmember{} bnds @ all-vars(snd(bt)))\} {}\mrightarrow{} varname(). ((\mforall{}x:\{v:varname()| (v \mmember{} bnds @ all-vars(snd(bt)))\} ((((f x) = nullvar()) {}\mRightarrow{} (x = nullvar())) \mwedge{} (\mneg{}(f x \mmember{} L)))) {}\mRightarrow{} binders-disjoint(opr;L;alpha-rename-aux(f;bnds;snd(bt)))))) 5. f : opr 6. bnds : varname() List 7. f@0 : \{v:varname()| (v \mmember{} bnds @ all-vars(mkterm(f;bts)))\} {}\mrightarrow{} varname() 8. \mforall{}x:\{v:varname()| (v \mmember{} bnds @ all-vars(mkterm(f;bts)))\} ((((f@0 x) = nullvar()) {}\mRightarrow{} (x = nullvar())) \mwedge{} (\mneg{}(f@0 x \mmember{} L))) 9. bts \mmember{} \{bt:varname() List \mtimes{} term(opr)| (bt \mmember{} bts)\} List 10. \mlambda{}bt.let vs,a = bt in <map(f@0;vs), alpha-rename-aux(f@0;rev(vs) + bnds;a)> \mmember{} \{bt:varname() List \mtimes{} term(opr)| (bt \mmember{} bts)\} {}\mrightarrow{} bound-term(opr) \mvdash{} (\mforall{}bt\mmember{}map(\mlambda{}bt.let vs,a = bt in <map(f@0;vs), alpha-rename-aux(f@0;rev(vs) + bnds;a)>bts). l\_disjoint(varname();fst(bt);L) \mwedge{} binders-disjoint(opr;L;snd(bt))) By Latex: ((RWO "l\_all\_map" 0 THENA Auto) THEN (D 0 THENA Auto) THEN ((InstHyp [\mkleeneopen{}bts[i]\mkleeneclose{}] 4\mcdot{} THENA Auto) THEN MoveToConcl (-1)) THEN (GenConclTerm \mkleeneopen{}bts[i]\mkleeneclose{}\mcdot{} THENA Auto) THEN Thin (-1) THEN D -1 THEN D -2 THEN Reduce 0 THEN (D 0 THENA Auto) THEN D 0) Home Index