Step * of Lemma l-ordered-decomp2

No Annotations
βˆ€[T:Type]. βˆ€[R:T βŸΆ T βŸΆ π”Ή]. βˆ€[x:T].
  (βˆ€[L:T List]
     (L (filter(Ξ»y.R[y;x];L) [x filter(Ξ»y.R[x;y];L)]) βˆˆ (T List)) supposing 
        (l-ordered(T;x,y.↑R[x;y];L) and 
        (x βˆˆ L))) supposing 
     (Trans(T;x,y.↑R[x;y]) and 
     Irrefl(T;x,y.↑R[x;y]) and 
     StAntiSym(T;x,y.↑R[x;y]))
BY
(InductionOnList
   THEN Reduce 0
   THEN RW ListC 0
   THEN Try (Complete (Auto))
   THEN Repeat (AutoSplit)
   THEN Auto
   THEN DProdsAndUnions
   THEN Try (Complete ((All(RepUR ``irrefl st_anti_sym``) THEN Assert βŒœFalseβŒβ‹… THEN Auto)))) }

1
1. Type
2. T βŸΆ T βŸΆ π”Ή
3. T
4. StAntiSym(T;x,y.↑R[x;y])
5. Irrefl(T;x,y.↑R[x;y])
6. Trans(T;x,y.↑R[x;y])
7. T
8. List
9. (v (filter(Ξ»y.R[y;x];v) [x filter(Ξ»y.R[x;y];v)]) βˆˆ (T List)) supposing 
      (l-ordered(T;x,y.↑R[x;y];v) and 
      (x βˆˆ v))
10. β†‘R[u;x]
11. β†‘R[x;u]
12. (x βˆˆ v)
13. l-ordered(T;x,y.↑R[x;y];v)
14. βˆ€y:T. ((y βˆˆ v) β‡’ (↑R[u;y]))
⊒ [u v] [u (filter(Ξ»y.R[y;x];v) [x; [u filter(Ξ»y.R[x;y];v)]])] βˆˆ (T List)

2
1. Type
2. T βŸΆ T βŸΆ π”Ή
3. T
4. StAntiSym(T;x,y.↑R[x;y])
5. Irrefl(T;x,y.↑R[x;y])
6. Trans(T;x,y.↑R[x;y])
7. T
8. Β¬β†‘R[x;u]
9. List
10. (v (filter(Ξ»y.R[y;x];v) [x filter(Ξ»y.R[x;y];v)]) βˆˆ (T List)) supposing 
       (l-ordered(T;x,y.↑R[x;y];v) and 
       (x βˆˆ v))
11. β†‘R[u;x]
12. (x βˆˆ v)
13. l-ordered(T;x,y.↑R[x;y];v)
14. βˆ€y:T. ((y βˆˆ v) β‡’ (↑R[u;y]))
⊒ [u v] [u (filter(Ξ»y.R[y;x];v) [x filter(Ξ»y.R[x;y];v)])] βˆˆ (T List)

3
1. Type
2. T βŸΆ T βŸΆ π”Ή
3. T
4. StAntiSym(T;x,y.↑R[x;y])
5. Irrefl(T;x,y.↑R[x;y])
6. Trans(T;x,y.↑R[x;y])
7. T
8. Β¬β†‘R[x;u]
9. Β¬β†‘R[u;x]
10. List
11. (v (filter(Ξ»y.R[y;x];v) [x filter(Ξ»y.R[x;y];v)]) βˆˆ (T List)) supposing 
       (l-ordered(T;x,y.↑R[x;y];v) and 
       (x βˆˆ v))
12. u βˆˆ T
13. l-ordered(T;x,y.↑R[x;y];v)
14. βˆ€y:T. ((y βˆˆ v) β‡’ (↑R[u;y]))
⊒ [u v] (filter(Ξ»y.R[y;x];v) [x filter(Ξ»y.R[x;y];v)]) βˆˆ (T List)


Latex:


Latex:
No  Annotations
\mforall{}[T:Type].  \mforall{}[R:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[x:T].
    (\mforall{}[L:T  List]
          (L  =  (filter(\mlambda{}y.R[y;x];L)  @  [x  /  filter(\mlambda{}y.R[x;y];L)]))  supposing 
                (l-ordered(T;x,y.\muparrow{}R[x;y];L)  and 
                (x  \mmember{}  L)))  supposing 
          (Trans(T;x,y.\muparrow{}R[x;y])  and 
          Irrefl(T;x,y.\muparrow{}R[x;y])  and 
          StAntiSym(T;x,y.\muparrow{}R[x;y]))


By


Latex:
(InductionOnList
  THEN  Reduce  0
  THEN  RW  ListC  0
  THEN  Try  (Complete  (Auto))
  THEN  Repeat  (AutoSplit)
  THEN  Auto
  THEN  DProdsAndUnions
  THEN  Try  (Complete  ((All(RepUR  ``irrefl  st\_anti\_sym``)  THEN  Assert  \mkleeneopen{}False\mkleeneclose{}\mcdot{}  THEN  Auto))))




Home Index