Proof of Nuprl Lemma : subst-term

Step * 2 1 of Lemma subst-term_functionality

1. [opr] : Type
2. s1 : (varname() × term(opr)) List
3. s2 : (varname() × term(opr)) List
4. equiv-substs(opr;s1;s2)
5. bts : bound-term(opr) List
6. ∀bt:bound-term(opr)
     ((bt ∈ bts)
     ⇒ (∀B:term(opr). ∀bnds1,bnds2:varname() List.
           (l_disjoint(varname();bnds1;vars-of-subst(s1))
           ⇒ l_disjoint(varname();bnds2;vars-of-subst(s2))
           ⇒ alpha-aux(opr;bnds1;bnds2;snd(bt);B)
           ⇒ binders-disjoint(opr;vars-of-subst(s1);snd(bt))
           ⇒ binders-disjoint(opr;vars-of-subst(s2);B)
           ⇒ alpha-aux(opr;bnds1;bnds2;replace-vars(s1;snd(bt));replace-vars(s2;B)))))
7. f : opr
8. b1 : bound-term(opr) List
9. ∀bt:bound-term(opr)
     ((bt ∈ b1)
     ⇒ (∀bnds1,bnds2:varname() List.
           (l_disjoint(varname();bnds1;vars-of-subst(s1))
           ⇒ l_disjoint(varname();bnds2;vars-of-subst(s2))
           ⇒ alpha-aux(opr;bnds1;bnds2;mkterm(f;bts);snd(bt))
           ⇒ binders-disjoint(opr;vars-of-subst(s1);mkterm(f;bts))
           ⇒ binders-disjoint(opr;vars-of-subst(s2);snd(bt))
           ⇒ alpha-aux(opr;bnds1;bnds2;replace-vars(s1;mkterm(f;bts));replace-vars(s2;snd(bt))))))
10. f1 : opr
11. bnds1 : varname() List
12. bnds2 : varname() List
13. l_disjoint(varname();bnds1;vars-of-subst(s1))
14. l_disjoint(varname();bnds2;vars-of-subst(s2))
15. f = f1 ∈ opr
16. ||bts|| = ||b1|| ∈ ℤ
17. ∀i:ℕ||bts||
      (alpha-aux(opr;rev(fst(bts[i])) + bnds1;rev(fst(b1[i])) + bnds2;snd(bts[i]);snd(b1[i]))
      ∧ (||fst(bts[i])|| = ||fst(b1[i])|| ∈ ℤ))
18. binders-disjoint(opr;vars-of-subst(s1);mkterm(f;bts))
19. binders-disjoint(opr;vars-of-subst(s2);mkterm(f1;b1))
20. i : ℕ||bts||
21. ||fst(bts[i])|| = ||fst(b1[i])|| ∈ ℤ
22. v2 : varname() List
23. v3 : term(opr)
24. bts[i] = <v2, v3> ∈ bound-term(opr)
25. v4 : varname() List
26. v5 : term(opr)
27. b1[i] = <v4, v5> ∈ bound-term(opr)
28. alpha-aux(opr;rev(v2) + bnds1;rev(v4) + bnds2;v3;v5)
⊢ alpha-aux(opr;rev(v2) + bnds1;rev(v4) + bnds2;replace-vars(s1;v3);replace-vars(s2;v5))
BY
{ ((InstHyp [⌜<v2, v3>⌝] 6⋅ THENA Auto) THEN (Reduce -1 THEN BHyp -1) THEN Auto) }

1
1. [opr] : Type
2. s1 : (varname() × term(opr)) List
3. s2 : (varname() × term(opr)) List
4. equiv-substs(opr;s1;s2)
5. bts : bound-term(opr) List
6. ∀bt:bound-term(opr)
     ((bt ∈ bts)
     ⇒ (∀B:term(opr). ∀bnds1,bnds2:varname() List.
           (l_disjoint(varname();bnds1;vars-of-subst(s1))
           ⇒ l_disjoint(varname();bnds2;vars-of-subst(s2))
           ⇒ alpha-aux(opr;bnds1;bnds2;snd(bt);B)
           ⇒ binders-disjoint(opr;vars-of-subst(s1);snd(bt))
           ⇒ binders-disjoint(opr;vars-of-subst(s2);B)
           ⇒ alpha-aux(opr;bnds1;bnds2;replace-vars(s1;snd(bt));replace-vars(s2;B)))))
