Next: Membership Up: List Previous: Lists and products

Intuitively, Adjoin a k l holds if it is possible to insert the element a in the list k and obtain the list l. This relation can be used to define permutations, as seen below.

{s|Type}{xs|list s}{a|s}{axs|list s}(Adjoin a xs axs)->{b:s}
Adjoin a (cons b xs) (cons b axs)
({a:s}{xs:list s}C_Adjoin a xs (cons a xs))->
({xs|list s}{a|s}{axs|list s}(Adjoin a xs axs)->{b:s}
[xs1:list s][xs|list s][a|s][axs|list s][x1:Adjoin a xs axs][b:s]

(Eq ys (cons a xs) \/
Ex ([xs':list s]
Ex ([ys':list s]
Ex ([c:s]
(Eq xs (cons c xs') /\ Eq ys (cons c ys') /\
{s|Type}{a,b|s}{xs,ys|list s}(Adjoin a (cons b xs) ys)->
(Eq ys (cons a (cons b xs)) \/
Ex ([ys':list s](Eq ys (cons b ys') /\ Adjoin a xs ys')))
{s|Type}{a,b|s}{xs,ys|list s}(Adjoin a xs (cons b ys))->
((Eq a b /\ Eq xs ys) \/
Ex ([xs':list s](Eq xs (cons b xs') /\ Adjoin a xs' ys)))
{s|Type}{a|s}{xs|list s}(Adjoin a (nil s) xs)->
Eq xs (cons a (nil s))
{s|Type}{a|s}{xs|list s}not (Adjoin a xs (nil s))
{s|Type}{a|s}{xs|list s}(Adjoin a xs (cons a (nil s)))->
Eq xs (nil s)