Proof of Nuprl Lemma : state-class2-inv

Step * 1 of Lemma state-class2-inv

1. [Info] : Type
2. [B] : Type
3. [A1] : Type
4. [A2] : Type
5. init : Id ─→ B@i
6. tr1 : Id ─→ A1 ─→ B ─→ B@i
7. tr2 : Id ─→ A2 ─→ B ─→ B@i
8. X1 : EClass(A1)@i'
9. X2 : EClass(A2)@i'
10. es : EO+(Info)@i'
11. e : E@i
12. P : E ─→ B ─→ ℙ@i'
13. v : B@i
14. single-valued-classrel(es;X1;A1)@i
15. single-valued-classrel(es;X2;A2)@i
16. disjoint-classrel(es;A1;X1;A2;X2)@i
17. ∀s:B. ∀e':E.
      (e' ≤loc e
      ⇒ if first(e')
         then s = (init loc(e')) ∈ B
         else s ∈ state-class2(init;tr1;X1;tr2;X2)(pred(e')) ∧ P[pred(e');s]
         fi
      ⇒ if e' ∈_b X1 then ∀a:A1. (a ∈ X1(e') ⇒ P[e';tr1 loc(e') a s])
         if e' ∈_b X2 then ∀a:A2. (a ∈ X2(e') ⇒ P[e';tr2 loc(e') a s])
         else P[e';s]
         fi )@i
18. v ∈ state-class2(init;tr1;X1;tr2;X2)(e)@i
⊢ P[e;v]
BY
{ (RepeatFor 2 (MoveToConcl (-6))
   THEN CausalInd'
   THEN (UnivCD THENA Auto)
   THEN (Assert ⌈v = state-class2(init;tr1;X1;tr2;X2)(e) ∈ B⌉⋅
         THENA (BLemma `classrel-classfun` THEN Auto THEN ProveFunctional THEN Auto)
         )
   THEN (RWO "-1" 0 THENA Auto)
   THEN (RWO "state-class2-fun-eq" 0 THENA (Auto THEN BLemma `state-class2-fun-eq` THEN Auto))
   THEN Repeat (AutoSplit)) }

1
1. [Info] : Type
2. [B] : Type
3. [A1] : Type
4. [A2] : Type
5. init : Id ─→ B@i
6. tr1 : Id ─→ A1 ─→ B ─→ B@i
7. tr2 : Id ─→ A2 ─→ B ─→ B@i
8. X1 : EClass(A1)@i'
9. X2 : EClass(A2)@i'
10. es : EO+(Info)@i'
11. P : E ─→ B ─→ ℙ@i'
12. single-valued-classrel(es;X1;A1)@i
13. single-valued-classrel(es;X2;A2)@i
14. disjoint-classrel(es;A1;X1;A2;X2)@i
15. e : E@i
16. ∀e1:E
      ((e1 < e)
      ⇒ (∀s:B. ∀e':E.
            (e' ≤loc e1
            ⇒ if first(e')
               then s = (init loc(e')) ∈ B
               else s ∈ state-class2(init;tr1;X1;tr2;X2)(pred(e')) ∧ P[pred(e');s]
               fi
            ⇒ if e' ∈_b X1 then ∀a:A1. (a ∈ X1(e') ⇒ P[e';tr1 loc(e') a s])
               if e' ∈_b X2 then ∀a:A2. (a ∈ X2(e') ⇒ P[e';tr2 loc(e') a s])
               else P[e';s]
               fi ))
      ⇒ (∀v:B. (v ∈ state-class2(init;tr1;X1;tr2;X2)(e1) ⇒ P[e1;v])))
17. ∀s:B. ∀e':E.
      (e' ≤loc e
      ⇒ if first(e')
         then s = (init loc(e')) ∈ B
         else s ∈ state-class2(init;tr1;X1;tr2;X2)(pred(e')) ∧ P[pred(e');s]
         fi
      ⇒ if e' ∈_b X1 then ∀a:A1. (a ∈ X1(e') ⇒ P[e';tr1 loc(e') a s])
         if e' ∈_b X2 then ∀a:A2. (a ∈ X2(e') ⇒ P[e';tr2 loc(e') a s])
         else P[e';s]
         fi )@i
18. v : B@i
19. v ∈ state-class2(init;tr1;X1;tr2;X2)(e)@i
20. v = state-class2(init;tr1;X1;tr2;X2)(e) ∈ B
21. ↑e ∈_b X1
22. ↑first(e)
⊢ P[e;tr1 loc(e) X1@e (init loc(e))]

