Indexed HOAS nat bijection

From The Twelf Project
Jump to: navigation, search
This is Literate Twelf
Code: here
Status: %% OK %%
Output: here.

Bijection from indexed HOAS to natural numbers

This file shows an *indexed* HOAS term type and a mapping from these terms to the natural numbers. It depends on John Boyland's library signatures, in particular void, bool, nat, natpair and multiset.

This file shows some of the extensions needed to handle indexed HOAS terms above and beyond those of "regular" HOAS terms (which is the topic of the [HOAS_nat_bijection] page). In the comments here, I emphasize those different aspects rather than repeat the same discussion.






Definitions

The syntax

Here we define multi-arity functions that are typed to avoid type errors (hence, no higher-order functions in the syntax -- but see "rec" which is the typed Y combinator). This syntax is rather impoverished, but it would be fairly easily to add "succ", "ifzero" terms. By "easy", I mean the addition would cause no new technical issues. It would still change al he arithmetic parts of the proofs dramatically. For this reason, I would like to implement a tool that would generate such proofs for any HOAS family of terms.

term : nat -> type.

%abbrev t = term z.


lit : nat -> t.

app : term (s N) -> t -> term N.

lam : (t -> term N) -> term (s N).

rec : (term (s N) -> term (s N)) -> term (s N).



%block blocksimple : some {n} block {v:term n}.

Equality

eq : term N1 -> term N2 -> type.


eq/ : eq T T.

Variable levels

As with the non-indexed case, a variable level is the (nonzero) natural number for a variable. But unlike before 'varlevel' is now an abbreviation for a more complex relation that permits adjustment of the index level.

varadjlevel : term N -> nat -> nat -> type.


%abbrev varlevel : term N -> nat -> type = [T] [L] varadjlevel T N L.


%block blockvar : some {n} {l} block {v:term n} {vl:varlevel v (s l)}.

Mapping

The bijection from terms to nat is called "tonat". There is a separate mapping for each index, which makes sense becaue each index represents a different type. Unlike the non-indexed case, we need to handle an unbounded number of different types of variables, so we can't just pass one extra int, or even a fixed number of ints. Instead we need to pass a structure that represents an unbounded number of ints. We use `multiset' to represent this structure. The elements of the multiset represent the levels that came "before".

Another interesting aspect is that not all constructors for the indexed type are available for all indices. For instane `lit' is only for the 0-index and rec only for non-zero indices. On the other hand, `app' can occur for any index. Since the mapping is separate for every index, and the mapping must be one-to-one as well as onto, we must work carefully that every natural number is mapped onto exactly once. Variables are handled (as before) by reserving the first VN spots for variables, where (unlike before) VN depends on the index. Ignoring variables, `lit' takes the veen numbers and `app' takes the odd numbers for the 0-indexed terms. For the nonzero-indexed terms, app takes the odd numbers (of course) and lam and rec share the even numbers.

tonat* : {N} multiset -> term N -> nat -> type.

%abbrev tonat = tonat* _ multiset/0.


tonat/var : 
	count MS N VN ->
	varlevel V L ->
	plus M L VN ->
    tonat* N MS V M.
	
tonat/lit :
	count MS z VN ->
	times (s (s z)) M TM ->
	plus VN TM M' ->
    tonat* z MS (lit M) M'.

tonat/app :
	count MS N VN ->
	tonat* _ MS T1 M1 ->
        tonat* _ MS T2 M2 ->
        natpair`pair2nat (natpair/ M1 M2) M ->
	times (s (s z)) M TM ->
	plus VN (s TM) M' ->
    tonat* N MS (app T1 T2) M'.