7. f : opr
8. b1 : bound-term(opr) List
9. ∀bt:bound-term(opr)
     ((bt ∈ b1)
     ⇒ (∀bnds1,bnds2:varname() List.
           (l_disjoint(varname();bnds1;vars-of-subst(s1))
           ⇒ l_disjoint(varname();bnds2;vars-of-subst(s2))
           ⇒ alpha-aux(opr;bnds1;bnds2;mkterm(f;bts);snd(bt))
           ⇒ binders-disjoint(opr;vars-of-subst(s1);mkterm(f;bts))
           ⇒ binders-disjoint(opr;vars-of-subst(s2);snd(bt))
           ⇒ alpha-aux(opr;bnds1;bnds2;replace-vars(s1;mkterm(f;bts));replace-vars(s2;snd(bt))))))
10. f1 : opr
11. bnds1 : varname() List
12. bnds2 : varname() List
13. l_disjoint(varname();bnds1;vars-of-subst(s1))
14. l_disjoint(varname();bnds2;vars-of-subst(s2))
15. f = f1 ∈ opr
16. ||bts|| = ||b1|| ∈ ℤ
17. ∀i:ℕ||bts||
      (alpha-aux(opr;rev(fst(bts[i])) + bnds1;rev(fst(b1[i])) + bnds2;snd(bts[i]);snd(b1[i]))
      ∧ (||fst(bts[i])|| = ||fst(b1[i])|| ∈ ℤ))
18. binders-disjoint(opr;vars-of-subst(s1);mkterm(f;bts))
19. binders-disjoint(opr;vars-of-subst(s2);mkterm(f1;b1))
20. i : ℕ||bts||
21. ||fst(bts[i])|| = ||fst(b1[i])|| ∈ ℤ
22. v2 : varname() List
23. v3 : term(opr)
24. bts[i] = <v2, v3> ∈ bound-term(opr)
25. v4 : varname() List
26. v5 : term(opr)
27. b1[i] = <v4, v5> ∈ bound-term(opr)
28. alpha-aux(opr;rev(v2) + bnds1;rev(v4) + bnds2;v3;v5)
29. ∀B:term(opr). ∀bnds1,bnds2:varname() List.
      (l_disjoint(varname();bnds1;vars-of-subst(s1))
      ⇒ l_disjoint(varname();bnds2;vars-of-subst(s2))
      ⇒ alpha-aux(opr;bnds1;bnds2;v3;B)
      ⇒ binders-disjoint(opr;vars-of-subst(s1);v3)
      ⇒ binders-disjoint(opr;vars-of-subst(s2);B)
      ⇒ alpha-aux(opr;bnds1;bnds2;replace-vars(s1;v3);replace-vars(s2;B)))
⊢ l_disjoint(varname();rev(v2) + bnds1;vars-of-subst(s1))

2
1. [opr] : Type
2. s1 : (varname() × term(opr)) List
3. s2 : (varname() × term(opr)) List
4. equiv-substs(opr;s1;s2)
5. bts : bound-term(opr) List
6. ∀bt:bound-term(opr)
     ((bt ∈ bts)
     ⇒ (∀B:term(opr). ∀bnds1,bnds2:varname() List.
           (l_disjoint(varname();bnds1;vars-of-subst(s1))
           ⇒ l_disjoint(varname();bnds2;vars-of-subst(s2))
           ⇒ alpha-aux(opr;bnds1;bnds2;snd(bt);B)
           ⇒ binders-disjoint(opr;vars-of-subst(s1);snd(bt))
           ⇒ binders-disjoint(opr;vars-of-subst(s2);B)
           ⇒ alpha-aux(opr;bnds1;bnds2;replace-vars(s1;snd(bt));replace-vars(s2;B)))))
7. f : opr
8. b1 : bound-term(opr) List
9. ∀bt:bound-term(opr)
     ((bt ∈ b1)
     ⇒ (∀bnds1,bnds2:varname() List.
           (l_disjoint(varname();bnds1;vars-of-subst(s1))
           ⇒ l_disjoint(varname();bnds2;vars-of-subst(s2))
           ⇒ alpha-aux(opr;bnds1;bnds2;mkterm(f;bts);snd(bt))
           ⇒ binders-disjoint(opr;vars-of-subst(s1);mkterm(f;bts))
           ⇒ binders-disjoint(opr;vars-of-subst(s2);snd(bt))
           ⇒ alpha-aux(opr;bnds1;bnds2;replace-vars(s1;mkterm(f;bts));replace-vars(s2;snd(bt))))))
