Proof of Nuprl Lemma : alpha-rename-alist-property

Step * 1 1 of Lemma alpha-rename-alist-property

.....assertion.....
1. [opr] : Type
2. t : term(opr)
3. L : varname() List
⊢ (L @ all-vars(t) ⊆ fst(accumulate (with value p and list item x):
                          let vs,tab = p
                          in eval x' = maybe_new_var(x;vs) in
                             <[x' / vs], [<x, x'> / tab]>
                         over list:
                           L
                         with starting value:
                          <L @ all-vars(t), []>))
  ∧ (∀x,x':varname().
       ((<x, x'> ∈ snd(accumulate (with value p and list item x):
                        let vs,tab = p
                        in eval x' = maybe_new_var(x;vs) in
                           <[x' / vs], [<x, x'> / tab]>
                       over list:
                         L
                       with starting value:
                        <L @ all-vars(t), []>)))
       ⇒ (x' ∈ fst(accumulate (with value p and list item x):
                     let vs,tab = p
                     in eval x' = maybe_new_var(x;vs) in
                        <[x' / vs], [<x, x'> / tab]>
                    over list:
                      L
                    with starting value:
                     <L @ all-vars(t), []>))))))
∧ (∀x,x':varname().
     ((<x, x'> ∈ snd(accumulate (with value p and list item x):
                      let vs,tab = p
                      in eval x' = maybe_new_var(x;vs) in
                         <[x' / vs], [<x, x'> / tab]>
                     over list:
                       L
                     with starting value:
                      <L @ all-vars(t), []>)))
     ⇒ ((x ∈ L) ∧ (¬(x' ∈ L @ all-vars(t))))))
∧ (∀x,x',y,y':varname().
     ((<x, x'> ∈ snd(accumulate (with value p and list item x):
                      let vs,tab = p
                      in eval x' = maybe_new_var(x;vs) in
                         <[x' / vs], [<x, x'> / tab]>
                     over list:
                       L
                     with starting value:
                      <L @ all-vars(t), []>)))
     ⇒ (<y, y'> ∈ snd(accumulate (with value p and list item x):
                        let vs,tab = p
                        in eval x' = maybe_new_var(x;vs) in
                           <[x' / vs], [<x, x'> / tab]>
                       over list:
                         L
                       with starting value:
                        <L @ all-vars(t), []>)))
     ⇒ (x' = y' ∈ varname())
     ⇒ (x = y ∈ varname())))