tonat/lam :
	count MS (s N) VN ->
	count MS z ZN ->
	multiset`add MS z MS' ->
	({v:term z} (varlevel v (s ZN)) ->
         tonat* N MS' (F v) M) ->
	times (s (s (s (s z)))) M TM ->
	plus VN TM M' ->
    tonat* (s N) MS (lam F) M'.

tonat/rec :
	count MS (s N) VN ->
	multiset`add MS (s N) MS' ->
	({f} (varlevel f (s VN)) ->
         tonat* (s N) MS' (F f) M) ->
	times (s (s (s (s z)))) M TM ->
	plus VN (s (s TM)) M' ->
    tonat* (s N) MS (rec F) M'.

Utility lemmas

The following theorems prove obvious simple things about the basic relations. They following the conventions established in John Boyland's library signatures.

%theorem false-implies-eq :
	forall* {N1} {N2} {T1:term N1} {T2:term N2}
	forall	{F:void}
	exists	{EQ:eq T1 T2}
	true.

%worlds (blocksimple) (false-implies-eq _ _).
%total { }  (false-implies-eq _ _).


%theorem false-implies-varlevel :
	forall*	{N} {V:term N} {L}
	forall	{F:void}
	exists	{VL:varlevel V L}
	true.

%worlds (blocksimple | blockvar) (false-implies-varlevel _ _).
%total { } (false-implies-varlevel _ _).


%theorem varlevel-respects-eq :
	forall* {N} {V:term N} {L1} {L2}
	forall	{VL1:varlevel V L1}
		{E:nat`eq L1 L2}
	exists	{VL2:varlevel V L2}
	true.

- : varlevel-respects-eq VL nat`eq/ VL.

%worlds (blocksimple | blockvar) (varlevel-respects-eq _ _ _).
%total { } (varlevel-respects-eq _ _ _).


%theorem false-implies-tonat :
	forall* {N} {MS} {T} {M}
	forall	{F:void}
	exists	{TN:tonat* N MS T M}
	true.

%worlds (blocksimple | blockvar) (false-implies-tonat _ _).
%total { } (false-implies-tonat _ _).


%theorem tonat-respects-eq :
	forall* {N1} {MS1} {T1} {M1}
		{N2} {MS2} {T2} {M2}
	forall	{TN1:tonat* N1 MS1 T1 M1}
		{EM: multiset`eq MS1 MS2}
		{ET: eq T1 T2}
		{EN: nat`eq M1 M2}
	exists	{TN2: tonat* N2 MS2 T2 M2}
	true.

- : tonat-respects-eq TN multiset`eq/ eq/ nat`eq/ TN.

%worlds (blocksimple | blockvar) (tonat-respects-eq _ _ _ _ _).
%total { } (tonat-respects-eq _ _ _ _ _).

Proof of totality of tonat

As with the non-indexed case, proving totality is surprisingly tricky. The problem is that when we get to a variable, we need to make sure that (1) the variable has a level associated with it and (2) the level is in the range 1..VN where VN is the number of variables of this index that have been seen in the context. Twelf's blocks are useful for (1) but not for (2) because there's no way to connect the context with the current nesting level.

For this proof, I generalized/extended the "case" technique to handle indexed variables. The proof is almost the same. The multisets add extra paremeters but the basic structure is the same.

Auxiliary definitions

raw variables

A variable is raw if we haven't verified that it has a level in range. Non variables are not raw.

israw* : {N} term N -> bool -> type.

%abbrev israw = israw* _.

%abbrev rawvar = [T] israw T true.


israw/lit : israw (lit _) false.

israw/app : israw (app _ _) false.

israw/lam : israw (lam _) false.

israw/rec : israw (rec _) false.

case analysis

We case analysis terms with two cases for variables. The raw case is used only internally and can be ignored in "clients" that don't use israw.

case* : {N} multiset -> term N -> type.

%abbrev case = case* _.


case/lit : case _ (lit _).

case/app : case MS T1 -> case MS T2 -> case MS (app T1 T2).

case/lam :
	count MS z VN ->
	add MS z MS' ->
	({v} varlevel v (s VN) -> 
	 case MS' (F v)) -> 
    case MS (lam F).

case/rec :
	count MS (s N) VN ->
	multiset`add MS (s N) MS' ->
	({f} varlevel f (s VN) ->
	 case MS' (F f)) ->
    case* (s N) MS (rec F).

case/var : 
	count MS N VN ->
	varlevel V FL ->
	nat`ge VN FL -> 
    case* N MS V.

case/raw : rawvar V -> case _ V.

Theorems about auxiliary definitions

%theorem israw-total* :
	forall* {N}
	forall	{T:term N}
	exists	{B} {I:israw T B}
	true.

%abbrev israw-total = israw-total* _ _.

- : israw-total israw/lit.

- : israw-total israw/app.

- : israw-total israw/lam.

- : israw-total israw/rec.

fake : type.
- : fake <- {i:israw-total* T B I} israw-total* T' B' I'.
- : fake <- {i:israw-total* T B I} israw T' B'.

%block blockraw : some {n} block {v:term n} {rv:rawvar v} {irt:israw-total rv}.

%worlds (blockraw) (israw-total* _ _ _).
%total { } (israw-total* _ _ _).

The following theorem handles one variable converting it from raw to handle a level that is in the required range. This is an important technique for handle variables in Twelf: one at a time. Unlike the one2one theorem (see later), we don't have to do extraordinary things to handle having multiple types. (Although we do need some extra lemmas to ahndle facts about multisets.)

%theorem var-gets-level :
	forall* {M} {N} {VN} {T:term M -> term N} {L} {MS}
	forall	{F: {v:term M} {rv:rawvar v} {i:israw-total rv} 
	            case MS (T v)}
		{MC: count MS M VN}
		{GE: nat`ge VN L}
	exists  {F': {v:term M} (varlevel v L) -> case MS (T v)}
	true.

- : var-gets-level ([f] [r] [i] (case/raw r)) MC GE
                   ([f] [fl] (case/var MC fl GE)).

- : var-gets-level ([f] [r] [i] (case/raw R)) _ _
                   ([f] [fl] (case/raw R)).

- : var-gets-level ([f] [r] [i] (case/var MC VL GE)) _ _
                   ([f] [fl] (case/var MC VL GE)).

- : var-gets-level ([f] [r] [i] (case/lit: case MS (lit O))) _ _
                   ([f] [fl] (case/lit)).

- : var-gets-level ([f] [r] [i] (case/app (C1 f r i) (C2 f r i))) MC GE
                   ([f] [fl] (case/app (C1' f fl) (C2' f fl)))
    <- var-gets-level C1 MC GE C1'
    <- var-gets-level C2 MC GE C2'.

%theorem var-gets-level/L :
	forall* {MS} {N1} {FN1} {N2} {FN2} {MS'} {L1} {B}
	forall	{MC1: multiset`count MS N1 FN1}
		{MC2: multiset`count MS N2 FN2}
		{MA2: multiset`add MS N2 MS'}
		{GE: nat`ge FN1 L1}
		{EQ?: nat`eq? N1 N2 B}
	exists	{FN1'}
		{MC1': multiset`count MS' N1 FN1'}
		{GE': nat`ge FN1' L1}
	true.

- : var-gets-level/L MC _ MA FN>=L nat`eq?/yes _ MC' (ge/> FN+1>L)
    <- ge-implies-succ-gt FN>=L FN+1>L
    <- multiset`count-add-implies-count MC MA MC'.

- : var-gets-level/L MC1 _ MA2 GE (nat`eq?/no N1<>N2) _ MC1' GE
    <- multiset`add-preserves-count MC1 MA2 N1<>N2 MC1'.

%worlds () (var-gets-level/L _ _ _ _ _ _ _ _).
%total { } (var-gets-level/L _ _ _ _ _ _ _ _).

- : var-gets-level 
	([f] [r] [i] (case/lam MS^0=FN' MSU ([v] [vl] C v vl f r i))) MC GE
        ([f] [fl]    (case/lam MS^0=FN' MSU ([v] [vl] C' v vl f fl)))
    <- nat`eq?-total EQ?
    <- var-gets-level/L MC MS^0=FN' MSU GE EQ? _ MC' GE'
    <- ({v} {vl:varlevel v _} (var-gets-level (C v vl) MC' GE' (C' v vl))).

- : var-gets-level 
	([f] [r] [i] (case/rec MS^N'=FN' MSU ([f'] [fl'] (C f' fl' f r i))))
        MS^N=FN FN>=L 
        ([f] [fl] (case/rec MS^N'=FN' MSU ([f'] [fl'] (C' f' fl' f fl))))
    <- nat`eq?-total EQ?
    <- var-gets-level/L MS^N=FN MS^N'=FN' MSU FN>=L EQ? _ MS'^N=FN'' FN''>=L
    <- ({f'} {fl'} (var-gets-level (C f' fl') MS'^N=FN'' FN''>=L (C' f' fl'))).

%worlds (blockvar | blockraw) (var-gets-level _ _ _ _).
%total F (var-gets-level F _ _ _).

We are now ready to prove that we can always "case" a term. This works almost the same as for non-indexed terms.

%theorem case-total* :
	forall* {N}
	forall	{T:term N}
	exists	{C:case multiset/0 T}
	true.

%abbrev case-total = case-total* _.

%theorem case-total/L :
	forall* {B} {N} {MS}
	forall	{T:term N} {I:israw T B}
	exists	{C:case MS T}
	true.

- : case-total/L _ _ (case/lit).

- : case-total/L _ _ (case/app C1 C2)
    <- israw-total I1
    <- case-total/L _ I1 C1
    <- israw-total I2
    <- case-total/L _ I2 C2.

- : case-total/L _ _ (case/lam MC MA ([f] [fl] (C' f fl)))
    <- multiset`count-total MC
    <- multiset`add-total MA
    <- ({v} {r:rawvar v} {i:israw-total r}
        israw-total (I v r i: israw _ B))
    <- ({v} {r:rawvar v} {i:israw-total r} 
        case-total/L _ (I v r i) (C v r i))
    <- multiset`count-add-implies-count MC MA MC'
    <- var-gets-level C MC' (nat`ge/= nat`eq/) C'.

- : case-total/L _ _ (case/rec MC MA ([f] [fl] (C' f fl)))
    <- multiset`count-total MC
    <- multiset`add-total MA
    <- ({v} {r:rawvar v} {i:israw-total r}
        israw-total (I v r i: israw _ B))
    <- ({v} {r:rawvar v} {i:israw-total r} 
        case-total/L _ (I v r i) (C v r i))
    <- multiset`count-add-implies-count MC MA MC'
    <- var-gets-level C MC' (nat`ge/= nat`eq/) C'.

- : case-total/L V R (case/raw R).

%worlds (blockraw) (case-total/L _ _ _).
%total T (case-total/L T _ _).

- : case-total* T C
    <- israw-total I
    <- case-total/L T I C.

%worlds () (case-total* _ _).
%total { } (case-total* _ _).

Main theorem

We are ready now to prove totality of the relation. We case the term first and then have everything we need to push through totality.

%theorem tonat-total* :
	forall* {N}
	forall	{T:term N}
	exists	{M:nat} {D:tonat T M}
	true.

%abbrev tonat-total = tonat-total* _ _.

%theorem tonat-total/L :
	forall* {N:nat} {T:term N} {MS}
	forall  {C:case MS T}
	exists  {M:nat} {D:tonat* N MS T M}
	true.

- : tonat-total/L (case/var MC VL GE) _ (tonat/var MC VL P)
    <- ge-implies-plus GE _ P.

- : tonat-total/L (case/lit) _ (tonat/lit MC T P)
    <- count-total MC
    <- times-total T
    <- plus-total P.

- : tonat-total/L (case/app C1 C2) _ (tonat/app MC TN1 TN2 P2N T P)
    <- count-total MC
    <- tonat-total/L C1 _ TN1
    <- tonat-total/L C2 _ TN2
    <- pair2nat-total P2N
    <- times-total T
    <- plus-total P.

- : tonat-total/L (case/lam MCz MSU ([v] [vl] (C v vl))) _ 
                  (tonat/lam MC MCz MSU ([v] [vl] (TN v vl)) T P)
    <- ({v} {vl:varlevel v (s N)} tonat-total/L (C v vl) _ (TN v vl))
    <- count-total MC
    <- times-total T
    <- plus-total P.

- : tonat-total/L (case/rec MC MA ([v] [vl] (C v vl))) _ 
                  (tonat/rec MC MA ([v] [vl] (TN v vl)) T P)
    <- ({v} {vl} tonat-total/L (C v vl) _ (TN v vl))
    <- times-total T
    <- plus-total P.

%worlds (blockvar) (tonat-total/L _ _ _).
%total (C) (tonat-total/L C _ _).

- : tonat-total TN
    <- case-total C
    <- tonat-total/L C _ TN.

%worlds () (tonat-total* _ _ _).
%total { } (tonat-total* _ _ _).

Proof of the determinicity of the mapping

As with the non-indexed case, this aspect is easy to prove.

Auxiliary theorems

We prove that variable levels are "unique" and that they are never zero. The proofs are trivial: Twelf can accept them from the context alone.

%theorem varlevel-deterministic :
	forall* {N} {V:term N} {L1} {L2}
	forall	{VL1:varlevel V L1}
		{VL2:varlevel V L2}
	exists	{E:nat`eq L1 L2}
	true.

- : varlevel-deterministic _ _ nat`eq/.

%worlds (blockvar) (varlevel-deterministic _ _ _).
%total { } (varlevel-deterministic _ _ _).


%theorem varlevel-contradiction :
	forall* {N} {V:term N} {L}
	forall	{VL:varlevel V L}
		{E:nat`eq L z}
	exists	{F:void}
	true.

%worlds (blockvar) (varlevel-contradiction _ _ _).
%total { }  (varlevel-contradiction _ _ _).

Main Theorem

%theorem tonat-deterministic :
	forall* {N1} {N2} {T1:term N1} {T2:term N2} {M1} {M2}
	forall	{TN1:tonat T1 M1} 
		{TN2:tonat T2 M2}
		{E: eq T1 T2}
	exists	{E: nat`eq M1 M2}
	true.

%theorem tonat-deterministic/L :
	forall* {N} {T:term N} {MS1} {MS2} {M1} {M2}
	forall	{TN1:tonat* N MS1 T M1} 
		{TN2:tonat* N MS2 T M2}
		{E: multiset`eq MS1 MS2}
	exists	{E: nat`eq M1 M2}
	true.

- : tonat-deterministic/L (tonat/var MC1 VL1 P1) (tonat/var MC2 VL2 P2) _ N1=N2
    <- count-deterministic MC1 MC2 multiset`eq/ nat`eq/ C1=C2
    <- varlevel-deterministic VL1 VL2 L1=L2
    <- plus-right-cancels P1 P2 L1=L2 C1=C2 N1=N2.

- : tonat-deterministic/L (tonat/lit MC1 T1 P1) (tonat/lit MC2 T2 P2) _ M1'=M2'
    <- count-deterministic MC1 MC2 multiset`eq/ nat`eq/ C1=C2
    <- times-deterministic T1 T2 nat`eq/ nat`eq/ TM1=TM2
    <- plus-deterministic P1 P2 C1=C2 TM1=TM2 M1'=M2'.

- : tonat-deterministic/L (tonat/app MC1 TN1a TN1b P2N1 T1 P1) 
                          (tonat/app MC2 TN2a TN2b P2N2 T2 P2) MSE M1'=M2'
    <- count-deterministic MC1 MC2 multiset`eq/ nat`eq/ C1=C2
    <- tonat-deterministic/L TN1a TN2a MSE M1a=M2a
    <- tonat-deterministic/L TN1b TN2b MSE M1b=M2b
    <- natpair`pair-preserves-eq M1a=M2a M1b=M2b P1=P2
    <- pair2nat-deterministic P2N1 P2N2 P1=P2 M1=M2
    <- times-deterministic T1 T2 nat`eq/ M1=M2 TM1=TM2
    <- succ-deterministic TM1=TM2 TM1+1=TM2+1
    <- plus-deterministic P1 P2 C1=C2 TM1+1=TM2+1 M1'=M2'.

%theorem tonat-deterministic/L2 :
	forall* {N1} {N2} {M1} {M2} {MS} {F:term N1 -> term N2} {M}
	forall	{F1:{f:term N1} {fl:varlevel f (s M1)} 
                    tonat* N2 MS (F f) M}
		{ME: nat`eq M1 M2}
	exists	{F2:{f:term N1} {fl:varlevel f (s M2)}
		    tonat* N2 MS (F f) M}
	true.

- : tonat-deterministic/L2 F nat`eq/ F.

%worlds (blockvar) (tonat-deterministic/L2 _ _ _).
%total { } (tonat-deterministic/L2 _ _ _).

- : tonat-deterministic/L (tonat/lam MC1 MCz1 MA1 ([v] [vl] (TN1 v vl)) T1 P1)
                          (tonat/lam MC2 MCz2 MA2 ([v] [vl] (TN2 v vl)) T2 P2)
                          MS1=MS2 M1'=M2'
    <- multiset`count-deterministic MC1 MC2 MS1=MS2 nat`eq/ VN1=VN2
    <- multiset`count-deterministic MCz1 MCz2 MS1=MS2 nat`eq/ ZN1=ZN2
    <- multiset`add-deterministic MA1 MA2 MS1=MS2 nat`eq/ MS1'=MS2'
    <- tonat-deterministic/L2 TN1 ZN1=ZN2 TN1'
    <- ({v} {vl:varlevel v (s ZN2)} tonat-deterministic/L (TN1' v vl) (TN2 v vl)
                                                          MS1'=MS2' M1=M2)
    <- times-deterministic T1 T2 nat`eq/ M1=M2 TM1=TM2
    <- plus-deterministic P1 P2 VN1=VN2 TM1=TM2 M1'=M2'.

- : tonat-deterministic/L (tonat/rec MC1 MA1 ([f] [fl] (TN1 f fl)) T1 P1)
                          (tonat/rec MC2 MA2 ([f] [fl] (TN2 f fl)) T2 P2) 
                          MS1=MS2 M1'=M2'
    <- multiset`count-deterministic MC1 MC2 MS1=MS2 nat`eq/ FN1=FN2
    <- multiset`add-deterministic MA1 MA2 MS1=MS2 nat`eq/ MS1'=MS2'
    <- tonat-deterministic/L2 TN1 FN1=FN2 TN1'
    <- ({f} {fl:varlevel f (s N)} tonat-deterministic/L (TN1' f fl) (TN2 f fl)
                                                        MS1'=MS2' M1=M2)
    <- times-deterministic T1 T2 nat`eq/ M1=M2 TM1=TM2
    <- succ-deterministic TM1=TM2 TM1'=TM2'
    <- succ-deterministic TM1'=TM2' TM1''=TM2''
    <- plus-deterministic P1 P2 FN1=FN2 TM1''=TM2'' M1'=M2'.

%worlds (blockvar) (tonat-deterministic/L _ _ _ _).
%total (T) (tonat-deterministic/L _ T _ _).

- : tonat-deterministic TN1 TN2 eq/ N1=N2
    <- tonat-deterministic/L TN1 TN2 multiset`eq/ N1=N2.

%worlds () (tonat-deterministic _ _ _ _).
%total { } (tonat-deterministic _ _ _ _).

Proving that the mapping is onto.

Again, this aspect has the same structure as with non-indexed terms.

Auxiliary definitions

We define a relation that builds on the context relation. In the non-indexed case, it took a nat, here it takes the multiset representing the levels of variables in the context.

upto : multiset -> type.


upto/0 : upto multiset/0.

upto/+ : 
	upto MS -> 
	multiset`count MS N FN ->
	varlevel (V:term N) (s FN) -> 
	multiset`add MS N MS' ->
    upto MS'.

Lemmas about regular definitions

%theorem term-inhabited :
	forall {N}
	exists {T:term N}
	true.

- : term-inhabited _ (lit z).

- : term-inhabited _ (lam ([x] T))
    <- term-inhabited _ T.

%worlds (blockvar) (term-inhabited _ _).
%total (N) (term-inhabited N _).

Theorems about auxiliary definitions

The obvious lemma that makes use of the main purpose of the relation: that a variable is always available.

%theorem upto-implies-varlevel :
	forall* {MS} {N} {L} {FN}
	forall	{U:upto MS}
		{MC:multiset`count MS N FN}
		{LT:nat`gt FN L}
	exists	{V:term N} {VL:varlevel V (s L)}
	true.

- : upto-implies-varlevel upto/0 MC FN>L T FL
    <- count-empty-is-zero MC FN=0
    <- nat`gt-respects-eq FN>L FN=0 nat`eq/ ZERO>L 
    <- term-inhabited _ T
    <- nat`gt-contradiction ZERO>L F
    <- false-implies-varlevel F FL.

%theorem upto-implies-varlevel/L :
	forall* {MS1} {N1} {L} {FN1} {MS2} {N2} {FN2} {V1:term N1} {B}
	forall	{U: upto MS1}
		{MC1: multiset`count MS1 N1 FN1}
		{FL1: varlevel V1 (s FN1)}
		{MA: multiset`add MS1 N1 MS2}
		{MC2: multiset`count MS2 N2 FN2}
		{LT:nat`gt FN2 L}
		{EQ?: nat`eq? N1 N2 B}
	exists	{V:term N2} {VL:varlevel V (s L)}
	true.

- : upto-implies-varlevel/L _ MC1 FL1 MA MC2 (gt/1) nat`eq?/yes _ FL2
    <- count-add-implies-count MC1 MA MC2'
    <- count-deterministic MC2' MC2 multiset`eq/ nat`eq/ FN1+1=FN2+1
    <- varlevel-respects-eq FL1 FN1+1=FN2+1 FL2.

- : upto-implies-varlevel/L U MC1 FL1 MA MC2 (gt/> FN2>L) nat`eq?/yes _ FL2
    <- count-add-implies-count MC1 MA MC2'
    <- count-deterministic MC2 MC2' multiset`eq/ nat`eq/ FN2+1=FN1+1
    <- succ-cancels FN2+1=FN1+1 FN2=FN1
    <- gt-respects-eq FN2>L FN2=FN1 nat`eq/ FN1>L
    <- upto-implies-varlevel U MC1 FN1>L _ FL2.
 
- : upto-implies-varlevel/L U _ _ MA MC2 GT (nat`eq?/no N1<>N2) _ FL
    <- nat`ne-symmetric N1<>N2 N2<>N1
    <- add-preserves-count-converse MC2 MA N2<>N1 MC1
    <- upto-implies-varlevel U MC1 GT _ FL.

- : upto-implies-varlevel (upto/+ U MC1 FL1 MA) MC2 GT _ FL
    <- nat`eq?-total EQ?
    <- upto-implies-varlevel/L U MC1 FL1 MA MC2 GT EQ? _ FL.

%worlds (blockvar) (upto-implies-varlevel/L _ _ _ _ _ _ _ _ _)
                   (upto-implies-varlevel _ _ _ _ _).

%total (U V) (upto-implies-varlevel U _ _ _ _)
             (upto-implies-varlevel/L V _ _ _ _ _ _ _ _).

Main theorem

We prove the main result using two lemmas that do the case analysis on the number against the nesting level and the parity. (In general, one would use a divisor counting all cases that are recursive.) The proofs are long but simply arithmetic manipulation. Proving termination uses meta-gt for strong induction over the natural numbers.

%theorem tonat-onto* :
	forall* {N}
	forall	{M:nat}
	exists	{T:term N} {TN:tonat T M}
	true.

%abbrev tonat-onto = tonat-onto* _ _.


%theorem tonat-onto/L :
	forall* {N} {MS:multiset}
	forall	{U:upto MS}
		{M:nat}
	exists	{T:term N} {TN:tonat* _ MS T M}
	true.

%theorem tonat-onto/L0 :
	forall* {N} {MS:multiset} {VN} {C}
	forall	{U:upto MS}
		{M:nat}
		{MC:count MS N VN}
		{CMP:nat`compare VN M C}
	exists	{T} {TN:tonat* N MS T M}
	true.

- : tonat-onto/L U M _ TN
    <- multiset`count-total MC
    <- nat`compare-total CMP
    <- tonat-onto/L0 U M MC CMP _ TN.

- : tonat-onto/L0 U M MC (compare/> VN>M) _ (tonat/var MC VL M+L+1=VN)
    <- nat`gt-implies-plus VN>M L L+1+M=VN
    <- plus-commutative L+1+M=VN M+L+1=VN
    <- plus-implies-ge M+L+1=VN VN>=L+1
    <- ge-succ-implies-gt VN>=L+1 VN>L
    <- upto-implies-varlevel U MC VN>L _ VL.

%theorem tonat-onto/L1 :
	forall*	{TM} {MS} {N} {VN}
	forall	{UF:upto MS}
		{M:nat}
		{MC:count MS N VN}
		{P:plus VN TM M}
		{Q} {R} {DR:divrem TM (s (s z)) Q R}
	exists	{T} {TN:tonat* N MS T M}
	true.

- : tonat-onto/L0 U M MC (compare/=) _ TN
    <- plus-right-identity _ P
    <- divrem-total M/2=Q,R
    <- tonat-onto/L1 U M MC P Q R M/2=Q,R _ TN.

- : tonat-onto/L0 U M MC (compare/< M>VN) _ TN
    <- gt-implies-plus M>VN _ Pc
    <- plus-commutative Pc P
    <- divrem-total M/2=Q,R
    <- tonat-onto/L1 U M MC P Q R M/2=Q,R _ TN.

- : tonat-onto/L1 _ _ _ _ _ (s (s _)) DR T TN
    <- divrem-contradiction DR (plus/s (plus/s plus/z)) F
    <- term-inhabited _ T
    <- false-implies-tonat F TN.

- : tonat-onto/L1 U M' MC VN+TM'=M' M (s z) TM'/2=M,1 
		  _ (tonat/app MC TN1 TN2 P2N TWO*M=TM VN+TM+1=M')
    <- plus-implies-ge VN+TM'=M' M'>=TM'
    <- divrem-can-be-inverted TM'/2=M,1 TM M*2=TM TM+ONE=TM'
    <- times-commutative M*2=TM TWO*M=TM
    <- plus-commutative (plus/s plus/z) TM+ONE=TM+1
    <- plus-deterministic TM+ONE=TM' TM+ONE=TM+1 nat`eq/ nat`eq/ TM'=TM+1
    <- plus-respects-eq VN+TM'=M' nat`eq/ TM'=TM+1 nat`eq/ VN+TM+1=M'
    <- nat2pair-total P2N
    <- quotient-of-nonzero-is-smaller TM'/2=M,1 TM'=TM+1 TM'>M
    <- nat`ge-transitive-gt M'>=TM' TM'>M M'>M
    <- nat2pair-implies-ge P2N M>=M1 M>=M2
    <- nat`gt-transitive-ge M'>M M>=M1 M'>M1
    <- nat`gt-transitive-ge M'>M M>=M2 M'>M2
    <- meta-gt _ _ M'>M1
    <- meta-gt _ _ M'>M2
    <- tonat-onto/L U M1 _ TN1
    <- tonat-onto/L U M2 _ TN2.

- : tonat-onto/L1 _ M' MC VN+TM=M' M z TM/2=M _ (tonat/lit MC TWO*M=TM VN+TM=M')
    <- div-can-be-inverted TM/2=M M*2=TM
    <- times-commutative M*2=TM TWO*M=TM.

%theorem tonat-onto/L2 :
	forall*	{TM} {MS} {N} {VN} {Q2}
	forall	{U:upto MS}
		{M:nat}
		{MC:count MS (s N) VN}
		{P:plus VN TM M}
		         {DR:divrem TM (s (s z)) Q2 z}
		{Q4} {R} {DR:divrem Q2 (s (s z)) Q4 R}
	exists	{T} {TN:tonat* (s N) MS T M}
	true.

- : tonat-onto/L1 U M' MC VN+FM=M' TM z FM/2=TM _ TN
    <- divrem-total TM/2=Q,R
    <- tonat-onto/L2 U M' MC VN+FM=M' FM/2=TM Q R TM/2=Q,R _ TN.

%abbrev 2*2=4 = (times/s (times/s times/z plus/z) (plus/s (plus/s plus/z))).

- : tonat-onto/L2 _ _ _ _ _ _ (s (s _)) DR T TN
    <- divrem-contradiction DR (plus/s (plus/s plus/z)) F
    <- term-inhabited _ T
    <- false-implies-tonat F TN.

- : tonat-onto/L2 U M' MC VN+FM'=M' FM'/2=TM' M (s z) TM'/2=M,1
		  _ (tonat/rec MC MA ([f] [fl] (TN f fl)) FOUR*M=FM VN+FM+2=M')
    <- divrem-can-be-inverted TM'/2=M,1 TM M*2=TM TM+ONE=TM'
    <- div-can-be-inverted FM'/2=TM' TM'*2=FM'
    <- times-total* TM (s (s z)) FM TM*2=FM 
    <- times-right-distributes-over-plus* 
	TM+ONE=TM' TM'*2=FM' TM*2=FM (times/s times/z plus/z) FM+TWO=FM'
    <- times-associative* M*2=TM TM*2=FM 2*2=4 M*4=FM
    <- times-commutative M*4=FM FOUR*M=FM
    <- plus-commutative (plus/s (plus/s plus/z)) FM+TWO=FM+2
    <- plus-deterministic FM+TWO=FM' FM+TWO=FM+2 nat`eq/ nat`eq/ FM'=FM+2
    <- plus-respects-eq VN+FM'=M' nat`eq/ FM'=FM+2 nat`eq/ VN+FM+2=M'
    <- plus-swap-succ-converse VN+FM+2=M' VN+1+FM+1=M'
    <- plus-swap-succ-converse VN+1+FM+1=M' VN+2+FM=M'
    <- multiset`add-total MA
    <- plus-implies-gt VN+2+FM=M' nat`eq/ M'>FM
    <- times-nonzero-implies-ge M*4=FM FM>=M
    <- nat`gt-transitive-ge M'>FM FM>=M M'>M
    <- meta-gt _ _ M'>M
    <- ({f} {fl} tonat-onto/L (upto/+ U MC fl MA) M _ (TN f fl)).

% 0 needs a special case for termination:

%theorem tonat-onto/0 :
	forall*	{MS}
	forall	{N} {U:upto MS} {VN}
		{MC:count MS N VN}
	exists	{T} {TN:tonat* N MS T z}
	true.

%abbrev 2*0=0 = (times/s (times/s times/z plus/z) plus/z).
%abbrev 4*0=0 = (times/s (times/s 2*0=0   plus/z) plus/z).

- : tonat-onto/0 _ U z MC _ (tonat/lit MC 2*0=0 plus/z).

- : tonat-onto/0 _ U z MC _ (tonat/lam MC MCz MA TN 4*0=0 plus/z)
    <- multiset`count-total MCz
    <- multiset`add-total MA
    <- multiset`count-total MC'
    <- ({v} {vl} (tonat-onto/0 _ (upto/+ U MCz vl MA) _ MC' _ (TN v vl))).

- : tonat-onto/0 N U (s VN-1) MC _ (tonat/var MC VL plus/z)
    <- upto-implies-varlevel U MC gt/1 _ VL.

%worlds (blockvar) (tonat-onto/0 _ _ _ _ _ _).
%total (N) (tonat-onto/0 N _ _ _ _ _).

- : tonat-onto/L2 U z MC _ _ _ _ _ _ TN
    <- tonat-onto/0 _ U _ MC _ TN.

%theorem tonat-onto/L2/L :
	forall* {M} {X} {Y} {Z} {XM}
	forall	{T:times M (s (s X)) XM}
		{P:plus Y XM (s Z)}
	exists	{G:gt (s Z) M}
	true.

- : tonat-onto/L2/L M*2=XM plus/z XM>M
    <- div-can-be-constructed M*2=XM XM/2=M
    <- quotient-of-nonzero-is-smaller XM/2=M nat`eq/ XM>M.

- : tonat-onto/L2/L M*2=XM Y+XM=X' X'>M
    <- plus-implies-gt Y+XM=X' nat`eq/ X'>MX
    <- times-nonzero-implies-ge M*2=XM XM>=M
    <- nat`gt-transitive-ge X'>MX XM>=M X'>M.

%worlds () (tonat-onto/L2/L _ _ _).
%total { } (tonat-onto/L2/L _ _ _).

- : tonat-onto/L2 U (s X) MC VN+FM=M' FM/2=TM M z TM/2=M
		  _ (tonat/lam MC MCz MA TN FOUR*M=FM VN+FM=M')
    <- div-can-be-inverted TM/2=M M*2=TM
    <- div-can-be-inverted FM/2=TM TM*2=FM
    <- times-associative* M*2=TM TM*2=FM 2*2=4 M*4=FM
    <- times-commutative M*4=FM FOUR*M=FM
    <- multiset`count-total MCz
    <- multiset`add-total MA
    <- tonat-onto/L2/L M*4=FM VN+FM=M' M'>M
    <- meta-gt (s X) M M'>M
    <- ({v} {vl} tonat-onto/L (upto/+ U MCz vl MA) _ _ (TN v vl)).

%worlds (blockvar)  (tonat-onto/L2 _ _ _ _ _ _ _ _ _ _)
                    (tonat-onto/L1 _ _ _ _ _ _ _ _ _)
		    (tonat-onto/L0 _ _ _ _ _ _)
		    (tonat-onto/L  _ _ _ _).
%total (M2 M1 M0 M) (tonat-onto/L2 _ M2 _ _ _ _ _ _ _ _)
                    (tonat-onto/L1 _ M1 _ _ _ _ _ _ _)
		    (tonat-onto/L0 _ M0 _ _ _ _)
		    (tonat-onto/L  _ M  _ _).

Proof that mapping is "one to one"

As with the simple HOAS syntax, this is the hardest of the four theorems to prove. As before, the basic structure is the same: we first show that the terms that result in the same number must be identical except that two variables may be equal just by having the same level.

As before we then 'chip' away at variables with low levels and shift the others down. We need to work at low levels because contexts cannot be parameterized by an 'N' and must be absolute. The additional problem with indexed terms is that the first variable we encounter may be of a higher-index than zero. In any case, there can be level 1 variables inside that have a different index than the one we are removing. So the context cannot simply assert that all variables will have level 2 or higher, as with did in the non-indexed case.

The basic idea is that we handle one index level at a time. But again because Twelf contexts cannot have be parameterized, we need to shift index levels down too. Of course, we cannot actually change index values. Instead, we keep a index-adjustment. Then a variable of index type (term N) has two parts to its level M L, where M+A=N and L is the original level. The multiset that keeps track of the next level is similarly shifted. We then do a shift such as we had for non-indexed terms while removing all variables of adjusted index zero (M = z). Then when these are all removed, we can adjust the indices one more step until there are no more variables of any index needing levels.

Auxiliary definitions

In this section, we use the full generality of varadjlevel because we need to recurse in two different directions: the original var level and the term level.

%block blockvaradj : some {m} {n} {l}
		      block {v:term n} {vl:varadjlevel v m (s l)}.

Equality (permitting variables with the same level).

Some variables are are bound with levels, others are not given levels. We do this in order to gradually squeeze out those that need levels. The lam1 and rec1 cases use variables that don't need levels, whereas the lam2, rec2 cases handle variables that still need level. We also take a natural number A that indicates the minimum term level that will be used. Notice that lam2 is only legal while A is still zero.

eql* : {N} {A:nat} multiset -> term N -> term N -> type.

%abbrev eql = eql* _.


eql/eq : eq T1 T2 -> eql A MS T1 T2.

eql/app : eql A MS F1 F2 -> eql A MS A1 A2 -> eql A MS (app F1 A1) (app F2 A2).

eql/lam1 : ({v} (eql A MS (F1 v) (F2 v))) -> eql A MS (lam F1) (lam F2).

eql/lam2 :
	count MS z VN -> 
	add MS z MS' -> 
	({v} {vl: varadjlevel v z (s VN)} eql z MS' (F1 v) (F2 v)) ->
    eql z MS (lam F1) (lam F2).

eql/rec1 : ({v} (eql A MS (F1 v) (F2 v))) -> eql A MS (rec F1) (rec F2).

eql/rec2 :
	plus A M (s N) ->
	count MS M VN ->
	add MS M MS' ->
	({v} {vl:varadjlevel v M (s VN)} eql A MS' (F1 v) (F2 v)) ->
    eql A MS (rec F1) (rec F2).

eql/var :
	plus A M N ->
	varadjlevel V1 M L -> 
	varadjlevel V2 M L -> 
    eql* N A MS V1 V2.

Measure of eql sizes.

We use this measure to be able to prove termination. We need eqlsize/var = eqlsize/eq, eqlsize/lam1 = eqlsize/lam2. (Less than is ok in each case but would require that we rephrase the lemmas.) We have three measures: N B M.

- N is the height of the term

- B is the minimum of any M for a varlevel (or (s z))

- M is greater than the M for any varlevel used.

The first measure is used to ensure that regular recursion through the tree terminates. We don't use normal structure recursion because everytime we change variable levels, the tree changes.

The second measure is not used for termination, but when non-zero means there are no variables with that need adjusted index zero. Once this is the case, we can adjust all levels down one notch.

The third measure is used to ensure that chipping away at indices eventually terminates: M is the maximum adjusted index used. Once M drops to zero, it means no variables need levels for equality and we can convert to an 'eq' proof easily.

eqlsize : (eql* A N MS T1 T2) -> nat -> nat -> nat -> type.


eqlsize/eq : eqlsize (eql/eq _) z (s z) z.

eqlsize/app : 
	eqlsize E1 N1 B1 M1 ->
	eqlsize E2 N2 B2 M2 ->
	nat`max N1 N2 N ->
	nat`min B1 B2 B ->
	nat`max M1 M2 M ->
    eqlsize (eql/app E1 E2) (s N) B M.
	
eqlsize/lam1 : ({v} eqlsize (E v) N B M) -> eqlsize (eql/lam1 E) (s N) B M.

eqlsize/lam2 : 
	({v} {vl} eqlsize (E v vl) N B M) -> 
	nat`max (s z) M M' ->
    eqlsize (eql/lam2 _ _ E) (s N) z M'.

eqlsize/rec1 : ({v} eqlsize (E v) N B M) -> eqlsize (eql/rec1 E) (s N) B M.

eqlsize/rec2 : 
	({v} {vl:varadjlevel v M _} eqlsize (E v vl) N B1 M1) -> 
	nat`min M B1 B2 ->
	nat`max (s M) M1 M2 ->
    eqlsize (eql/rec2 _ _ _ E) (s N) B2 M2.

eqlsize/var : eqlsize (eql/var _ _ _) z (s z) z.

Copied definitions

As with the non-indexed case, we need to use an alternate form for levels as we shift them down or adjust them down. (Remember there are two dimensions to a level!)

varadjlevel' : term N -> nat -> nat -> type.


eql*' : {N} {A:nat} multiset -> term N -> term N -> type.

%abbrev eql' = eql*' _.


eql'/eq : eq T1 T2 -> eql' A MS T1 T2.

eql'/app : 
	eql' A MS F1 F2 -> 
	eql' A MS A1 A2 -> 
    eql' A MS (app F1 A1) (app F2 A2).

eql'/lam1 : ({v} (eql' A MS (F1 v) (F2 v))) -> eql' A MS (lam F1) (lam F2).

eql'/lam2 :
	count MS z VN -> 
	add MS z MS' -> 
	({v} {vl: varadjlevel' v z (s VN)} eql' z MS' (F1 v) (F2 v)) ->
    eql' z MS (lam F1) (lam F2).

eql'/rec1 : ({v} (eql' A MS (F1 v) (F2 v))) -> eql' A MS (rec F1) (rec F2).

eql'/rec2 :
	plus A M (s N) ->
	count MS M VN ->
	add MS M MS' ->
	({v} {vl:varadjlevel' v M (s VN)} eql' A MS' (F1 v) (F2 v)) ->
    eql' A MS (rec F1) (rec F2).

eql'/var :
	plus A M N ->
	varadjlevel' V1 M L -> 
	varadjlevel' V2 M L -> 
    eql*' N A MS V1 V2.



eqlsize' : (eql*' A N MS T1 T2) -> nat -> nat -> nat -> type.


eqlsize'/eq : eqlsize' (eql'/eq _) z (s z) z.

eqlsize'/app : 
	eqlsize' E1 N1 B1 M1 ->
	eqlsize' E2 N2 B2 M2 ->
	nat`max N1 N2 N ->
	nat`min B1 B2 B ->
	nat`max M1 M2 M ->
    eqlsize' (eql'/app E1 E2) (s N) B M.
	
eqlsize'/lam1 : ({v} eqlsize' (E v) N B M) -> eqlsize' (eql'/lam1 E) (s N) B M.

eqlsize'/lam2 : 
	({v} {vl} eqlsize' (E v vl) N B M1) -> 
	nat`max (s z) M1 M2 ->
    eqlsize' (eql'/lam2 _ _ E) (s N) z M2.

eqlsize'/rec1 : ({v} eqlsize' (E v) N B M) -> eqlsize' (eql'/rec1 E) (s N) B M.

eqlsize'/rec2 : 
	({v} {vl:varadjlevel' v M _} eqlsize' (E v vl) N B1 M1) -> 
	nat`min M B1 B2 ->
	nat`max (s M) M1 M2 ->
    eqlsize' (eql'/rec2 _ _ _ E) (s N) B2 M2.

eqlsize'/var : eqlsize' (eql'/var _ _ _) z (s z) z.

Theorems about auxiliary definitions

Some of the lemmas that would normally belong here are proved later when we have more blocks available.

%theorem false-implies-eql :
	forall* {MS} {N} {A} {T1} {T2} 
	forall	{F:void}
	exists	{E:eql* N A MS T1 T2}
	true.

%worlds (blocksimple | blockvaradj) (false-implies-eql _ _).
%total { }  (false-implies-eql _ _).


%theorem false-implies-eqlsize :
	forall* {N} {A} {MS} {T1} {T2} {S} {B} {M}
		{E:eql* N A MS T1 T2}
	forall	{F:void}
	exists	{ES1:eqlsize E S B M}
	true.

%worlds (blocksimple | blockvaradj) (false-implies-eqlsize _ _).
%total { } (false-implies-eqlsize _ _).


%theorem eqlsize-total* :
	forall*	{N} {A} {MS} {T1} {T2}
	forall  {E:eql* N A MS T1 T2}
	exists  {S} {M} {B} {ES:eqlsize E S B M}
	true.

%abbrev eqlsize-total = eqlsize-total* _ _ _ _.

- : eqlsize-total eqlsize/eq.

- : eqlsize-total (eqlsize/app S1 S2 M B M2)
    <- eqlsize-total S1
    <- eqlsize-total S2
    <- nat`max-total M
    <- nat`min-total B
    <- nat`max-total M2.

- : eqlsize-total (eqlsize/lam1 F)
    <- ({v} eqlsize-total (F v)).

- : eqlsize-total (eqlsize/lam2 F M)
    <- ({v} {vl} (eqlsize-total (F v vl)))
    <- nat`max-total M.

- : eqlsize-total (eqlsize/rec1 F)
    <- ({v} eqlsize-total (F v)).

- : eqlsize-total (eqlsize/rec2 F MN M)
    <- ({v} {vl} (eqlsize-total (F v vl)))
    <- nat`min-total MN
    <- nat`max-total M.

- : eqlsize-total eqlsize/var.

%worlds (blocksimple | blockvaradj) (eqlsize-total* _ _ _ _ _).
%total (E)  (eqlsize-total* E _ _ _ _).

Shifting varlevels down

Now as with the non-indexed case, we shift variable levels down. As before, we need to use the alternate definitions.

The astute reader will notice that we don't have a block that just handles nonzero (adjusted) index variables being shifted over. Instead we handle a double context "noshift" that handles both directions. That's because when these lemmas are used to shift levels down, the outer context may have non-zero (adjusted) index that will need to handle being shifted in both directions.

%theorem varlevel-zero-shifts-down :
	forall* {N} {V:term N} {L}
	forall	{VL:varadjlevel V z (s (s L))}
	exists	{VL':varadjlevel' V z (s L)}
	true.

%theorem varlevel-nonzero-shifts-over :
	forall* {N} {V:term N} {M} {L}
	forall	{VL:varadjlevel V (s M) (s L)}
	exists	{VL':varadjlevel' V (s M) (s L)}
	true.

%theorem varlevel-shifts-back :
	forall* {N} {V:term N} {M} {L}
	forall	{VL':varadjlevel' V M (s L)}
	exists	{VL:varadjlevel V M (s L)}
	true.


%block shiftdown : some {l} {n} 
		    block {v:term n} 
		    {vl:varadjlevel v z (s (s l))} 
		    {vl':varadjlevel' v z (s l)}
		    {vsd:varlevel-zero-shifts-down vl vl'}.

%block noshift : some {l} {m} {n}
		  block {v:term n}
		  {vl:varadjlevel v (s m) (s l)}
		  {vl':varadjlevel' v (s m) (s l)}
		  {vsd:varlevel-nonzero-shifts-over vl vl'}
		  {vsd:varlevel-shifts-back vl' vl}.

%block shiftback : some {n} {m} {l} 
		    block {v:term n} 
		    {vl':varadjlevel' v m (s l)} 
		    {vl:varadjlevel v m (s l)}
		    {vsb:varlevel-shifts-back vl' vl}.

fake : type.
- : fake <- ({x:varlevel-zero-shifts-down X Y} varlevel-zero-shifts-down X' Y').
- : fake <- ({x:varlevel-nonzero-shifts-over X Y}
	       varlevel-nonzero-shifts-over X' Y').
- : fake <- ({x:varlevel-shifts-back X Y} varlevel-shifts-back X' Y').

%worlds (blocksimple | shiftdown | noshift) 
	(varlevel-zero-shifts-down _ _).
%worlds (blocksimple | shiftdown | noshift) 
	(varlevel-nonzero-shifts-over _ _).
%worlds (blocksimple | shiftback | noshift) 
        (varlevel-shifts-back _ _).

%total { } (varlevel-zero-shifts-down _ _).
%total { } (varlevel-nonzero-shifts-over _ _).
%total { } (varlevel-shifts-back _ _).



%theorem shift-varlevel/L1 :
	forall* {N} {A} {M0} {M1} {T1} {T2} {S} {MN} {MM}
	forall	{E: eql* N A M1 T1 T2}
		{ES:eqlsize E S MN MM}
		{MA:multiset`add M0 z M1}
	exists	{E': eql*' N A M0 T1 T2}
		{ES':eqlsize' E' S MN MM}
	true.

- : shift-varlevel/L1 (eql/eq eq/) eqlsize/eq _ (eql'/eq eq/) eqlsize'/eq.

- : shift-varlevel/L1 (eql/app E1 E2) (eqlsize/app ES1 ES2 MX MN MX2) MA
		      (eql'/app E1' E2') (eqlsize'/app ES1' ES2' MX MN MX2)
    <- shift-varlevel/L1 E1 ES1 MA E1' ES1'
    <- shift-varlevel/L1 E2 ES2 MA E2' ES2'.

- : shift-varlevel/L1 (eql/lam1 ([v] (F v))) (eqlsize/lam1 FS) MA
                      (eql'/lam1 ([v] (F' v))) (eqlsize'/lam1 FS')
    <- {v} shift-varlevel/L1 (F v) (FS v) MA (F' v) (FS' v).

%theorem shift-varlevel/L1/rec :
	forall* {N0} {N} {N'} {N1} {F1} {F2} {A} {S} {M1} {M2} {MN} {MM}
	forall	{F: {v:term N0} {vl:varadjlevel v z (s N)}
		     (eql* N1 A M2 (F1 v) (F2 v))}
		{FS: {v:term N0} {vl:varadjlevel v z (s N)}
		      (eqlsize (F v vl) S MN MM)}
		{MA1: multiset`add M1 z M2}
		{EQ: nat`eq N (s N')}
	exists	{F': {v:term N0} {vl':varadjlevel' v z (s N')}
		      (eql*' N1 A M1 (F1 v) (F2 v))}
		{FS': {v:term N0} {vl':varadjlevel' v z (s N')}
		       (eqlsize' (F' v vl') S MN MM)}
	true.

- : shift-varlevel/L1/rec F FS MA1 nat`eq/ F' FS'
    <- {v} {vl} {vl':varadjlevel' v z (s N)} 
       {vsd:varlevel-zero-shifts-down vl vl'}
       shift-varlevel/L1 (F v vl) (FS v vl) MA1 (F' v vl') (FS' v vl').

- : shift-varlevel/L1 
	(eql/lam2 MC1 MA1 ([v] [vl:varadjlevel v z (s N)] (F v vl)))
	(eqlsize/lam2 FS MM) MA0
        (eql'/lam2 MC0 MA0 ([v] [vl:varadjlevel' v z (s N')] (F' v vl)))
	(eqlsize'/lam2 FS' MM)
    <- multiset`count-total MC0
    <- count-add-implies-count MC0 MA0 MC1'
    <- count-deterministic MC1 MC1' multiset`eq/ nat`eq/ EQ
    <- shift-varlevel/L1/rec F FS MA1 EQ F' FS'.

- : shift-varlevel/L1 (eql/rec1 ([v] (F v))) (eqlsize/rec1 FS) MA
                      (eql'/rec1 ([v] (F' v))) (eqlsize'/rec1 FS')
    <- {v} shift-varlevel/L1 (F v) (FS v) MA (F' v) (FS' v).

- : shift-varlevel/L1 
	(eql/rec2 P MC1 MA1 ([v] [vl:varadjlevel v z (s N)] (F v vl)))
	(eqlsize/rec2 FS MN MM) MA0
        (eql'/rec2 P MC0 MA0 ([v] [vl:varadjlevel' v z (s N')] (F' v vl)))
	(eqlsize'/rec2 FS' MN MM)
    <- multiset`count-total MC0
    <- count-add-implies-count MC0 MA0 MC1'
    <- count-deterministic MC1 MC1' multiset`eq/ nat`eq/ EQ
    <- shift-varlevel/L1/rec F FS MA1 EQ F' FS'.

- : shift-varlevel/L1 
	(eql/rec2 P MC1 MA1 ([v] [vl:varadjlevel v (s M) (s N)] (F v vl)))
	(eqlsize/rec2 FS MN MM) MA
        (eql'/rec2 P MC1' MA1' ([v] [vl:varadjlevel' v (s M) (s N)] (F' v vl)))
	(eqlsize'/rec2 FS' MN MM)
    <- add-commutes MA MA1 _ MA1' MA'
    <- succ-implies-gt-zero _ GT
    <- add-preserves-count-converse MC1 MA (nat`ne/> GT) MC1'
    <- {v} {vl} {vl':varadjlevel' v (s M) (s N)} 
       {vsd:varlevel-nonzero-shifts-over vl vl'}
       {vsb:varlevel-shifts-back vl' vl}
       shift-varlevel/L1 (F v vl) (FS v vl) MA' (F' v vl') (FS' v vl').

- : shift-varlevel/L1 
	(eql/var P VL1 VL2) eqlsize/var MA
	(eql'/var P VL1' VL2') eqlsize'/var
    <- varlevel-zero-shifts-down VL1 VL1'
    <- varlevel-zero-shifts-down VL2 VL2'.

- : shift-varlevel/L1
	(eql/var P VL1 VL2) eqlsize/var MA
	(eql'/var P VL1' VL2') eqlsize'/var
    <- varlevel-nonzero-shifts-over VL1 VL1'
    <- varlevel-nonzero-shifts-over VL2 VL2'.

%worlds (blocksimple | shiftdown | noshift) 
	(shift-varlevel/L1 _ _ _ _ _)
	(shift-varlevel/L1/rec _ _ _ _ _ _).
%total (E El) (shift-varlevel/L1 E _ _ _ _)
              (shift-varlevel/L1/rec El _ _ _ _ _).
 

%theorem shift-varlevel/L2 :
	forall* {N} {M} {A} {T1} {T2} {S} {MN} {MM}
	forall	{E': eql*' N M A T1 T2}
		{ES': eqlsize' E' S MN MM}
	exists	{E: eql* N M A T1 T2}
		{ES: eqlsize E S MN MM}
	true.

- : shift-varlevel/L2 (eql'/eq eq/) eqlsize'/eq (eql/eq eq/) eqlsize/eq.

- : shift-varlevel/L2
	(eql'/app E1' E2') (eqlsize'/app ES1' ES2' MAX MIN MAX2)
	(eql/app E1 E2) (eqlsize/app ES1 ES2 MAX MIN MAX2)
    <- shift-varlevel/L2 E1' ES1' E1 ES1
    <- shift-varlevel/L2 E2' ES2' E2 ES2.

- : shift-varlevel/L2 (eql'/lam1 ([v] (F v))) (eqlsize'/lam1 FS)
                      (eql/lam1 ([v] (F' v))) (eqlsize/lam1 FS')
    <- {v} shift-varlevel/L2 (F v) (FS v) (F' v) (FS' v).

- : shift-varlevel/L2 (eql'/lam2 MC MA ([v] [vl'] (F v vl')))
		      (eqlsize'/lam2 FS MM)
                      (eql/lam2 MC MA ([v] [vl] (F' v vl)))
		      (eqlsize/lam2 FS' MM)
    <- {v} {vl'} {vl} {vsb:varlevel-shifts-back vl' vl}
       shift-varlevel/L2 (F v vl') (FS v vl') (F' v vl) (FS' v vl).

- : shift-varlevel/L2 (eql'/rec1 ([v] (F v))) (eqlsize'/rec1 FS)
                      (eql/rec1 ([v] (F' v))) (eqlsize/rec1 FS')
    <- {v} shift-varlevel/L2 (F v) (FS v) (F' v) (FS' v).

- : shift-varlevel/L2 (eql'/rec2 P MC MA ([v] [vl'] (F v vl')))
		      (eqlsize'/rec2 FS MN MM)
                      (eql/rec2 P MC MA ([v] [vl] (F' v vl)))
		      (eqlsize/rec2 FS' MN MM)
    <- {v} {vl'} {vl} {vsb:varlevel-shifts-back vl' vl}
       shift-varlevel/L2 (F v vl') (FS v vl') (F' v vl) (FS' v vl).

- : shift-varlevel/L2 (eql'/var P VL1 VL2) eqlsize'/var 
                      (eql/var P VL1' VL2') eqlsize/var
    <- varlevel-shifts-back VL1 VL1'
    <- varlevel-shifts-back VL2 VL2'.

%worlds (blocksimple | shiftback | noshift) (shift-varlevel/L2 _ _ _ _).
%total (E)  (shift-varlevel/L2 E _ _ _).

Now we put these two parts into one that hides the alternative definitions.

%theorem shift-varlevel :
	forall* {N} {A} {M0} {M1} {T1} {T2} {S} {MN} {MM}
	forall	{E: eql* N A M1 T1 T2}
		{ES:eqlsize E S MN MM}
		{MA:multiset`add M0 z M1}
	exists	{E': eql* N A M0 T1 T2}
		{ES':eqlsize E' S MN MM}
	true.

- : shift-varlevel E1 ES1 MA E3 ES3
    <- shift-varlevel/L1 E1 ES1 MA E2 ES2
    <- shift-varlevel/L2 E2 ES2 E3 ES3.

%worlds (blocksimple | noshift) (shift-varlevel _ _ _ _ _).
%total { } (shift-varlevel _ _ _ _ _).

Now the whole reason for the two stage var-levels: we have a lemma that says we can adjust the M of all variables down if the minimum varlevel used is greater than zero. First we need some helper lemmas and the ubiquitous blocks.

%theorem varlevel-adjusts-down :
	forall* {N} {V:term N} {M} {L}
	forall	{VL:varadjlevel V (s M) (s L)}
	exists	{VL':varadjlevel' V M (s L)}
	true.

%block adjustdown : some {n} {m} {l}
		     block {v:term n} 
		      {vl:varadjlevel v (s m) (s l)}
		      {vl':varadjlevel' v m (s l)}
		      {vsd:varlevel-adjusts-down vl vl'}.

fake : type.
- : fake <- ({x:varlevel-adjusts-down X Y} varlevel-adjusts-down X' Y').

%worlds (blocksimple | adjustdown) (varlevel-adjusts-down _ _).

%total { } (varlevel-adjusts-down _ _).


%theorem false-implies-eql' :
	forall* {MS} {N} {A} {T1} {T2} 
	forall	{F:void}
	exists	{E:eql*' N A MS T1 T2}
	true.

%worlds (blocksimple | adjustdown) (false-implies-eql' _ _).
%total { }  (false-implies-eql' _ _).


%theorem false-implies-eqlsize' :
	forall* {N} {A} {MS} {T1} {T2} {S} {B} {M}
		{E:eql*' N A MS T1 T2}
	forall	{F:void}
	exists	{ES1:eqlsize' E S B M}
	true.

%worlds (blocksimple | adjustdown) (false-implies-eqlsize' _ _).
%total { } (false-implies-eqlsize' _ _).


%theorem eqlsize-respects-eq :
	forall* {N} {A} {MS} {T1} {T2} 
		{S1} {B1} {M1}
		{S2} {B2} {M2}
		{E:eql* N A MS T1 T2}
	forall	{ES1:eqlsize E S1 B1 M1}
		{SE: nat`eq S1 S2}
		{BE: nat`eq B1 B2}
		{ME: nat`eq M1 M2}
	exists	{ES2:eqlsize E S2 B2 M2}
	true.

- : eqlsize-respects-eq ES nat`eq/ nat`eq/ nat`eq/ ES.

%worlds (blocksimple | blockvaradj | adjustdown) 
	(eqlsize-respects-eq _ _ _ _ _).
%total { } (eqlsize-respects-eq _ _ _ _ _).


%theorem adjust-varlevel/L0 :
	forall* {N} {A} {M0} {M1} {T1} {T2} {S} {MN}
	forall	{E: eql* N A M1 T1 T2}
		{ES:eqlsize E S (s MN) z}
	exists	{E': eql*' N (s A) M0 T1 T2} {MN'}
		{ES':eqlsize' E' S MN' z}
	true.

- : adjust-varlevel/L0
	(eql/eq eq/) (eqlsize/eq) (eql'/eq eq/) _ (eqlsize'/eq).

- : adjust-varlevel/L0
	(eql/app E1 E2) (eqlsize/app ES1 ES2 MAX MIN MAX2)
	(eql'/app E1' E2') _ (eqlsize'/app ES1'' ES2'' MAX MIN' nat`max/=)
    <- max-implies-ge MAX2 ZERO>=M1 ZERO>=M2
    <- ge-zero-always M1 M1>=0
    <- ge-zero-always M2 M2>=0
    <- nat`ge-anti-symmetric M1>=0 ZERO>=M1 M1=0
    <- nat`ge-anti-symmetric M2>=0 ZERO>=M2 M2=0
    <- min-implies-ge MIN B1>=B+1 B2>=B+1
    <- ge-succ-implies-gt B1>=B+1 B1>B
    <- ge-succ-implies-gt B2>=B+1 B2>B
    <- gt-implies-positive B1>B B1' B1=B1'+1
    <- gt-implies-positive B2>B B2' B2=B2'+1
    <- eqlsize-respects-eq ES1 nat`eq/ B1=B1'+1 M1=0 ES1'
    <- eqlsize-respects-eq ES2 nat`eq/ B2=B2'+1 M2=0 ES2'
    <- adjust-varlevel/L0 E1 ES1' E1' _ ES1''
    <- adjust-varlevel/L0 E2 ES2' E2' _ ES2''
    <- nat`min-total MIN'.
   
- : adjust-varlevel/L0 (eql/lam1 ([v] (F v))) (eqlsize/lam1 FS)
                      (eql'/lam1 ([v] (F' v))) MN' (eqlsize'/lam1 FS')
    <- {v} adjust-varlevel/L0 (F v) (FS v) (F' v) MN' (FS' v).

- : adjust-varlevel/L0 (eql/rec1 ([v] (F v))) (eqlsize/rec1 FS)
                      (eql'/rec1 ([v] (F' v))) MN' (eqlsize'/rec1 FS')
    <- {v} adjust-varlevel/L0 (F v) (FS v) (F' v) MN' (FS' v).

- : adjust-varlevel/L0
	(eql/var P VL1 VL2) eqlsize/var
	(eql'/var P' VL1' VL2') _ eqlsize'/var
    <- plus-swap-succ-converse P P'
    <- varlevel-adjusts-down VL1 VL1'
    <- varlevel-adjusts-down VL2 VL2'.

%worlds (blocksimple | adjustdown) (adjust-varlevel/L0 _ _ _ _ _).
%total (E) (adjust-varlevel/L0 E _ _ _ _).


%theorem adjust-varlevel/L1 :
	forall* {N} {A} {M0} {M1} {T1} {T2} {S} {MN} {MM}
	forall	{E: eql* N A M1 T1 T2}
		{ES:eqlsize E S (s MN) (s MM)}
		{MS:multiset`shift z M0 M1}
	exists	{E': eql*' N (s A) M0 T1 T2} {MN'}
		{ES':eqlsize' E' S MN' MM}
	true.

% MAX2 = max z z case (contradiction)
- : adjust-varlevel/L1 
	(eql/app E1 E2) (eqlsize/app ES1 ES2 MAX MIN (MAX2:nat`max z z (s MM)))
         _ E' z ES'
    <- nat`max-deterministic nat`max/= MAX2 nat`eq/ nat`eq/ ZERO=MM+1
    <- nat`eq-contradiction ZERO=MM+1 F
    <- false-implies-eql' F E'
    <- false-implies-eqlsize' F ES'.

% MAX2 = max z (s MM2) (s MM)
- : adjust-varlevel/L1 
	(eql/app E1 E2) (eqlsize/app ES1 ES2 MAX MIN MAX2) MS
	(eql'/app E1' E2') _ (eqlsize'/app ES1'' ES2'' MAX MIN' MAX2')
    <- min-implies-ge MIN B1>=B+1 B2>=B+1
    <- ge-succ-implies-gt B1>=B+1 B1>B
    <- ge-succ-implies-gt B2>=B+1 B2>B
    <- gt-implies-positive B1>B B1' B1=B1'+1
    <- gt-implies-positive B2>B B2' B2=B2'+1
    <- eqlsize-respects-eq ES1 nat`eq/ B1=B1'+1 nat`eq/ ES1'
    <- eqlsize-respects-eq ES2 nat`eq/ B2=B2'+1 nat`eq/ ES2'
    <- adjust-varlevel/L0 E1 ES1' E1' _ ES1''
    <- adjust-varlevel/L1 E2 ES2' MS E2' _ ES2''
    <- succ-implies-gt-zero _ MM2+1>0
    <- nat`max-deterministic (max/< MM2+1>0) MAX2 nat`eq/ nat`eq/ MM2+1=MM+1
    <- succ-cancels MM2+1=MM+1 MM2=MM
    <- nat`ge-zero-always _ MM2>=0
    <- nat`le-implies-max MM2>=0 MAX2''
    <- nat`max-respects-eq MAX2'' nat`eq/ nat`eq/ MM2=MM MAX2'
    <- nat`min-total MIN'.

% MAX2 = max (s MM1) z (s MM)
- : adjust-varlevel/L1 
	(eql/app E1 E2) (eqlsize/app ES1 ES2 MAX MIN MAX2) MS
	(eql'/app E1' E2') _ (eqlsize'/app ES1'' ES2'' MAX MIN' MAX2')
    <- min-implies-ge MIN B1>=B+1 B2>=B+1
    <- ge-succ-implies-gt B1>=B+1 B1>B
    <- ge-succ-implies-gt B2>=B+1 B2>B
    <- gt-implies-positive B1>B B1' B1=B1'+1
    <- gt-implies-positive B2>B B2' B2=B2'+1
    <- eqlsize-respects-eq ES1 nat`eq/ B1=B1'+1 nat`eq/ ES1'
    <- eqlsize-respects-eq ES2 nat`eq/ B2=B2'+1 nat`eq/ ES2'
    <- adjust-varlevel/L1 E1 ES1' MS E1' _ ES1''
    <- adjust-varlevel/L0 E2 ES2' E2' _ ES2''
    <- succ-implies-gt-zero _ MM1+1>0
    <- nat`max-deterministic (max/> MM1+1>0) MAX2 nat`eq/ nat`eq/ MM1+1=MM+1
    <- succ-cancels MM1+1=MM+1 MM1=MM
    <- nat`ge-zero-always _ MM1>=0
    <- nat`ge-implies-max MM1>=0 MAX2''
    <- nat`max-respects-eq MAX2'' nat`eq/ nat`eq/ MM1=MM MAX2'
    <- nat`min-total MIN'.

- : adjust-varlevel/L1 
	(eql/app E1 E2) (eqlsize/app ES1 ES2 MAX MIN MAX2) MS
	(eql'/app E1' E2') _ (eqlsize'/app ES1'' ES2'' MAX MIN' MAX2')
    <- min-implies-ge MIN B1>=B+1 B2>=B+1
    <- ge-succ-implies-gt B1>=B+1 B1>B
    <- ge-succ-implies-gt B2>=B+1 B2>B
    <- gt-implies-positive B1>B B1' B1=B1'+1
    <- gt-implies-positive B2>B B2' B2=B2'+1
    <- eqlsize-respects-eq ES1 nat`eq/ B1=B1'+1 nat`eq/ ES1'
    <- eqlsize-respects-eq ES2 nat`eq/ B2=B2'+1 nat`eq/ ES2'
    <- adjust-varlevel/L1 E1 ES1' MS E1' _ ES1''
    <- adjust-varlevel/L1 E2 ES2' MS E2' _ ES2''
    <- succ-preserves-max-converse MAX2 MAX2'
    <- nat`min-total MIN'.

- : adjust-varlevel/L1 (eql/lam1 ([v] (F v))) (eqlsize/lam1 FS) MS
                      (eql'/lam1 ([v] (F' v))) MN' (eqlsize'/lam1 FS')
    <- {v} adjust-varlevel/L1 (F v) (FS v) MS (F' v) MN' (FS' v).

- : adjust-varlevel/L1 (eql/rec1 ([v] (F v))) (eqlsize/rec1 FS) MS
                      (eql'/rec1 ([v] (F' v))) MN' (eqlsize'/rec1 FS')
    <- {v} adjust-varlevel/L1 (F v) (FS v) MS (F' v) MN' (FS' v).

- : adjust-varlevel/L1 
	(eql/rec2 P MC1 MA1 ([v] [vl:varadjlevel v z (s N)] (F v vl)))
	(eqlsize/rec2 FS MN MM) _ EQ z ES
    <- min-implies-ge MN ZERO>=B+1 _
    <- ge-succ-implies-gt ZERO>=B+1 ZERO>B
    <- gt-contradiction ZERO>B V
    <- false-implies-eql' V EQ
    <- false-implies-eqlsize' V ES.

- : adjust-varlevel/L1 
	(eql/rec2 P MC1 MA1 ([v] [vl:varadjlevel v (s M) (s N)] (F v vl)))
	(eqlsize/rec2 FS MN MM) MS
        (eql'/rec2 P' MC1' MA1' ([v] [vl:varadjlevel' v M (s N)] (F' v vl))) _
	(eqlsize'/rec2 FS'' MN' MM')
    <- plus-swap-succ-converse P P'
    <- nat`min-implies-ge MN _ B2>=B+1
    <- ge-succ-implies-gt B2>=B+1 B2>B
    <- gt-implies-positive B2>B B2' B2=B2'+1    
    <- ({v} {vl} 
	  eqlsize-respects-eq (FS v vl) nat`eq/ B2=B2'+1 nat`eq/ (FS' v vl))
    <- shift-preserves-add-converse MA1 MS (plus/s plus/z) _ MS' MA1'
    <- ({v} {vl} {vl':varadjlevel' v M (s N)} 
	  {vsd:varlevel-adjusts-down vl vl'}
	  adjust-varlevel/L0 (F v vl) (FS' v vl) (F' v vl') _ (FS'' v vl'))
    <- shift-preserves-count-converse MC1 MS (plus/s plus/z) MC1'
    <- succ-implies-gt-zero _ MM1+1>0
    <- nat`max-deterministic (max/> MM1+1>0) MM nat`eq/ nat`eq/ MM1+1=MM+1
    <- succ-cancels MM1+1=MM+1 MM1=MM
    <- nat`ge-zero-always _ MM1>=0
    <- nat`ge-implies-max MM1>=0 MAX2''
    <- nat`max-respects-eq MAX2'' nat`eq/ nat`eq/ MM1=MM MM'
    <- nat`min-total MN'.

- : adjust-varlevel/L1 
	(eql/rec2 P MC1 MA1 ([v] [vl:varadjlevel v (s M) (s N)] (F v vl)))
	(eqlsize/rec2 FS MN MM) MS
        (eql'/rec2 P' MC1' MA1' ([v] [vl:varadjlevel' v M (s N)] (F' v vl))) _
	(eqlsize'/rec2 FS'' MN' MM')
    <- plus-swap-succ-converse P P'
    <- nat`min-implies-ge MN _ B2>=B+1
    <- ge-succ-implies-gt B2>=B+1 B2>B
    <- gt-implies-positive B2>B B2' B2=B2'+1    
    <- ({v} {vl} 
	  eqlsize-respects-eq (FS v vl) nat`eq/ B2=B2'+1 nat`eq/ (FS' v vl))
    <- shift-preserves-add-converse MA1 MS (plus/s plus/z) _ MS' MA1'
    <- ({v} {vl} {vl':varadjlevel' v M (s N)} 
	  {vsd:varlevel-adjusts-down vl vl'}
	  adjust-varlevel/L1 (F v vl) (FS' v vl) MS' (F' v vl') _ (FS'' v vl'))
    <- shift-preserves-count-converse MC1 MS (plus/s plus/z) MC1'
    <- nat`min-total MN'
    <- succ-preserves-max-converse MM MM'.

%worlds (blocksimple | adjustdown) (adjust-varlevel/L1 _ _ _ _ _ _).
%total (E) (adjust-varlevel/L1 E _ _ _ _ _).


%theorem adjust-varlevel :
	forall* {N} {A} {M0} {M1} {T1} {T2} {S} {MN} {MM}
	forall	{E: eql* N A M1 T1 T2}
		{ES:eqlsize E S (s MN) (s MM)}
		{MS:multiset`shift z M0 M1}
	exists	{E': eql* N (s A) M0 T1 T2} {MN'}
		{ES':eqlsize E' S MN' MM}
	true.

- : adjust-varlevel E ES MS E'' _ ES''
    <- adjust-varlevel/L1 E ES MS E' _ ES'
    <- shift-varlevel/L2 E' ES' E'' ES''.

%worlds (blocksimple) (adjust-varlevel _ _ _ _ _ _).
%total { } (adjust-varlevel _ _ _ _ _ _).

Removing variable levels altogether

The following blocks are used when we remove the level for the outermost (level 1) variable of adjusted index zero. All other variables are at least level 2 or non-zero adjusted index. "blockvar2" and "blockvaradj" makes this context explicit. (I probably could substitute noshift for blockvaradj

%block blockvar2 : some {l} {n}  
		    block {v:term n} {vl:varadjlevel v z (s (s l))}.
%block blockvaradj : some {m} {l} {n}
		      block {v:term n} {vl:varadjlevel v (s m) (s l)}.

%theorem remove-one-var :
	forall* {N} {N'} {F1} {F2} {S} {A} {M} {NZ} {MN} {MM}
	forall  {E:{v:term N} {vl:varadjlevel v z (s z)} 
		     (eql* N' A M (F1 v) (F2 v))}
	        {ES:{v} {vl} eqlsize (E v vl) S MN MM}
		{MC: multiset`count M z (s NZ)}
	exists	{E':{v:term N} (eql A M (F1 v) (F2 v))}
		{ES':{v} eqlsize (E' v) S MN MM}
	true.

- : remove-one-var ([v] [vl] eql/eq eq/) ([v] [vl] eqlsize/eq) _
                   ([v] eql/eq eq/) ([v] eqlsize/eq).

- : remove-one-var ([v] [vl] (eql/app (FE v vl) (AE v vl))) 
		   ([v] [vl] (eqlsize/app (ESF v vl) (ESA v vl) MX MN MX2)) MC
                   ([v] (eql/app (FE' v) (AE' v)))
                   ([v] (eqlsize/app (ESF' v) (ESA' v) MX MN MX2))
    <- remove-one-var FE ESF MC FE' ESF'
    <- remove-one-var AE ESA MC AE' ESA'.

- : remove-one-var ([v] [vl] eql/lam1 ([v'] (F v' v vl)))
		   ([v] [vl] eqlsize/lam1 ([v'] (FS v' v vl))) MC
                   ([v] eql/lam1 ([v'] (F' v' v)))
                   ([v] eqlsize/lam1 ([v'] (FS' v' v)))
    <- {v'} remove-one-var (F v') (FS v') MC (F' v') (FS' v').

%theorem remove-one-var/lam2 :
	forall* {N0} {N1} {N2} {N3} {N1'} {S} {A} {M0} {M1} {F1} {F2} {MN} {MM}
	forall	{E:{v':term N0} {vl':varadjlevel v' z (s N1)}
		     {v:term N2} {vl:varadjlevel v z (s z)}
		     (eql* N3 A M1 (F1 v' v) (F2 v' v))}
		{ES:{v':term N0} {vl':varadjlevel v' z (s N1)}
		     {v:term N2} {vl:varadjlevel v z (s z)}
		     (eqlsize (E v' vl' v vl) S MN MM)}
		{MC: multiset`count M0 z N1}
		{MA: multiset`add M0 z M1}
		{EQ: nat`eq N1 (s N1')}
	exists	{E': {v':term N0} {vl':varadjlevel v' z (s N1)}
		      {v:term N2}
		      (eql* N3 A M1 (F1 v' v) (F2 v' v))}
		{ES':{v':term N0} {vl':varadjlevel v' z (s N1)}
		       {v:term N2}
		       (eqlsize (E' v' vl' v) S MN MM)}
	true.

- : remove-one-var/lam2 E ES MC0 MA nat`eq/ E' ES'		     
    <- count-add-implies-count MC0 MA MC1
    <- {v'} {vl'} remove-one-var (E v' vl') (ES v' vl') MC1 
                                 (E' v' vl') (ES' v' vl').

- : remove-one-var ([v] [vl] eql/lam2 MC MA  ([v'] [vl'] (F v' vl' v vl)))
		   ([v] [vl] eqlsize/lam2 ([v'] [vl'] (FS v' vl' v vl)) MM) MC0
                   ([v] eql/lam2 MC MA ([v'] [vl'] (F' v' vl' v)))
                   ([v] eqlsize/lam2 ([v'] [vl'] (FS' v' vl' v)) MM)
    <- count-deterministic MC MC0 multiset`eq/ nat`eq/ EQ
    <- remove-one-var/lam2 F FS MC (MA:add M0 z M1) EQ F' FS'.

- : remove-one-var ([v] [vl] eql/rec1 ([v'] (F v' v vl)))
		   ([v] [vl] eqlsize/rec1 ([v'] (FS v' v vl))) MC
                   ([v] eql/rec1 ([v'] (F' v' v)))
                   ([v] eqlsize/rec1 ([v'] (FS' v' v)))
    <- {v'} remove-one-var (F v') (FS v') MC (F' v') (FS' v').

- : remove-one-var ([v] [vl] eql/rec2 P MC MA  ([v'] [vl'] (F v' vl' v vl)))
		   ([v] [vl] eqlsize/rec2 ([v'] [vl'] (FS v' vl' v vl)) MN MM) MC0
                   ([v] eql/rec2 P MC MA ([v'] [vl'] (F' v' vl' v)))
                   ([v] eqlsize/rec2 ([v'] [vl'] (FS' v' vl' v)) MN MM)
    <- count-deterministic MC MC0 multiset`eq/ nat`eq/ EQ
    <- remove-one-var/lam2 F FS MC MA EQ F' FS'.

- : remove-one-var ([v] [vl] eql/rec2 P MC MA  ([v'] [vl'] (F v' vl' v vl)))
		   ([v] [vl] eqlsize/rec2 ([v'] [vl'] (FS v' vl' v vl)) MN MM) MC0
                   ([v] eql/rec2 P MC MA ([v'] [vl'] (F' v' vl' v)))
                   ([v] eqlsize/rec2 ([v'] [vl'] (FS' v' vl' v)) MN MM)
    <- succ-implies-gt-zero _ GT
    <- add-preserves-count MC0 MA (nat`ne/< GT) MC1
    <- {v'} {vl'} remove-one-var (F v' vl') (FS v' vl') MC1 
                                 (F' v' vl') (FS' v' vl').

- : remove-one-var ([v] [vl] eql/var P vl vl) ([v] [vl] eqlsize/var) _
                   ([v] eql/eq eq/) ([v] eqlsize/eq).

- : remove-one-var ([v] [vl] eql/var P VL1 VL2) ([v] [vl] eqlsize/var) _
                   ([v] eql/var P VL1 VL2) ([v] eqlsize/var).

%worlds (blocksimple | blockvar2 | blockvaradj | noshift) 
        (remove-one-var _ _ _ _ _) (remove-one-var/lam2 _ _ _ _ _ _ _).
%total (E El) (remove-one-var E _ _ _ _)
              (remove-one-var/lam2 El _ _ _ _ _ _).

We now have the machinery needed to get rid of all level 0 variables in one recursive sweep.

%theorem remove-zero-index-vars :
	forall* {N} {A} {MS} {T1} {T2} {MN} {MM}
	forall	{E: eql* N A MS T1 T2} {S}
		{ES:eqlsize E S MN MM}
		{MC:multiset`count MS z z} 
	exists	{E': eql* N A MS T1 T2} {MN'} {MM'}
		{ES':eqlsize E' S (s MN') MM'}
		{G: nat`ge MM MM'}
	true.

- : remove-zero-index-vars
	(eql/eq E) _ (eqlsize/eq) _ (eql/eq E) _ _ (eqlsize/eq) 
	(nat`ge/= nat`eq/).

- : remove-zero-index-vars
	(eql/app E1 E2) (s S) (eqlsize/app ES1 ES2 MAX1 _ MAX2) MC
	(eql/app E1' E2') _ _ (eqlsize/app ES1' ES2' MAX1 MIN' MAX2')
	GE
    <- nat`max-implies-ge MAX1 S>=S1 S>=S2
    <- ge-implies-succ-gt S>=S1 S+1>S1
    <- ge-implies-succ-gt S>=S2 S+1>S2
    <- nat`meta-gt _ _ S+1>S1
    <- nat`meta-gt _ _ S+1>S2
    <- remove-zero-index-vars E1 S1 ES1 MC E1' _ _ ES1' GE1
    <- remove-zero-index-vars E2 S2 ES2 MC E2' _ _ ES2' GE2
    <- nat`min-total MIN
    <- succ-preserves-min MIN MIN'
    <- nat`max-total MAX2'
    <- max-preserves-ge* GE1 GE2 MAX2 MAX2' GE.

- : remove-zero-index-vars
	(eql/lam1 FE) _ (eqlsize/lam1 FES) MC
	(eql/lam1 FE') _ _ (eqlsize/lam1 FES') GE
    <- {v} remove-zero-index-vars (FE v) _ (FES v) MC (FE' v) _ _ (FES' v) GE.

- : remove-zero-index-vars 
	(eql/lam2 MC0 (MA0:add MS0 z MS1) ([v] [vl] FE0 v vl)) _
	(eqlsize/lam2 ([v] [vl] FES0 v vl) MAX) MC
        (eql/lam1 ([v] FE3 v)) _ _ 
	(eqlsize/lam1 ([v] FES3 v)) GE'
    <- count-add-implies-count MC0 MA0 MC1
    <- remove-one-var FE0 FES0 MC1 FE1 FES1
    <- ({v} shift-varlevel (FE1 v) (FES1 v) MA0 (FE2 v) (FES2 v))
    <- ({v} remove-zero-index-vars (FE2 v) S' (FES2 v) MC
	  (FE3 v) _ _ (FES3 v) GE)
    <- nat`max-implies-ge MAX _ GE1
    <- nat`ge-transitive GE1 GE GE'.

- : remove-zero-index-vars 
	(eql/lam2 (MC0:count MS0 z (s C)) MA0 ([v] [vl] FE0 v vl)) _
	(eqlsize/lam2 ([v] [vl] FES0 v vl) MAX) MC
        EQ z z EQS GE
    <- multiset`count-deterministic MC MC0 multiset`eq/ nat`eq/ ZERO=C+1
    <- nat`eq-contradiction ZERO=C+1 F
    <- false-implies-eql F EQ
    <- false-implies-eqlsize F EQS
    <- nat`false-implies-ge F GE.

- : remove-zero-index-vars
	(eql/rec1 FE) _ (eqlsize/rec1 FES) MC
	(eql/rec1 FE') _ _ (eqlsize/rec1 FES') GE
    <- {v} remove-zero-index-vars (FE v) _ (FES v) MC (FE' v) _ _ (FES' v) GE.

- : remove-zero-index-vars 
	(eql/rec2 P MC0 (MA0:add MS0 z MS1) ([v] [vl] FE0 v vl)) _
	(eqlsize/rec2 ([v] [vl] FES0 v vl) MIN MAX) MC
        (eql/rec1 ([v] FE3 v)) _ _
	(eqlsize/rec1 ([v] FES3 v)) GE'
    <- count-add-implies-count MC0 MA0 MC1
    <- remove-one-var FE0 FES0 MC1 FE1 FES1
    <- ({v} shift-varlevel (FE1 v) (FES1 v) MA0 (FE2 v) (FES2 v))
    <- ({v} remove-zero-index-vars (FE2 v) S' (FES2 v) MC
	  (FE3 v) _ _ (FES3 v) GE)
    <- nat`max-implies-ge MAX _ GE1
    <- nat`ge-transitive GE1 GE GE'.

- : remove-zero-index-vars 
	(eql/rec2 P MC0 (MA0:add MS0 z MS1) ([v] [vl] FE0 v vl)) _
	(eqlsize/rec2 ([v] [vl] FES0 v vl) MIN MAX) MC
        EQ z z EQS GE
    <- multiset`count-deterministic MC MC0 multiset`eq/ nat`eq/ ZERO=C+1
    <- nat`eq-contradiction ZERO=C+1 F
    <- false-implies-eql F EQ
    <- false-implies-eqlsize F EQS
    <- nat`false-implies-ge F GE.

- : remove-zero-index-vars 
	(eql/rec2 P MC0 (MA0:add MS0 (s M) MS1) ([v] [vl] FE0 v vl)) _
	(eqlsize/rec2 ([v] [vl] FES0 v vl) _ (MAX:max (s (s M)) MM2 MM)) MC
        (eql/rec2 P MC0 MA0 ([v] [vl] FE1 v vl)) _ _
	(eqlsize/rec2 ([v] [vl] FES1 v vl) MIN' MAX') GE'
    <- ge-zero-always M M>=0
    <- ge-implies-succ-gt M>=0 M+1>0
    <- add-preserves-count MC MA0 (nat`ne/< M+1>0) MC'
    <- ({v} {vl} {vl'} (varlevel-nonzero-shifts-over vl vl')
	  -> (varlevel-shifts-back vl' vl) 
	  -> (remove-zero-index-vars (FE0 v vl) S' (FES0 v vl) MC'
		(FE1 v vl) _ _ (FES1 v vl) GE))
    <- nat`min-total MIN
    <- succ-preserves-min MIN MIN'
    <- nat`max-total MAX'
    <- max-preserves-ge* (nat`ge/= nat`eq/) GE MAX MAX' GE'.

- : remove-zero-index-vars
	(eql/var P VL1 VL2) _ (eqlsize/var) _
	(eql/var P VL1 VL2) _ _ (eqlsize/var) (nat`ge/= nat`eq/).

%worlds (blocksimple | noshift) (remove-zero-index-vars _ _ _ _ _ _ _ _ _).
%total (S) (remove-zero-index-vars _ S _ _ _ _ _ _ _).


%theorem lit-preserves-eq :
	forall* {M1} {M2}
	forall	{EQ:nat`eq M1 M2}
	exists	{EQ':eq (lit M1) (lit M2)}
	true.

- : lit-preserves-eq nat`eq/ eq/.

%worlds (blocksimple | blockvar) (lit-preserves-eq _ _).
%total { } (lit-preserves-eq _ _).


%theorem app-preserves-eq :
	forall* {N1} {N2}
		{T1:term (s N1)} {T2:term (s N2)} {T3} {T4}
	forall	{E:eq T1 T2} {E: eq T3 T4}
	exists	{BE:eq (app T1 T3) (app T2 T4)}
	true.

- : app-preserves-eq eq/ eq/ eq/.

%worlds (blocksimple) (app-preserves-eq _ _ _).
%total { } (app-preserves-eq _ _ _).


%theorem lam-preserves-eq :
	forall* {N1} {N2} {F1:t -> term N1} {F2: t -> term N2}
	forall	{E:{v} eq (F1 v) (F2 v)}
	exists	{E:eq (lam F1) (lam F2)}
	true.

- : lam-preserves-eq ([v] eq/) eq/.

%worlds (blocksimple) (lam-preserves-eq _ _).
%total { } (lam-preserves-eq _ _).


%theorem rec-preserves-eq :
	forall* {N}
		{F1:term (s N) -> term (s N)} 
		{F2:term (s N) -> term (s N)}
	forall	{E:{v} eq (F1 v) (F2 v)}
	exists	{E:eq (rec F1) (rec F2)}
	true.

- : rec-preserves-eq ([v] eq/) eq/.

%worlds (blocksimple) (rec-preserves-eq _ _).
%total { } (rec-preserves-eq _ _).

Next the main lemma that says we can avoid looking at varlevels in checking equality. We remove the outside variable, shift remaining variables, and then recurse (hence the need for tracking eqlsize). Note that we never put var levels in the context.

%theorem eql-implies-eq :
	forall* {N} {T1:term N} {T2:term N}
	forall	{E:eql z multiset`map/0 T1 T2}
	exists	{E':eq T1 T2}
	true.

%theorem eql-implies-eq/L0 :
	forall* {N} {A} {MS} {T1} {T2} {S} {MN}
	forall	{E: eql* N A MS T1 T2}
		{ES:eqlsize E S MN z}
	exists	{E: eq T1 T2}
	true.

- : eql-implies-eq/L0 (eql/eq E) _ E.

- : eql-implies-eq/L0 (eql/app E1 E2) (eqlsize/app ES1 ES2 MAX1 MIN MAX2) E'
    <- max-implies-ge MAX2 ZERO>=M1 ZERO>=M2
    <- ge-zero-always _ M1>=0
    <- ge-zero-always _ M2>=0
    <- ge-anti-symmetric M1>=0 ZERO>=M1 M1=0
    <- ge-anti-symmetric M2>=0 ZERO>=M2 M2=0
    <- eqlsize-respects-eq ES1 nat`eq/ nat`eq/ M1=0 ES1'
    <- eqlsize-respects-eq ES2 nat`eq/ nat`eq/ M2=0 ES2'
    <- eql-implies-eq/L0 E1 ES1' E1'
    <- eql-implies-eq/L0 E2 ES2' E2'
    <- app-preserves-eq E1' E2' E'.

- : eql-implies-eq/L0 (eql/lam1 ([v] E v)) (eqlsize/lam1 ([v] ES v)) E''
    <- ({v} eql-implies-eq/L0 (E v) (ES v) (E' v))
    <- lam-preserves-eq E' E''.

- : eql-implies-eq/L0 (eql/lam2 _ _ _) (eqlsize/lam2 _ MAX) E
    <- nat`max-implies-ge MAX ZERO>=ONE _
    <- ge-succ-implies-gt ZERO>=ONE ZERO>ZERO
    <- nat`gt-contradiction ZERO>ZERO F
    <- false-implies-eq F E.

- : eql-implies-eq/L0 (eql/rec1 ([v] E v)) (eqlsize/rec1 ([v] ES v)) E''
    <- ({v} eql-implies-eq/L0 (E v) (ES v) (E' v))
    <- rec-preserves-eq E' E''.

- : eql-implies-eq/L0 (eql/rec2 _ _ _ _) (eqlsize/rec2 _ _ MAX) E
    <- nat`max-implies-ge MAX ZERO>=ONE _
    <- ge-succ-implies-gt ZERO>=ONE ZERO>ZERO
    <- nat`gt-contradiction ZERO>ZERO F
    <- false-implies-eq F E.

%worlds (blocksimple) (eql-implies-eq/L0 _ _ _).
%total (E) (eql-implies-eq/L0 E _ _).

%theorem eql-implies-eq/L1 :
	forall* {N} {A} {T1} {T2} {S} {MN}
	forall	{E: eql* N A multiset`map/0 T1 T2} {MM}
		{ES:eqlsize E S MN MM}
	exists	{E: eq T1 T2}
	true.

- : eql-implies-eq/L1 EQL z ES E
    <- eql-implies-eq/L0 EQL ES E. 

%theorem eql-implies-eq/L2 :
	forall* {N} {A} {T1} {T2} {S} {MN}
	forall	{E: eql* N A multiset`map/0 T1 T2} {MM}
		{ES:eqlsize E S (s MN) MM}
	exists	{E: eq T1 T2}
	true.

- : eql-implies-eq/L2 EQL z ES E
    <- eql-implies-eq/L0 EQL ES E. 

- : eql-implies-eq/L2 EQL (s M) ES E
    <- adjust-varlevel EQL ES multiset`shift/0 E' _ ES'
    <- eql-implies-eq/L1 E' _ ES' E.

- : eql-implies-eq/L1 EQL (s M) ES E
    <- remove-zero-index-vars EQL _ ES (multiset`count/z multiset`not-member/0)
	EQL' _ _ ES' GE
    <- meta-ge _ _ GE
    <- eql-implies-eq/L2 EQL' _ ES' E.

%worlds () (eql-implies-eq/L1 _ _ _ _) (eql-implies-eq/L2 _ _ _ _).
%total (M1 M2) 
	(eql-implies-eq/L2 _ M2 _ _)
	(eql-implies-eq/L1 _ M1 _ _).

- : eql-implies-eq E E'
    <- eqlsize-total ES
    <- eql-implies-eq/L1 E _ ES E'.

%worlds () (eql-implies-eq _ _).
%total { } (eql-implies-eq _ _).

Main Theorem

Finally the statement of the main theorem of this section. As with the non-indexed case, it is proved by using eql as a between station. Again, as with the non-indexed code, this theorem (or rather its main lemma) uses reasoning-from-false extensively because the cases cannot be distinguished by Twelf's case analysis. It also uses the "divrem" part of the nat signature extensively as well as theorems about plus and times. The proofs of the cases are uninteresting arithmetic fiddling.

%theorem tonat-one2one :
	forall*	{N} {T1:term N} {N1} {T2:term N} {N2}
	forall	{TN1:tonat T1 N1}
		{TN2:tonat T2 N2}
		{E:nat`eq N1 N2}
	exists	{ET:eq T1 T2}
	true.

%theorem tonat-one2one/L :
	forall*	{N} {MS} {T1} {M1} {T2} {M2}
	forall	{TN1:tonat* N MS T1 M1}
		{TN2:tonat* N MS T2 M2}
		{E:nat`eq M1 M2}
	exists	{ET:eql* N z MS T1 T2}
	true.

- : tonat-one2one/L (tonat/var MC1 VL1 P1) (tonat/var MC2 VL2 P2) nat`eq/
		    (eql/var plus/z VL1' VL2)
    <- count-deterministic MC1 MC2 multiset`eq/ nat`eq/ VN1=VN2
    <- plus-left-cancels P1 P2 nat`eq/ VN1=VN2 L1=L2
    <- varlevel-respects-eq VL1 L1=L2 VL1'.

- : tonat-one2one/L (tonat/var MC VL M+L=VN) 
                    (tonat/lit MC' _ VN'+X=M) nat`eq/ E
    <- count-deterministic MC' MC multiset`eq/ nat`eq/ VN'=VN
    <- plus-respects-eq VN'+X=M VN'=VN nat`eq/ nat`eq/ VN+X=M
    <- plus-commutative VN+X=M X+VN=M
    <- plus-commutative M+L=VN L+M=VN
    <- plus-implies-ge X+VN=M M>=VN
    <- plus-implies-ge L+M=VN VN>=M
    <- nat`ge-anti-symmetric M>=VN VN>=M M=VN
    <- plus-right-cancels L+M=VN plus/z M=VN nat`eq/ L=0
    <- varlevel-contradiction VL L=0 F
    <- false-implies-eql F E.

- : tonat-one2one/L (tonat/lit MC' _ VN'+X=M) 
                    (tonat/var MC VL M+L=VN) nat`eq/ E
    <- count-deterministic MC' MC multiset`eq/ nat`eq/ VN'=VN
    <- plus-respects-eq VN'+X=M VN'=VN nat`eq/ nat`eq/ VN+X=M
    <- plus-commutative VN+X=M X+VN=M
    <- plus-commutative M+L=VN L+M=VN
    <- plus-implies-ge X+VN=M M>=VN
    <- plus-implies-ge L+M=VN VN>=M
    <- nat`ge-anti-symmetric M>=VN VN>=M M=VN
    <- plus-right-cancels L+M=VN plus/z M=VN nat`eq/ L=0
    <- varlevel-contradiction VL L=0 F
    <- false-implies-eql F E.

- : tonat-one2one/L (tonat/var MC VL M+L=VN) 
                    (tonat/app MC' _ _ _ _ VN'+X=M) nat`eq/ E
    <- count-deterministic MC' MC multiset`eq/ nat`eq/ VN'=VN
    <- plus-respects-eq VN'+X=M VN'=VN nat`eq/ nat`eq/ VN+X=M
    <- plus-commutative VN+X=M X+VN=M
    <- plus-commutative M+L=VN L+M=VN
    <- plus-implies-ge X+VN=M M>=VN
    <- plus-implies-ge L+M=VN VN>=M
    <- nat`ge-anti-symmetric M>=VN VN>=M M=VN
    <- plus-right-cancels L+M=VN plus/z M=VN nat`eq/ L=0
    <- varlevel-contradiction VL L=0 F
    <- false-implies-eql F E.

- : tonat-one2one/L (tonat/app MC' _ _ _ _ VN'+X=M) 
                    (tonat/var MC VL M+L=VN) nat`eq/ E
    <- count-deterministic MC' MC multiset`eq/ nat`eq/ VN'=VN
    <- plus-respects-eq VN'+X=M VN'=VN nat`eq/ nat`eq/ VN+X=M
    <- plus-commutative VN+X=M X+VN=M
    <- plus-commutative M+L=VN L+M=VN
    <- plus-implies-ge X+VN=M M>=VN
    <- plus-implies-ge L+M=VN VN>=M
    <- nat`ge-anti-symmetric M>=VN VN>=M M=VN
    <- plus-right-cancels L+M=VN plus/z M=VN nat`eq/ L=0
    <- varlevel-contradiction VL L=0 F
    <- false-implies-eql F E.

- : tonat-one2one/L (tonat/var MC VL M+L=VN) 
                    (tonat/lam MC' _ _ _ _ VN'+X=M) nat`eq/ E
    <- count-deterministic MC' MC multiset`eq/ nat`eq/ VN'=VN
    <- plus-respects-eq VN'+X=M VN'=VN nat`eq/ nat`eq/ VN+X=M
    <- plus-commutative VN+X=M X+VN=M
    <- plus-commutative M+L=VN L+M=VN
    <- plus-implies-ge X+VN=M M>=VN
    <- plus-implies-ge L+M=VN VN>=M
    <- nat`ge-anti-symmetric M>=VN VN>=M M=VN
    <- plus-right-cancels L+M=VN plus/z M=VN nat`eq/ L=0
    <- varlevel-contradiction VL L=0 F
    <- false-implies-eql F E.

- : tonat-one2one/L (tonat/lam MC' _ _ _ _ VN'+X=M) 
                    (tonat/var MC VL M+L=VN) nat`eq/ E
    <- count-deterministic MC' MC multiset`eq/ nat`eq/ VN'=VN
    <- plus-respects-eq VN'+X=M VN'=VN nat`eq/ nat`eq/ VN+X=M
    <- plus-commutative VN+X=M X+VN=M
    <- plus-commutative M+L=VN L+M=VN
    <- plus-implies-ge X+VN=M M>=VN
    <- plus-implies-ge L+M=VN VN>=M
    <- nat`ge-anti-symmetric M>=VN VN>=M M=VN
    <- plus-right-cancels L+M=VN plus/z M=VN nat`eq/ L=0
    <- varlevel-contradiction VL L=0 F
    <- false-implies-eql F E.

- : tonat-one2one/L (tonat/var MC VL M+L=VN) 
                    (tonat/rec MC' _ _ _ VN'+X=M) nat`eq/ E
    <- count-deterministic MC' MC multiset`eq/ nat`eq/ VN'=VN
    <- plus-respects-eq VN'+X=M VN'=VN nat`eq/ nat`eq/ VN+X=M
    <- plus-commutative VN+X=M X+VN=M
    <- plus-commutative M+L=VN L+M=VN
    <- plus-implies-ge X+VN=M M>=VN
    <- plus-implies-ge L+M=VN VN>=M
    <- nat`ge-anti-symmetric M>=VN VN>=M M=VN
    <- plus-right-cancels L+M=VN plus/z M=VN nat`eq/ L=0
    <- varlevel-contradiction VL L=0 F
    <- false-implies-eql F E.

- : tonat-one2one/L (tonat/rec MC' _ _ _ VN'+X=M) 
                    (tonat/var MC VL M+L=VN) nat`eq/ E
    <- count-deterministic MC' MC multiset`eq/ nat`eq/ VN'=VN
    <- plus-respects-eq VN'+X=M VN'=VN nat`eq/ nat`eq/ VN+X=M
    <- plus-commutative VN+X=M X+VN=M
    <- plus-commutative M+L=VN L+M=VN
    <- plus-implies-ge X+VN=M M>=VN
    <- plus-implies-ge L+M=VN VN>=M
    <- nat`ge-anti-symmetric M>=VN VN>=M M=VN
    <- plus-right-cancels L+M=VN plus/z M=VN nat`eq/ L=0
    <- varlevel-contradiction VL L=0 F
    <- false-implies-eql F E.

- : tonat-one2one/L (tonat/lit MC1 T1 P1) (tonat/lit MC2 T2 P2) nat`eq/
		    (eql/eq T1=T2)
    <- count-deterministic MC1 MC2 multiset`eq/ nat`eq/ VN1=VN2
    <- plus-left-cancels P1 P2 VN1=VN2 nat`eq/ TM1=TM2
    <- times-left-cancels T1 T2 nat`eq/ TM1=TM2 M1=M2
    <- lit-preserves-eq M1=M2 T1=T2.

%abbrev 2>1 = gt/1.

- : tonat-one2one/L (tonat/lit MC T P) (tonat/app MC' _ _ _ T' P') nat`eq/ E
    <- count-deterministic MC' MC multiset`eq/ nat`eq/ VN'=VN
    <- plus-left-cancels P' P VN'=VN nat`eq/ TM'+1=TM
    <- times-commutative T Tc
    <- div-can-be-constructed Tc DR
    <- plus-commutative (plus/s plus/z) TM'+ONE=TM'+1
    <- plus-respects-eq TM'+ONE=TM'+1 nat`eq/ nat`eq/ TM'+1=TM TM'+ONE=TM
    <- times-commutative T' Tc'
    <- divrem-can-be-constructed Tc' TM'+ONE=TM 2>1 DR'
    <- divrem-deterministic DR DR' nat`eq/ nat`eq/ QE ZERO=ONE
    <- nat`eq-contradiction ZERO=ONE F
    <- false-implies-eql F E.

- : tonat-one2one/L (tonat/app MC' _ _ _ T' P') (tonat/lit MC T P) nat`eq/ E
    <- count-deterministic MC' MC multiset`eq/ nat`eq/ VN'=VN
    <- plus-left-cancels P' P VN'=VN nat`eq/ TM'+1=TM
    <- times-commutative T Tc
    <- div-can-be-constructed Tc DR
    <- plus-commutative (plus/s plus/z) TM'+ONE=TM'+1
    <- plus-respects-eq TM'+ONE=TM'+1 nat`eq/ nat`eq/ TM'+1=TM TM'+ONE=TM
    <- times-commutative T' Tc'
    <- divrem-can-be-constructed Tc' TM'+ONE=TM 2>1 DR'
    <- divrem-deterministic DR DR' nat`eq/ nat`eq/ QE ZERO=ONE
    <- nat`eq-contradiction ZERO=ONE F
    <- false-implies-eql F E.

- : tonat-one2one/L (tonat/app MC1 TN1a TN1b P2N1 T1 P1)
		    (tonat/app MC2 TN2a TN2b P2N2 T2 P2) nat`eq/ 
		    (eql/app E1 E2)
    <- count-deterministic MC1 MC2 multiset`eq/ nat`eq/ VN1=VN2
    <- plus-left-cancels P1 P2 VN1=VN2 nat`eq/ TM1+1=TM2+1
    <- succ-cancels TM1+1=TM2+1 TM1=TM2
    <- times-left-cancels T1 T2 nat`eq/ TM1=TM2 (M1=M2:nat`eq M1 M2)
    <- nat2pair-deterministic P2N1 P2N2 M1=M2 PR1=PR2
    <- natpair`pair-eq-implies-eq PR1=PR2 EQa EQb
    <- tonat-one2one/L TN1a TN2a EQa E1
    <- tonat-one2one/L TN1b TN2b EQb E2.

%abbrev 2+2=4 : plus (s (s z)) (s (s z)) (s (s (s (s z))))
		 = (plus/s (plus/s plus/z)).
%abbrev 2x2=4 : times (s (s z)) (s (s z)) (s (s (s (s z))))
		 = (times/s (times/s times/z plus/z) 2+2=4).
 
- : tonat-one2one/L (tonat/app MC1 TN1a TN1b P2N1 T1 P1)
                    (tonat/lam MC2 MC0 MA0 _ T2 P2) nat`eq/ E
    <- count-deterministic MC1 MC2 multiset`eq/ nat`eq/ VN1=VN2
    <- plus-left-cancels P1 P2 VN1=VN2 nat`eq/ TM1+1=TM2
    <- times-associative 2x2=4 T2 _ T2' T2''
    <- times-commutative T2'' T2''c
    <- div-can-be-constructed T2''c DR2
    <- plus-commutative (plus/s plus/z) TM1+ONE=TM1+1
    <- plus-respects-eq TM1+ONE=TM1+1 nat`eq/ nat`eq/ TM1+1=TM2 TM1+ONE=TM2
    <- times-commutative T1 T1c
    <- divrem-can-be-constructed T1c TM1+ONE=TM2 2>1 DR1
    <- divrem-deterministic DR2 DR1 nat`eq/ nat`eq/ QE ZERO=ONE
    <- nat`eq-contradiction ZERO=ONE F
    <- false-implies-eql F E.

- : tonat-one2one/L (tonat/lam MC2 MC0 MA0 _ T2 P2)
                    (tonat/app MC1 TN1a TN1b P2N1 T1 P1) nat`eq/ E
    <- count-deterministic MC1 MC2 multiset`eq/ nat`eq/ VN1=VN2
    <- plus-left-cancels P1 P2 VN1=VN2 nat`eq/ TM1+1=TM2
    <- times-associative 2x2=4 T2 _ T2' T2''
    <- times-commutative T2'' T2''c
    <- div-can-be-constructed T2''c DR2
    <- plus-commutative (plus/s plus/z) TM1+ONE=TM1+1
    <- plus-respects-eq TM1+ONE=TM1+1 nat`eq/ nat`eq/ TM1+1=TM2 TM1+ONE=TM2
    <- times-commutative T1 T1c
    <- divrem-can-be-constructed T1c TM1+ONE=TM2 2>1 DR1
    <- divrem-deterministic DR2 DR1 nat`eq/ nat`eq/ QE ZERO=ONE
    <- nat`eq-contradiction ZERO=ONE F
    <- false-implies-eql F E.

- : tonat-one2one/L (tonat/app MC1 _ _ _ T1 P1)
                    (tonat/rec MC2 _ _ T2 P2) nat`eq/ E
    <- count-deterministic MC1 MC2 multiset`eq/ nat`eq/ VN1=VN2
    <- plus-left-cancels P1 P2 VN1=VN2 nat`eq/ TM1+1=TM2+2
    <- times-associative 2x2=4 T2 _ _ T2'
    <- times-commutative T2' T2'c
    <- plus-commutative (plus/s (plus/s plus/z)) P2'c
    <- div-can-be-constructed (times/s T2'c P2'c) DR2
    <- plus-commutative (plus/s plus/z) TM1+ONE=TM1+1
    <- plus-respects-eq TM1+ONE=TM1+1 nat`eq/ nat`eq/ TM1+1=TM2+2 TM1+ONE=TM2+2
    <- times-commutative T1 T1c
    <- divrem-can-be-constructed T1c TM1+ONE=TM2+2 2>1 DR1
    <- divrem-deterministic DR2 DR1 nat`eq/ nat`eq/ QE ZERO=ONE
    <- nat`eq-contradiction ZERO=ONE F
    <- false-implies-eql F E.

- : tonat-one2one/L (tonat/rec MC2 _ _ T2 P2) 
                    (tonat/app MC1 _ _ _ T1 P1) nat`eq/ E
    <- count-deterministic MC1 MC2 multiset`eq/ nat`eq/ VN1=VN2
    <- plus-left-cancels P1 P2 VN1=VN2 nat`eq/ TM1+1=TM2+2
    <- times-associative 2x2=4 T2 _ _ T2'
    <- times-commutative T2' T2'c
    <- plus-commutative (plus/s (plus/s plus/z)) P2'c
    <- div-can-be-constructed (times/s T2'c P2'c) DR2
    <- plus-commutative (plus/s plus/z) TM1+ONE=TM1+1
    <- plus-respects-eq TM1+ONE=TM1+1 nat`eq/ nat`eq/ TM1+1=TM2+2 TM1+ONE=TM2+2
    <- times-commutative T1 T1c
    <- divrem-can-be-constructed T1c TM1+ONE=TM2+2 2>1 DR1
    <- divrem-deterministic DR2 DR1 nat`eq/ nat`eq/ QE ZERO=ONE
    <- nat`eq-contradiction ZERO=ONE F
    <- false-implies-eql F E.

%theorem tonat-one2one/L/eq :
	forall*	{N} {VN1} {VN2} {N1} {MS1} {MS2} {M} {F}
	forall	{FTN: {v:term N} (varlevel v (s VN1)) 
		       -> tonat* N1 MS1 (F v) M}
		{EQ: nat`eq VN1 VN2}
		{ME: multiset`eq MS1 MS2}
	exists	{FTN': {v:term N} (varlevel v (s VN2))
		       -> tonat* N1 MS2 (F v) M}
	true.

- : tonat-one2one/L/eq FTN nat`eq/ multiset`eq/ FTN.

%worlds (blocksimple | blockvar) (tonat-one2one/L/eq _ _ _ _).
%total { } (tonat-one2one/L/eq _ _ _ _).
%reduces F1 = F2 (tonat-one2one/L/eq F1 _ _ F2).

- : tonat-one2one/L (tonat/lam MC1 MC01 MA1 ([v] [vl] (F1 v vl)) T1 P1)
                    (tonat/lam MC2 MC02 MA2 ([v] [vl] (F2 v vl)) T2 P2)
                    nat`eq/ (eql/lam2 MC02 MA2 FE)
    <- count-deterministic MC1 MC2 multiset`eq/ nat`eq/ VN1=VN2
    <- plus-left-cancels P1 P2 VN1=VN2 nat`eq/ TM1=TM2
    <- times-left-cancels T1 T2 nat`eq/ TM1=TM2 M1=M2
    <- count-deterministic MC01 MC02 multiset`eq/ nat`eq/ ZN1=ZN2
    <- add-deterministic MA1 MA2 multiset`eq/ nat`eq/ MS1=MS2
    <- tonat-one2one/L/eq F1 ZN1=ZN2 MS1=MS2 F1'
    <- ({v} {vl:varlevel v (s ZN2)} 
        tonat-one2one/L (F1' v vl) (F2 v vl) M1=M2 (FE v vl)).

%abbrev 4>2 : nat`gt (s (s (s (s z)))) (s (s z)) 
	       = (gt/> gt/1).

- : tonat-one2one/L (tonat/lam MC1 _ _ _ T1 P1)
                    (tonat/rec MC2 _ _ T2 P2) nat`eq/ E
    <- count-deterministic MC2 MC1 multiset`eq/ nat`eq/ VN2=VN1
    <- plus-left-cancels P2 P1 VN2=VN1 nat`eq/ TM2+2=TM1
    <- times-commutative T1 T1c
    <- div-can-be-constructed T1c DR1
    <- plus-commutative (plus/s (plus/s plus/z)) TM2+TWO=TM2+2
    <- plus-respects-eq TM2+TWO=TM2+2 nat`eq/ nat`eq/ TM2+2=TM1 TM2+TWO=TM1
    <- times-commutative T2 T2c
    <- divrem-can-be-constructed T2c TM2+TWO=TM1 4>2 DR2
    <- divrem-deterministic DR1 DR2 nat`eq/ nat`eq/ QE ZERO=TWO
    <- nat`eq-contradiction ZERO=TWO F
    <- false-implies-eql F E.

- : tonat-one2one/L (tonat/rec MC2 _ _ T2 P2) 
                    (tonat/lam MC1 _ _ _ T1 P1) nat`eq/ E
    <- count-deterministic MC2 MC1 multiset`eq/ nat`eq/ VN2=VN1
    <- plus-left-cancels P2 P1 VN2=VN1 nat`eq/ TM2+2=TM1
    <- times-commutative T1 T1c
    <- div-can-be-constructed T1c DR1
    <- plus-commutative (plus/s (plus/s plus/z)) TM2+TWO=TM2+2
    <- plus-respects-eq TM2+TWO=TM2+2 nat`eq/ nat`eq/ TM2+2=TM1 TM2+TWO=TM1
    <- times-commutative T2 T2c
    <- divrem-can-be-constructed T2c TM2+TWO=TM1 4>2 DR2
    <- divrem-deterministic DR1 DR2 nat`eq/ nat`eq/ QE ZERO=TWO
    <- nat`eq-contradiction ZERO=TWO F
    <- false-implies-eql F E.

- : tonat-one2one/L (tonat/rec MC1 MA1 ([v] [vl] (F1 v vl)) T1 P1)
                    (tonat/rec MC2 MA2 ([v] [vl] (F2 v vl)) T2 P2)
                    nat`eq/ (eql/rec2 plus/z MC2 MA2 FE)
    <- count-deterministic MC1 MC2 multiset`eq/ nat`eq/ VN1=VN2
    <- plus-left-cancels P1 P2 VN1=VN2 nat`eq/ TM1+2=TM2+2
    <- succ-cancels TM1+2=TM2+2 TM1+1=TM2+1
    <- succ-cancels TM1+1=TM2+1 TM1=TM2
    <- times-left-cancels T1 T2 nat`eq/ TM1=TM2 M1=M2
    <- add-deterministic MA1 MA2 multiset`eq/ nat`eq/ MS1=MS2
    <- tonat-one2one/L/eq F1 VN1=VN2 MS1=MS2 F1'
    <- ({v} {vl:varlevel v (s VN2)} 
        tonat-one2one/L (F1' v vl) (F2 v vl) M1=M2 (FE v vl)).

%worlds (blockvar) (tonat-one2one/L _ _ _ _).
%total (T) (tonat-one2one/L T _ _ _).

- : tonat-one2one TN1 TN2 EQ TEQ
    <- tonat-one2one/L TN1 TN2 EQ EQL
    <- eql-implies-eq EQL TEQ.

%worlds () (tonat-one2one _ _ _ _).
%total { } (tonat-one2one _ _ _ _).