10. f1 : opr
11. bnds1 : varname() List
12. bnds2 : varname() List
13. l_disjoint(varname();bnds1;vars-of-subst(s1))
14. l_disjoint(varname();bnds2;vars-of-subst(s2))
15. f = f1 ∈ opr
16. ||bts|| = ||b1|| ∈ ℤ
17. ∀i:ℕ||bts||
      (alpha-aux(opr;rev(fst(bts[i])) + bnds1;rev(fst(b1[i])) + bnds2;snd(bts[i]);snd(b1[i]))
      ∧ (||fst(bts[i])|| = ||fst(b1[i])|| ∈ ℤ))
18. binders-disjoint(opr;vars-of-subst(s1);mkterm(f;bts))
19. binders-disjoint(opr;vars-of-subst(s2);mkterm(f1;b1))
20. i : ℕ||bts||
21. ||fst(bts[i])|| = ||fst(b1[i])|| ∈ ℤ
22. v2 : varname() List
23. v3 : term(opr)
24. bts[i] = <v2, v3> ∈ bound-term(opr)
25. v4 : varname() List
26. v5 : term(opr)
27. b1[i] = <v4, v5> ∈ bound-term(opr)
28. alpha-aux(opr;rev(v2) + bnds1;rev(v4) + bnds2;v3;v5)
29. ∀B:term(opr). ∀bnds1,bnds2:varname() List.
      (l_disjoint(varname();bnds1;vars-of-subst(s1))
      ⇒ l_disjoint(varname();bnds2;vars-of-subst(s2))
      ⇒ alpha-aux(opr;bnds1;bnds2;v3;B)
      ⇒ binders-disjoint(opr;vars-of-subst(s1);v3)
      ⇒ binders-disjoint(opr;vars-of-subst(s2);B)
      ⇒ alpha-aux(opr;bnds1;bnds2;replace-vars(s1;v3);replace-vars(s2;B)))
⊢ l_disjoint(varname();rev(v4) + bnds2;vars-of-subst(s2))

3
1. [opr] : Type
2. s1 : (varname() × term(opr)) List
3. s2 : (varname() × term(opr)) List
4. equiv-substs(opr;s1;s2)
5. bts : bound-term(opr) List
6. ∀bt:bound-term(opr)
     ((bt ∈ bts)
     ⇒ (∀B:term(opr). ∀bnds1,bnds2:varname() List.
           (l_disjoint(varname();bnds1;vars-of-subst(s1))
           ⇒ l_disjoint(varname();bnds2;vars-of-subst(s2))
           ⇒ alpha-aux(opr;bnds1;bnds2;snd(bt);B)
           ⇒ binders-disjoint(opr;vars-of-subst(s1);snd(bt))
           ⇒ binders-disjoint(opr;vars-of-subst(s2);B)
           ⇒ alpha-aux(opr;bnds1;bnds2;replace-vars(s1;snd(bt));replace-vars(s2;B)))))
7. f : opr
8. b1 : bound-term(opr) List
9. ∀bt:bound-term(opr)
     ((bt ∈ b1)
     ⇒ (∀bnds1,bnds2:varname() List.
           (l_disjoint(varname();bnds1;vars-of-subst(s1))
           ⇒ l_disjoint(varname();bnds2;vars-of-subst(s2))
           ⇒ alpha-aux(opr;bnds1;bnds2;mkterm(f;bts);snd(bt))
           ⇒ binders-disjoint(opr;vars-of-subst(s1);mkterm(f;bts))
           ⇒ binders-disjoint(opr;vars-of-subst(s2);snd(bt))
           ⇒ alpha-aux(opr;bnds1;bnds2;replace-vars(s1;mkterm(f;bts));replace-vars(s2;snd(bt))))))
10. f1 : opr
11. bnds1 : varname() List
12. bnds2 : varname() List
13. l_disjoint(varname();bnds1;vars-of-subst(s1))
14. l_disjoint(varname();bnds2;vars-of-subst(s2))
15. f = f1 ∈ opr
16. ||bts|| = ||b1|| ∈ ℤ
17. ∀i:ℕ||bts||
      (alpha-aux(opr;rev(fst(bts[i])) + bnds1;rev(fst(b1[i])) + bnds2;snd(bts[i]);snd(b1[i]))
      ∧ (||fst(bts[i])|| = ||fst(b1[i])|| ∈ ℤ))