2
1. [Info] : Type
2. [B] : Type
3. [A1] : Type
4. [A2] : Type
5. init : Id ─→ B@i
6. tr1 : Id ─→ A1 ─→ B ─→ B@i
7. tr2 : Id ─→ A2 ─→ B ─→ B@i
8. X1 : EClass(A1)@i'
9. X2 : EClass(A2)@i'
10. es : EO+(Info)@i'
11. P : E ─→ B ─→ ℙ@i'
12. single-valued-classrel(es;X1;A1)@i
13. single-valued-classrel(es;X2;A2)@i
14. disjoint-classrel(es;A1;X1;A2;X2)@i
15. e : E@i
16. ¬↑first(e)
17. ∀e1:E
      ((e1 < e)
      ⇒ (∀s:B. ∀e':E.
            (e' ≤loc e1
            ⇒ if first(e')
               then s = (init loc(e')) ∈ B
               else s ∈ state-class2(init;tr1;X1;tr2;X2)(pred(e')) ∧ P[pred(e');s]
               fi
            ⇒ if e' ∈_b X1 then ∀a:A1. (a ∈ X1(e') ⇒ P[e';tr1 loc(e') a s])
               if e' ∈_b X2 then ∀a:A2. (a ∈ X2(e') ⇒ P[e';tr2 loc(e') a s])
               else P[e';s]
               fi ))
      ⇒ (∀v:B. (v ∈ state-class2(init;tr1;X1;tr2;X2)(e1) ⇒ P[e1;v])))
18. ∀s:B. ∀e':E.
      (e' ≤loc e
      ⇒ if first(e')
         then s = (init loc(e')) ∈ B
         else s ∈ state-class2(init;tr1;X1;tr2;X2)(pred(e')) ∧ P[pred(e');s]
         fi
      ⇒ if e' ∈_b X1 then ∀a:A1. (a ∈ X1(e') ⇒ P[e';tr1 loc(e') a s])
         if e' ∈_b X2 then ∀a:A2. (a ∈ X2(e') ⇒ P[e';tr2 loc(e') a s])
         else P[e';s]
         fi )@i
19. v : B@i
20. v ∈ state-class2(init;tr1;X1;tr2;X2)(e)@i
21. v = state-class2(init;tr1;X1;tr2;X2)(e) ∈ B
22. ↑e ∈_b X1
⊢ P[e;tr1 loc(e) X1@e state-class2(init;tr1;X1;tr2;X2)(pred(e))]

3
1. [Info] : Type
2. [B] : Type
3. [A1] : Type
4. [A2] : Type
5. init : Id ─→ B@i
6. tr1 : Id ─→ A1 ─→ B ─→ B@i
7. tr2 : Id ─→ A2 ─→ B ─→ B@i
8. X1 : EClass(A1)@i'
9. X2 : EClass(A2)@i'
10. es : EO+(Info)@i'
11. P : E ─→ B ─→ ℙ@i'
12. single-valued-classrel(es;X1;A1)@i
13. single-valued-classrel(es;X2;A2)@i
14. disjoint-classrel(es;A1;X1;A2;X2)@i
15. e : E@i
16. ¬↑e ∈_b X1
17. ∀e1:E
      ((e1 < e)
      ⇒ (∀s:B. ∀e':E.
            (e' ≤loc e1
            ⇒ if first(e')
               then s = (init loc(e')) ∈ B
               else s ∈ state-class2(init;tr1;X1;tr2;X2)(pred(e')) ∧ P[pred(e');s]
               fi
            ⇒ if e' ∈_b X1 then ∀a:A1. (a ∈ X1(e') ⇒ P[e';tr1 loc(e') a s])
               if e' ∈_b X2 then ∀a:A2. (a ∈ X2(e') ⇒ P[e';tr2 loc(e') a s])
               else P[e';s]
               fi ))
      ⇒ (∀v:B. (v ∈ state-class2(init;tr1;X1;tr2;X2)(e1) ⇒ P[e1;v])))
18. ∀s:B. ∀e':E.
      (e' ≤loc e
      ⇒ if first(e')
         then s = (init loc(e')) ∈ B
         else s ∈ state-class2(init;tr1;X1;tr2;X2)(pred(e')) ∧ P[pred(e');s]
         fi
      ⇒ if e' ∈_b X1 then ∀a:A1. (a ∈ X1(e') ⇒ P[e';tr1 loc(e') a s])
         if e' ∈_b X2 then ∀a:A2. (a ∈ X2(e') ⇒ P[e';tr2 loc(e') a s])
         else P[e';s]
         fi )@i
19. v : B@i
20. v ∈ state-class2(init;tr1;X1;tr2;X2)(e)@i
21. v = state-class2(init;tr1;X1;tr2;X2)(e) ∈ B
22. ↑e ∈_b X2
23. ↑first(e)
⊢ P[e;tr2 loc(e) X2@e (init loc(e))]