BY
{ (ProveListAccumInvWithType ⌜varname() List × ((varname() × varname()) List)⌝⋅
   THEN Try (Complete (Auto))
   THEN Intros
   THEN D 0
   THEN Reduce 0
   THEN Try (Complete (Auto))
   THEN DVar `a'
   THEN Reduce 0
   THEN (GenConcl ⌜maybe_new_var(x;a1) = x' ∈ varname()⌝⋅ THENA Auto)
   THEN (CallByValueReduce 0 THENA Auto)
   THEN All Reduce
   THEN SplitAndConcl
   THEN (Complete (EAuto 1)
   ORELSE (Intros THEN SplitAndHyps THEN (GenListD (-1) ORELSE GenListD (-2)) THEN SplitOrHyps)
   )) }

1
1. [opr] : Type
2. t : term(opr)
3. L : varname() List
4. a1 : varname() List
5. a2 : (varname() × varname()) List
6. x : varname()
7. (x ∈ L)
8. L @ all-vars(t) ⊆ a1
9. ∀x,x':varname().  ((<x, x'> ∈ a2) ⇒ (x' ∈ a1))
10. ∀x,x':varname().  ((<x, x'> ∈ a2) ⇒ ((x ∈ L) ∧ (¬(x' ∈ L @ all-vars(t)))))
11. ∀x,x',y,y':varname().  ((<x, x'> ∈ a2) ⇒ (<y, y'> ∈ a2) ⇒ (x' = y' ∈ varname()) ⇒ (x = y ∈ varname()))
12. x' : varname()
13. maybe_new_var(x;a1) = x' ∈ varname()
14. x@0 : varname()
15. x'@0 : varname()
16. <x@0, x'@0> = <x, x'> ∈ (varname() × varname())
⊢ (x'@0 ∈ [x' / a1])

2
1. [opr] : Type
2. t : term(opr)
3. L : varname() List
4. a1 : varname() List
5. a2 : (varname() × varname()) List
6. x : varname()
7. (x ∈ L)
8. L @ all-vars(t) ⊆ a1
9. ∀x,x':varname().  ((<x, x'> ∈ a2) ⇒ (x' ∈ a1))
10. ∀x,x':varname().  ((<x, x'> ∈ a2) ⇒ ((x ∈ L) ∧ (¬(x' ∈ L @ all-vars(t)))))
11. ∀x,x',y,y':varname().  ((<x, x'> ∈ a2) ⇒ (<y, y'> ∈ a2) ⇒ (x' = y' ∈ varname()) ⇒ (x = y ∈ varname()))
12. x' : varname()
13. maybe_new_var(x;a1) = x' ∈ varname()
14. x@0 : varname()
15. x'@0 : varname()
16. (<x@0, x'@0> ∈ a2)
⊢ (x'@0 ∈ [x' / a1])

3
1. [opr] : Type
2. t : term(opr)
3. L : varname() List
4. a1 : varname() List
5. a2 : (varname() × varname()) List
6. x : varname()
7. (x ∈ L)
8. L @ all-vars(t) ⊆ a1
9. ∀x,x':varname().  ((<x, x'> ∈ a2) ⇒ (x' ∈ a1))
10. ∀x,x':varname().  ((<x, x'> ∈ a2) ⇒ ((x ∈ L) ∧ (¬(x' ∈ L @ all-vars(t)))))
11. ∀x,x',y,y':varname().  ((<x, x'> ∈ a2) ⇒ (<y, y'> ∈ a2) ⇒ (x' = y' ∈ varname()) ⇒ (x = y ∈ varname()))
12. x' : varname()
13. maybe_new_var(x;a1) = x' ∈ varname()
14. x@0 : varname()
15. x'@0 : varname()
16. <x@0, x'@0> = <x, x'> ∈ (varname() × varname())
⊢ (x@0 ∈ L) ∧ (¬(x'@0 ∈ L @ all-vars(t)))

4
1. [opr] : Type
2. t : term(opr)
3. L : varname() List
4. a1 : varname() List
5. a2 : (varname() × varname()) List
6. x : varname()
7. (x ∈ L)
8. L @ all-vars(t) ⊆ a1
9. ∀x,x':varname().  ((<x, x'> ∈ a2) ⇒ (x' ∈ a1))
10. ∀x,x':varname().  ((<x, x'> ∈ a2) ⇒ ((x ∈ L) ∧ (¬(x' ∈ L @ all-vars(t)))))
11. ∀x,x',y,y':varname().  ((<x, x'> ∈ a2) ⇒ (<y, y'> ∈ a2) ⇒ (x' = y' ∈ varname()) ⇒ (x = y ∈ varname()))
12. x' : varname()
13. maybe_new_var(x;a1) = x' ∈ varname()
14. x@0 : varname()
15. x'@0 : varname()
16. (<x@0, x'@0> ∈ a2)
⊢ (x@0 ∈ L) ∧ (¬(x'@0 ∈ L @ all-vars(t)))

5
1. opr : Type
2. t : term(opr)
3. L : varname() List
4. a1 : varname() List
5. a2 : (varname() × varname()) List
6. x : varname()
7. (x ∈ L)
8. L @ all-vars(t) ⊆ a1
9. ∀x,x':varname().  ((<x, x'> ∈ a2) ⇒ (x' ∈ a1))
10. ∀x,x':varname().  ((<x, x'> ∈ a2) ⇒ ((x ∈ L) ∧ (¬(x' ∈ L @ all-vars(t)))))
11. ∀x,x',y,y':varname().  ((<x, x'> ∈ a2) ⇒ (<y, y'> ∈ a2) ⇒ (x' = y' ∈ varname()) ⇒ (x = y ∈ varname()))
12. x' : varname()
13. maybe_new_var(x;a1) = x' ∈ varname()
14. x@0 : varname()
15. x'@0 : varname()
16. y : varname()
17. y' : varname()
18. (<x@0, x'@0> ∈ [<x, x'> / a2])
19. <y, y'> = <x, x'> ∈ (varname() × varname())
20. x'@0 = y' ∈ varname()
⊢ x@0 = y ∈ varname()

6
1. opr : Type
2. t : term(opr)
3. L : varname() List
4. a1 : varname() List
5. a2 : (varname() × varname()) List
6. x : varname()
7. (x ∈ L)
8. L @ all-vars(t) ⊆ a1
9. ∀x,x':varname().  ((<x, x'> ∈ a2) ⇒ (x' ∈ a1))
10. ∀x,x':varname().  ((<x, x'> ∈ a2) ⇒ ((x ∈ L) ∧ (¬(x' ∈ L @ all-vars(t)))))
11. ∀x,x',y,y':varname().  ((<x, x'> ∈ a2) ⇒ (<y, y'> ∈ a2) ⇒ (x' = y' ∈ varname()) ⇒ (x = y ∈ varname()))
12. x' : varname()
13. maybe_new_var(x;a1) = x' ∈ varname()
14. x@0 : varname()
15. x'@0 : varname()
16. y : varname()
17. y' : varname()
18. (<x@0, x'@0> ∈ [<x, x'> / a2])
19. (<y, y'> ∈ a2)
20. x'@0 = y' ∈ varname()
⊢ x@0 = y ∈ varname()

Latex:

Latex:
.....assertion..... 1. [opr] : Type 2. t : term(opr) 3. L : varname() List \mvdash{} (L @ all-vars(t) \msubseteq{} fst(accumulate (with value p and list item x): let vs,tab = p in eval x' = maybe\_new\_var(x;vs) in <[x' / vs], [<x, x'> / tab]> over list: L with starting value: <L @ all-vars(t), []>)) \mwedge{} (\mforall{}x,x':varname(). ((<x, x'> \mmember{} snd(accumulate (with value p and list item x): let vs,tab = p in eval x' = maybe\_new\_var(x;vs) in <[x' / vs], [<x, x'> / tab]> over list: L with starting value: <L @ all-vars(t), []>))) {}\mRightarrow{} (x' \mmember{} fst(accumulate (with value p and list item x): let vs,tab = p in eval x' = maybe\_new\_var(x;vs) in <[x' / vs], [<x, x'> / tab]> over list: L with starting value: <L @ all-vars(t), []>)))))) \mwedge{} (\mforall{}x,x':varname(). ((<x, x'> \mmember{} snd(accumulate (with value p and list item x): let vs,tab = p in eval x' = maybe\_new\_var(x;vs) in <[x' / vs], [<x, x'> / tab]> over list: L with starting value: <L @ all-vars(t), []>))) {}\mRightarrow{} ((x \mmember{} L) \mwedge{} (\mneg{}(x' \mmember{} L @ all-vars(t)))))) \mwedge{} (\mforall{}x,x',y,y':varname(). ((<x, x'> \mmember{} snd(accumulate (with value p and list item x): let vs,tab = p in eval x' = maybe\_new\_var(x;vs) in <[x' / vs], [<x, x'> / tab]> over list: L with starting value: <L @ all-vars(t), []>))) {}\mRightarrow{} (<y, y'> \mmember{} snd(accumulate (with value p and list item x): let vs,tab = p in eval x' = maybe\_new\_var(x;vs) in <[x' / vs], [<x, x'> / tab]> over list: L with starting value: <L @ all-vars(t), []>))) {}\mRightarrow{} (x' = y') {}\mRightarrow{} (x = y))) By Latex: (ProveListAccumInvWithType \mkleeneopen{}varname() List \mtimes{} ((varname() \mtimes{} varname()) List)\mkleeneclose{}\mcdot{} THEN Try (Complete (Auto)) THEN Intros THEN D 0 THEN Reduce 0 THEN Try (Complete (Auto)) THEN DVar `a' THEN Reduce 0 THEN (GenConcl \mkleeneopen{}maybe\_new\_var(x;a1) = x'\mkleeneclose{}\mcdot{} THENA Auto) THEN (CallByValueReduce 0 THENA Auto) THEN All Reduce THEN SplitAndConcl THEN (Complete (EAuto 1) ORELSE (Intros THEN SplitAndHyps THEN (GenListD (-1) ORELSE GenListD (-2)) THEN SplitOrHyps) )) Home Index