18. binders-disjoint(opr;vars-of-subst(s1);mkterm(f;bts))
19. binders-disjoint(opr;vars-of-subst(s2);mkterm(f1;b1))
20. i : ℕ||bts||
21. ||fst(bts[i])|| = ||fst(b1[i])|| ∈ ℤ
22. v2 : varname() List
23. v3 : term(opr)
24. bts[i] = <v2, v3> ∈ bound-term(opr)
25. v4 : varname() List
26. v5 : term(opr)
27. b1[i] = <v4, v5> ∈ bound-term(opr)
28. alpha-aux(opr;rev(v2) + bnds1;rev(v4) + bnds2;v3;v5)
29. ∀B:term(opr). ∀bnds1,bnds2:varname() List.
      (l_disjoint(varname();bnds1;vars-of-subst(s1))
      ⇒ l_disjoint(varname();bnds2;vars-of-subst(s2))
      ⇒ alpha-aux(opr;bnds1;bnds2;v3;B)
      ⇒ binders-disjoint(opr;vars-of-subst(s1);v3)
      ⇒ binders-disjoint(opr;vars-of-subst(s2);B)
      ⇒ alpha-aux(opr;bnds1;bnds2;replace-vars(s1;v3);replace-vars(s2;B)))
⊢ binders-disjoint(opr;vars-of-subst(s1);v3)

4
1. [opr] : Type
2. s1 : (varname() × term(opr)) List
3. s2 : (varname() × term(opr)) List
4. equiv-substs(opr;s1;s2)
5. bts : bound-term(opr) List
6. ∀bt:bound-term(opr)
     ((bt ∈ bts)
     ⇒ (∀B:term(opr). ∀bnds1,bnds2:varname() List.
           (l_disjoint(varname();bnds1;vars-of-subst(s1))
           ⇒ l_disjoint(varname();bnds2;vars-of-subst(s2))
           ⇒ alpha-aux(opr;bnds1;bnds2;snd(bt);B)
           ⇒ binders-disjoint(opr;vars-of-subst(s1);snd(bt))
           ⇒ binders-disjoint(opr;vars-of-subst(s2);B)
           ⇒ alpha-aux(opr;bnds1;bnds2;replace-vars(s1;snd(bt));replace-vars(s2;B)))))
7. f : opr
8. b1 : bound-term(opr) List
9. ∀bt:bound-term(opr)
     ((bt ∈ b1)
     ⇒ (∀bnds1,bnds2:varname() List.
           (l_disjoint(varname();bnds1;vars-of-subst(s1))
           ⇒ l_disjoint(varname();bnds2;vars-of-subst(s2))
           ⇒ alpha-aux(opr;bnds1;bnds2;mkterm(f;bts);snd(bt))
           ⇒ binders-disjoint(opr;vars-of-subst(s1);mkterm(f;bts))
           ⇒ binders-disjoint(opr;vars-of-subst(s2);snd(bt))
           ⇒ alpha-aux(opr;bnds1;bnds2;replace-vars(s1;mkterm(f;bts));replace-vars(s2;snd(bt))))))
10. f1 : opr
11. bnds1 : varname() List
12. bnds2 : varname() List
13. l_disjoint(varname();bnds1;vars-of-subst(s1))
14. l_disjoint(varname();bnds2;vars-of-subst(s2))
15. f = f1 ∈ opr
16. ||bts|| = ||b1|| ∈ ℤ
17. ∀i:ℕ||bts||
      (alpha-aux(opr;rev(fst(bts[i])) + bnds1;rev(fst(b1[i])) + bnds2;snd(bts[i]);snd(b1[i]))
      ∧ (||fst(bts[i])|| = ||fst(b1[i])|| ∈ ℤ))