4
1. [Info] : Type
2. [B] : Type
3. [A1] : Type
4. [A2] : Type
5. init : Id ─→ B@i
6. tr1 : Id ─→ A1 ─→ B ─→ B@i
7. tr2 : Id ─→ A2 ─→ B ─→ B@i
8. X1 : EClass(A1)@i'
9. X2 : EClass(A2)@i'
10. es : EO+(Info)@i'
11. P : E ─→ B ─→ ℙ@i'
12. single-valued-classrel(es;X1;A1)@i
13. single-valued-classrel(es;X2;A2)@i
14. disjoint-classrel(es;A1;X1;A2;X2)@i
15. e : E@i
16. ¬↑first(e)
17. ¬↑e ∈_b X1
18. ∀e1:E
      ((e1 < e)
      ⇒ (∀s:B. ∀e':E.
            (e' ≤loc e1
            ⇒ if first(e')
               then s = (init loc(e')) ∈ B
               else s ∈ state-class2(init;tr1;X1;tr2;X2)(pred(e')) ∧ P[pred(e');s]
               fi
            ⇒ if e' ∈_b X1 then ∀a:A1. (a ∈ X1(e') ⇒ P[e';tr1 loc(e') a s])
               if e' ∈_b X2 then ∀a:A2. (a ∈ X2(e') ⇒ P[e';tr2 loc(e') a s])
               else P[e';s]
               fi ))
      ⇒ (∀v:B. (v ∈ state-class2(init;tr1;X1;tr2;X2)(e1) ⇒ P[e1;v])))
19. ∀s:B. ∀e':E.
      (e' ≤loc e
      ⇒ if first(e')
         then s = (init loc(e')) ∈ B
         else s ∈ state-class2(init;tr1;X1;tr2;X2)(pred(e')) ∧ P[pred(e');s]
         fi
      ⇒ if e' ∈_b X1 then ∀a:A1. (a ∈ X1(e') ⇒ P[e';tr1 loc(e') a s])
         if e' ∈_b X2 then ∀a:A2. (a ∈ X2(e') ⇒ P[e';tr2 loc(e') a s])
         else P[e';s]
         fi )@i
20. v : B@i
21. v ∈ state-class2(init;tr1;X1;tr2;X2)(e)@i
22. v = state-class2(init;tr1;X1;tr2;X2)(e) ∈ B
23. ↑e ∈_b X2
⊢ P[e;tr2 loc(e) X2@e state-class2(init;tr1;X1;tr2;X2)(pred(e))]

5
1. [Info] : Type
2. [B] : Type
3. [A1] : Type
4. [A2] : Type
5. init : Id ─→ B@i
6. tr1 : Id ─→ A1 ─→ B ─→ B@i
7. tr2 : Id ─→ A2 ─→ B ─→ B@i
8. X1 : EClass(A1)@i'
9. X2 : EClass(A2)@i'
10. es : EO+(Info)@i'
11. P : E ─→ B ─→ ℙ@i'
12. single-valued-classrel(es;X1;A1)@i
13. single-valued-classrel(es;X2;A2)@i
14. disjoint-classrel(es;A1;X1;A2;X2)@i
15. e : E@i
16. ¬↑e ∈_b X2
17. ¬↑e ∈_b X1
18. ∀e1:E
      ((e1 < e)
      ⇒ (∀s:B. ∀e':E.
            (e' ≤loc e1
            ⇒ if first(e')
               then s = (init loc(e')) ∈ B
               else s ∈ state-class2(init;tr1;X1;tr2;X2)(pred(e')) ∧ P[pred(e');s]
               fi
            ⇒ if e' ∈_b X1 then ∀a:A1. (a ∈ X1(e') ⇒ P[e';tr1 loc(e') a s])
               if e' ∈_b X2 then ∀a:A2. (a ∈ X2(e') ⇒ P[e';tr2 loc(e') a s])
               else P[e';s]
               fi ))
      ⇒ (∀v:B. (v ∈ state-class2(init;tr1;X1;tr2;X2)(e1) ⇒ P[e1;v])))
19. ∀s:B. ∀e':E.
      (e' ≤loc e
      ⇒ if first(e')
         then s = (init loc(e')) ∈ B
         else s ∈ state-class2(init;tr1;X1;tr2;X2)(pred(e')) ∧ P[pred(e');s]
         fi
      ⇒ if e' ∈_b X1 then ∀a:A1. (a ∈ X1(e') ⇒ P[e';tr1 loc(e') a s])
         if e' ∈_b X2 then ∀a:A2. (a ∈ X2(e') ⇒ P[e';tr2 loc(e') a s])
         else P[e';s]
         fi )@i
20. v : B@i
21. v ∈ state-class2(init;tr1;X1;tr2;X2)(e)@i
22. v = state-class2(init;tr1;X1;tr2;X2)(e) ∈ B
23. ↑first(e)
⊢ P[e;init loc(e)]

