%{
This is an extended example of a proof of correctness of mergesort for lists without duplicates. In particular, it is an example of showing that an implementation of sorting (mergesort) matches up with a declarative definition that relates a list to its sort (i.e. the sorted list is a permutation of the unsorted list). 
}%


%{
=== Definitions ===

==== Declarative definitions ====

We must first define natural numbers, lists of natural numbers, comparison on natural numbers, and what it means for one list to be the sorted version of another.
}%

nat : type.

z : nat.
s : nat -> nat.



nat-less	: nat -> nat -> type.

nat-less/z	: nat-less z (s _).

nat-less/s	: nat-less (s N) (s N')
		   <- nat-less N N'. 


nat-list	: type. 

nat-list/nil	: nat-list.

nat-list/cons	: nat -> nat-list -> nat-list. 



nat-list-head-less	: nat -> nat-list -> type. 

nat-list-head-less/nil	: nat-list-head-less N nat-list/nil. 

nat-list-head-less/cons	: nat-list-head-less N (nat-list/cons N' _)
			   <- nat-less N N'. 


nat-list-sorted	: nat-list -> type. 

nat-list-sorted/nil	: nat-list-sorted nat-list/nil.

nat-list-sorted/cons	: nat-list-sorted (nat-list/cons N NL)
			   <- nat-list-head-less N NL
			   <- nat-list-sorted NL. 



in-nat-list	: nat -> nat-list -> type. 

in-nat-list/hit	: in-nat-list N (nat-list/cons N NL).

in-nat-list/miss: in-nat-list N (nat-list/cons N' NL)
		   <- in-nat-list N NL. 

all-in-nat-list	: nat-list -> nat-list -> type. 

all-in-nat-list/nil	: all-in-nat-list nat-list/nil NL. 

all-in-nat-list/cons	: all-in-nat-list (nat-list/cons N NL) NL'
			   <- in-nat-list N NL'
			   <- all-in-nat-list NL NL'. 


%{
For the purposes of this proof, we use a set-theoretic extensional definition of permutation, where two lists are permutations of each other if they contain the same set of elements. This is only a proper definition of permutation if we assume both lists contain no duplicates. This invariant is baked into both our definition of sorted and our definition of mergesort. 
}%

nat-list-permute	: nat-list -> nat-list -> type. 

nat-list-permute/i	: nat-list-permute NL NL'
			   <- all-in-nat-list NL NL'
			   <- all-in-nat-list NL' NL. 



nat-list-declarative-sort	: nat-list -> nat-list -> type. 

nat-list-declarative-sort/i	: nat-list-declarative-sort NL NL'
				   <- nat-list-permute NL NL'
				   <- nat-list-sorted NL'.

%{
==== Definitions used to define mergesort ====
}%

split	: nat-list -> nat-list -> nat-list -> type. 

split/nil	: split nat-list/nil nat-list/nil nat-list/nil.

split/1		: split (nat-list/cons N nat-list/nil) (nat-list/cons N nat-list/nil) 
		   nat-list/nil.

split/cons	: split (nat-list/cons N (nat-list/cons N' NL))
		   (nat-list/cons N NL1)
		   (nat-list/cons N' NL2)
		   <- split NL NL1 NL2.


merge	: nat-list -> nat-list -> nat-list -> type. 

merge/nil-1	: merge nat-list/nil N N. 

merge/nil-2	: merge (nat-list/cons N NL) nat-list/nil (nat-list/cons N NL). 

merge/cons-1	: merge (nat-list/cons N1 NL1)
		   (nat-list/cons N2 NL2) 
		   (nat-list/cons N1 NL)
		   <- nat-less N1 N2
		   <- merge NL1 (nat-list/cons N2 NL2) NL.

merge/cons-2	: merge (nat-list/cons N1 NL1)
		   (nat-list/cons N2 NL2) 
		   (nat-list/cons N2 NL)
		   <- nat-less N2 N1
		   <- merge NL2 (nat-list/cons N1 NL1) NL.

mergesort	: nat-list -> nat-list -> type. 

mergesort/nil	: mergesort nat-list/nil nat-list/nil. 

mergesort/1	: mergesort (nat-list/cons N nat-list/nil) 
		   (nat-list/cons N nat-list/nil). 

mergesort/cons	: mergesort NL1 NL2
		   <- split NL1 NLA NLB
		   <- mergesort NLA NLA'
		   <- mergesort NLB NLB'
		   <- merge NLA' NLB' NL2. 

%{ === Helper definitions used in proofs  === 

<tt>all-in-2 N1 N2 N3</tt> is a judgment that holds when all the elements in <tt>N1</tt> are in the union of <tt>N1</tt> and <tt>N2</tt>/

}%

% all-in-2 N1 N2 N3, everything in N1 is either in N2 or N3

all-in-2	:  nat-list -> nat-list -> nat-list -> type. 

all-in-2/nil	: all-in-2 nat-list/nil NL1 NL2. 

all-in-2/cons-1	: all-in-2 (nat-list/cons N NL) NL1 NL2
		   <- in-nat-list N NL1
		   <- all-in-2 NL NL1 NL2.

all-in-2/cons-2	: all-in-2 (nat-list/cons N NL) NL1 NL2
		   <- in-nat-list N NL2
		   <- all-in-2 NL NL1 NL2.

%{ === Proof that mergesort returns a sorted result === }%

nat-less-trans	: nat-less N1 N2
		   -> nat-less N2 N3
		   -> nat-less N1 N3
		   -> type.
%mode nat-less-trans +D1 +D2 -D3.

-	: nat-less-trans nat-less/z D1 nat-less/z.

-	: nat-less-trans (nat-less/s D1) (nat-less/s D2) (nat-less/s D3)
	   <- nat-less-trans D1 D2 D3.

%worlds () (nat-less-trans _ _ _).
%total (D1) (nat-less-trans D1 _ _). 



merge-head-less	: nat-list-head-less N NL
		   -> nat-less N N'
		   -> merge NL (nat-list/cons N' NL') NL''
		   -> nat-list-head-less N NL''
		   -> type.
%mode merge-head-less +D1 +D2 +D3 -D4.


-	: merge-head-less _ DL merge/nil-1 (nat-list-head-less/cons DL).

-	: merge-head-less _ DL (merge/cons-2 _ _)
	   (nat-list-head-less/cons DL).

-	: merge-head-less (nat-list-head-less/cons DL) _
	   (merge/cons-1 _ _)
	   (nat-list-head-less/cons DL). 


%worlds () (merge-head-less _ _  _ _).
%total (D1) (merge-head-less _ _ D1 _).


merge-sorted	: nat-list-sorted NL1
		   -> nat-list-sorted NL2
		   -> merge NL1 NL2 NL3
		   -> nat-list-sorted NL3
		   -> type.
%mode merge-sorted +D1 +D2 +D3 -D4.

-	: merge-sorted _ D1 merge/nil-1 D1.

-	: merge-sorted D1 _ merge/nil-2 D1.

-	: merge-sorted (nat-list-sorted/cons D1 DHL) D2 
	   (merge/cons-1 DM DL)
	   (nat-list-sorted/cons DS DHL')
	   <- merge-head-less DHL DL DM DHL'
	   <- merge-sorted D1 D2 DM DS.

-	: merge-sorted D2 (nat-list-sorted/cons D1 DHL)
	   (merge/cons-2 DM DL)
	   (nat-list-sorted/cons DS DHL')
	   <- merge-head-less DHL DL DM DHL'
	   <- merge-sorted D1 D2 DM DS.

%worlds () (merge-sorted _ _ _ _).
%total (D1) (merge-sorted _ _ D1 _).


mergesort-sorted	: mergesort NL NL'
			   -> nat-list-sorted NL'
			   -> type.
%mode mergesort-sorted +D1 -D2.

-	: mergesort-sorted mergesort/nil nat-list-sorted/nil.

-	: mergesort-sorted mergesort/1 (nat-list-sorted/cons nat-list-sorted/nil nat-list-head-less/nil).

-	: mergesort-sorted (mergesort/cons DM D2 D1 _) DS
	   <- mergesort-sorted D1 DS1
	   <- mergesort-sorted D2 DS2
	   <- merge-sorted DS1 DS2 DM DS.

%worlds () (mergesort-sorted _ _). 
%total (D1) (mergesort-sorted D1 _).



%{ === Proof that mergesort returns a permutation of the input === }%

all-in-2-wkn-l	: {N}
		   all-in-2 NL NA NB
		   -> all-in-2 NL (nat-list/cons N NA) NB
		   -> type. 
%mode all-in-2-wkn-l +D1 +D2 -D3.

-	: all-in-2-wkn-l _ all-in-2/nil all-in-2/nil.

-	: all-in-2-wkn-l _ (all-in-2/cons-1 DHL DIN)
	   (all-in-2/cons-1 DHL' (in-nat-list/miss DIN))
	   <- all-in-2-wkn-l _ DHL DHL'. 

-	: all-in-2-wkn-l _ (all-in-2/cons-2 DHL DIN)
	   (all-in-2/cons-2 DHL' DIN)
	   <- all-in-2-wkn-l _ DHL DHL'. 

%worlds () (all-in-2-wkn-l _ _ _).
%total (D1) (all-in-2-wkn-l _ D1 _). 



all-in-2-wkn-r	: {N}
		   all-in-2 NL NA NB
		   -> all-in-2 NL NA (nat-list/cons N NB)
		   -> type. 
%mode all-in-2-wkn-r +D1 +D2 -D3.


-	: all-in-2-wkn-r _ all-in-2/nil all-in-2/nil.

-	: all-in-2-wkn-r _ (all-in-2/cons-2 DHL DIN)
	   (all-in-2/cons-2 DHL' (in-nat-list/miss DIN))
	   <- all-in-2-wkn-r _ DHL DHL'. 

-	: all-in-2-wkn-r _ (all-in-2/cons-1 DHL DIN)
	   (all-in-2/cons-1 DHL' DIN)
	   <- all-in-2-wkn-r _ DHL DHL'. 

%worlds () (all-in-2-wkn-r _ _ _).
%total (D1) (all-in-2-wkn-r _ D1 _). 




split-all-in-2	: split NL NA NB
		   -> all-in-2 NL NA NB
		   -> type. 
%mode split-all-in-2 +D1 -D2.

-	: split-all-in-2 split/nil all-in-2/nil.

-	: split-all-in-2 split/1 
	   (all-in-2/cons-1 all-in-2/nil in-nat-list/hit).

-	: split-all-in-2 (split/cons DS1)
	   (all-in-2/cons-1 
	      (all-in-2/cons-2 DS1''' in-nat-list/hit) in-nat-list/hit)
	   <- split-all-in-2 DS1 DS1'
	   <- all-in-2-wkn-l _ DS1' DS1''
	   <- all-in-2-wkn-r _ DS1'' DS1'''.

%worlds () (split-all-in-2 _ _).
%total (D1) (split-all-in-2 D1 _). 


all-in-nat-list-wkn	: {N}
			   all-in-nat-list NL NL'
			   -> all-in-nat-list NL (nat-list/cons N NL')
			   -> type. 
%mode all-in-nat-list-wkn +D1 +D2 -D3.

-	: all-in-nat-list-wkn _ all-in-nat-list/nil all-in-nat-list/nil.

-	: all-in-nat-list-wkn _ (all-in-nat-list/cons DAS DIN)
	   (all-in-nat-list/cons DAS' (in-nat-list/miss DIN))
	   <- all-in-nat-list-wkn _ DAS DAS'.

%worlds () (all-in-nat-list-wkn _ _ _). 
%total (D1) (all-in-nat-list-wkn _ D1 _). 


all-in-nat-list-refl	: {NL}
			   all-in-nat-list NL NL
			   -> type. 
%mode all-in-nat-list-refl +D1 -D2. 

-	: all-in-nat-list-refl _ all-in-nat-list/nil.

-	: all-in-nat-list-refl (nat-list/cons _ NL)
	   (all-in-nat-list/cons DHL' in-nat-list/hit)
	   <- all-in-nat-list-refl NL DHL
	   <- all-in-nat-list-wkn _ DHL DHL'.

%worlds () (all-in-nat-list-refl _ _).
%total (D1) (all-in-nat-list-refl D1 _). 


merge-all-in	: merge NLA NLB NL
		   -> all-in-nat-list NLA NL
		   -> all-in-nat-list NLB NL
		   -> type.
%mode merge-all-in +D1 -D2 -D3.

-	: merge-all-in merge/nil-1 all-in-nat-list/nil D1
	   <- all-in-nat-list-refl _ D1.

-	: merge-all-in merge/nil-2 D1 all-in-nat-list/nil
	   <- all-in-nat-list-refl _ D1. 

-	: merge-all-in (merge/cons-1 DM1 DL)
	   (all-in-nat-list/cons DHL1' in-nat-list/hit)
	   DHL2'
	   <- merge-all-in DM1 DHL1 DHL2
	   <- all-in-nat-list-wkn _ DHL1 DHL1'
	   <- all-in-nat-list-wkn _ DHL2 DHL2'. 

-	: merge-all-in (merge/cons-2 DM1 DL)
	   DHL1'
	   (all-in-nat-list/cons DHL2' in-nat-list/hit)
	   <- merge-all-in DM1 DHL2 DHL1
	   <- all-in-nat-list-wkn _ DHL1 DHL1'
	   <- all-in-nat-list-wkn _ DHL2 DHL2'. 


%worlds () (merge-all-in _ _ _). 
%total (D1) (merge-all-in D1 _ _). 



in-nat-list-trans	: in-nat-list N NL
			   -> all-in-nat-list NL NL'
			   -> in-nat-list N NL'
			   -> type. 
%mode in-nat-list-trans +D1 +D2 -D3. 

-	: in-nat-list-trans in-nat-list/hit
	   (all-in-nat-list/cons _ D1) D1.

-	: in-nat-list-trans (in-nat-list/miss D1)
	   (all-in-nat-list/cons D _)
	   D1'
	   <- in-nat-list-trans D1 D D1'.

%worlds () (in-nat-list-trans _ _ _). 
%total (D1) (in-nat-list-trans D1 _ _). 


all-in-2-trans	: all-in-2 NL NA NB
		   -> all-in-nat-list NA NL'
		   -> all-in-nat-list NB NL'
		   -> all-in-nat-list NL NL'
		   -> type. 
%mode all-in-2-trans +D1 +D2 +D3 -D4. 

-	: all-in-2-trans all-in-2/nil _ _ all-in-nat-list/nil.

-	: all-in-2-trans (all-in-2/cons-1 DHL DIN) 
	   DA DB
	   (all-in-nat-list/cons DHL' DIN')
	   <- all-in-2-trans DHL DA DB DHL'
	   <- in-nat-list-trans DIN DA DIN'.

-	: all-in-2-trans (all-in-2/cons-2 DHL DIN) 
	   DA DB
	   (all-in-nat-list/cons DHL' DIN')
	   <- all-in-2-trans DHL DA DB DHL'
	   <- in-nat-list-trans DIN DB DIN'.

%worlds () (all-in-2-trans _ _ _ _).
%total (D1) (all-in-2-trans D1 _ _ _). 


all-in-2-trans-a	: all-in-2 NL NA NB
			   -> all-in-nat-list NA NA'
			   -> all-in-nat-list NB NB'
			   -> all-in-2 NL NA' NB'
			   -> type. 
%mode all-in-2-trans-a +D1 +D2 +D3 -D4. 

-	: all-in-2-trans-a all-in-2/nil _ _ all-in-2/nil.

-	: all-in-2-trans-a (all-in-2/cons-1 DHL DIN) 
	   DA DB
	   (all-in-2/cons-1 DHL' DIN')
	   <- all-in-2-trans-a DHL DA DB DHL'
	   <- in-nat-list-trans DIN DA DIN'.

-	: all-in-2-trans-a (all-in-2/cons-2 DHL DIN) 
	   DA DB
	   (all-in-2/cons-2 DHL' DIN')
	   <- all-in-2-trans-a DHL DA DB DHL'
	   <- in-nat-list-trans DIN DB DIN'.

%worlds () (all-in-2-trans-a _ _ _ _).
%total (D1) (all-in-2-trans-a D1 _ _ _). 



mergesort-all-in	: mergesort NL1 NL2
			   -> all-in-nat-list NL1 NL2
			   -> type. 
%mode mergesort-all-in +D1 -D2. 

-	: mergesort-all-in mergesort/nil all-in-nat-list/nil.

-	: mergesort-all-in mergesort/1 (all-in-nat-list/cons all-in-nat-list/nil in-nat-list/hit).

-	: mergesort-all-in (mergesort/cons Dmerge Dms2 Dms1 Dsplit)
	   DHLtwo''
	   <- split-all-in-2 Dsplit 
	      (DHLtwo : all-in-2 NL NA NB)
	   <- mergesort-all-in Dms1 
	      (DHL1  : all-in-nat-list NA NA')
	   <- mergesort-all-in Dms2 DHL2
	   <- merge-all-in Dmerge DHL3 DHL4
	   <- all-in-2-trans-a DHLtwo DHL1 DHL2 DHLtwo'
	   <- all-in-2-trans DHLtwo' DHL3 DHL4 DHLtwo''.

%worlds () (mergesort-all-in _ _).
%total (D1) (mergesort-all-in D1 _).



all-in-2-refl-r	: {NL} {NL'}
		   all-in-2 NL NL' NL
		   -> type. 
%mode all-in-2-refl-r +D1 +D2 -D3.

-	: all-in-2-refl-r _ _ all-in-2/nil.

-	: all-in-2-refl-r (nat-list/cons N NL) _ 
	   (all-in-2/cons-2 DHL' in-nat-list/hit)
	   <- all-in-2-refl-r NL _ DHL
	   <- all-in-2-wkn-r _ DHL DHL'.

%worlds () (all-in-2-refl-r _ _ _).
%total (D1) (all-in-2-refl-r D1 _ _). 



all-in-2-refl-l	: {NL} {NL'}
		   all-in-2 NL NL NL'
		   -> type. 
%mode all-in-2-refl-l +D1 +D2 -D3.

-	: all-in-2-refl-l _ _ all-in-2/nil.

-	: all-in-2-refl-l (nat-list/cons N NL) _ 
	   (all-in-2/cons-1 DHL' in-nat-list/hit)
	   <- all-in-2-refl-l NL _ DHL
	   <- all-in-2-wkn-l _ DHL DHL'.

%worlds () (all-in-2-refl-l _ _ _).
%total (D1) (all-in-2-refl-l D1 _ _). 


all-in-2-sym	: all-in-2 NL NA NB
		   -> all-in-2 NL NB NA
		   -> type. 
%mode all-in-2-sym +D1 -D2. 

-	: all-in-2-sym all-in-2/nil all-in-2/nil. 

-	: all-in-2-sym (all-in-2/cons-1 DHL DIN) 
	   (all-in-2/cons-2 DHL' DIN)
	   <- all-in-2-sym DHL DHL'.

-	: all-in-2-sym (all-in-2/cons-2 DHL DIN) 
	   (all-in-2/cons-1 DHL' DIN)
	   <- all-in-2-sym DHL DHL'.

%worlds () (all-in-2-sym _ _).
%total (D1) (all-in-2-sym D1 _).



merge-all-in-2	: merge NA NB NL
		   -> all-in-2 NL NA NB
		   -> type. 
%mode merge-all-in-2 +D1 -D2. 

-	: merge-all-in-2 merge/nil-1  D1
	   <- all-in-2-refl-r  _ _ D1.

-	: merge-all-in-2 merge/nil-2  D1
	   <- all-in-2-refl-l  _ _ D1.

-	: merge-all-in-2 (merge/cons-1 DM _)
	   (all-in-2/cons-1 DHL' in-nat-list/hit)
	   <- merge-all-in-2 DM DHL
	   <- all-in-2-wkn-l _ DHL DHL'. 

-	: merge-all-in-2 (merge/cons-2 DM _)
	   (all-in-2/cons-2 DHL'' in-nat-list/hit)
	   <- merge-all-in-2 DM DHL
	   <- all-in-2-wkn-l _ DHL DHL'
	   <- all-in-2-sym DHL' DHL''. 

%worlds () (merge-all-in-2 _ _). 
%total (D1) (merge-all-in-2 D1 _). 



split-all-in	: split NL NLA NLB
		   -> all-in-nat-list NLA NL
		   -> all-in-nat-list NLB NL
		   -> type.
%mode split-all-in +D1 -D2 -D3.

-	: split-all-in split/nil all-in-nat-list/nil all-in-nat-list/nil.

-	: split-all-in split/1 (all-in-nat-list/cons all-in-nat-list/nil in-nat-list/hit) all-in-nat-list/nil. 

-	: split-all-in (split/cons DS)
	   (all-in-nat-list/cons DHL'' in-nat-list/hit)
	   (all-in-nat-list/cons DBL'' (in-nat-list/miss in-nat-list/hit))
	   <- split-all-in DS DHL DBL
	   <- all-in-nat-list-wkn _ DHL DHL'
	   <- all-in-nat-list-wkn _ DHL' DHL''
	   <- all-in-nat-list-wkn _ DBL DBL'
	   <- all-in-nat-list-wkn _ DBL' DBL''.

%worlds () (split-all-in _ _ _).
%total (D1) (split-all-in D1 _ _). 



mergesort-all-in-r	: mergesort NLA NLB
			   -> all-in-nat-list NLB NLA
			   -> type. 
%mode mergesort-all-in-r +D1 -D2.

-	: mergesort-all-in-r mergesort/nil all-in-nat-list/nil.

-	: mergesort-all-in-r mergesort/1 (all-in-nat-list/cons all-in-nat-list/nil in-nat-list/hit).

-	: mergesort-all-in-r (mergesort/cons Dmerge Dms2 Dms1 Dsplit)
	   DHLtwo''
	   <- merge-all-in-2 Dmerge
	      (DHLtwo : all-in-2 NL NA NB)
	   <- mergesort-all-in-r Dms1 
	      (DHL1  : all-in-nat-list NA NA')
	   <- mergesort-all-in-r Dms2 DHL2
	   <- split-all-in Dsplit DHL3 DHL4
	   <- all-in-2-trans-a DHLtwo DHL1 DHL2 DHLtwo'
	   <- all-in-2-trans DHLtwo' DHL3 DHL4 DHLtwo''.

%worlds () (mergesort-all-in-r _ _). 
%total (D1) (mergesort-all-in-r D1 _). 



mergesort-permute	: mergesort N1 N2
			   -> nat-list-permute N1 N2
			   -> type.
%mode mergesort-permute +D1 -D2. 

-	: mergesort-permute D1 (nat-list-permute/i DB DA)
	   <- mergesort-all-in D1 DA
	   <- mergesort-all-in-r D1 DB. 

%worlds () (mergesort-permute _ _).
%total {} (mergesort-permute _ _).


%{ === Final result === 
Showing the final result merely requires composing the two big intermediate results, namely that mergesort produces a sorted output and that mergesort's output is a permutation of the input.

}%

mergesort-correct	: mergesort N1 N2
			   -> nat-list-declarative-sort N1 N2
			   -> type. 
%mode mergesort-correct +D1 -D2.

-	: mergesort-correct D1 (nat-list-declarative-sort/i Dsorted Dpermute)
	   <- mergesort-permute D1 Dpermute
	   <- mergesort-sorted D1 Dsorted.

%worlds () (mergesort-correct _ _).
%total {} (mergesort-correct _ _). 


%{

----

== Equivalence of definitions of permutations ==

We can also show that <tt>nat-list-permute</tt> under the right constraints (implied by <tt>nat-list-sorted</tt> is equivalent to a definition of permutations as a composition of swaps.

Note: Maybe this should be its own article?

}%


all-in-nat-list-trans	: all-in-nat-list N1 N2
			   -> all-in-nat-list N2 N3
			   -> all-in-nat-list N1 N3
			   -> type. 
%mode all-in-nat-list-trans +D1 +D2 -D3. 

-	: all-in-nat-list-trans all-in-nat-list/nil _ all-in-nat-list/nil.

-	: all-in-nat-list-trans (all-in-nat-list/cons D2 D1) D3
	   (all-in-nat-list/cons D5 D4)
	   <- in-nat-list-trans D1 D3 D4
	   <- all-in-nat-list-trans D2 D3 D5.

%worlds () (all-in-nat-list-trans _ _ _).
%total (D1) (all-in-nat-list-trans D1 _ _). 



nat-list-permutes	: nat-list -> nat-list -> type. 

nat-list-permutes/nil	: nat-list-permutes nat-list/nil nat-list/nil.

nat-list-permutes/cons	: nat-list-permutes (nat-list/cons N1 NL)
			   (nat-list/cons N1 NL')
			   <- nat-list-permutes NL NL'.

nat-list-permutes/swap	: nat-list-permutes 
			   (nat-list/cons N1 (nat-list/cons N2 NL))
			   (nat-list/cons N2 (nat-list/cons N1 NL)).

nat-list-permutes/trans	: nat-list-permutes N1 N3
			   <- nat-list-permutes N1 N2
			   <- nat-list-permutes N2 N3.



nat-list-permutes-all-in: nat-list-permutes N1 N2
			   -> all-in-nat-list N1 N2
			   -> type. 
%mode nat-list-permutes-all-in +D1 -D2.

-	: nat-list-permutes-all-in nat-list-permutes/nil
	   all-in-nat-list/nil.

-	: nat-list-permutes-all-in (nat-list-permutes/cons D1)
	   (all-in-nat-list/cons D2' in-nat-list/hit)
	   <- nat-list-permutes-all-in D1 D2
	   <- all-in-nat-list-wkn _ D2 D2'.

-	: nat-list-permutes-all-in nat-list-permutes/swap
	   (all-in-nat-list/cons 
	      (all-in-nat-list/cons D1'' in-nat-list/hit)
	      (in-nat-list/miss in-nat-list/hit))
	   <- all-in-nat-list-refl _ D1
	   <- all-in-nat-list-wkn _ D1 D1'
	   <- all-in-nat-list-wkn _ D1' D1''.

-	: nat-list-permutes-all-in (nat-list-permutes/trans D2 D1) D3'
	   <- nat-list-permutes-all-in D1 D1'
	   <- nat-list-permutes-all-in D2 D2'
	   <- all-in-nat-list-trans D1' D2' D3'. 

%worlds () (nat-list-permutes-all-in _ _).
%total (D1) (nat-list-permutes-all-in D1 _). 

nat-neq	: nat -> nat -> type.

nat-neq/l	: nat-neq N1 N2
		   <- nat-less N1 N2.
nat-neq/r	: nat-neq N1 N2
		   <- nat-less N2 N1.  

nin-nat-list	: nat -> nat-list -> type.

nin-nat-list/nil	: nin-nat-list N1 nat-list/nil.

nin-nat-list/cons	: nin-nat-list N1 (nat-list/cons N2 NL)
			   <- nat-neq N1 N2
			   <- nin-nat-list N1 NL.

nat-list-no-dups	: nat-list -> type. 

nat-list-no-dups/nil	: nat-list-no-dups nat-list/nil.

nat-list-no-dups/cons	: nat-list-no-dups (nat-list/cons N1 NL)
			   <- nin-nat-list N1 NL
			   <- nat-list-no-dups NL.


nat-list-permutes-refl	: {NL} nat-list-permutes NL NL
			   -> type.
%mode nat-list-permutes-refl +D1 -D2.

-	: nat-list-permutes-refl nat-list/nil nat-list-permutes/nil.

-	: nat-list-permutes-refl (nat-list/cons _ NL)
	   (nat-list-permutes/cons D1)
	   <- nat-list-permutes-refl NL D1. 

%worlds () (nat-list-permutes-refl _ _).
%total (D1) (nat-list-permutes-refl D1 _).



nat-list-permutes-sym	: nat-list-permutes N1 N2
			   -> nat-list-permutes N2 N1
			   -> type.
%mode nat-list-permutes-sym +D1 -D2.

-	: nat-list-permutes-sym nat-list-permutes/nil nat-list-permutes/nil.

-	: nat-list-permutes-sym (nat-list-permutes/cons D1)
	   (nat-list-permutes/cons D1')
	   <- nat-list-permutes-sym D1 D1'.

-	: nat-list-permutes-sym nat-list-permutes/swap nat-list-permutes/swap. 

-	: nat-list-permutes-sym (nat-list-permutes/trans D2 D1)
	   (nat-list-permutes/trans D1' D2')
	   <- nat-list-permutes-sym D1 D1'
	   <- nat-list-permutes-sym D2 D2'.

%worlds () (nat-list-permutes-sym _ _).
%total (D1) (nat-list-permutes-sym D1 _).


nat-list-permutes-swap-head-2	: nat-list-permutes  NN
				   (nat-list/cons N1 (nat-list/cons N2 NL))
				   -> nat-list-permutes 
				      NN
				      (nat-list/cons N2 (nat-list/cons N1 NL))
				   -> type. 
%mode nat-list-permutes-swap-head-2 +D1 -D4.

-	: nat-list-permutes-swap-head-2 D1 
	   (nat-list-permutes/trans nat-list-permutes/swap D1).

%worlds () (nat-list-permutes-swap-head-2 _ _).
%total {} (nat-list-permutes-swap-head-2 _ _).



in-nat-list-permutes	: in-nat-list N1 NL
			   -> nat-list-permutes NL (nat-list/cons N1 NL')
			   -> type. 
%mode in-nat-list-permutes +D1 -D2. 

-	: in-nat-list-permutes in-nat-list/hit D1
	   <- nat-list-permutes-refl _ D1.

-	: in-nat-list-permutes 
	   (in-nat-list/miss (D1 : in-nat-list N (nat-list/cons N2 NL)))
	   DP
	   <- in-nat-list-permutes D1 
	      (DL : nat-list-permutes (nat-list/cons N2 NL) 
		     (nat-list/cons N NL'))
	   <- nat-list-permutes-swap-head-2 (nat-list-permutes/cons DL) DP.

%worlds () (in-nat-list-permutes _ _).
%total (D1) (in-nat-list-permutes D1 _). 



nin-nat-list-permutes	: nin-nat-list N1 NL
			   -> nat-list-permutes NL NL'
			   -> nin-nat-list N1 NL'
			   -> type.
%mode nin-nat-list-permutes +D1 +D2 -D3.

-	: nin-nat-list-permutes _ nat-list-permutes/nil nin-nat-list/nil.

-	: nin-nat-list-permutes (nin-nat-list/cons D1 Dneq)
	   (nat-list-permutes/cons D2)
	   (nin-nat-list/cons D1' Dneq)
	   <- nin-nat-list-permutes D1 D2 D1'.

-	: nin-nat-list-permutes 
	   (nin-nat-list/cons (nin-nat-list/cons D1 Dneq2) Dneq1)
	   nat-list-permutes/swap
	   (nin-nat-list/cons (nin-nat-list/cons D1 Dneq1) Dneq2).

-	: nin-nat-list-permutes D1 (nat-list-permutes/trans D3 D2) 
	   D1''
	   <- nin-nat-list-permutes D1 D2 D1'
	   <- nin-nat-list-permutes D1' D3 D1''.

%worlds () (nin-nat-list-permutes _ _ _). 
%total (D1) (nin-nat-list-permutes _ D1 _).


nat-neq-sym	: nat-neq N1 N2
		   -> nat-neq N2 N1
		   -> type.
%mode nat-neq-sym +D1 -D2.

-	: nat-neq-sym (nat-neq/l D1) (nat-neq/r D1).

-	: nat-neq-sym (nat-neq/r D1) (nat-neq/l D1).

%worlds () (nat-neq-sym _ _).
%total {} (nat-neq-sym _ _).


no-dups-permutes	: nat-list-no-dups N1 
			   -> nat-list-permutes N1 N2
			   -> nat-list-no-dups N2
			   -> type.
%mode no-dups-permutes +D1 +D2 -D3.

-	: no-dups-permutes _ nat-list-permutes/nil nat-list-no-dups/nil.

-	: no-dups-permutes (nat-list-no-dups/cons D2 D1)
	   (nat-list-permutes/cons D3) 
	   (nat-list-no-dups/cons D2' D1')
	   <- nin-nat-list-permutes D1 D3 D1'
	   <- no-dups-permutes D2 D3 D2'.

-	: no-dups-permutes 
	   (nat-list-no-dups/cons 
	      (nat-list-no-dups/cons D3 DninB)
	      (nin-nat-list/cons DninA DneqA1))
	   nat-list-permutes/swap 
	   (nat-list-no-dups/cons 
	      (nat-list-no-dups/cons D3 DninA)
	      (nin-nat-list/cons DninB DneqA1'))
	   <- nat-neq-sym DneqA1 DneqA1'.

-	: no-dups-permutes D1 (nat-list-permutes/trans D3 D2) D1''
	   <- no-dups-permutes D1 D2 D1'
	   <- no-dups-permutes D1' D3 D1''.

%worlds () (no-dups-permutes _ _ _).
%total (D1) (no-dups-permutes _ D1 _).


nat-list-length	: nat-list -> nat -> type.

nat-list-length/z	: nat-list-length nat-list/nil z.

nat-list-length/s	: nat-list-length (nat-list/cons _ NL) (s N)
			   <- nat-list-length NL N.


permutes-length	: nat-list-length NL N
		   -> nat-list-permutes NL NL'
		   -> nat-list-length NL' N
		   -> type.
%mode permutes-length +D1 +D2 -D3.

-	: permutes-length _ nat-list-permutes/nil nat-list-length/z.

-	: permutes-length (nat-list-length/s D1)
	   (nat-list-permutes/cons D2)
	   (nat-list-length/s D3)
	   <- permutes-length D1 D2 D3.

-	: permutes-length (nat-list-length/s (nat-list-length/s D1))
	   nat-list-permutes/swap
	   (nat-list-length/s (nat-list-length/s D1)).

-	: permutes-length D1 (nat-list-permutes/trans D3 D2) 
	   D3'
	   <- permutes-length D1 D2 D1'
	   <- permutes-length D1' D3 D3'.

%worlds () (permutes-length _ _ _).
%total (D1) (permutes-length _ D1 _).



uninhabited	: type.

nat-less-irrefl	: nat-less N1 N1
		   -> uninhabited
		   -> type.
%mode nat-less-irrefl +D1 -D3.

-	: nat-less-irrefl (nat-less/s D1) DU
	   <- nat-less-irrefl D1 DU.

%worlds () (nat-less-irrefl _ _).
%total (D1) (nat-less-irrefl D1 _).

nat-neq-irrefl	: nat-neq N1 N1
		   -> uninhabited
		   -> type.
%mode nat-neq-irrefl +D1 -D2.

-	: nat-neq-irrefl (nat-neq/l D1) DU
	   <- nat-less-irrefl D1 DU.

-	: nat-neq-irrefl (nat-neq/r D1) DU
	   <- nat-less-irrefl D1 DU.

%worlds () (nat-neq-irrefl _ _).
%total {} (nat-neq-irrefl _ _).


uninhabited-in-nat-list	: {N1}{NL}
			   uninhabited
			   -> in-nat-list N1 NL
			   -> type.
%mode uninhabited-in-nat-list +D1 +D2 +D3 -D4.

%worlds () (uninhabited-in-nat-list _ _ _ _).
%total {} (uninhabited-in-nat-list _ _ _ _).

in-nat-list-strengthen	: nat-neq N1 NA
			   -> in-nat-list NA (nat-list/cons N1 NL')
			   -> in-nat-list NA NL'
			   -> type.
%mode in-nat-list-strengthen +D1 +D2 -D4.

-	: in-nat-list-strengthen _ (in-nat-list/miss D1) D1.

-	: in-nat-list-strengthen D1 in-nat-list/hit D1'
	   <- nat-neq-irrefl D1 DU
	   <- uninhabited-in-nat-list _ _ DU D1'.

%worlds () (in-nat-list-strengthen _ _ _).
%total (D1) (in-nat-list-strengthen _ D1 _). 

all-in-strengthen	: nin-nat-list N1 NL
			   -> all-in-nat-list NL (nat-list/cons N1 NL')
			   -> all-in-nat-list NL NL'
			   -> type. 
%mode all-in-strengthen +D1 +D2 -D3.

-	: all-in-strengthen _ all-in-nat-list/nil all-in-nat-list/nil.

-	: all-in-strengthen (nin-nat-list/cons D1 Dneq)
	   (all-in-nat-list/cons DB DA)
	   (all-in-nat-list/cons DB' DA')
	   <- all-in-strengthen D1 DB DB'
	   <- in-nat-list-strengthen Dneq DA DA'.

%worlds () (all-in-strengthen _ _ _).
%total (D1) (all-in-strengthen _ D1 _).



all-in-no-dups-permutes	: {N}
			   nat-list-no-dups NL
 			   -> nat-list-length NL N
 			   -> nat-list-length NL' N
			   -> all-in-nat-list NL NL'
			   -> nat-list-permutes NL NL'
			   -> type.
%mode all-in-no-dups-permutes +N +D1 +D2 +D3 +D4 -D5.

-	: all-in-no-dups-permutes _ _ _ _ all-in-nat-list/nil
	   nat-list-permutes/nil.

-	: all-in-no-dups-permutes 
	   _
	   (nat-list-no-dups/cons D1 DNINN)
	   (nat-list-length/s Dl1)
	   DN
	   (all-in-nat-list/cons (DA : all-in-nat-list NL NL') DIN)
	   (nat-list-permutes/trans DP' (nat-list-permutes/cons DPP))
	   <- in-nat-list-permutes DIN 
	      (DP : nat-list-permutes NL' (nat-list/cons N1 NL''))
 	   <- nat-list-permutes-all-in DP 
	      (DIN' : all-in-nat-list NL' (nat-list/cons N1 NL''))
	   <- permutes-length DN
	      DP (nat-list-length/s D3')
	   <- all-in-nat-list-trans DA DIN' DIN''
 	   <- all-in-strengthen DNINN DIN'' DIN'''
	   <- all-in-no-dups-permutes _ D1 Dl1 D3' DIN''' DPP
 	   <- nat-list-permutes-sym DP DP'.

%worlds () (all-in-no-dups-permutes _ _ _ _ _ _). 
%total (D1) (all-in-no-dups-permutes D1 _ _ _ _ _).

%{

TODO: Finish commentary on the proof. 

{{stub}}
}%