Proof of Nuprl Lemma : global-class-iff-bounded-local-class

Step * 3 1 of Lemma global-class-iff-bounded-local-class

1. Info : Type
2. A : {A:Type| valueall-type(A)}
3. X : EClass(A)
4. F : Id ─→ hdataflow(Info;A)@i'
5. ∀es:EO+(Info). ∀e:E.  (X(e) = (snd(F loc(e)*(map(λx.info(x);before(e)))(info(e)))) ∈ bag(A))
6. L : bag(Id)@i'
7. ∀es:EO+(Info). ∀v:A. ∀e:E.  (v ∈ X(e) ⇒ loc(e) ↓∈ L)@i'
8. es : EO+(Info)
9. e : E
10. loc(e) ↓∈ L
⊢ X(e)
= bag-union(bag-mapfilter(λx.(snd(F x*(map(λx@0.info(x@0);before(e)))(info(e))));λx.x = loc(e);
                          bag-remove-repeats(IdDeq;L)))
∈ bag(A)
BY
{ (RepUR ``bag-mapfilter`` 0
   THEN (Assert ⌈[x∈bag-remove-repeats(IdDeq;L)|x = loc(e)] = {loc(e)} ∈ bag(Id)⌉⋅
         THENA (Symmetry
                THEN InstLemma `bag-extensionality2` [⌈Id⌉;⌈IdDeq⌉;⌈{loc(e)}⌉;
                ⌈[x∈bag-remove-repeats(IdDeq;L)|x = loc(e)]⌉]⋅
                THEN Auto
                THEN BackThruSomeHyp
                THEN Auto
                THEN Try (Complete (((BagMemberD (-1) THEN Auto)
                                     THEN (RW assert_pushdownC (-1) THEN Auto)
                                     THEN BagMemberD 0
                                     THEN Auto)))
                THEN BagMemberD (-1)

                THEN (InstLemma `bag-count-filter` [⌈Id⌉;⌈λ₂x.x = loc(e)⌉;⌈IdDeq⌉;⌈x⌉;⌈bag-remove-repeats(IdDeq;L)⌉]⋅

                      THENA Auto
                      )
                THEN (RWO "count-bag-remove-repeats" (-1) THENA Auto)
                THEN (SplitOnHypITE (-1) THENA Auto)
                THEN Try (Complete (((Assert ⌈False⌉⋅ THEN Auto)

                                     THEN (InstLemma `bag-member-count` [⌈Id⌉;⌈IdDeq⌉;⌈loc(e)⌉;⌈L⌉]⋅ THEN Auto)

                                     THEN (D (-2) THEN Auto)
                                     THEN RWO "-5<" (-1)
                                     THEN Auto)))
                THEN RepUR ``single-bag`` 0
                THEN (RWO "bag-count-single" 0 THENA Auto)
                THEN AutoSplit

                THEN Try (Complete ((Fold `eq_id` (-4) THEN RW assert_pushdownC (-4) THEN Auto)))

                THEN (Assert ⌈x ↓∈ [x∈bag-remove-repeats(IdDeq;L)|x = loc(e)]⌉⋅
                      THENA RepeatFor 2 ((BagMemberD 0 THEN Auto))
                      )

                THEN InstLemma `bag-member-count` [⌈Id⌉;⌈IdDeq⌉;⌈x⌉;⌈[x∈bag-remove-repeats(IdDeq;L)|x = loc(e)]⌉]⋅

                THEN Auto
                THEN D (-2)
                THEN Auto)
         )
   ) }

1
1. Info : Type
2. A : {A:Type| valueall-type(A)}
3. X : EClass(A)
4. F : Id ─→ hdataflow(Info;A)@i'
5. ∀es:EO+(Info). ∀e:E.  (X(e) = (snd(F loc(e)*(map(λx.info(x);before(e)))(info(e)))) ∈ bag(A))
6. L : bag(Id)@i'
7. ∀es:EO+(Info). ∀v:A. ∀e:E.  (v ∈ X(e) ⇒ loc(e) ↓∈ L)@i'
8. es : EO+(Info)
9. e : E
10. loc(e) ↓∈ L
11. [x∈bag-remove-repeats(IdDeq;L)|x = loc(e)] = {loc(e)} ∈ bag(Id)
⊢ X(e)