6
1. [Info] : Type
2. [B] : Type
3. [A1] : Type
4. [A2] : Type
5. init : Id ─→ B@i
6. tr1 : Id ─→ A1 ─→ B ─→ B@i
7. tr2 : Id ─→ A2 ─→ B ─→ B@i
8. X1 : EClass(A1)@i'
9. X2 : EClass(A2)@i'
10. es : EO+(Info)@i'
11. P : E ─→ B ─→ ℙ@i'
12. single-valued-classrel(es;X1;A1)@i
13. single-valued-classrel(es;X2;A2)@i
14. disjoint-classrel(es;A1;X1;A2;X2)@i
15. e : E@i
16. ¬↑first(e)
17. ¬↑e ∈_b X2
18. ¬↑e ∈_b X1
19. ∀e1:E
      ((e1 < e)
      ⇒ (∀s:B. ∀e':E.
            (e' ≤loc e1
            ⇒ if first(e')
               then s = (init loc(e')) ∈ B
               else s ∈ state-class2(init;tr1;X1;tr2;X2)(pred(e')) ∧ P[pred(e');s]
               fi
            ⇒ if e' ∈_b X1 then ∀a:A1. (a ∈ X1(e') ⇒ P[e';tr1 loc(e') a s])
               if e' ∈_b X2 then ∀a:A2. (a ∈ X2(e') ⇒ P[e';tr2 loc(e') a s])
               else P[e';s]
               fi ))
      ⇒ (∀v:B. (v ∈ state-class2(init;tr1;X1;tr2;X2)(e1) ⇒ P[e1;v])))
20. ∀s:B. ∀e':E.
      (e' ≤loc e
      ⇒ if first(e')
         then s = (init loc(e')) ∈ B
         else s ∈ state-class2(init;tr1;X1;tr2;X2)(pred(e')) ∧ P[pred(e');s]
         fi
      ⇒ if e' ∈_b X1 then ∀a:A1. (a ∈ X1(e') ⇒ P[e';tr1 loc(e') a s])
         if e' ∈_b X2 then ∀a:A2. (a ∈ X2(e') ⇒ P[e';tr2 loc(e') a s])
         else P[e';s]
         fi )@i
21. v : B@i
22. v ∈ state-class2(init;tr1;X1;tr2;X2)(e)@i
23. v = state-class2(init;tr1;X1;tr2;X2)(e) ∈ B
⊢ P[e;state-class2(init;tr1;X1;tr2;X2)(pred(e))]

Latex:

Latex:
1. [Info] : Type 2. [B] : Type 3. [A1] : Type 4. [A2] : Type 5. init : Id {}\mrightarrow{} B@i 6. tr1 : Id {}\mrightarrow{} A1 {}\mrightarrow{} B {}\mrightarrow{} B@i 7. tr2 : Id {}\mrightarrow{} A2 {}\mrightarrow{} B {}\mrightarrow{} B@i 8. X1 : EClass(A1)@i' 9. X2 : EClass(A2)@i' 10. es : EO+(Info)@i' 11. e : E@i 12. P : E {}\mrightarrow{} B {}\mrightarrow{} \mBbbP{}@i' 13. v : B@i 14. single-valued-classrel(es;X1;A1)@i 15. single-valued-classrel(es;X2;A2)@i 16. disjoint-classrel(es;A1;X1;A2;X2)@i 17. \mforall{}s:B. \mforall{}e':E. (e' \mleq{}loc e {}\mRightarrow{} if first(e') then s = (init loc(e')) else s \mmember{} state-class2(init;tr1;X1;tr2;X2)(pred(e')) \mwedge{} P[pred(e');s] fi {}\mRightarrow{} if e' \mmember{}\msubb{} X1 then \mforall{}a:A1. (a \mmember{} X1(e') {}\mRightarrow{} P[e';tr1 loc(e') a s]) if e' \mmember{}\msubb{} X2 then \mforall{}a:A2. (a \mmember{} X2(e') {}\mRightarrow{} P[e';tr2 loc(e') a s]) else P[e';s] fi )@i 18. v \mmember{} state-class2(init;tr1;X1;tr2;X2)(e)@i \mvdash{} P[e;v] By Latex: (RepeatFor 2 (MoveToConcl (-6)) THEN CausalInd' THEN (UnivCD THENA Auto) THEN (Assert \mkleeneopen{}v = state-class2(init;tr1;X1;tr2;X2)(e)\mkleeneclose{}\mcdot{} THENA (BLemma `classrel-classfun` THEN Auto THEN ProveFunctional THEN Auto) ) THEN (RWO "-1" 0 THENA Auto) THEN (RWO "state-class2-fun-eq" 0 THENA (Auto THEN BLemma `state-class2-fun-eq` THEN Auto)) THEN Repeat (AutoSplit)) Home Index