Step * 1 2 1 of Lemma face-maps-commute


1. {Cname List}
2. : ℤ
3. 2 ≤ x
4. (x ∈ I)
5. : ℤ
6. 0 ≤ i
7. i < 2
8. : ℤ
9. 2 ≤ y
10. (y ∈ I)
11. : ℤ
12. 0 ≤ j
13. j < 2
14. (y:=j) ∈ name-morph(I-[x];I-[x; y])
15. : ℤ
16. 2 ≤ a
17. (a ∈ I)
18. x ∈ ℤ
19. y ∈ ℤ
20. y ∈ ℤ
⊢ y ∈ Cname
BY
(D THEN RevHypSubst' (-1) THEN RevHypSubst' (-2) THEN Auto) }


Latex:


Latex:

1.  I  :  \{Cname  List\}
2.  x  :  \mBbbZ{}
3.  2  \mleq{}  x
4.  (x  \mmember{}  I)
5.  i  :  \mBbbZ{}
6.  0  \mleq{}  i
7.  i  <  2
8.  y  :  \mBbbZ{}
9.  2  \mleq{}  y
10.  (y  \mmember{}  I)
11.  j  :  \mBbbZ{}
12.  0  \mleq{}  j
13.  j  <  2
14.  (y:=j)  \mmember{}  name-morph(I-[x];I-[x;  y])
15.  a  :  \mBbbZ{}
16.  2  \mleq{}  a
17.  (a  \mmember{}  I)
18.  a  =  x
19.  a  =  y
20.  x  =  y
\mvdash{}  y  =  y


By


Latex:
(D  6  THEN  RevHypSubst'  (-1)  0  THEN  RevHypSubst'  (-2)  0  THEN  Auto)




Home Index