From da0f8fd05212d97395ca7a9e20bf78149e755d9e Mon Sep 17 00:00:00 2001 From: Matthew Yacavone Date: Thu, 25 Feb 2021 13:48:09 -0500 Subject: [PATCH] add iso-recursive types to Prelude.sawcore for GaloisInc/heapster-saw#74 --- .../generated/CryptolToCoq/SAWCorePrelude.v | 68 ++++++ saw-core/prelude/Prelude.sawcore | 206 ++++++++++++++++++ 2 files changed, 274 insertions(+) diff --git a/saw-core-coq/coq/generated/CryptolToCoq/SAWCorePrelude.v b/saw-core-coq/coq/generated/CryptolToCoq/SAWCorePrelude.v index fe3a843f..b2874e9b 100644 --- a/saw-core-coq/coq/generated/CryptolToCoq/SAWCorePrelude.v +++ b/saw-core-coq/coq/generated/CryptolToCoq/SAWCorePrelude.v @@ -920,6 +920,9 @@ Definition updSliceBVVec : forall (n : @SAWCoreScaffolding.Nat), forall (len : @ (* Prelude.Sigma_proj2 was skipped *) +Definition uncurrySigma : forall (a : Type), forall (b : a -> Type), forall (c : Type), (forall (pa : a), b pa -> c) -> @sigT a b -> c := + fun (a : Type) (b : a -> Type) (c : Type) => @sigT_rect a b (fun (_1 : @sigT a b) => c). + (* Prelude.List was skipped *) Definition List_def : forall (a : Type), Type := @@ -933,6 +936,20 @@ Definition unfoldList : forall (a : Type), @Datatypes.list a -> @Either unit (pr Definition foldList : forall (a : Type), @Either unit (prod a (prod (@Datatypes.list a) unit)) -> @Datatypes.list a := fun (a : Type) => @either unit (prod a (prod (@Datatypes.list a) unit)) (@Datatypes.list a) (fun (_1 : unit) => @Datatypes.nil a) (fun (tup : prod a (prod (@Datatypes.list a) unit)) => @Datatypes.cons a (SAWCoreScaffolding.fst tup) (SAWCoreScaffolding.fst (SAWCoreScaffolding.snd tup))). +Inductive ListSort : Type := +| LS_Nil : @ListSort +| LS_Cons : Type -> @ListSort -> @ListSort +. + +Definition ListSort__rec : forall (P : @ListSort -> Type), P (@LS_Nil) -> (forall (A : Type), forall (l : @ListSort), P l -> P (@LS_Cons A l)) -> forall (l : @ListSort), P l := + fun (P : @ListSort -> Type) (f1 : P (@LS_Nil)) (f2 : forall (A : Type), forall (l : @ListSort), P l -> P (@LS_Cons A l)) (l : @ListSort) => SAWCorePrelude.ListSort_rect P f1 f2 l. + +Definition listSortGet : @ListSort -> @SAWCoreScaffolding.Nat -> Type := + @ListSort__rec (fun (_1 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_1 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_1 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n : @SAWCoreScaffolding.Nat) (_2 : Type) => rec n)). + +Definition listSortDrop : @ListSort -> @SAWCoreScaffolding.Nat -> @ListSort := + @ListSort__rec (fun (_1 : @ListSort) => @SAWCoreScaffolding.Nat -> @ListSort) (fun (_1 : @SAWCoreScaffolding.Nat) => @LS_Nil) (fun (_1 : Type) (Ds : @ListSort) (rec : @SAWCoreScaffolding.Nat -> @ListSort) => @Nat_cases (@ListSort) Ds (fun (n : @SAWCoreScaffolding.Nat) (_2 : @ListSort) => rec n)). + Inductive W64List : Type := | W64Nil : @W64List | W64Cons : @bitvector 64 -> @W64List -> @W64List @@ -947,6 +964,57 @@ Definition unfoldW64List : @W64List -> @unfoldedW64List := Definition foldW64List : @unfoldedW64List -> @W64List := @either unit (prod (@sigT (@bitvector 64) (fun (_1 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit)) (prod (@W64List) unit)) (@W64List) (fun (_1 : unit) => @W64Nil) (fun (bv_l : prod (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (_1 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit)) (prod (@W64List) unit)) => @W64Cons (@projT1 (@bitvector 64) (fun (_1 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit) (SAWCoreScaffolding.fst bv_l)) (SAWCoreScaffolding.fst (SAWCoreScaffolding.snd bv_l))). +Inductive IRTDesc (As : @ListSort) : Type := +| IRT_varD : @SAWCoreScaffolding.Nat -> @IRTDesc As +| IRT_mu : @IRTDesc As -> @IRTDesc As +| IRT_Either : @IRTDesc As -> @IRTDesc As -> @IRTDesc As +| IRT_prod : @IRTDesc As -> @IRTDesc As -> @IRTDesc As +| IRT_sigT : forall (n : @SAWCoreScaffolding.Nat), (@listSortGet As n -> @IRTDesc As) -> @IRTDesc As +| IRT_unit : @IRTDesc As +| IRT_empty : @IRTDesc As +| IRT_varT : @SAWCoreScaffolding.Nat -> @IRTDesc As +. + +Definition IRTDesc__rec : forall (As : @ListSort), forall (P : @IRTDesc As -> Type), (forall (n : @SAWCoreScaffolding.Nat), P (@IRT_varD As n)) -> (forall (D : @IRTDesc As), P D -> P (@IRT_mu As D)) -> (forall (Dl : @IRTDesc As), P Dl -> forall (Dr : @IRTDesc As), P Dr -> P (@IRT_Either As Dl Dr)) -> (forall (Dl : @IRTDesc As), P Dl -> forall (Dr : @IRTDesc As), P Dr -> P (@IRT_prod As Dl Dr)) -> (forall (n : @SAWCoreScaffolding.Nat), forall (Df : @listSortGet As n -> @IRTDesc As), (forall (a : @listSortGet As n), P (Df a)) -> P (@IRT_sigT As n Df)) -> P (@IRT_unit As) -> P (@IRT_empty As) -> (forall (n : @SAWCoreScaffolding.Nat), P (@IRT_varT As n)) -> forall (D : @IRTDesc As), P D := + fun (As : @ListSort) (P : @IRTDesc As -> Type) (f1 : forall (n : @SAWCoreScaffolding.Nat), P (@IRT_varD As n)) (f2 : forall (D : @IRTDesc As), P D -> P (@IRT_mu As D)) (f3 : forall (Dl : @IRTDesc As), P Dl -> forall (Dr : @IRTDesc As), P Dr -> P (@IRT_Either As Dl Dr)) (f4 : forall (Dl : @IRTDesc As), P Dl -> forall (Dr : @IRTDesc As), P Dr -> P (@IRT_prod As Dl Dr)) (f5 : forall (n : @SAWCoreScaffolding.Nat), forall (Df : SAWCorePrelude.ListSort_rect (fun (_1 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_1 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_1 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n1 : @SAWCoreScaffolding.Nat) (_2 : Type) => rec n1)) As n -> @IRTDesc As), (forall (a : SAWCorePrelude.ListSort_rect (fun (_1 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_1 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_1 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n1 : @SAWCoreScaffolding.Nat) (_2 : Type) => rec n1)) As n), P (Df a)) -> P (@IRT_sigT As n Df)) (f6 : P (@IRT_unit As)) (f7 : P (@IRT_empty As)) (f8 : forall (n : @SAWCoreScaffolding.Nat), P (@IRT_varT As n)) (D : @IRTDesc As) => SAWCorePrelude.IRTDesc_rect As P f1 f2 f3 f4 f5 f6 f7 f8 D. + +Inductive IRTSubsts (As : @ListSort) : Type := +| IRTs_Nil : @IRTSubsts As +| IRTs_Cons : @IRTDesc As -> @IRTSubsts As -> @IRTSubsts As +. + +Definition IRTSubsts__rec : forall (As : @ListSort), forall (P : @IRTSubsts As -> Type), P (@IRTs_Nil As) -> (forall (D : @IRTDesc As), forall (Ds : @IRTSubsts As), P Ds -> P (@IRTs_Cons As D Ds)) -> forall (Ds : @IRTSubsts As), P Ds := + fun (As : @ListSort) (P : @IRTSubsts As -> Type) (f1 : P (@IRTs_Nil As)) (f2 : forall (D : @IRTDesc As), forall (Ds : @IRTSubsts As), P Ds -> P (@IRTs_Cons As D Ds)) (Ds : @IRTSubsts As) => SAWCorePrelude.IRTSubsts_rect As P f1 f2 Ds. + +Definition atIRTs : forall (As : @ListSort), @IRTSubsts As -> @SAWCoreScaffolding.Nat -> @IRTDesc As := + fun (As : @ListSort) => @IRTSubsts__rec As (fun (_1 : @IRTSubsts As) => @SAWCoreScaffolding.Nat -> @IRTDesc As) (fun (_1 : @SAWCoreScaffolding.Nat) => @IRT_empty As) (fun (D : @IRTDesc As) (_1 : @IRTSubsts As) (rec : @SAWCoreScaffolding.Nat -> @IRTDesc As) => @Nat_cases (@IRTDesc As) D (fun (n : @SAWCoreScaffolding.Nat) (_2 : @IRTDesc As) => rec n)). + +Definition dropIRTs : forall (As : @ListSort), @IRTSubsts As -> @SAWCoreScaffolding.Nat -> @IRTSubsts As := + fun (As : @ListSort) => @IRTSubsts__rec As (fun (_1 : @IRTSubsts As) => @SAWCoreScaffolding.Nat -> @IRTSubsts As) (fun (_1 : @SAWCoreScaffolding.Nat) => @IRTs_Nil As) (fun (_1 : @IRTDesc As) (Ds : @IRTSubsts As) (rec : @SAWCoreScaffolding.Nat -> @IRTSubsts As) => @Nat_cases (@IRTSubsts As) Ds (fun (n : @SAWCoreScaffolding.Nat) (_2 : @IRTSubsts As) => rec n)). + +Inductive IRT (As : @ListSort) : forall (_1 : @IRTSubsts As), forall (_2 : @IRTDesc As), Type := +| IRT_elemD : forall (Ds : @IRTSubsts As), forall (n : @SAWCoreScaffolding.Nat), @IRT As (@dropIRTs As Ds (@SAWCoreScaffolding.Succ n)) (@atIRTs As Ds n) -> @IRT As Ds (@IRT_varD As n) +| IRT_fold : forall (Ds : @IRTSubsts As), forall (D : @IRTDesc As), @IRT As (@IRTs_Cons As (@IRT_mu As D) Ds) D -> @IRT As Ds (@IRT_mu As D) +| IRT_Left : forall (Ds : @IRTSubsts As), forall (Dl : @IRTDesc As), forall (Dr : @IRTDesc As), @IRT As Ds Dl -> @IRT As Ds (@IRT_Either As Dl Dr) +| IRT_Right : forall (Ds : @IRTSubsts As), forall (Dl : @IRTDesc As), forall (Dr : @IRTDesc As), @IRT As Ds Dr -> @IRT As Ds (@IRT_Either As Dl Dr) +| IRT_pair : forall (Ds : @IRTSubsts As), forall (Dl : @IRTDesc As), forall (Dr : @IRTDesc As), @IRT As Ds Dl -> @IRT As Ds Dr -> @IRT As Ds (@IRT_prod As Dl Dr) +| IRT_existT : forall (Ds : @IRTSubsts As), forall (n : @SAWCoreScaffolding.Nat), forall (Df : @listSortGet As n -> @IRTDesc As), forall (a : @listSortGet As n), @IRT As Ds (Df a) -> @IRT As Ds (@IRT_sigT As n Df) +| IRT_tt : forall (Ds : @IRTSubsts As), @IRT As Ds (@IRT_unit As) +| IRT_elemT : forall (Ds : @IRTSubsts As), forall (n : @SAWCoreScaffolding.Nat), @listSortGet As n -> @IRT As Ds (@IRT_varT As n) +. + +Definition IRT__rec : forall (As : @ListSort), forall (P : forall (Ds : @IRTSubsts As), forall (D : @IRTDesc As), @IRT As Ds D -> Type), (forall (Ds : @IRTSubsts As), forall (n : @SAWCoreScaffolding.Nat), forall (x : @IRT As (@dropIRTs As Ds (@SAWCoreScaffolding.Succ n)) (@atIRTs As Ds n)), P (@dropIRTs As Ds (@SAWCoreScaffolding.Succ n)) (@atIRTs As Ds n) x -> P Ds (@IRT_varD As n) (@IRT_elemD As Ds n x)) -> (forall (Ds : @IRTSubsts As), forall (D : @IRTDesc As), forall (x : @IRT As (@IRTs_Cons As (@IRT_mu As D) Ds) D), P (@IRTs_Cons As (@IRT_mu As D) Ds) D x -> P Ds (@IRT_mu As D) (@IRT_fold As Ds D x)) -> (forall (Ds : @IRTSubsts As), forall (Dl : @IRTDesc As), forall (Dr : @IRTDesc As), forall (xl : @IRT As Ds Dl), P Ds Dl xl -> P Ds (@IRT_Either As Dl Dr) (@IRT_Left As Ds Dl Dr xl)) -> (forall (Ds : @IRTSubsts As), forall (Dl : @IRTDesc As), forall (Dr : @IRTDesc As), forall (xr : @IRT As Ds Dr), P Ds Dr xr -> P Ds (@IRT_Either As Dl Dr) (@IRT_Right As Ds Dl Dr xr)) -> (forall (Ds : @IRTSubsts As), forall (Dl : @IRTDesc As), forall (Dr : @IRTDesc As), forall (xl : @IRT As Ds Dl), P Ds Dl xl -> forall (xr : @IRT As Ds Dr), P Ds Dr xr -> P Ds (@IRT_prod As Dl Dr) (@IRT_pair As Ds Dl Dr xl xr)) -> (forall (Ds : @IRTSubsts As), forall (n : @SAWCoreScaffolding.Nat), forall (Df : @listSortGet As n -> @IRTDesc As), forall (a : @listSortGet As n), forall (xf : @IRT As Ds (Df a)), P Ds (Df a) xf -> P Ds (@IRT_sigT As n Df) (@IRT_existT As Ds n Df a xf)) -> (forall (Ds : @IRTSubsts As), P Ds (@IRT_unit As) (@IRT_tt As Ds)) -> (forall (Ds : @IRTSubsts As), forall (n : @SAWCoreScaffolding.Nat), forall (a : @listSortGet As n), P Ds (@IRT_varT As n) (@IRT_elemT As Ds n a)) -> forall (Ds : @IRTSubsts As), forall (D : @IRTDesc As), forall (x : @IRT As Ds D), P Ds D x := + fun (As : @ListSort) (P : forall (Ds : @IRTSubsts As), forall (D : @IRTDesc As), @IRT As Ds D -> Type) (f1 : forall (Ds : @IRTSubsts As), forall (n : @SAWCoreScaffolding.Nat), forall (x : @IRT As (SAWCorePrelude.IRTSubsts_rect As (fun (_1 : @IRTSubsts As) => @SAWCoreScaffolding.Nat -> @IRTSubsts As) (fun (_1 : @SAWCoreScaffolding.Nat) => @IRTs_Nil As) (fun (_1 : @IRTDesc As) (Ds1 : @IRTSubsts As) (rec : @SAWCoreScaffolding.Nat -> @IRTSubsts As) => @Nat_cases (@IRTSubsts As) Ds1 (fun (n1 : @SAWCoreScaffolding.Nat) (_2 : @IRTSubsts As) => rec n1)) Ds (@SAWCoreScaffolding.Succ n)) (SAWCorePrelude.IRTSubsts_rect As (fun (_1 : @IRTSubsts As) => @SAWCoreScaffolding.Nat -> @IRTDesc As) (fun (_1 : @SAWCoreScaffolding.Nat) => @IRT_empty As) (fun (D : @IRTDesc As) (_1 : @IRTSubsts As) (rec : @SAWCoreScaffolding.Nat -> @IRTDesc As) => @Nat_cases (@IRTDesc As) D (fun (n1 : @SAWCoreScaffolding.Nat) (_2 : @IRTDesc As) => rec n1)) Ds n)), P (@dropIRTs As Ds (@SAWCoreScaffolding.Succ n)) (@atIRTs As Ds n) x -> P Ds (@IRT_varD As n) (@IRT_elemD As Ds n x)) (f2 : forall (Ds : @IRTSubsts As), forall (D : @IRTDesc As), forall (x : @IRT As (@IRTs_Cons As (@IRT_mu As D) Ds) D), P (@IRTs_Cons As (@IRT_mu As D) Ds) D x -> P Ds (@IRT_mu As D) (@IRT_fold As Ds D x)) (f3 : forall (Ds : @IRTSubsts As), forall (Dl : @IRTDesc As), forall (Dr : @IRTDesc As), forall (xl : @IRT As Ds Dl), P Ds Dl xl -> P Ds (@IRT_Either As Dl Dr) (@IRT_Left As Ds Dl Dr xl)) (f4 : forall (Ds : @IRTSubsts As), forall (Dl : @IRTDesc As), forall (Dr : @IRTDesc As), forall (xr : @IRT As Ds Dr), P Ds Dr xr -> P Ds (@IRT_Either As Dl Dr) (@IRT_Right As Ds Dl Dr xr)) (f5 : forall (Ds : @IRTSubsts As), forall (Dl : @IRTDesc As), forall (Dr : @IRTDesc As), forall (xl : @IRT As Ds Dl), P Ds Dl xl -> forall (xr : @IRT As Ds Dr), P Ds Dr xr -> P Ds (@IRT_prod As Dl Dr) (@IRT_pair As Ds Dl Dr xl xr)) (f6 : forall (Ds : @IRTSubsts As), forall (n : @SAWCoreScaffolding.Nat), forall (Df : SAWCorePrelude.ListSort_rect (fun (_1 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_1 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_1 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n1 : @SAWCoreScaffolding.Nat) (_2 : Type) => rec n1)) As n -> @IRTDesc As), forall (a : SAWCorePrelude.ListSort_rect (fun (_1 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_1 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_1 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n1 : @SAWCoreScaffolding.Nat) (_2 : Type) => rec n1)) As n), forall (xf : @IRT As Ds (Df a)), P Ds (Df a) xf -> P Ds (@IRT_sigT As n Df) (@IRT_existT As Ds n Df a xf)) (f7 : forall (Ds : @IRTSubsts As), P Ds (@IRT_unit As) (@IRT_tt As Ds)) (f8 : forall (Ds : @IRTSubsts As), forall (n : @SAWCoreScaffolding.Nat), forall (a : SAWCorePrelude.ListSort_rect (fun (_1 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_1 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_1 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n1 : @SAWCoreScaffolding.Nat) (_2 : Type) => rec n1)) As n), P Ds (@IRT_varT As n) (@IRT_elemT As Ds n a)) (Ds : @IRTSubsts As) (D : @IRTDesc As) (x : @IRT As Ds D) => SAWCorePrelude.IRT_rect As P f1 f2 f3 f4 f5 f6 f7 f8 Ds D x. + +Definition UnfoldedIRT : forall (As : @ListSort), @IRTSubsts As -> @IRTDesc As -> Type := + fun (As : @ListSort) (Ds : @IRTSubsts As) (D : @IRTDesc As) => @IRTDesc__rec As (fun (_1 : @IRTDesc As) => @IRTSubsts As -> Type) (fun (n : @SAWCoreScaffolding.Nat) (Ds1 : @IRTSubsts As) => @IRT As (@dropIRTs As Ds1 (@SAWCoreScaffolding.Succ n)) (@atIRTs As Ds1 n)) (fun (D1 : @IRTDesc As) (rec : @IRTSubsts As -> Type) (Ds1 : @IRTSubsts As) => rec (@IRTs_Cons As (@IRT_mu As D1) Ds1)) (fun (_1 : @IRTDesc As) (recl : @IRTSubsts As -> Type) (_2 : @IRTDesc As) (recr : @IRTSubsts As -> Type) (Ds1 : @IRTSubsts As) => @Either (recl Ds1) (recr Ds1)) (fun (_1 : @IRTDesc As) (recl : @IRTSubsts As -> Type) (_2 : @IRTDesc As) (recr : @IRTSubsts As -> Type) (Ds1 : @IRTSubsts As) => prod (recl Ds1) (recr Ds1)) (fun (n : @SAWCoreScaffolding.Nat) (_1 : SAWCorePrelude.ListSort_rect (fun (_1 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_1 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_1 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n1 : @SAWCoreScaffolding.Nat) (_2 : Type) => rec n1)) As n -> @IRTDesc As) (recf : SAWCorePrelude.ListSort_rect (fun (_2 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_2 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_2 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n1 : @SAWCoreScaffolding.Nat) (_3 : Type) => rec n1)) As n -> @IRTSubsts As -> Type) (Ds1 : @IRTSubsts As) => @sigT (@listSortGet As n) (fun (a : SAWCorePrelude.ListSort_rect (fun (_2 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_2 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_2 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n1 : @SAWCoreScaffolding.Nat) (_3 : Type) => rec n1)) As n) => recf a Ds1)) (fun (_1 : @IRTSubsts As) => unit) (fun (_1 : @IRTSubsts As) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (n : @SAWCoreScaffolding.Nat) (_1 : @IRTSubsts As) => @listSortGet As n) D Ds. + +Definition unfoldIRT : forall (As : @ListSort), forall (Ds : @IRTSubsts As), forall (D : @IRTDesc As), @IRT As Ds D -> @UnfoldedIRT As Ds D := + fun (As : @ListSort) => @IRT__rec As (fun (Ds : @IRTSubsts As) (D : @IRTDesc As) (_1 : @IRT As Ds D) => @UnfoldedIRT As Ds D) (fun (Ds : @IRTSubsts As) (n : @SAWCoreScaffolding.Nat) (x : @IRT As (SAWCorePrelude.IRTSubsts_rect As (fun (_1 : @IRTSubsts As) => @SAWCoreScaffolding.Nat -> @IRTSubsts As) (fun (_1 : @SAWCoreScaffolding.Nat) => @IRTs_Nil As) (fun (_1 : @IRTDesc As) (Ds1 : @IRTSubsts As) (rec : @SAWCoreScaffolding.Nat -> @IRTSubsts As) => @Nat_cases (@IRTSubsts As) Ds1 (fun (n1 : @SAWCoreScaffolding.Nat) (_2 : @IRTSubsts As) => rec n1)) Ds (@SAWCoreScaffolding.Succ n)) (SAWCorePrelude.IRTSubsts_rect As (fun (_1 : @IRTSubsts As) => @SAWCoreScaffolding.Nat -> @IRTDesc As) (fun (_1 : @SAWCoreScaffolding.Nat) => @IRT_empty As) (fun (D : @IRTDesc As) (_1 : @IRTSubsts As) (rec : @SAWCoreScaffolding.Nat -> @IRTDesc As) => @Nat_cases (@IRTDesc As) D (fun (n1 : @SAWCoreScaffolding.Nat) (_2 : @IRTDesc As) => rec n1)) Ds n)) (_1 : SAWCorePrelude.IRTDesc_rect As (fun (_1 : @IRTDesc As) => @IRTSubsts As -> Type) (fun (n1 : @SAWCoreScaffolding.Nat) (Ds1 : @IRTSubsts As) => @IRT As (@dropIRTs As Ds1 (@SAWCoreScaffolding.Succ n1)) (@atIRTs As Ds1 n1)) (fun (D : @IRTDesc As) (rec : @IRTSubsts As -> Type) (Ds1 : @IRTSubsts As) => rec (@IRTs_Cons As (@IRT_mu As D) Ds1)) (fun (_1 : @IRTDesc As) (recl : @IRTSubsts As -> Type) (_2 : @IRTDesc As) (recr : @IRTSubsts As -> Type) (Ds1 : @IRTSubsts As) => @Either (recl Ds1) (recr Ds1)) (fun (_1 : @IRTDesc As) (recl : @IRTSubsts As -> Type) (_2 : @IRTDesc As) (recr : @IRTSubsts As -> Type) (Ds1 : @IRTSubsts As) => prod (recl Ds1) (recr Ds1)) (fun (n1 : @SAWCoreScaffolding.Nat) (_1 : SAWCorePrelude.ListSort_rect (fun (_1 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_1 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_1 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n2 : @SAWCoreScaffolding.Nat) (_2 : Type) => rec n2)) As n1 -> @IRTDesc As) (recf : SAWCorePrelude.ListSort_rect (fun (_2 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_2 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_2 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n2 : @SAWCoreScaffolding.Nat) (_3 : Type) => rec n2)) As n1 -> @IRTSubsts As -> Type) (Ds1 : @IRTSubsts As) => @sigT (@listSortGet As n1) (fun (a : SAWCorePrelude.ListSort_rect (fun (_2 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_2 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_2 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n2 : @SAWCoreScaffolding.Nat) (_3 : Type) => rec n2)) As n1) => recf a Ds1)) (fun (_1 : @IRTSubsts As) => unit) (fun (_1 : @IRTSubsts As) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (n1 : @SAWCoreScaffolding.Nat) (_1 : @IRTSubsts As) => @listSortGet As n1) (SAWCorePrelude.IRTSubsts_rect As (fun (_1 : @IRTSubsts As) => @SAWCoreScaffolding.Nat -> @IRTDesc As) (fun (_1 : @SAWCoreScaffolding.Nat) => @IRT_empty As) (fun (D : @IRTDesc As) (_1 : @IRTSubsts As) (rec : @SAWCoreScaffolding.Nat -> @IRTDesc As) => @Nat_cases (@IRTDesc As) D (fun (n1 : @SAWCoreScaffolding.Nat) (_2 : @IRTDesc As) => rec n1)) Ds n) (@dropIRTs As Ds (@SAWCoreScaffolding.Succ n))) => x) (fun (Ds : @IRTSubsts As) (D : @IRTDesc As) (_1 : @IRT As (@IRTs_Cons As (@IRT_mu As D) Ds) D) (rec : SAWCorePrelude.IRTDesc_rect As (fun (_2 : @IRTDesc As) => @IRTSubsts As -> Type) (fun (n : @SAWCoreScaffolding.Nat) (Ds1 : @IRTSubsts As) => @IRT As (@dropIRTs As Ds1 (@SAWCoreScaffolding.Succ n)) (@atIRTs As Ds1 n)) (fun (D1 : @IRTDesc As) (rec : @IRTSubsts As -> Type) (Ds1 : @IRTSubsts As) => rec (@IRTs_Cons As (@IRT_mu As D1) Ds1)) (fun (_2 : @IRTDesc As) (recl : @IRTSubsts As -> Type) (_3 : @IRTDesc As) (recr : @IRTSubsts As -> Type) (Ds1 : @IRTSubsts As) => @Either (recl Ds1) (recr Ds1)) (fun (_2 : @IRTDesc As) (recl : @IRTSubsts As -> Type) (_3 : @IRTDesc As) (recr : @IRTSubsts As -> Type) (Ds1 : @IRTSubsts As) => prod (recl Ds1) (recr Ds1)) (fun (n : @SAWCoreScaffolding.Nat) (_2 : SAWCorePrelude.ListSort_rect (fun (_2 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_2 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_2 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n1 : @SAWCoreScaffolding.Nat) (_3 : Type) => rec n1)) As n -> @IRTDesc As) (recf : SAWCorePrelude.ListSort_rect (fun (_3 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_3 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_3 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n1 : @SAWCoreScaffolding.Nat) (_4 : Type) => rec n1)) As n -> @IRTSubsts As -> Type) (Ds1 : @IRTSubsts As) => @sigT (@listSortGet As n) (fun (a : SAWCorePrelude.ListSort_rect (fun (_3 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_3 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_3 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n1 : @SAWCoreScaffolding.Nat) (_4 : Type) => rec n1)) As n) => recf a Ds1)) (fun (_2 : @IRTSubsts As) => unit) (fun (_2 : @IRTSubsts As) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (n : @SAWCoreScaffolding.Nat) (_2 : @IRTSubsts As) => @listSortGet As n) D (@IRTs_Cons As (@IRT_mu As D) Ds)) => rec) (fun (Ds : @IRTSubsts As) (Dl : @IRTDesc As) (Dr : @IRTDesc As) (_1 : @IRT As Ds Dl) (recl : SAWCorePrelude.IRTDesc_rect As (fun (_2 : @IRTDesc As) => @IRTSubsts As -> Type) (fun (n : @SAWCoreScaffolding.Nat) (Ds1 : @IRTSubsts As) => @IRT As (@dropIRTs As Ds1 (@SAWCoreScaffolding.Succ n)) (@atIRTs As Ds1 n)) (fun (D : @IRTDesc As) (rec : @IRTSubsts As -> Type) (Ds1 : @IRTSubsts As) => rec (@IRTs_Cons As (@IRT_mu As D) Ds1)) (fun (_2 : @IRTDesc As) (recl : @IRTSubsts As -> Type) (_3 : @IRTDesc As) (recr : @IRTSubsts As -> Type) (Ds1 : @IRTSubsts As) => @Either (recl Ds1) (recr Ds1)) (fun (_2 : @IRTDesc As) (recl : @IRTSubsts As -> Type) (_3 : @IRTDesc As) (recr : @IRTSubsts As -> Type) (Ds1 : @IRTSubsts As) => prod (recl Ds1) (recr Ds1)) (fun (n : @SAWCoreScaffolding.Nat) (_2 : SAWCorePrelude.ListSort_rect (fun (_2 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_2 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_2 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n1 : @SAWCoreScaffolding.Nat) (_3 : Type) => rec n1)) As n -> @IRTDesc As) (recf : SAWCorePrelude.ListSort_rect (fun (_3 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_3 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_3 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n1 : @SAWCoreScaffolding.Nat) (_4 : Type) => rec n1)) As n -> @IRTSubsts As -> Type) (Ds1 : @IRTSubsts As) => @sigT (@listSortGet As n) (fun (a : SAWCorePrelude.ListSort_rect (fun (_3 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_3 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_3 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n1 : @SAWCoreScaffolding.Nat) (_4 : Type) => rec n1)) As n) => recf a Ds1)) (fun (_2 : @IRTSubsts As) => unit) (fun (_2 : @IRTSubsts As) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (n : @SAWCoreScaffolding.Nat) (_2 : @IRTSubsts As) => @listSortGet As n) Dl Ds) => @Left (@UnfoldedIRT As Ds Dl) (@UnfoldedIRT As Ds Dr) recl) (fun (Ds : @IRTSubsts As) (Dl : @IRTDesc As) (Dr : @IRTDesc As) (_1 : @IRT As Ds Dr) (recr : SAWCorePrelude.IRTDesc_rect As (fun (_2 : @IRTDesc As) => @IRTSubsts As -> Type) (fun (n : @SAWCoreScaffolding.Nat) (Ds1 : @IRTSubsts As) => @IRT As (@dropIRTs As Ds1 (@SAWCoreScaffolding.Succ n)) (@atIRTs As Ds1 n)) (fun (D : @IRTDesc As) (rec : @IRTSubsts As -> Type) (Ds1 : @IRTSubsts As) => rec (@IRTs_Cons As (@IRT_mu As D) Ds1)) (fun (_2 : @IRTDesc As) (recl : @IRTSubsts As -> Type) (_3 : @IRTDesc As) (recr : @IRTSubsts As -> Type) (Ds1 : @IRTSubsts As) => @Either (recl Ds1) (recr Ds1)) (fun (_2 : @IRTDesc As) (recl : @IRTSubsts As -> Type) (_3 : @IRTDesc As) (recr : @IRTSubsts As -> Type) (Ds1 : @IRTSubsts As) => prod (recl Ds1) (recr Ds1)) (fun (n : @SAWCoreScaffolding.Nat) (_2 : SAWCorePrelude.ListSort_rect (fun (_2 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_2 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_2 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n1 : @SAWCoreScaffolding.Nat) (_3 : Type) => rec n1)) As n -> @IRTDesc As) (recf : SAWCorePrelude.ListSort_rect (fun (_3 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_3 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_3 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n1 : @SAWCoreScaffolding.Nat) (_4 : Type) => rec n1)) As n -> @IRTSubsts As -> Type) (Ds1 : @IRTSubsts As) => @sigT (@listSortGet As n) (fun (a : SAWCorePrelude.ListSort_rect (fun (_3 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_3 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_3 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n1 : @SAWCoreScaffolding.Nat) (_4 : Type) => rec n1)) As n) => recf a Ds1)) (fun (_2 : @IRTSubsts As) => unit) (fun (_2 : @IRTSubsts As) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (n : @SAWCoreScaffolding.Nat) (_2 : @IRTSubsts As) => @listSortGet As n) Dr Ds) => @Right (@UnfoldedIRT As Ds Dl) (@UnfoldedIRT As Ds Dr) recr) (fun (Ds : @IRTSubsts As) (Dl : @IRTDesc As) (Dr : @IRTDesc As) (_1 : @IRT As Ds Dl) (recl : SAWCorePrelude.IRTDesc_rect As (fun (_2 : @IRTDesc As) => @IRTSubsts As -> Type) (fun (n : @SAWCoreScaffolding.Nat) (Ds1 : @IRTSubsts As) => @IRT As (@dropIRTs As Ds1 (@SAWCoreScaffolding.Succ n)) (@atIRTs As Ds1 n)) (fun (D : @IRTDesc As) (rec : @IRTSubsts As -> Type) (Ds1 : @IRTSubsts As) => rec (@IRTs_Cons As (@IRT_mu As D) Ds1)) (fun (_2 : @IRTDesc As) (recl : @IRTSubsts As -> Type) (_3 : @IRTDesc As) (recr : @IRTSubsts As -> Type) (Ds1 : @IRTSubsts As) => @Either (recl Ds1) (recr Ds1)) (fun (_2 : @IRTDesc As) (recl : @IRTSubsts As -> Type) (_3 : @IRTDesc As) (recr : @IRTSubsts As -> Type) (Ds1 : @IRTSubsts As) => prod (recl Ds1) (recr Ds1)) (fun (n : @SAWCoreScaffolding.Nat) (_2 : SAWCorePrelude.ListSort_rect (fun (_2 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_2 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_2 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n1 : @SAWCoreScaffolding.Nat) (_3 : Type) => rec n1)) As n -> @IRTDesc As) (recf : SAWCorePrelude.ListSort_rect (fun (_3 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_3 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_3 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n1 : @SAWCoreScaffolding.Nat) (_4 : Type) => rec n1)) As n -> @IRTSubsts As -> Type) (Ds1 : @IRTSubsts As) => @sigT (@listSortGet As n) (fun (a : SAWCorePrelude.ListSort_rect (fun (_3 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_3 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_3 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n1 : @SAWCoreScaffolding.Nat) (_4 : Type) => rec n1)) As n) => recf a Ds1)) (fun (_2 : @IRTSubsts As) => unit) (fun (_2 : @IRTSubsts As) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (n : @SAWCoreScaffolding.Nat) (_2 : @IRTSubsts As) => @listSortGet As n) Dl Ds) (_2 : @IRT As Ds Dr) (recr : SAWCorePrelude.IRTDesc_rect As (fun (_3 : @IRTDesc As) => @IRTSubsts As -> Type) (fun (n : @SAWCoreScaffolding.Nat) (Ds1 : @IRTSubsts As) => @IRT As (@dropIRTs As Ds1 (@SAWCoreScaffolding.Succ n)) (@atIRTs As Ds1 n)) (fun (D : @IRTDesc As) (rec : @IRTSubsts As -> Type) (Ds1 : @IRTSubsts As) => rec (@IRTs_Cons As (@IRT_mu As D) Ds1)) (fun (_3 : @IRTDesc As) (recl1 : @IRTSubsts As -> Type) (_4 : @IRTDesc As) (recr : @IRTSubsts As -> Type) (Ds1 : @IRTSubsts As) => @Either (recl1 Ds1) (recr Ds1)) (fun (_3 : @IRTDesc As) (recl1 : @IRTSubsts As -> Type) (_4 : @IRTDesc As) (recr : @IRTSubsts As -> Type) (Ds1 : @IRTSubsts As) => prod (recl1 Ds1) (recr Ds1)) (fun (n : @SAWCoreScaffolding.Nat) (_3 : SAWCorePrelude.ListSort_rect (fun (_3 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_3 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_3 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n1 : @SAWCoreScaffolding.Nat) (_4 : Type) => rec n1)) As n -> @IRTDesc As) (recf : SAWCorePrelude.ListSort_rect (fun (_4 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_4 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_4 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n1 : @SAWCoreScaffolding.Nat) (_5 : Type) => rec n1)) As n -> @IRTSubsts As -> Type) (Ds1 : @IRTSubsts As) => @sigT (@listSortGet As n) (fun (a : SAWCorePrelude.ListSort_rect (fun (_4 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_4 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_4 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n1 : @SAWCoreScaffolding.Nat) (_5 : Type) => rec n1)) As n) => recf a Ds1)) (fun (_3 : @IRTSubsts As) => unit) (fun (_3 : @IRTSubsts As) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (n : @SAWCoreScaffolding.Nat) (_3 : @IRTSubsts As) => @listSortGet As n) Dr Ds) => pair recl recr) (fun (Ds : @IRTSubsts As) (n : @SAWCoreScaffolding.Nat) (Df : SAWCorePrelude.ListSort_rect (fun (_1 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_1 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_1 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n1 : @SAWCoreScaffolding.Nat) (_2 : Type) => rec n1)) As n -> @IRTDesc As) (a : SAWCorePrelude.ListSort_rect (fun (_1 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_1 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_1 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n1 : @SAWCoreScaffolding.Nat) (_2 : Type) => rec n1)) As n) (_1 : @IRT As Ds (Df a)) (recf : SAWCorePrelude.IRTDesc_rect As (fun (_2 : @IRTDesc As) => @IRTSubsts As -> Type) (fun (n1 : @SAWCoreScaffolding.Nat) (Ds1 : @IRTSubsts As) => @IRT As (@dropIRTs As Ds1 (@SAWCoreScaffolding.Succ n1)) (@atIRTs As Ds1 n1)) (fun (D : @IRTDesc As) (rec : @IRTSubsts As -> Type) (Ds1 : @IRTSubsts As) => rec (@IRTs_Cons As (@IRT_mu As D) Ds1)) (fun (_2 : @IRTDesc As) (recl : @IRTSubsts As -> Type) (_3 : @IRTDesc As) (recr : @IRTSubsts As -> Type) (Ds1 : @IRTSubsts As) => @Either (recl Ds1) (recr Ds1)) (fun (_2 : @IRTDesc As) (recl : @IRTSubsts As -> Type) (_3 : @IRTDesc As) (recr : @IRTSubsts As -> Type) (Ds1 : @IRTSubsts As) => prod (recl Ds1) (recr Ds1)) (fun (n1 : @SAWCoreScaffolding.Nat) (_2 : SAWCorePrelude.ListSort_rect (fun (_2 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_2 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_2 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n2 : @SAWCoreScaffolding.Nat) (_3 : Type) => rec n2)) As n1 -> @IRTDesc As) (recf : SAWCorePrelude.ListSort_rect (fun (_3 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_3 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_3 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n2 : @SAWCoreScaffolding.Nat) (_4 : Type) => rec n2)) As n1 -> @IRTSubsts As -> Type) (Ds1 : @IRTSubsts As) => @sigT (@listSortGet As n1) (fun (a1 : SAWCorePrelude.ListSort_rect (fun (_3 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_3 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_3 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n2 : @SAWCoreScaffolding.Nat) (_4 : Type) => rec n2)) As n1) => recf a1 Ds1)) (fun (_2 : @IRTSubsts As) => unit) (fun (_2 : @IRTSubsts As) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (n1 : @SAWCoreScaffolding.Nat) (_2 : @IRTSubsts As) => @listSortGet As n1) (Df a) Ds) => @existT (@listSortGet As n) (fun (a1 : SAWCorePrelude.ListSort_rect (fun (_2 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_2 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_2 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n1 : @SAWCoreScaffolding.Nat) (_3 : Type) => rec n1)) As n) => @UnfoldedIRT As Ds (Df a1)) a recf) (fun (Ds : @IRTSubsts As) => tt) (fun (Ds : @IRTSubsts As) (n : @SAWCoreScaffolding.Nat) (a : SAWCorePrelude.ListSort_rect (fun (_1 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_1 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_1 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n1 : @SAWCoreScaffolding.Nat) (_2 : Type) => rec n1)) As n) => a). + +Definition foldIRT : forall (As : @ListSort), forall (Ds : @IRTSubsts As), forall (D : @IRTDesc As), @UnfoldedIRT As Ds D -> @IRT As Ds D := + fun (As : @ListSort) (Ds : @IRTSubsts As) (D : @IRTDesc As) => @IRTDesc__rec As (fun (D1 : @IRTDesc As) => forall (Ds1 : @IRTSubsts As), @UnfoldedIRT As Ds1 D1 -> @IRT As Ds1 D1) (fun (n : @SAWCoreScaffolding.Nat) (Ds1 : @IRTSubsts As) (x : @IRT As (SAWCorePrelude.IRTSubsts_rect As (fun (_1 : @IRTSubsts As) => @SAWCoreScaffolding.Nat -> @IRTSubsts As) (fun (_1 : @SAWCoreScaffolding.Nat) => @IRTs_Nil As) (fun (_1 : @IRTDesc As) (Ds2 : @IRTSubsts As) (rec : @SAWCoreScaffolding.Nat -> @IRTSubsts As) => @Nat_cases (@IRTSubsts As) Ds2 (fun (n1 : @SAWCoreScaffolding.Nat) (_2 : @IRTSubsts As) => rec n1)) Ds1 (@SAWCoreScaffolding.Succ n)) (SAWCorePrelude.IRTSubsts_rect As (fun (_1 : @IRTSubsts As) => @SAWCoreScaffolding.Nat -> @IRTDesc As) (fun (_1 : @SAWCoreScaffolding.Nat) => @IRT_empty As) (fun (D1 : @IRTDesc As) (_1 : @IRTSubsts As) (rec : @SAWCoreScaffolding.Nat -> @IRTDesc As) => @Nat_cases (@IRTDesc As) D1 (fun (n1 : @SAWCoreScaffolding.Nat) (_2 : @IRTDesc As) => rec n1)) Ds1 n)) => @IRT_elemD As Ds1 n x) (fun (D1 : @IRTDesc As) (rec : forall (Ds1 : @IRTSubsts As), SAWCorePrelude.IRTDesc_rect As (fun (_1 : @IRTDesc As) => @IRTSubsts As -> Type) (fun (n : @SAWCoreScaffolding.Nat) (Ds2 : @IRTSubsts As) => @IRT As (@dropIRTs As Ds2 (@SAWCoreScaffolding.Succ n)) (@atIRTs As Ds2 n)) (fun (D2 : @IRTDesc As) (rec : @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => rec (@IRTs_Cons As (@IRT_mu As D2) Ds2)) (fun (_1 : @IRTDesc As) (recl : @IRTSubsts As -> Type) (_2 : @IRTDesc As) (recr : @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => @Either (recl Ds2) (recr Ds2)) (fun (_1 : @IRTDesc As) (recl : @IRTSubsts As -> Type) (_2 : @IRTDesc As) (recr : @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => prod (recl Ds2) (recr Ds2)) (fun (n : @SAWCoreScaffolding.Nat) (_1 : SAWCorePrelude.ListSort_rect (fun (_1 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_1 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_1 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n1 : @SAWCoreScaffolding.Nat) (_2 : Type) => rec n1)) As n -> @IRTDesc As) (recf : SAWCorePrelude.ListSort_rect (fun (_2 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_2 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_2 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n1 : @SAWCoreScaffolding.Nat) (_3 : Type) => rec n1)) As n -> @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => @sigT (@listSortGet As n) (fun (a : SAWCorePrelude.ListSort_rect (fun (_2 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_2 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_2 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n1 : @SAWCoreScaffolding.Nat) (_3 : Type) => rec n1)) As n) => recf a Ds2)) (fun (_1 : @IRTSubsts As) => unit) (fun (_1 : @IRTSubsts As) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (n : @SAWCoreScaffolding.Nat) (_1 : @IRTSubsts As) => @listSortGet As n) D1 Ds1 -> @IRT As Ds1 D1) (Ds1 : @IRTSubsts As) (x : SAWCorePrelude.IRTDesc_rect As (fun (_1 : @IRTDesc As) => @IRTSubsts As -> Type) (fun (n : @SAWCoreScaffolding.Nat) (Ds2 : @IRTSubsts As) => @IRT As (@dropIRTs As Ds2 (@SAWCoreScaffolding.Succ n)) (@atIRTs As Ds2 n)) (fun (D2 : @IRTDesc As) (rec1 : @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => rec1 (@IRTs_Cons As (@IRT_mu As D2) Ds2)) (fun (_1 : @IRTDesc As) (recl : @IRTSubsts As -> Type) (_2 : @IRTDesc As) (recr : @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => @Either (recl Ds2) (recr Ds2)) (fun (_1 : @IRTDesc As) (recl : @IRTSubsts As -> Type) (_2 : @IRTDesc As) (recr : @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => prod (recl Ds2) (recr Ds2)) (fun (n : @SAWCoreScaffolding.Nat) (_1 : SAWCorePrelude.ListSort_rect (fun (_1 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_1 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_1 : @ListSort) (rec1 : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n1 : @SAWCoreScaffolding.Nat) (_2 : Type) => rec1 n1)) As n -> @IRTDesc As) (recf : SAWCorePrelude.ListSort_rect (fun (_2 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_2 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_2 : @ListSort) (rec1 : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n1 : @SAWCoreScaffolding.Nat) (_3 : Type) => rec1 n1)) As n -> @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => @sigT (@listSortGet As n) (fun (a : SAWCorePrelude.ListSort_rect (fun (_2 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_2 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_2 : @ListSort) (rec1 : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n1 : @SAWCoreScaffolding.Nat) (_3 : Type) => rec1 n1)) As n) => recf a Ds2)) (fun (_1 : @IRTSubsts As) => unit) (fun (_1 : @IRTSubsts As) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (n : @SAWCoreScaffolding.Nat) (_1 : @IRTSubsts As) => @listSortGet As n) D1 (@IRTs_Cons As (@IRT_mu As D1) Ds1)) => @IRT_fold As Ds1 D1 (rec (@IRTs_Cons As (@IRT_mu As D1) Ds1) x)) (fun (Dl : @IRTDesc As) (recl : forall (Ds1 : @IRTSubsts As), SAWCorePrelude.IRTDesc_rect As (fun (_1 : @IRTDesc As) => @IRTSubsts As -> Type) (fun (n : @SAWCoreScaffolding.Nat) (Ds2 : @IRTSubsts As) => @IRT As (@dropIRTs As Ds2 (@SAWCoreScaffolding.Succ n)) (@atIRTs As Ds2 n)) (fun (D1 : @IRTDesc As) (rec : @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => rec (@IRTs_Cons As (@IRT_mu As D1) Ds2)) (fun (_1 : @IRTDesc As) (recl : @IRTSubsts As -> Type) (_2 : @IRTDesc As) (recr : @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => @Either (recl Ds2) (recr Ds2)) (fun (_1 : @IRTDesc As) (recl : @IRTSubsts As -> Type) (_2 : @IRTDesc As) (recr : @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => prod (recl Ds2) (recr Ds2)) (fun (n : @SAWCoreScaffolding.Nat) (_1 : SAWCorePrelude.ListSort_rect (fun (_1 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_1 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_1 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n1 : @SAWCoreScaffolding.Nat) (_2 : Type) => rec n1)) As n -> @IRTDesc As) (recf : SAWCorePrelude.ListSort_rect (fun (_2 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_2 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_2 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n1 : @SAWCoreScaffolding.Nat) (_3 : Type) => rec n1)) As n -> @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => @sigT (@listSortGet As n) (fun (a : SAWCorePrelude.ListSort_rect (fun (_2 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_2 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_2 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n1 : @SAWCoreScaffolding.Nat) (_3 : Type) => rec n1)) As n) => recf a Ds2)) (fun (_1 : @IRTSubsts As) => unit) (fun (_1 : @IRTSubsts As) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (n : @SAWCoreScaffolding.Nat) (_1 : @IRTSubsts As) => @listSortGet As n) Dl Ds1 -> @IRT As Ds1 Dl) (Dr : @IRTDesc As) (recr : forall (Ds1 : @IRTSubsts As), SAWCorePrelude.IRTDesc_rect As (fun (_1 : @IRTDesc As) => @IRTSubsts As -> Type) (fun (n : @SAWCoreScaffolding.Nat) (Ds2 : @IRTSubsts As) => @IRT As (@dropIRTs As Ds2 (@SAWCoreScaffolding.Succ n)) (@atIRTs As Ds2 n)) (fun (D1 : @IRTDesc As) (rec : @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => rec (@IRTs_Cons As (@IRT_mu As D1) Ds2)) (fun (_1 : @IRTDesc As) (recl1 : @IRTSubsts As -> Type) (_2 : @IRTDesc As) (recr : @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => @Either (recl1 Ds2) (recr Ds2)) (fun (_1 : @IRTDesc As) (recl1 : @IRTSubsts As -> Type) (_2 : @IRTDesc As) (recr : @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => prod (recl1 Ds2) (recr Ds2)) (fun (n : @SAWCoreScaffolding.Nat) (_1 : SAWCorePrelude.ListSort_rect (fun (_1 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_1 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_1 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n1 : @SAWCoreScaffolding.Nat) (_2 : Type) => rec n1)) As n -> @IRTDesc As) (recf : SAWCorePrelude.ListSort_rect (fun (_2 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_2 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_2 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n1 : @SAWCoreScaffolding.Nat) (_3 : Type) => rec n1)) As n -> @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => @sigT (@listSortGet As n) (fun (a : SAWCorePrelude.ListSort_rect (fun (_2 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_2 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_2 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n1 : @SAWCoreScaffolding.Nat) (_3 : Type) => rec n1)) As n) => recf a Ds2)) (fun (_1 : @IRTSubsts As) => unit) (fun (_1 : @IRTSubsts As) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (n : @SAWCoreScaffolding.Nat) (_1 : @IRTSubsts As) => @listSortGet As n) Dr Ds1 -> @IRT As Ds1 Dr) (Ds1 : @IRTSubsts As) (x : @Either (SAWCorePrelude.IRTDesc_rect As (fun (_1 : @IRTDesc As) => @IRTSubsts As -> Type) (fun (n : @SAWCoreScaffolding.Nat) (Ds2 : @IRTSubsts As) => @IRT As (@dropIRTs As Ds2 (@SAWCoreScaffolding.Succ n)) (@atIRTs As Ds2 n)) (fun (D1 : @IRTDesc As) (rec : @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => rec (@IRTs_Cons As (@IRT_mu As D1) Ds2)) (fun (_1 : @IRTDesc As) (recl1 : @IRTSubsts As -> Type) (_2 : @IRTDesc As) (recr1 : @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => @Either (recl1 Ds2) (recr1 Ds2)) (fun (_1 : @IRTDesc As) (recl1 : @IRTSubsts As -> Type) (_2 : @IRTDesc As) (recr1 : @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => prod (recl1 Ds2) (recr1 Ds2)) (fun (n : @SAWCoreScaffolding.Nat) (_1 : SAWCorePrelude.ListSort_rect (fun (_1 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_1 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_1 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n1 : @SAWCoreScaffolding.Nat) (_2 : Type) => rec n1)) As n -> @IRTDesc As) (recf : SAWCorePrelude.ListSort_rect (fun (_2 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_2 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_2 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n1 : @SAWCoreScaffolding.Nat) (_3 : Type) => rec n1)) As n -> @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => @sigT (@listSortGet As n) (fun (a : SAWCorePrelude.ListSort_rect (fun (_2 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_2 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_2 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n1 : @SAWCoreScaffolding.Nat) (_3 : Type) => rec n1)) As n) => recf a Ds2)) (fun (_1 : @IRTSubsts As) => unit) (fun (_1 : @IRTSubsts As) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (n : @SAWCoreScaffolding.Nat) (_1 : @IRTSubsts As) => @listSortGet As n) Dl Ds1) (SAWCorePrelude.IRTDesc_rect As (fun (_1 : @IRTDesc As) => @IRTSubsts As -> Type) (fun (n : @SAWCoreScaffolding.Nat) (Ds2 : @IRTSubsts As) => @IRT As (@dropIRTs As Ds2 (@SAWCoreScaffolding.Succ n)) (@atIRTs As Ds2 n)) (fun (D1 : @IRTDesc As) (rec : @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => rec (@IRTs_Cons As (@IRT_mu As D1) Ds2)) (fun (_1 : @IRTDesc As) (recl1 : @IRTSubsts As -> Type) (_2 : @IRTDesc As) (recr1 : @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => @Either (recl1 Ds2) (recr1 Ds2)) (fun (_1 : @IRTDesc As) (recl1 : @IRTSubsts As -> Type) (_2 : @IRTDesc As) (recr1 : @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => prod (recl1 Ds2) (recr1 Ds2)) (fun (n : @SAWCoreScaffolding.Nat) (_1 : SAWCorePrelude.ListSort_rect (fun (_1 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_1 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_1 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n1 : @SAWCoreScaffolding.Nat) (_2 : Type) => rec n1)) As n -> @IRTDesc As) (recf : SAWCorePrelude.ListSort_rect (fun (_2 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_2 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_2 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n1 : @SAWCoreScaffolding.Nat) (_3 : Type) => rec n1)) As n -> @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => @sigT (@listSortGet As n) (fun (a : SAWCorePrelude.ListSort_rect (fun (_2 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_2 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_2 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n1 : @SAWCoreScaffolding.Nat) (_3 : Type) => rec n1)) As n) => recf a Ds2)) (fun (_1 : @IRTSubsts As) => unit) (fun (_1 : @IRTSubsts As) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (n : @SAWCoreScaffolding.Nat) (_1 : @IRTSubsts As) => @listSortGet As n) Dr Ds1)) => @either (@UnfoldedIRT As Ds1 Dl) (@UnfoldedIRT As Ds1 Dr) (@IRT As Ds1 (@IRT_Either As Dl Dr)) (fun (xl : SAWCorePrelude.IRTDesc_rect As (fun (_1 : @IRTDesc As) => @IRTSubsts As -> Type) (fun (n : @SAWCoreScaffolding.Nat) (Ds2 : @IRTSubsts As) => @IRT As (@dropIRTs As Ds2 (@SAWCoreScaffolding.Succ n)) (@atIRTs As Ds2 n)) (fun (D1 : @IRTDesc As) (rec : @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => rec (@IRTs_Cons As (@IRT_mu As D1) Ds2)) (fun (_1 : @IRTDesc As) (recl1 : @IRTSubsts As -> Type) (_2 : @IRTDesc As) (recr1 : @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => @Either (recl1 Ds2) (recr1 Ds2)) (fun (_1 : @IRTDesc As) (recl1 : @IRTSubsts As -> Type) (_2 : @IRTDesc As) (recr1 : @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => prod (recl1 Ds2) (recr1 Ds2)) (fun (n : @SAWCoreScaffolding.Nat) (_1 : SAWCorePrelude.ListSort_rect (fun (_1 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_1 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_1 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n1 : @SAWCoreScaffolding.Nat) (_2 : Type) => rec n1)) As n -> @IRTDesc As) (recf : SAWCorePrelude.ListSort_rect (fun (_2 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_2 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_2 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n1 : @SAWCoreScaffolding.Nat) (_3 : Type) => rec n1)) As n -> @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => @sigT (@listSortGet As n) (fun (a : SAWCorePrelude.ListSort_rect (fun (_2 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_2 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_2 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n1 : @SAWCoreScaffolding.Nat) (_3 : Type) => rec n1)) As n) => recf a Ds2)) (fun (_1 : @IRTSubsts As) => unit) (fun (_1 : @IRTSubsts As) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (n : @SAWCoreScaffolding.Nat) (_1 : @IRTSubsts As) => @listSortGet As n) Dl Ds1) => @IRT_Left As Ds1 Dl Dr (recl Ds1 xl)) (fun (xr : SAWCorePrelude.IRTDesc_rect As (fun (_1 : @IRTDesc As) => @IRTSubsts As -> Type) (fun (n : @SAWCoreScaffolding.Nat) (Ds2 : @IRTSubsts As) => @IRT As (@dropIRTs As Ds2 (@SAWCoreScaffolding.Succ n)) (@atIRTs As Ds2 n)) (fun (D1 : @IRTDesc As) (rec : @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => rec (@IRTs_Cons As (@IRT_mu As D1) Ds2)) (fun (_1 : @IRTDesc As) (recl1 : @IRTSubsts As -> Type) (_2 : @IRTDesc As) (recr1 : @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => @Either (recl1 Ds2) (recr1 Ds2)) (fun (_1 : @IRTDesc As) (recl1 : @IRTSubsts As -> Type) (_2 : @IRTDesc As) (recr1 : @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => prod (recl1 Ds2) (recr1 Ds2)) (fun (n : @SAWCoreScaffolding.Nat) (_1 : SAWCorePrelude.ListSort_rect (fun (_1 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_1 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_1 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n1 : @SAWCoreScaffolding.Nat) (_2 : Type) => rec n1)) As n -> @IRTDesc As) (recf : SAWCorePrelude.ListSort_rect (fun (_2 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_2 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_2 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n1 : @SAWCoreScaffolding.Nat) (_3 : Type) => rec n1)) As n -> @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => @sigT (@listSortGet As n) (fun (a : SAWCorePrelude.ListSort_rect (fun (_2 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_2 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_2 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n1 : @SAWCoreScaffolding.Nat) (_3 : Type) => rec n1)) As n) => recf a Ds2)) (fun (_1 : @IRTSubsts As) => unit) (fun (_1 : @IRTSubsts As) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (n : @SAWCoreScaffolding.Nat) (_1 : @IRTSubsts As) => @listSortGet As n) Dr Ds1) => @IRT_Right As Ds1 Dl Dr (recr Ds1 xr)) x) (fun (Dl : @IRTDesc As) (recl : forall (Ds1 : @IRTSubsts As), SAWCorePrelude.IRTDesc_rect As (fun (_1 : @IRTDesc As) => @IRTSubsts As -> Type) (fun (n : @SAWCoreScaffolding.Nat) (Ds2 : @IRTSubsts As) => @IRT As (@dropIRTs As Ds2 (@SAWCoreScaffolding.Succ n)) (@atIRTs As Ds2 n)) (fun (D1 : @IRTDesc As) (rec : @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => rec (@IRTs_Cons As (@IRT_mu As D1) Ds2)) (fun (_1 : @IRTDesc As) (recl : @IRTSubsts As -> Type) (_2 : @IRTDesc As) (recr : @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => @Either (recl Ds2) (recr Ds2)) (fun (_1 : @IRTDesc As) (recl : @IRTSubsts As -> Type) (_2 : @IRTDesc As) (recr : @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => prod (recl Ds2) (recr Ds2)) (fun (n : @SAWCoreScaffolding.Nat) (_1 : SAWCorePrelude.ListSort_rect (fun (_1 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_1 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_1 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n1 : @SAWCoreScaffolding.Nat) (_2 : Type) => rec n1)) As n -> @IRTDesc As) (recf : SAWCorePrelude.ListSort_rect (fun (_2 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_2 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_2 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n1 : @SAWCoreScaffolding.Nat) (_3 : Type) => rec n1)) As n -> @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => @sigT (@listSortGet As n) (fun (a : SAWCorePrelude.ListSort_rect (fun (_2 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_2 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_2 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n1 : @SAWCoreScaffolding.Nat) (_3 : Type) => rec n1)) As n) => recf a Ds2)) (fun (_1 : @IRTSubsts As) => unit) (fun (_1 : @IRTSubsts As) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (n : @SAWCoreScaffolding.Nat) (_1 : @IRTSubsts As) => @listSortGet As n) Dl Ds1 -> @IRT As Ds1 Dl) (Dr : @IRTDesc As) (recr : forall (Ds1 : @IRTSubsts As), SAWCorePrelude.IRTDesc_rect As (fun (_1 : @IRTDesc As) => @IRTSubsts As -> Type) (fun (n : @SAWCoreScaffolding.Nat) (Ds2 : @IRTSubsts As) => @IRT As (@dropIRTs As Ds2 (@SAWCoreScaffolding.Succ n)) (@atIRTs As Ds2 n)) (fun (D1 : @IRTDesc As) (rec : @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => rec (@IRTs_Cons As (@IRT_mu As D1) Ds2)) (fun (_1 : @IRTDesc As) (recl1 : @IRTSubsts As -> Type) (_2 : @IRTDesc As) (recr : @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => @Either (recl1 Ds2) (recr Ds2)) (fun (_1 : @IRTDesc As) (recl1 : @IRTSubsts As -> Type) (_2 : @IRTDesc As) (recr : @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => prod (recl1 Ds2) (recr Ds2)) (fun (n : @SAWCoreScaffolding.Nat) (_1 : SAWCorePrelude.ListSort_rect (fun (_1 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_1 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_1 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n1 : @SAWCoreScaffolding.Nat) (_2 : Type) => rec n1)) As n -> @IRTDesc As) (recf : SAWCorePrelude.ListSort_rect (fun (_2 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_2 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_2 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n1 : @SAWCoreScaffolding.Nat) (_3 : Type) => rec n1)) As n -> @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => @sigT (@listSortGet As n) (fun (a : SAWCorePrelude.ListSort_rect (fun (_2 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_2 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_2 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n1 : @SAWCoreScaffolding.Nat) (_3 : Type) => rec n1)) As n) => recf a Ds2)) (fun (_1 : @IRTSubsts As) => unit) (fun (_1 : @IRTSubsts As) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (n : @SAWCoreScaffolding.Nat) (_1 : @IRTSubsts As) => @listSortGet As n) Dr Ds1 -> @IRT As Ds1 Dr) (Ds1 : @IRTSubsts As) (x : prod (SAWCorePrelude.IRTDesc_rect As (fun (_1 : @IRTDesc As) => @IRTSubsts As -> Type) (fun (n : @SAWCoreScaffolding.Nat) (Ds2 : @IRTSubsts As) => @IRT As (@dropIRTs As Ds2 (@SAWCoreScaffolding.Succ n)) (@atIRTs As Ds2 n)) (fun (D1 : @IRTDesc As) (rec : @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => rec (@IRTs_Cons As (@IRT_mu As D1) Ds2)) (fun (_1 : @IRTDesc As) (recl1 : @IRTSubsts As -> Type) (_2 : @IRTDesc As) (recr1 : @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => @Either (recl1 Ds2) (recr1 Ds2)) (fun (_1 : @IRTDesc As) (recl1 : @IRTSubsts As -> Type) (_2 : @IRTDesc As) (recr1 : @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => prod (recl1 Ds2) (recr1 Ds2)) (fun (n : @SAWCoreScaffolding.Nat) (_1 : SAWCorePrelude.ListSort_rect (fun (_1 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_1 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_1 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n1 : @SAWCoreScaffolding.Nat) (_2 : Type) => rec n1)) As n -> @IRTDesc As) (recf : SAWCorePrelude.ListSort_rect (fun (_2 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_2 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_2 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n1 : @SAWCoreScaffolding.Nat) (_3 : Type) => rec n1)) As n -> @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => @sigT (@listSortGet As n) (fun (a : SAWCorePrelude.ListSort_rect (fun (_2 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_2 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_2 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n1 : @SAWCoreScaffolding.Nat) (_3 : Type) => rec n1)) As n) => recf a Ds2)) (fun (_1 : @IRTSubsts As) => unit) (fun (_1 : @IRTSubsts As) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (n : @SAWCoreScaffolding.Nat) (_1 : @IRTSubsts As) => @listSortGet As n) Dl Ds1) (SAWCorePrelude.IRTDesc_rect As (fun (_1 : @IRTDesc As) => @IRTSubsts As -> Type) (fun (n : @SAWCoreScaffolding.Nat) (Ds2 : @IRTSubsts As) => @IRT As (@dropIRTs As Ds2 (@SAWCoreScaffolding.Succ n)) (@atIRTs As Ds2 n)) (fun (D1 : @IRTDesc As) (rec : @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => rec (@IRTs_Cons As (@IRT_mu As D1) Ds2)) (fun (_1 : @IRTDesc As) (recl1 : @IRTSubsts As -> Type) (_2 : @IRTDesc As) (recr1 : @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => @Either (recl1 Ds2) (recr1 Ds2)) (fun (_1 : @IRTDesc As) (recl1 : @IRTSubsts As -> Type) (_2 : @IRTDesc As) (recr1 : @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => prod (recl1 Ds2) (recr1 Ds2)) (fun (n : @SAWCoreScaffolding.Nat) (_1 : SAWCorePrelude.ListSort_rect (fun (_1 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_1 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_1 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n1 : @SAWCoreScaffolding.Nat) (_2 : Type) => rec n1)) As n -> @IRTDesc As) (recf : SAWCorePrelude.ListSort_rect (fun (_2 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_2 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_2 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n1 : @SAWCoreScaffolding.Nat) (_3 : Type) => rec n1)) As n -> @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => @sigT (@listSortGet As n) (fun (a : SAWCorePrelude.ListSort_rect (fun (_2 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_2 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_2 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n1 : @SAWCoreScaffolding.Nat) (_3 : Type) => rec n1)) As n) => recf a Ds2)) (fun (_1 : @IRTSubsts As) => unit) (fun (_1 : @IRTSubsts As) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (n : @SAWCoreScaffolding.Nat) (_1 : @IRTSubsts As) => @listSortGet As n) Dr Ds1)) => @uncurry (@UnfoldedIRT As Ds1 Dl) (@UnfoldedIRT As Ds1 Dr) (@IRT As Ds1 (@IRT_prod As Dl Dr)) (fun (xl : SAWCorePrelude.IRTDesc_rect As (fun (_1 : @IRTDesc As) => @IRTSubsts As -> Type) (fun (n : @SAWCoreScaffolding.Nat) (Ds2 : @IRTSubsts As) => @IRT As (@dropIRTs As Ds2 (@SAWCoreScaffolding.Succ n)) (@atIRTs As Ds2 n)) (fun (D1 : @IRTDesc As) (rec : @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => rec (@IRTs_Cons As (@IRT_mu As D1) Ds2)) (fun (_1 : @IRTDesc As) (recl1 : @IRTSubsts As -> Type) (_2 : @IRTDesc As) (recr1 : @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => @Either (recl1 Ds2) (recr1 Ds2)) (fun (_1 : @IRTDesc As) (recl1 : @IRTSubsts As -> Type) (_2 : @IRTDesc As) (recr1 : @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => prod (recl1 Ds2) (recr1 Ds2)) (fun (n : @SAWCoreScaffolding.Nat) (_1 : SAWCorePrelude.ListSort_rect (fun (_1 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_1 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_1 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n1 : @SAWCoreScaffolding.Nat) (_2 : Type) => rec n1)) As n -> @IRTDesc As) (recf : SAWCorePrelude.ListSort_rect (fun (_2 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_2 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_2 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n1 : @SAWCoreScaffolding.Nat) (_3 : Type) => rec n1)) As n -> @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => @sigT (@listSortGet As n) (fun (a : SAWCorePrelude.ListSort_rect (fun (_2 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_2 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_2 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n1 : @SAWCoreScaffolding.Nat) (_3 : Type) => rec n1)) As n) => recf a Ds2)) (fun (_1 : @IRTSubsts As) => unit) (fun (_1 : @IRTSubsts As) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (n : @SAWCoreScaffolding.Nat) (_1 : @IRTSubsts As) => @listSortGet As n) Dl Ds1) (xr : SAWCorePrelude.IRTDesc_rect As (fun (_1 : @IRTDesc As) => @IRTSubsts As -> Type) (fun (n : @SAWCoreScaffolding.Nat) (Ds2 : @IRTSubsts As) => @IRT As (@dropIRTs As Ds2 (@SAWCoreScaffolding.Succ n)) (@atIRTs As Ds2 n)) (fun (D1 : @IRTDesc As) (rec : @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => rec (@IRTs_Cons As (@IRT_mu As D1) Ds2)) (fun (_1 : @IRTDesc As) (recl1 : @IRTSubsts As -> Type) (_2 : @IRTDesc As) (recr1 : @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => @Either (recl1 Ds2) (recr1 Ds2)) (fun (_1 : @IRTDesc As) (recl1 : @IRTSubsts As -> Type) (_2 : @IRTDesc As) (recr1 : @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => prod (recl1 Ds2) (recr1 Ds2)) (fun (n : @SAWCoreScaffolding.Nat) (_1 : SAWCorePrelude.ListSort_rect (fun (_1 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_1 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_1 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n1 : @SAWCoreScaffolding.Nat) (_2 : Type) => rec n1)) As n -> @IRTDesc As) (recf : SAWCorePrelude.ListSort_rect (fun (_2 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_2 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_2 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n1 : @SAWCoreScaffolding.Nat) (_3 : Type) => rec n1)) As n -> @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => @sigT (@listSortGet As n) (fun (a : SAWCorePrelude.ListSort_rect (fun (_2 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_2 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_2 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n1 : @SAWCoreScaffolding.Nat) (_3 : Type) => rec n1)) As n) => recf a Ds2)) (fun (_1 : @IRTSubsts As) => unit) (fun (_1 : @IRTSubsts As) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (n : @SAWCoreScaffolding.Nat) (_1 : @IRTSubsts As) => @listSortGet As n) Dr Ds1) => @IRT_pair As Ds1 Dl Dr (recl Ds1 xl) (recr Ds1 xr)) x) (fun (n : @SAWCoreScaffolding.Nat) (Df : SAWCorePrelude.ListSort_rect (fun (_1 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_1 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_1 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n1 : @SAWCoreScaffolding.Nat) (_2 : Type) => rec n1)) As n -> @IRTDesc As) (recf : forall (a : SAWCorePrelude.ListSort_rect (fun (_1 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_1 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_1 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n1 : @SAWCoreScaffolding.Nat) (_2 : Type) => rec n1)) As n), forall (Ds1 : @IRTSubsts As), SAWCorePrelude.IRTDesc_rect As (fun (_1 : @IRTDesc As) => @IRTSubsts As -> Type) (fun (n1 : @SAWCoreScaffolding.Nat) (Ds2 : @IRTSubsts As) => @IRT As (@dropIRTs As Ds2 (@SAWCoreScaffolding.Succ n1)) (@atIRTs As Ds2 n1)) (fun (D1 : @IRTDesc As) (rec : @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => rec (@IRTs_Cons As (@IRT_mu As D1) Ds2)) (fun (_1 : @IRTDesc As) (recl : @IRTSubsts As -> Type) (_2 : @IRTDesc As) (recr : @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => @Either (recl Ds2) (recr Ds2)) (fun (_1 : @IRTDesc As) (recl : @IRTSubsts As -> Type) (_2 : @IRTDesc As) (recr : @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => prod (recl Ds2) (recr Ds2)) (fun (n1 : @SAWCoreScaffolding.Nat) (_1 : SAWCorePrelude.ListSort_rect (fun (_1 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_1 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_1 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n2 : @SAWCoreScaffolding.Nat) (_2 : Type) => rec n2)) As n1 -> @IRTDesc As) (recf : SAWCorePrelude.ListSort_rect (fun (_2 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_2 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_2 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n2 : @SAWCoreScaffolding.Nat) (_3 : Type) => rec n2)) As n1 -> @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => @sigT (@listSortGet As n1) (fun (a1 : SAWCorePrelude.ListSort_rect (fun (_2 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_2 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_2 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n2 : @SAWCoreScaffolding.Nat) (_3 : Type) => rec n2)) As n1) => recf a1 Ds2)) (fun (_1 : @IRTSubsts As) => unit) (fun (_1 : @IRTSubsts As) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (n1 : @SAWCoreScaffolding.Nat) (_1 : @IRTSubsts As) => @listSortGet As n1) (Df a) Ds1 -> @IRT As Ds1 (Df a)) (Ds1 : @IRTSubsts As) (x : @sigT (SAWCorePrelude.ListSort_rect (fun (_1 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_1 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_1 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n1 : @SAWCoreScaffolding.Nat) (_2 : Type) => rec n1)) As n) (fun (a : SAWCorePrelude.ListSort_rect (fun (_1 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_1 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_1 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n1 : @SAWCoreScaffolding.Nat) (_2 : Type) => rec n1)) As n) => @UnfoldedIRT As Ds1 (Df a))) => @uncurrySigma (@listSortGet As n) (fun (a : SAWCorePrelude.ListSort_rect (fun (_1 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_1 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_1 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n1 : @SAWCoreScaffolding.Nat) (_2 : Type) => rec n1)) As n) => @UnfoldedIRT As Ds1 (Df a)) (@IRT As Ds1 (@IRT_sigT As n Df)) (fun (a : SAWCorePrelude.ListSort_rect (fun (_1 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_1 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_1 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n1 : @SAWCoreScaffolding.Nat) (_2 : Type) => rec n1)) As n) (xf : SAWCorePrelude.IRTDesc_rect As (fun (_1 : @IRTDesc As) => @IRTSubsts As -> Type) (fun (n1 : @SAWCoreScaffolding.Nat) (Ds2 : @IRTSubsts As) => @IRT As (@dropIRTs As Ds2 (@SAWCoreScaffolding.Succ n1)) (@atIRTs As Ds2 n1)) (fun (D1 : @IRTDesc As) (rec : @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => rec (@IRTs_Cons As (@IRT_mu As D1) Ds2)) (fun (_1 : @IRTDesc As) (recl : @IRTSubsts As -> Type) (_2 : @IRTDesc As) (recr : @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => @Either (recl Ds2) (recr Ds2)) (fun (_1 : @IRTDesc As) (recl : @IRTSubsts As -> Type) (_2 : @IRTDesc As) (recr : @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => prod (recl Ds2) (recr Ds2)) (fun (n1 : @SAWCoreScaffolding.Nat) (_1 : SAWCorePrelude.ListSort_rect (fun (_1 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_1 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_1 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n2 : @SAWCoreScaffolding.Nat) (_2 : Type) => rec n2)) As n1 -> @IRTDesc As) (recf1 : SAWCorePrelude.ListSort_rect (fun (_2 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_2 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_2 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n2 : @SAWCoreScaffolding.Nat) (_3 : Type) => rec n2)) As n1 -> @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => @sigT (@listSortGet As n1) (fun (a1 : SAWCorePrelude.ListSort_rect (fun (_2 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_2 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_2 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n2 : @SAWCoreScaffolding.Nat) (_3 : Type) => rec n2)) As n1) => recf1 a1 Ds2)) (fun (_1 : @IRTSubsts As) => unit) (fun (_1 : @IRTSubsts As) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (n1 : @SAWCoreScaffolding.Nat) (_1 : @IRTSubsts As) => @listSortGet As n1) (Df a) Ds1) => @IRT_existT As Ds1 n Df a (recf a Ds1 xf)) x) (fun (Ds1 : @IRTSubsts As) (x : unit) => @IRT_tt As Ds1) (fun (Ds1 : @IRTSubsts As) (x : @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) => @efq (@IRT As Ds1 (@IRT_empty As)) x) (fun (n : @SAWCoreScaffolding.Nat) (Ds1 : @IRTSubsts As) (x : SAWCorePrelude.ListSort_rect (fun (_1 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_1 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_1 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n1 : @SAWCoreScaffolding.Nat) (_2 : Type) => rec n1)) As n) => @IRT_elemT As Ds1 n x) D Ds. + (* Prelude.CompM was skipped *) (* Prelude.returnM was skipped *) diff --git a/saw-core/prelude/Prelude.sawcore b/saw-core/prelude/Prelude.sawcore index 8a19f570..6e538295 100644 --- a/saw-core/prelude/Prelude.sawcore +++ b/saw-core/prelude/Prelude.sawcore @@ -1689,6 +1689,10 @@ Sigma_proj2 a b = Sigma__rec a b (\ (p:Sigma a b) -> b (Sigma_proj1 a b p)) (\ (pa:a) (pb: b pa) -> pb); +uncurrySigma : (a : sort 0) -> (b : a -> sort 0) -> (c : sort 0) -> + ((pa : a) -> b pa -> c) -> Sigma a b -> c; +uncurrySigma a b c = Sigma__rec a b (\ (_:Sigma a b) -> c); + -------------------------------------------------------------------------------- -- Lists @@ -1722,6 +1726,32 @@ foldList a = (\ (tup : (a * List a * #())) -> Cons a tup.(1) tup.(2).(1)); +-- A list of types, i.e. `List (sort 0)` if `List` was universe polymorphic +data ListSort : sort 1 where { + LS_Nil : ListSort; + LS_Cons : sort 0 -> ListSort -> ListSort; +} + +ListSort__rec : (P : ListSort -> sort 1) -> P LS_Nil -> + ((A:sort 0) -> (l:ListSort) -> P l -> P (LS_Cons A l)) -> + (l:ListSort) -> P l; +ListSort__rec P f1 f2 l = ListSort#rec P f1 f2 l; + +-- The sort at the given index in a ListSort or `EqP Bool True False` if +-- the index is out of bounds +listSortGet : ListSort -> Nat -> sort 0; +listSortGet = ListSort__rec (\ (_:ListSort) -> Nat -> sort 0) + (\ (_:Nat) -> EqP Bool True False) + (\ (A:sort 0) (_:ListSort) (rec : Nat -> sort 0) -> + Nat_cases (sort 0) A (\ (n:Nat) (_:sort 0) -> rec n)); + +-- A ListSort with the first n (or all, if n > length) entries removed +listSortDrop : ListSort -> Nat -> ListSort; +listSortDrop = ListSort__rec (\ (_:ListSort) -> Nat -> ListSort) + (\ (_:Nat) -> LS_Nil) + (\ (_:sort 0) (Ds:ListSort) (rec : Nat -> ListSort) -> + Nat_cases ListSort Ds (\ (n:Nat) (_ : ListSort) -> rec n)); + -------------------------------------------------------------------------------- -- Lists of 64-bit words (for testing Heapster) @@ -1758,6 +1788,182 @@ foldW64List = bv_l.(2).(1)); +-------------------------------------------------------------------------------- +-- Iso-recursive types + +data IRTDesc (As:ListSort) : sort 0 where { + IRT_varD : Nat -> IRTDesc As; -- a IRTDesc var + IRT_mu : IRTDesc As -> IRTDesc As; -- binds a varD + IRT_Either : IRTDesc As -> IRTDesc As -> IRTDesc As; + IRT_prod : IRTDesc As -> IRTDesc As -> IRTDesc As; + IRT_sigT : (n:Nat) -> (listSortGet As n -> IRTDesc As) -> IRTDesc As; + IRT_unit : IRTDesc As; + IRT_empty : IRTDesc As; + IRT_varT : Nat -> IRTDesc As; -- a sort var, i.e. an index into `As` +} + +IRTDesc__rec : (As:ListSort) -> (P : IRTDesc As -> sort 1) -> + ((n:Nat) -> P (IRT_varD As n)) -> + ((D:IRTDesc As) -> P D -> P (IRT_mu As D)) -> + ((Dl:IRTDesc As) -> P Dl -> (Dr:IRTDesc As) -> P Dr -> + P (IRT_Either As Dl Dr)) -> + ((Dl:IRTDesc As) -> P Dl -> (Dr:IRTDesc As) -> P Dr -> + P (IRT_prod As Dl Dr)) -> + ((n:Nat) -> (Df : listSortGet As n -> IRTDesc As) -> + ((a:listSortGet As n) -> P (Df a)) -> P (IRT_sigT As n Df)) -> + P (IRT_unit As) -> P (IRT_empty As) -> + ((n:Nat) -> P (IRT_varT As n)) -> + (D:IRTDesc As) -> P D; +IRTDesc__rec As P f1 f2 f3 f4 f5 f6 f7 f8 D = IRTDesc#rec As P f1 f2 f3 f4 f5 f6 f7 f8 D; + +-- A list of substitutions for a context of iso-recursive type descriptions +data IRTSubsts (As:ListSort) : sort 0 where { + IRTs_Nil : IRTSubsts As; + IRTs_Cons : IRTDesc As -> IRTSubsts As -> IRTSubsts As; +} + +IRTSubsts__rec : (As:ListSort) -> (P : IRTSubsts As -> sort 1) -> P (IRTs_Nil As) -> + ((D:IRTDesc As) -> (Ds:IRTSubsts As) -> P Ds -> P (IRTs_Cons As D Ds)) -> + (Ds:IRTSubsts As) -> P Ds; +IRTSubsts__rec As P f1 f2 Ds = IRTSubsts#rec As P f1 f2 Ds; + +-- The IRTDesc at the given index in an IRTSubsts or IRT_empty if the +-- index is out of bounds +atIRTs : (As:ListSort) -> IRTSubsts As -> Nat -> IRTDesc As; +atIRTs As = IRTSubsts__rec As (\ (_:IRTSubsts As) -> Nat -> IRTDesc As) + (\ (_:Nat) -> IRT_empty As) + (\ (D:IRTDesc As) (_:IRTSubsts As) (rec : Nat -> IRTDesc As) -> + Nat_cases (IRTDesc As) D (\ (n:Nat) (_:IRTDesc As) -> rec n)); + +-- A IRTSubsts with the first n (or all, if n > length) entries removed +dropIRTs : (As:ListSort) -> IRTSubsts As -> Nat -> IRTSubsts As; +dropIRTs As = IRTSubsts__rec As (\ (_:IRTSubsts As) -> Nat -> IRTSubsts As) + (\ (_:Nat) -> IRTs_Nil As) + (\ (_:IRTDesc As) (Ds:IRTSubsts As) (rec : Nat -> IRTSubsts As) -> + Nat_cases (IRTSubsts As) Ds (\ (n:Nat) (_ : IRTSubsts As) -> rec n)); + +-- The type corresponding to an iso-recursive type description +data IRT (As:ListSort) : IRTSubsts As -> IRTDesc As -> sort 0 where { + IRT_elemD : (Ds:IRTSubsts As) -> (n:Nat) -> + IRT As (dropIRTs As Ds (Succ n)) (atIRTs As Ds n) -> + IRT As Ds (IRT_varD As n); + IRT_fold : (Ds:IRTSubsts As) -> (D:IRTDesc As) -> + IRT As (IRTs_Cons As (IRT_mu As D) Ds) D -> IRT As Ds (IRT_mu As D); + IRT_Left : (Ds:IRTSubsts As) -> (Dl:IRTDesc As) -> (Dr:IRTDesc As) -> + IRT As Ds Dl -> IRT As Ds (IRT_Either As Dl Dr); + IRT_Right : (Ds:IRTSubsts As) -> (Dl:IRTDesc As) -> (Dr:IRTDesc As) -> + IRT As Ds Dr -> IRT As Ds (IRT_Either As Dl Dr); + IRT_pair : (Ds:IRTSubsts As) -> (Dl:IRTDesc As) -> (Dr:IRTDesc As) -> + IRT As Ds Dl -> IRT As Ds Dr -> IRT As Ds (IRT_prod As Dl Dr); + IRT_existT : (Ds:IRTSubsts As) -> (n:Nat) -> (Df : listSortGet As n -> IRTDesc As) -> + (a:listSortGet As n) -> IRT As Ds (Df a) -> IRT As Ds (IRT_sigT As n Df); + IRT_tt : (Ds:IRTSubsts As) -> IRT As Ds (IRT_unit As); + IRT_elemT : (Ds:IRTSubsts As) -> (n:Nat) -> + listSortGet As n -> IRT As Ds (IRT_varT As n); +} + +IRT__rec : (As:ListSort) -> (P : (Ds:IRTSubsts As) -> (D:IRTDesc As) -> IRT As Ds D -> sort 1) -> + ((Ds:IRTSubsts As) -> (n:Nat) -> + (x:IRT As (dropIRTs As Ds (Succ n)) (atIRTs As Ds n)) -> + P (dropIRTs As Ds (Succ n)) (atIRTs As Ds n) x -> + P Ds (IRT_varD As n) (IRT_elemD As Ds n x)) -> + ((Ds:IRTSubsts As) -> (D:IRTDesc As) -> + (x:IRT As (IRTs_Cons As (IRT_mu As D) Ds) D) -> + P (IRTs_Cons As (IRT_mu As D) Ds) D x -> + P Ds (IRT_mu As D) (IRT_fold As Ds D x)) -> + ((Ds:IRTSubsts As) -> (Dl:IRTDesc As) -> (Dr:IRTDesc As) -> (xl:IRT As Ds Dl) -> + P Ds Dl xl -> P Ds (IRT_Either As Dl Dr) (IRT_Left As Ds Dl Dr xl)) -> + ((Ds:IRTSubsts As) -> (Dl:IRTDesc As) -> (Dr:IRTDesc As) -> (xr:IRT As Ds Dr) -> + P Ds Dr xr -> P Ds (IRT_Either As Dl Dr) (IRT_Right As Ds Dl Dr xr)) -> + ((Ds:IRTSubsts As) -> (Dl:IRTDesc As) -> (Dr:IRTDesc As) -> + (xl:IRT As Ds Dl) -> P Ds Dl xl -> + (xr:IRT As Ds Dr) -> P Ds Dr xr -> + P Ds (IRT_prod As Dl Dr) (IRT_pair As Ds Dl Dr xl xr)) -> + ((Ds:IRTSubsts As) -> (n:Nat) -> (Df : listSortGet As n -> IRTDesc As) -> + (a:listSortGet As n) -> (xf:IRT As Ds (Df a)) -> P Ds (Df a) xf -> + P Ds (IRT_sigT As n Df) (IRT_existT As Ds n Df a xf)) -> + ((Ds:IRTSubsts As) -> P Ds (IRT_unit As) (IRT_tt As Ds)) -> + ((Ds:IRTSubsts As) -> (n:Nat) -> (a:listSortGet As n) -> + P Ds (IRT_varT As n) (IRT_elemT As Ds n a)) -> + (Ds:IRTSubsts As) -> (D:IRTDesc As) -> (x:IRT As Ds D) -> P Ds D x; +IRT__rec As P f1 f2 f3 f4 f5 f6 f7 f8 Ds D x = IRT#rec As P f1 f2 f3 f4 f5 f6 f7 f8 Ds D x; + +-- The type of a once-unfolded iso-recursive type +UnfoldedIRT : (As:ListSort) -> IRTSubsts As -> IRTDesc As -> sort 0; +UnfoldedIRT As Ds D = IRTDesc__rec As (\ (_:IRTDesc As) -> IRTSubsts As -> sort 0) + (\ (n:Nat) (Ds:IRTSubsts As) -> + IRT As (dropIRTs As Ds (Succ n)) (atIRTs As Ds n)) + (\ (D:IRTDesc As) (rec : IRTSubsts As -> sort 0) (Ds:IRTSubsts As) -> + rec (IRTs_Cons As (IRT_mu As D) Ds)) + (\ (_:IRTDesc As) (recl : IRTSubsts As -> sort 0) + (_:IRTDesc As) (recr : IRTSubsts As -> sort 0) (Ds:IRTSubsts As) -> + Either (recl Ds) (recr Ds)) + (\ (_:IRTDesc As) (recl : IRTSubsts As -> sort 0) + (_:IRTDesc As) (recr : IRTSubsts As -> sort 0) (Ds:IRTSubsts As) -> + recl Ds * recr Ds) + (\ (n:Nat) (_ : listSortGet As n -> IRTDesc As) + (recf : listSortGet As n -> IRTSubsts As -> sort 0) (Ds:IRTSubsts As) -> + Sigma (listSortGet As n) (\ (a:listSortGet As n) -> recf a Ds)) + (\ (_:IRTSubsts As) -> #()) + (\ (_:IRTSubsts As) -> EqP Bool True False) + (\ (n:Nat) (_:IRTSubsts As) -> listSortGet As n) D Ds; + +-- `fold` and `unfold` for IRTs + +unfoldIRT : (As:ListSort) -> (Ds:IRTSubsts As) -> (D:IRTDesc As) -> + IRT As Ds D -> UnfoldedIRT As Ds D; +unfoldIRT As = IRT__rec As (\ (Ds:IRTSubsts As) (D:IRTDesc As) (_:IRT As Ds D) -> UnfoldedIRT As Ds D) + (\ (Ds:IRTSubsts As) (n:Nat) (x:IRT As (dropIRTs As Ds (Succ n)) (atIRTs As Ds n)) + (_:UnfoldedIRT As (dropIRTs As Ds (Succ n)) (atIRTs As Ds n)) -> x) + (\ (Ds:IRTSubsts As) (D:IRTDesc As) (_:IRT As (IRTs_Cons As (IRT_mu As D) Ds) D) + (rec: UnfoldedIRT As (IRTs_Cons As (IRT_mu As D) Ds) D) -> rec) + (\ (Ds:IRTSubsts As) (Dl:IRTDesc As) (Dr:IRTDesc As) + (_:IRT As Ds Dl) (recl:UnfoldedIRT As Ds Dl) -> + Left (UnfoldedIRT As Ds Dl) (UnfoldedIRT As Ds Dr) recl) + (\ (Ds:IRTSubsts As) (Dl:IRTDesc As) (Dr:IRTDesc As) + (_:IRT As Ds Dr) (recr:UnfoldedIRT As Ds Dr) -> + Right (UnfoldedIRT As Ds Dl) (UnfoldedIRT As Ds Dr) recr) + (\ (Ds:IRTSubsts As) (Dl:IRTDesc As) (Dr:IRTDesc As) + (_:IRT As Ds Dl) (recl:UnfoldedIRT As Ds Dl) + (_:IRT As Ds Dr) (recr:UnfoldedIRT As Ds Dr) -> + (recl, recr)) + (\ (Ds:IRTSubsts As) (n:Nat) (Df : listSortGet As n -> IRTDesc As) (a:listSortGet As n) + (_:IRT As Ds (Df a)) (recf:UnfoldedIRT As Ds (Df a)) -> + exists (listSortGet As n) (\ (a:listSortGet As n) -> UnfoldedIRT As Ds (Df a)) a recf) + (\ (Ds:IRTSubsts As) -> ()) + (\ (Ds:IRTSubsts As) (n:Nat) (a:listSortGet As n) -> a); + +foldIRT : (As:ListSort) -> (Ds:IRTSubsts As) -> (D:IRTDesc As) -> + UnfoldedIRT As Ds D -> IRT As Ds D; +foldIRT As Ds D = IRTDesc__rec As (\ (D:IRTDesc As) -> (Ds:IRTSubsts As) -> UnfoldedIRT As Ds D -> IRT As Ds D) + (\ (n:Nat) (Ds:IRTSubsts As) (x:IRT As (dropIRTs As Ds (Succ n)) (atIRTs As Ds n)) -> + IRT_elemD As Ds n x) + (\ (D:IRTDesc As) (rec : (Ds:IRTSubsts As) -> UnfoldedIRT As Ds D -> IRT As Ds D) + (Ds:IRTSubsts As) (x:UnfoldedIRT As (IRTs_Cons As (IRT_mu As D) Ds) D) -> + IRT_fold As Ds D (rec (IRTs_Cons As (IRT_mu As D) Ds) x)) + (\ (Dl:IRTDesc As) (recl : (Ds:IRTSubsts As) -> UnfoldedIRT As Ds Dl -> IRT As Ds Dl) + (Dr:IRTDesc As) (recr : (Ds:IRTSubsts As) -> UnfoldedIRT As Ds Dr -> IRT As Ds Dr) + (Ds:IRTSubsts As) (x:Either (UnfoldedIRT As Ds Dl) (UnfoldedIRT As Ds Dr)) -> + either (UnfoldedIRT As Ds Dl) (UnfoldedIRT As Ds Dr) (IRT As Ds (IRT_Either As Dl Dr)) + (\ (xl:UnfoldedIRT As Ds Dl) -> IRT_Left As Ds Dl Dr (recl Ds xl)) + (\ (xr:UnfoldedIRT As Ds Dr) -> IRT_Right As Ds Dl Dr (recr Ds xr)) x) + (\ (Dl:IRTDesc As) (recl : (Ds:IRTSubsts As) -> UnfoldedIRT As Ds Dl -> IRT As Ds Dl) + (Dr:IRTDesc As) (recr : (Ds:IRTSubsts As) -> UnfoldedIRT As Ds Dr -> IRT As Ds Dr) + (Ds:IRTSubsts As) (x:UnfoldedIRT As Ds Dl * UnfoldedIRT As Ds Dr) -> + uncurry (UnfoldedIRT As Ds Dl) (UnfoldedIRT As Ds Dr) (IRT As Ds (IRT_prod As Dl Dr)) + (\ (xl:UnfoldedIRT As Ds Dl) (xr:UnfoldedIRT As Ds Dr) -> + IRT_pair As Ds Dl Dr (recl Ds xl) (recr Ds xr)) x) + (\ (n:Nat) (Df : listSortGet As n -> IRTDesc As) + (recf : (a:listSortGet As n) -> (Ds:IRTSubsts As) -> UnfoldedIRT As Ds (Df a) -> IRT As Ds (Df a)) + (Ds:IRTSubsts As) (x:Sigma (listSortGet As n) (\ (a:listSortGet As n) -> UnfoldedIRT As Ds (Df a))) -> + uncurrySigma (listSortGet As n) (\ (a:listSortGet As n) -> UnfoldedIRT As Ds (Df a)) (IRT As Ds (IRT_sigT As n Df)) + (\ (a:listSortGet As n) (xf:UnfoldedIRT As Ds (Df a)) -> + IRT_existT As Ds n Df a (recf a Ds xf)) x) + (\ (Ds:IRTSubsts As) (x:#()) -> IRT_tt As Ds) + (\ (Ds:IRTSubsts As) (x:EqP Bool True False) -> efq (IRT As Ds (IRT_empty As)) x) + (\ (n:Nat) (Ds:IRTSubsts As) (x:listSortGet As n) -> IRT_elemT As Ds n x) D Ds; + + -------------------------------------------------------------------------------- -- Computation monad