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. T : Type
2. R : T βΆ T βΆ πΉ
3. x : 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. u : T
8. v : T 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. T : Type
2. R : T βΆ T βΆ πΉ
3. x : 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. u : T
8. Β¬βR[x;u]
9. v : T 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. T : Type
2. R : T βΆ T βΆ πΉ
3. x : 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. u : T
8. Β¬βR[x;u]
9. Β¬βR[u;x]
10. v : T 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. x = 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