Proof of Nuprl Lemma : decidable_

Step * 1 1 2 2 2 3 1 of Lemma decidable__cs-archive-blocked

1. [V] : Type
2. ∀v1,v2:V.  Dec(v1 = v2 ∈ V)@i
3. ∃v,v':V. (¬(v = v' ∈ V))@i
4. A : Id List@i
5. W : {a:Id| (a ∈ A)}  List List@i
6. ws : {a:Id| (a ∈ A)}  List@i
7. ws' : {a:Id| (a ∈ A)}  List@i
8. s : ConsensusState@i
9. i : ℤ@i
10. v : V@i
11. L : V List

12. ∀b:{a:Id| (a ∈ A)} . ∀v:V. ∀j:ℤ.  ((v ∈ L)) supposing ((Estimate(s;b)(j) = v ∈ V) and (↑j ∈ dom(Estimate(s;b))))

13. (∃b∈ws. (b ∈ ws'))
14. in state s, ws' blocks ws from archiving v in inning i
⇐⇒ ∃j:ℕi
     (∃v'∈L. (¬(v' = v ∈ V))
     ∧ (∀b∈ws.(b ∈ ws')
          ⇒ ((λv',b,j. ((↑j ∈ dom(Estimate(s;b)))
                       ∧ (Estimate(s;b)(j) = v' ∈ V)
                       ∧ (∀k:{j + 1..i^-}. ((↑k ∈ dom(Estimate(s;b))) ⇒ (Estimate(s;b)(k) = v' ∈ V)))))
              v'
              b
              j)))
15. λv',b,j. ((↑j ∈ dom(Estimate(s;b)))
            ∧ (Estimate(s;b)(j) = v' ∈ V)
            ∧ (∀k:{j + 1..i^-}. ((↑k ∈ dom(Estimate(s;b))) ⇒ (Estimate(s;b)(k) = v' ∈ V)))) ∈ V ⟶ {a:Id| (a ∈ A)}  ⟶ ℤ\000C ⟶ ℙ
⊢ ∀j:ℕi
    Dec((∃v'∈L. (¬(v' = v ∈ V))
    ∧ (∀b∈ws.(b ∈ ws')
         ⇒ ((λv',b,j. ((↑j ∈ dom(Estimate(s;b)))
                      ∧ (Estimate(s;b)(j) = v' ∈ V)
                      ∧ (∀k:{j + 1..i^-}. ((↑k ∈ dom(Estimate(s;b))) ⇒ (Estimate(s;b)(k) = v' ∈ V)))))
             v'
             b
             j))))
BY
{ D 0 }

1
1. [V] : Type
2. ∀v1,v2:V.  Dec(v1 = v2 ∈ V)@i
3. ∃v,v':V. (¬(v = v' ∈ V))@i
4. A : Id List@i
5. W : {a:Id| (a ∈ A)}  List List@i
6. ws : {a:Id| (a ∈ A)}  List@i
7. ws' : {a:Id| (a ∈ A)}  List@i
8. s : ConsensusState@i
9. i : ℤ@i
10. v : V@i
11. L : V List

12. ∀b:{a:Id| (a ∈ A)} . ∀v:V. ∀j:ℤ.  ((v ∈ L)) supposing ((Estimate(s;b)(j) = v ∈ V) and (↑j ∈ dom(Estimate(s;b))))

13. (∃b∈ws. (b ∈ ws'))
14. in state s, ws' blocks ws from archiving v in inning i
⇐⇒ ∃j:ℕi
     (∃v'∈L. (¬(v' = v ∈ V))
     ∧ (∀b∈ws.(b ∈ ws')
          ⇒ ((λv',b,j. ((↑j ∈ dom(Estimate(s;b)))
                       ∧ (Estimate(s;b)(j) = v' ∈ V)
                       ∧ (∀k:{j + 1..i^-}. ((↑k ∈ dom(Estimate(s;b))) ⇒ (Estimate(s;b)(k) = v' ∈ V)))))
              v'
              b
              j)))
15. λv',b,j. ((↑j ∈ dom(Estimate(s;b)))
            ∧ (Estimate(s;b)(j) = v' ∈ V)
            ∧ (∀k:{j + 1..i^-}. ((↑k ∈ dom(Estimate(s;b))) ⇒ (Estimate(s;b)(k) = v' ∈ V)))) ∈ V ⟶ {a:Id| (a ∈ A)}  ⟶ ℤ\000C ⟶ ℙ
16. j : ℕi@i
⊢ Dec((∃v'∈L. (¬(v' = v ∈ V))
∧ (∀b∈ws.(b ∈ ws')
     ⇒ ((λv',b,j. ((↑j ∈ dom(Estimate(s;b)))
                  ∧ (Estimate(s;b)(j) = v' ∈ V)
                  ∧ (∀k:{j + 1..i^-}. ((↑k ∈ dom(Estimate(s;b))) ⇒ (Estimate(s;b)(k) = v' ∈ V)))))
         v'
         b
         j))))

2
.....wf.....
1. V : Type
2. ∀v1,v2:V.  Dec(v1 = v2 ∈ V)@i
3. ∃v,v':V. (¬(v = v' ∈ V))@i
4. A : Id List@i
5. W : {a:Id| (a ∈ A)}  List List@i
6. ws : {a:Id| (a ∈ A)}  List@i
7. ws' : {a:Id| (a ∈ A)}  List@i
8. s : ConsensusState@i
9. i : ℤ@i
10. v : V@i
11. L : V List

12. ∀b:{a:Id| (a ∈ A)} . ∀v:V. ∀j:ℤ.  ((v ∈ L)) supposing ((Estimate(s;b)(j) = v ∈ V) and (↑j ∈ dom(Estimate(s;b))))

Latex:

Latex:
1. [V] : Type 2. \mforall{}v1,v2:V. Dec(v1 = v2)@i 3. \mexists{}v,v':V. (\mneg{}(v = v'))@i 4. A : Id List@i 5. W : \{a:Id| (a \mmember{} A)\} List List@i 6. ws : \{a:Id| (a \mmember{} A)\} List@i 7. ws' : \{a:Id| (a \mmember{} A)\} List@i 8. s : ConsensusState@i 9. i : \mBbbZ{}@i 10. v : V@i 11. L : V List 12. \mforall{}b:\{a:Id| (a \mmember{} A)\} . \mforall{}v:V. \mforall{}j:\mBbbZ{}. ((v \mmember{} L)) supposing ((Estimate(s;b)(j) = v) and (\muparrow{}j \mmember{} dom(Estimate(s;b)))) 13. (\mexists{}b\mmember{}ws. (b \mmember{} ws')) 14. in state s, ws' blocks ws from archiving v in inning i \mLeftarrow{}{}\mRightarrow{} \mexists{}j:\mBbbN{}i (\mexists{}v'\mmember{}L. (\mneg{}(v' = v)) \mwedge{} (\mforall{}b\mmember{}ws.(b \mmember{} ws') {}\mRightarrow{} ((\mlambda{}v',b,j. ((\muparrow{}j \mmember{} dom(Estimate(s;b))) \mwedge{} (Estimate(s;b)(j) = v') \mwedge{} (\mforall{}k:\{j + 1..i\msupminus{}\}. ((\muparrow{}k \mmember{} dom(Estimate(s;b))) {}\mRightarrow{} (Estimate(s;b)(k) = v'))))) v' b j))) 15. \mlambda{}v',b,j. ((\muparrow{}j \mmember{} dom(Estimate(s;b))) \mwedge{} (Estimate(s;b)(j) = v') \mwedge{} (\mforall{}k:\{j + 1..i\msupminus{}\}. ((\muparrow{}k \mmember{} dom(Estimate(s;b))) {}\mRightarrow{} (Estimate(s;b)(k) = v')))) \mmember{} V {}\mrightarrow{} \{a:Id| (a \mmember{} A)\} {}\mrightarrow{} \mBbbZ{} {}\mrightarrow{} \mBbbP{} \mvdash{} \mforall{}j:\mBbbN{}i Dec((\mexists{}v'\mmember{}L. (\mneg{}(v' = v)) \mwedge{} (\mforall{}b\mmember{}ws.(b \mmember{} ws') {}\mRightarrow{} ((\mlambda{}v',b,j. ((\muparrow{}j \mmember{} dom(Estimate(s;b))) \mwedge{} (Estimate(s;b)(j) = v') \mwedge{} (\mforall{}k:\{j + 1..i\msupminus{}\}. ((\muparrow{}k \mmember{} dom(Estimate(s;b))) {}\mRightarrow{} (Estimate(s;b)(k) = v'))))) v' b j)))) By Latex: D 0 Home Index