18. binders-disjoint(opr;vars-of-subst(s1);mkterm(f;bts))
19. binders-disjoint(opr;vars-of-subst(s2);mkterm(f1;b1))
20. i : ℕ||bts||
21. ||fst(bts[i])|| = ||fst(b1[i])|| ∈ ℤ
22. v2 : varname() List
23. v3 : term(opr)
24. bts[i] = <v2, v3> ∈ bound-term(opr)
25. v4 : varname() List
26. v5 : term(opr)
27. b1[i] = <v4, v5> ∈ bound-term(opr)
28. alpha-aux(opr;rev(v2) + bnds1;rev(v4) + bnds2;v3;v5)
29. ∀B:term(opr). ∀bnds1,bnds2:varname() List.
      (l_disjoint(varname();bnds1;vars-of-subst(s1))
      ⇒ l_disjoint(varname();bnds2;vars-of-subst(s2))
      ⇒ alpha-aux(opr;bnds1;bnds2;v3;B)
      ⇒ binders-disjoint(opr;vars-of-subst(s1);v3)
      ⇒ binders-disjoint(opr;vars-of-subst(s2);B)
      ⇒ alpha-aux(opr;bnds1;bnds2;replace-vars(s1;v3);replace-vars(s2;B)))
⊢ binders-disjoint(opr;vars-of-subst(s2);v5)

Latex:

Latex:
1. [opr] : Type 2. s1 : (varname() \mtimes{} term(opr)) List 3. s2 : (varname() \mtimes{} term(opr)) List 4. equiv-substs(opr;s1;s2) 5. bts : bound-term(opr) List 6. \mforall{}bt:bound-term(opr) ((bt \mmember{} bts) {}\mRightarrow{} (\mforall{}B:term(opr). \mforall{}bnds1,bnds2:varname() List. (l\_disjoint(varname();bnds1;vars-of-subst(s1)) {}\mRightarrow{} l\_disjoint(varname();bnds2;vars-of-subst(s2)) {}\mRightarrow{} alpha-aux(opr;bnds1;bnds2;snd(bt);B) {}\mRightarrow{} binders-disjoint(opr;vars-of-subst(s1);snd(bt)) {}\mRightarrow{} binders-disjoint(opr;vars-of-subst(s2);B) {}\mRightarrow{} alpha-aux(opr;bnds1;bnds2;replace-vars(s1;snd(bt));replace-vars(s2;B))))) 7. f : opr 8. b1 : bound-term(opr) List 9. \mforall{}bt:bound-term(opr) ((bt \mmember{} b1) {}\mRightarrow{} (\mforall{}bnds1,bnds2:varname() List. (l\_disjoint(varname();bnds1;vars-of-subst(s1)) {}\mRightarrow{} l\_disjoint(varname();bnds2;vars-of-subst(s2)) {}\mRightarrow{} alpha-aux(opr;bnds1;bnds2;mkterm(f;bts);snd(bt)) {}\mRightarrow{} binders-disjoint(opr;vars-of-subst(s1);mkterm(f;bts)) {}\mRightarrow{} binders-disjoint(opr;vars-of-subst(s2);snd(bt)) {}\mRightarrow{} alpha-aux(opr;bnds1;bnds2;replace-vars(s1;mkterm(f;bts));replace-vars(s2;snd(bt)))))) 10. f1 : opr 11. bnds1 : varname() List 12. bnds2 : varname() List 13. l\_disjoint(varname();bnds1;vars-of-subst(s1)) 14. l\_disjoint(varname();bnds2;vars-of-subst(s2)) 15. f = f1 16. ||bts|| = ||b1|| 17. \mforall{}i:\mBbbN{}||bts|| (alpha-aux(opr;rev(fst(bts[i])) + bnds1;rev(fst(b1[i])) + bnds2;snd(bts[i]);snd(b1[i])) \mwedge{} (||fst(bts[i])|| = ||fst(b1[i])||)) 18. binders-disjoint(opr;vars-of-subst(s1);mkterm(f;bts)) 19. binders-disjoint(opr;vars-of-subst(s2);mkterm(f1;b1)) 20. i : \mBbbN{}||bts|| 21. ||fst(bts[i])|| = ||fst(b1[i])|| 22. v2 : varname() List 23. v3 : term(opr) 24. bts[i] = <v2, v3> 25. v4 : varname() List 26. v5 : term(opr) 27. b1[i] = <v4, v5> 28. alpha-aux(opr;rev(v2) + bnds1;rev(v4) + bnds2;v3;v5) \mvdash{} alpha-aux(opr;rev(v2) + bnds1;rev(v4) + bnds2;replace-vars(s1;v3);replace-vars(s2;v5)) By Latex: ((InstHyp [\mkleeneopen{}<v2, v3>\mkleeneclose{}] 6\mcdot{} THENA Auto) THEN (Reduce -1 THEN BHyp -1) THEN Auto) Home Index