Proof of Nuprl Lemma : A-open-box-image

Step * 1 1 2 2 3 1 2 2 of Lemma A-open-box-image_wf

1. X : CubicalSet
2. A : {X ⊢ _}
3. I : Cname List
4. J : Cname List
5. K : Cname List
6. alpha : X(I)
7. f : name-morph(I;K)
8. nameset(map(f;J)) ⊆r nameset(K)
9. x : nameset(I)
10. ∀x:nameset([x / J]). (f x ∈ nameset(K))
11. i : ℕ2
12. nameset([x / J]) ⊆r name-morph-domain(f;I)
13. bx : A-face(X;A;I;alpha) List
14. A-adjacent-compatible(X;A;I;alpha;bx)
15. ¬(x ∈ J)
16. l_subset(Cname;J;I)

17. (∀f∈bx.(fst(f) ∈ [x / J])) ∧ (∀f1,f2∈bx.  ¬(A-face-name(f1) = A-face-name(f2) ∈ (nameset(I) × ℕ2)))

    (¬(A-face-name(map(λface.A-face-image(X;A;I;K;f;alpha;face);bx)[i@0]) = <f x, 1 - i> ∈ (nameset(K) × ℕ2)))

BY
{ (ParallelOp -6
   THEN (RWO "select-map" 0 THENA Auto)
   THEN MoveToConcl (-1)
   THEN ((Assert (fst(bx[i@0]) ∈ [x / J]) BY Auto) THEN MoveToConcl (-1))
   THEN (GenConclTerm ⌜bx[i@0]⌝⋅ THENA Auto)
   THEN RepeatFor 2 (D -2)
   THEN RepUR ``A-face-image A-face-name`` 0) }

1
1. X : CubicalSet
2. A : {X ⊢ _}
3. I : Cname List
4. J : Cname List
5. K : Cname List
6. alpha : X(I)
7. f : name-morph(I;K)
8. nameset(map(f;J)) ⊆r nameset(K)
9. x : nameset(I)
10. ∀x:nameset([x / J]). (f x ∈ nameset(K))
11. i : ℕ2
12. nameset([x / J]) ⊆r name-morph-domain(f;I)
13. bx : A-face(X;A;I;alpha) List
14. A-adjacent-compatible(X;A;I;alpha;bx)
15. ¬(x ∈ J)
16. l_subset(Cname;J;I)

17. (∀f∈bx.(fst(f) ∈ [x / J])) ∧ (∀f1,f2∈bx.  ¬(A-face-name(f1) = A-face-name(f2) ∈ (nameset(I) × ℕ2)))

18. ∀y:nameset(J). ∀c:ℕ2. (∃f∈bx. A-face-name(f) = <y, c> ∈ (nameset(I) × ℕ2))
19. (∃f∈bx. A-face-name(f) = <x, i> ∈ (nameset(I) × ℕ2))
20. ∀i@0:ℕ||bx||. (¬(A-face-name(bx[i@0]) = <x, 1 - i> ∈ (nameset(I) × ℕ2)))
21. ∀x:nameset(J). (f x ∈ nameset(K))
22. map(f;J) ∈ nameset(K) List
23. f x ∈ nameset(K)
24. ∀fc:A-face(X;A;I;alpha). ((fc ∈ bx) ⇒ (fst(fc) ∈ [x / J]))
25. ∀fc:A-face(X;A;I;alpha). ((fc ∈ bx) ⇒ (↑isname(f (fst(fc)))))
26. i@0 : ℕ||bx||
27. x1 : nameset(I)
28. i1 : ℕ2
29. v2 : A((x1:=i1)(alpha))
30. bx[i@0] = <x1, i1, v2> ∈ A-face(X;A;I;alpha)
⊢ (x1 ∈ [x / J]) ⇒ (¬(<x1, i1> = <x, 1 - i> ∈ (nameset(I) × ℕ2))) ⇒ (¬(<f x1, i1> = <f x, 1 - i> ∈ (nameset(K) × ℕ2)))

Latex:

Latex:
1. X : CubicalSet 2. A : \{X \mvdash{} \_\} 3. I : Cname List 4. J : Cname List 5. K : Cname List 6. alpha : X(I) 7. f : name-morph(I;K) 8. nameset(map(f;J)) \msubseteq{}r nameset(K) 9. x : nameset(I) 10. \mforall{}x:nameset([x / J]). (f x \mmember{} nameset(K)) 11. i : \mBbbN{}2 12. nameset([x / J]) \msubseteq{}r name-morph-domain(f;I) 13. bx : A-face(X;A;I;alpha) List 14. A-adjacent-compatible(X;A;I;alpha;bx) 15. \mneg{}(x \mmember{} J) 16. l\_subset(Cname;J;I) 17. (\mforall{}f\mmember{}bx.(fst(f) \mmember{} [x / J])) \mwedge{} (\mforall{}f1,f2\mmember{}bx. \mneg{}(A-face-name(f1) = A-face-name(f2))) 18. \mforall{}y:nameset(J). \mforall{}c:\mBbbN{}2. (\mexists{}f\mmember{}bx. A-face-name(f) = <y, c>) 19. (\mexists{}f\mmember{}bx. A-face-name(f) = <x, i>) 20. \mforall{}i@0:\mBbbN{}||bx||. (\mneg{}(A-face-name(bx[i@0]) = <x, 1 - i>)) 21. \mforall{}x:nameset(J). (f x \mmember{} nameset(K)) 22. map(f;J) \mmember{} nameset(K) List 23. f x \mmember{} nameset(K) 24. \mforall{}fc:A-face(X;A;I;alpha). ((fc \mmember{} bx) {}\mRightarrow{} (fst(fc) \mmember{} [x / J])) 25. \mforall{}fc:A-face(X;A;I;alpha). ((fc \mmember{} bx) {}\mRightarrow{} (\muparrow{}isname(f (fst(fc))))) \mvdash{} \mforall{}i@0:\mBbbN{}||bx|| (\mneg{}(A-face-name(map(\mlambda{}face.A-face-image(X;A;I;K;f;alpha;face);bx)[i@0]) = <f x, 1 - i>)) By Latex: (ParallelOp -6 THEN (RWO "select-map" 0 THENA Auto) THEN MoveToConcl (-1) THEN ((Assert (fst(bx[i@0]) \mmember{} [x / J]) BY Auto) THEN MoveToConcl (-1)) THEN (GenConclTerm \mkleeneopen{}bx[i@0]\mkleeneclose{}\mcdot{} THENA Auto) THEN RepeatFor 2 (D -2) THEN RepUR ``A-face-image A-face-name`` 0) Home Index