Step * 1 1 1 1 1 1 of Lemma cosetTC-least


1. coSet{i:l}
2. transitive-set(s)
3. : ℤ
4. n ≠ 0
5. [%2] 0 < n
6. 0 <  (∀x:coSet{i:l}. ((x ⊆ s)  (∀p:coPath(T.T;x;n 1). (coPath-at(n 1;x;p) ∈ s))))
7. 0 < n
8. coSet{i:l}
9. (x ⊆ s)
10. coW-dom(T.T;x)
11. p1 coPath(T.T;coW-item(x;t);n 1)
⊢ (coPath-at(n 1;coW-item(x;t);p1) ∈ s)
BY
((Assert coW-item(x;t) set-item(x;t) BY
          Computation)
   THEN (RWO "-1" THENA Auto)
   THEN (RWO "-1" (-2) THENA Auto)
   THEN Thin (-1)) }

1
1. coSet{i:l}
2. transitive-set(s)
3. : ℤ
4. n ≠ 0
5. [%2] 0 < n
6. 0 <  (∀x:coSet{i:l}. ((x ⊆ s)  (∀p:coPath(T.T;x;n 1). (coPath-at(n 1;x;p) ∈ s))))
7. 0 < n
8. coSet{i:l}
9. (x ⊆ s)
10. coW-dom(T.T;x)
11. p1 coPath(T.T;set-item(x;t);n 1)
⊢ (coPath-at(n 1;set-item(x;t);p1) ∈ s)


Latex:


Latex:

1.  s  :  coSet\{i:l\}
2.  transitive-set(s)
3.  n  :  \mBbbZ{}
4.  n  \mneq{}  0
5.  [\%2]  :  0  <  n
6.  0  <  n  -  1  {}\mRightarrow{}  (\mforall{}x:coSet\{i:l\}.  ((x  \msubseteq{}  s)  {}\mRightarrow{}  (\mforall{}p:coPath(T.T;x;n  -  1).  (coPath-at(n  -  1;x;p)  \mmember{}  s))))
7.  0  <  n
8.  x  :  coSet\{i:l\}
9.  (x  \msubseteq{}  s)
10.  t  :  coW-dom(T.T;x)
11.  p1  :  coPath(T.T;coW-item(x;t);n  -  1)
\mvdash{}  (coPath-at(n  -  1;coW-item(x;t);p1)  \mmember{}  s)


By


Latex:
((Assert  coW-item(x;t)  \msim{}  set-item(x;t)  BY
                Computation)
  THEN  (RWO  "-1"  0  THENA  Auto)
  THEN  (RWO  "-1"  (-2)  THENA  Auto)
  THEN  Thin  (-1))




Home Index