= bag-union(bag-map(λx.(snd(F x*(map(λx@0.info(x@0);before(e)))(info(e))));[x∈bag-remove-repeats(IdDeq;L)|x = loc(e)]))

∈ bag(A)

Latex:

1. Info : Type 2. A : \{A:Type| valueall-type(A)\} 3. X : EClass(A) 4. F : Id {}\mrightarrow{} hdataflow(Info;A)@i' 5. \mforall{}es:EO+(Info). \mforall{}e:E. (X(e) = (snd(F loc(e)*(map(\mlambda{}x.info(x);before(e)))(info(e))))) 6. L : bag(Id)@i' 7. \mforall{}es:EO+(Info). \mforall{}v:A. \mforall{}e:E. (v \mmember{} X(e) {}\mRightarrow{} loc(e) \mdownarrow{}\mmember{} L)@i' 8. es : EO+(Info) 9. e : E 10. loc(e) \mdownarrow{}\mmember{} L \mvdash{} X(e) = bag-union(bag-mapfilter(\mlambda{}x.(snd(F x*(map(\mlambda{}x@0.info(x@0);before(e)))(info(e))));\mlambda{}x.x = loc(e); bag-remove-repeats(IdDeq;L))) By (RepUR ``bag-mapfilter`` 0 THEN (Assert \mkleeneopen{}[x\mmember{}bag-remove-repeats(IdDeq;L)|x = loc(e)] = \{loc(e)\}\mkleeneclose{}\mcdot{} THENA (Symmetry THEN InstLemma `bag-extensionality2` [\mkleeneopen{}Id\mkleeneclose{};\mkleeneopen{}IdDeq\mkleeneclose{};\mkleeneopen{}\{loc(e)\}\mkleeneclose{}; \mkleeneopen{}[x\mmember{}bag-remove-repeats(IdDeq;L)|x = loc(e)]\mkleeneclose{}]\mcdot{} THEN Auto THEN BackThruSomeHyp THEN Auto THEN Try (Complete (((BagMemberD (-1) THEN Auto) THEN (RW assert\_pushdownC (-1) THEN Auto) THEN BagMemberD 0 THEN Auto))) THEN BagMemberD (-1) THEN (InstLemma `bag-count-filter` [\mkleeneopen{}Id\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x.x = loc(e)\mkleeneclose{};\mkleeneopen{}IdDeq\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}; \mkleeneopen{}bag-remove-repeats(IdDeq;L)\mkleeneclose{}]\mcdot{} THENA Auto ) THEN (RWO "count-bag-remove-repeats" (-1) THENA Auto) THEN (SplitOnHypITE (-1) THENA Auto) THEN Try (Complete (((Assert \mkleeneopen{}False\mkleeneclose{}\mcdot{} THEN Auto) THEN (InstLemma `bag-member-count` [\mkleeneopen{}Id\mkleeneclose{};\mkleeneopen{}IdDeq\mkleeneclose{};\mkleeneopen{}loc(e)\mkleeneclose{};\mkleeneopen{}L\mkleeneclose{}]\mcdot{} THEN Auto ) THEN (D (-2) THEN Auto) THEN RWO "-5<" (-1) THEN Auto))) THEN RepUR ``single-bag`` 0 THEN (RWO "bag-count-single" 0 THENA Auto) THEN AutoSplit THEN Try (Complete ((Fold `eq\_id` (-4) THEN RW assert\_pushdownC (-4) THEN Auto))) THEN (Assert \mkleeneopen{}x \mdownarrow{}\mmember{} [x\mmember{}bag-remove-repeats(IdDeq;L)|x = loc(e)]\mkleeneclose{}\mcdot{} THENA RepeatFor 2 ((BagMemberD 0 THEN Auto)) ) THEN InstLemma `bag-member-count` [\mkleeneopen{}Id\mkleeneclose{};\mkleeneopen{}IdDeq\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}; \mkleeneopen{}[x\mmember{}bag-remove-repeats(IdDeq;L)|x = loc(e)]\mkleeneclose{}]\mcdot{} THEN Auto THEN D (-2) THEN Auto) ) ) Home Index