Step * of Lemma insert-by-sorted-by

βˆ€[T:Type]
  βˆ€eq,r:T βŸΆ T βŸΆ π”Ή.
    Linorder(T;a,b.↑(r a b))
    β‡’ (βˆ€x:T. βˆ€L:T List.  (sorted-by(Ξ»x,y. (↑(r x y));L) β‡’ sorted-by(Ξ»x,y. (↑(r x y));insert-by(eq;r;x;L)))) 
    supposing βˆ€a,b:T.  (↑(eq a b) β‡β‡’ a = b βˆˆ T)
BY
{ InductionOnListβ‹… }

1
1. [T] : Type
2. eq : T βŸΆ T βŸΆ π”Ή
3. r : T βŸΆ T βŸΆ π”Ή
4. βˆ€a,b:T.  (↑(eq a b) β‡β‡’ a = b βˆˆ T)
5. Linorder(T;a,b.↑(r a b))
6. x : T
⊒ sorted-by(Ξ»x,y. (↑(r x y));[]) β‡’ sorted-by(Ξ»x,y. (↑(r x y));insert-by(eq;r;x;[]))

2
1. [T] : Type
2. eq : T βŸΆ T βŸΆ π”Ή
3. r : T βŸΆ T βŸΆ π”Ή
4. βˆ€a,b:T.  (↑(eq a b) β‡β‡’ a = b βˆˆ T)
5. Linorder(T;a,b.↑(r a b))
6. x : T
7. u : T
8. v : T List
9. sorted-by(Ξ»x,y. (↑(r x y));v) β‡’ sorted-by(Ξ»x,y. (↑(r x y));insert-by(eq;r;x;v))
⊒ sorted-by(Ξ»x,y. (↑(r x y));[u / v]) β‡’ sorted-by(Ξ»x,y. (↑(r x y));insert-by(eq;r;x;[u / v]))

Latex:

Latex:
\mforall{}[T:Type]
    \mforall{}eq,r:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbB{}.
        Linorder(T;a,b.\muparrow{}(r  a  b))
        {}\mRightarrow{}  (\mforall{}x:T.  \mforall{}L:T  List.
                    (sorted-by(\mlambda{}x,y.  (\muparrow{}(r  x  y));L)  {}\mRightarrow{}  sorted-by(\mlambda{}x,y.  (\muparrow{}(r  x  y));insert-by(eq;r;x;L)))) 
        supposing  \mforall{}a,b:T.    (\muparrow{}(eq  a  b)  \mLeftarrow{}{}\mRightarrow{}  a  =  b)


By

Latex:
InductionOnList\mcdot{}



Home Index