Definition: C_TYPEco
`C_TYPEco() ==`
`  corec(X.lbl:Atom × if lbl =a "Void" then Unit`
`                     if lbl =a "Int" then Unit`
`                     if lbl =a "Struct" then (Atom × X) List`
`                     if lbl =a "Array" then length:ℕ × X`
`                     if lbl =a "Pointer" then X`
`                     else Void`
`                     fi )`

Lemma: C_TYPEco_wf
`C_TYPEco() ∈ Type`

Lemma: C_TYPEco-ext
`C_TYPEco() ≡ lbl:Atom × if lbl =a "Void" then Unit`
`                        if lbl =a "Int" then Unit`
`                        if lbl =a "Struct" then (Atom × C_TYPEco()) List`
`                        if lbl =a "Array" then length:ℕ × C_TYPEco()`
`                        if lbl =a "Pointer" then C_TYPEco()`
`                        else Void`
`                        fi `

Definition: C_TYPEco_size
`C_TYPEco_size(p) ==`
`  fix((λsize,p. let lbl,x = p `
`                in if lbl =a "Void" then 0`
`                   if lbl =a "Int" then 0`
`                   if lbl =a "Struct" then 1 + Σ(size (snd(x[i])) | i < ||x||)`
`                   if lbl =a "Array" then 1 + (size (snd(x)))`
`                   if lbl =a "Pointer" then 1 + (size x)`
`                   else 0`
`                   fi )) `
`  p`

Lemma: C_TYPEco_size_wf
`∀[p:C_TYPEco()]. (C_TYPEco_size(p) ∈ partial(ℕ))`

Definition: C_TYPE
`C_TYPE() ==  {p:C_TYPEco()| (C_TYPEco_size(p))↓} `

Lemma: C_TYPE_wf
`C_TYPE() ∈ Type`

Definition: C_TYPE_size
`C_TYPE_size(p) ==`
`  fix((λsize,p. let lbl,x = p `
`                in if lbl =a "Void" then 0`
`                   if lbl =a "Int" then 0`
`                   if lbl =a "Struct" then 1 + Σ(size (snd(x[i])) | i < ||x||)`
`                   if lbl =a "Array" then 1 + (size (snd(x)))`
`                   if lbl =a "Pointer" then 1 + (size x)`
`                   else 0`
`                   fi )) `
`  p`

Lemma: C_TYPE_size_wf
`∀[p:C_TYPE()]. (C_TYPE_size(p) ∈ ℕ)`

Lemma: C_TYPE-ext
`C_TYPE() ≡ lbl:Atom × if lbl =a "Void" then Unit`
`                      if lbl =a "Int" then Unit`
`                      if lbl =a "Struct" then (Atom × C_TYPE()) List`
`                      if lbl =a "Array" then length:ℕ × C_TYPE()`
`                      if lbl =a "Pointer" then C_TYPE()`
`                      else Void`
`                      fi `

Definition: C_Void
`C_Void() ==  <"Void", ⋅>`

Lemma: C_Void_wf
`C_Void() ∈ C_TYPE()`

Definition: C_Int
`C_Int() ==  <"Int", ⋅>`

Lemma: C_Int_wf
`C_Int() ∈ C_TYPE()`

Definition: C_Struct
`C_Struct(fields) ==  <"Struct", fields>`

Lemma: C_Struct_wf
`∀[fields:(Atom × C_TYPE()) List]. (C_Struct(fields) ∈ C_TYPE())`

Definition: C_Array
`C_Array(length;elems) ==  <"Array", length, elems>`

Lemma: C_Array_wf
`∀[length:ℕ]. ∀[elems:C_TYPE()].  (C_Array(length;elems) ∈ C_TYPE())`

Definition: C_Pointer
`C_Pointer(to) ==  <"Pointer", to>`

Lemma: C_Pointer_wf
`∀[to:C_TYPE()]. (C_Pointer(to) ∈ C_TYPE())`

Definition: C_Void?
`C_Void?(v) ==  fst(v) =a "Void"`

Lemma: C_Void?_wf
`∀[v:C_TYPE()]. (C_Void?(v) ∈ 𝔹)`

Definition: C_Int?
`C_Int?(v) ==  fst(v) =a "Int"`

Lemma: C_Int?_wf
`∀[v:C_TYPE()]. (C_Int?(v) ∈ 𝔹)`

Definition: C_Struct?
`C_Struct?(v) ==  fst(v) =a "Struct"`

Lemma: C_Struct?_wf
`∀[v:C_TYPE()]. (C_Struct?(v) ∈ 𝔹)`

Definition: C_Struct-fields
`C_Struct-fields(v) ==  snd(v)`

Lemma: C_Struct-fields_wf
`∀[v:C_TYPE()]. C_Struct-fields(v) ∈ (Atom × C_TYPE()) List supposing ↑C_Struct?(v)`

Definition: C_Array?
`C_Array?(v) ==  fst(v) =a "Array"`

Lemma: C_Array?_wf
`∀[v:C_TYPE()]. (C_Array?(v) ∈ 𝔹)`

Definition: C_Array-length
`C_Array-length(v) ==  fst(snd(v))`

Lemma: C_Array-length_wf
`∀[v:C_TYPE()]. C_Array-length(v) ∈ ℕ supposing ↑C_Array?(v)`

Definition: C_Array-elems
`C_Array-elems(v) ==  snd(snd(v))`

Lemma: C_Array-elems_wf
`∀[v:C_TYPE()]. C_Array-elems(v) ∈ C_TYPE() supposing ↑C_Array?(v)`

Definition: C_Pointer?
`C_Pointer?(v) ==  fst(v) =a "Pointer"`

Lemma: C_Pointer?_wf
`∀[v:C_TYPE()]. (C_Pointer?(v) ∈ 𝔹)`

Definition: C_Pointer-to
`C_Pointer-to(v) ==  snd(v)`

Lemma: C_Pointer-to_wf
`∀[v:C_TYPE()]. C_Pointer-to(v) ∈ C_TYPE() supposing ↑C_Pointer?(v)`

Lemma: C_TYPE-induction
`∀[P:C_TYPE() ─→ ℙ]`
`  (P[C_Void()]`
`  `` P[C_Int()]`
`  `` (∀fields:(Atom × C_TYPE()) List. ((∀u∈fields.let u1,u2 = u in P[u2]) `` P[C_Struct(fields)]))`
`  `` (∀length:ℕ. ∀elems:C_TYPE().  (P[elems] `` P[C_Array(length;elems)]))`
`  `` (∀to:C_TYPE(). (P[to] `` P[C_Pointer(to)]))`
`  `` {∀v:C_TYPE(). P[v]})`

Lemma: C_TYPE-definition
`∀[A:Type]. ∀[R:A ─→ C_TYPE() ─→ ℙ].`
`  ({x:A| R[x;C_Void()]} `
`  `` {x:A| R[x;C_Int()]} `
`  `` (∀fields:(Atom × C_TYPE()) List. ((∀u∈fields.let u1,u2 = u in {x:A| R[x;u2]} ) `` {x:A| R[x;C_Struct(fields)]} ))`
`  `` (∀length:ℕ. ∀elems:C_TYPE().  ({x:A| R[x;elems]}  `` {x:A| R[x;C_Array(length;elems)]} ))`
`  `` (∀to:C_TYPE(). ({x:A| R[x;to]}  `` {x:A| R[x;C_Pointer(to)]} ))`
`  `` {∀v:C_TYPE(). {x:A| R[x;v]} })`

Definition: C_TYPE_ind
`C_TYPE_ind(v`
`Void=>Void`
`Int=>Int`
`Struct(fields)=>rec1.Struct[fields; rec1]`
`Array(length,elems)=>rec2.Array[length; elems; rec2]`
`Pointer(to)=>rec3.Pointer[to; rec3]) ==`
`  fix((λC_TYPE_ind,v. let lbl,v1 = v `
`                      in if lbl="Void" then Void`
`                         if lbl="Int" then Int`
`                         if lbl="Struct" then Struct[v1; λi.let v2,v3 = v1[i] in C_TYPE_ind v3]`
`                         if lbl="Array" then let length,v2 = v1 in Array[length; v2; C_TYPE_ind v2]`
`                         if lbl="Pointer" then Pointer[v1; C_TYPE_ind v1]`
`                         else ⊥`
`                         fi )) `
`  v`

Lemma: C_TYPE_ind_wf
`∀[A:Type]. ∀[R:A ─→ C_TYPE() ─→ ℙ]. ∀[v:C_TYPE()]. ∀[Void:{x:A| R[x;C_Void()]} ]. ∀[Int:{x:A| R[x;C_Int()]} ].`
`∀[Struct:fields:((Atom × C_TYPE()) List)`
`         ─→ (∀u∈fields.let u1,u2 = u `
`                       in {x:A| R[x;u2]} )`
`         ─→ {x:A| R[x;C_Struct(fields)]} ]. ∀[Array:length:ℕ`
`                                                   ─→ elems:C_TYPE()`
`                                                   ─→ {x:A| R[x;elems]} `
`                                                   ─→ {x:A| R[x;C_Array(length;elems)]} ].`
`∀[Pointer:to:C_TYPE() ─→ {x:A| R[x;to]}  ─→ {x:A| R[x;C_Pointer(to)]} ].`
`  (C_TYPE_ind(v`
`   Void=>Void`
`   Int=>Int`
`   Struct(fields)=>rec1.Struct[fields;rec1]`
`   Array(length,elems)=>rec2.Array[length;elems;rec2]`
`   Pointer(to)=>rec3.Pointer[to;rec3]) ∈ {x:A| R[x;v]} )`

Lemma: C_TYPE_ind_wf_simple
`∀[A:Type]. ∀[v:C_TYPE()]. ∀[Void,Int:A].`
`∀[Struct:fields:((Atom × C_TYPE()) List) ─→ (∀u∈fields.let u1,u2 = u in A) ─→ A]. ∀[Array:length:ℕ`
`                                                                                          ─→ elems:C_TYPE()`
`                                                                                          ─→ A`
`                                                                                          ─→ A]. ∀[Pointer:to:C_TYPE()`
`                                                                                                           ─→ A`
`                                                                                                           ─→ A].`
`  (C_TYPE_ind(v`
`   Void=>Void`
`   Int=>Int`
`   Struct(fields)=>rec1.Struct[fields;rec1]`
`   Array(length,elems)=>rec2.Array[length;elems;rec2]`
`   Pointer(to)=>rec3.Pointer[to;rec3]) ∈ A)`

Lemma: C_TYPE_subtype_base
`C_TYPE() ⊆r Base`

Definition: C_TYPE_eq_fun
`C_TYPE_eq_fun(a) ==`
`  C_TYPE_ind(a`
`  Void=>λb.C_Void?(b)`
`  Int=>λb.C_Int?(b)`
`  Struct(fields)=>rec.λb.(C_Struct?(b)`
`                         ∧b (||fields|| =z ||C_Struct-fields(b)||)`
`                         ∧b (∀i∈upto(||fields||).fst(fields[i]) =a fst(C_Struct-fields(b)[i])`
`                               ∧b (rec i (snd(C_Struct-fields(b)[i]))))_b)`
`  Array(length,elems)=>rec.λb.(C_Array?(b) ∧b (length =z C_Array-length(b)) ∧b (rec C_Array-elems(b)))`
`  Pointer(to)=>rec.λb.(C_Pointer?(b) ∧b (rec C_Pointer-to(b))))`

Lemma: C_TYPE_eq_fun_wf
`∀[a:C_TYPE()]. (C_TYPE_eq_fun(a) ∈ C_TYPE() ─→ 𝔹)`

Definition: C_TYPE_eq
`C_TYPE_eq(a;b) ==  C_TYPE_eq_fun(a) b`

Lemma: C_TYPE_eq_wf
`∀[a,b:C_TYPE()].  (C_TYPE_eq(a;b) ∈ 𝔹)`

Lemma: assert-C_TYPE_eq
`∀[a,b:C_TYPE()].  uiff(↑C_TYPE_eq(a;b);a = b ∈ C_TYPE())`

Lemma: C_TYPE-induction2
`∀[P:C_TYPE() ─→ ℙ]`
`  (P[C_Void()]`
`  `` P[C_Int()]`
`  `` (∀fields:(Atom × C_TYPE()) List. ((∀i:ℕ||fields||. P[snd(fields[i])]) `` P[C_Struct(fields)]))`
`  `` (∀length:ℕ. ∀elems:C_TYPE().  (P[elems] `` P[C_Array(length;elems)]))`
`  `` (∀to:C_TYPE(). (P[to] `` P[C_Pointer(to)]))`
`  `` {∀x:C_TYPE(). P[x]})`

Lemma: C_TYPE-induction3
`∀[P:C_TYPE() ─→ ℙ]`
`  (P[C_Void()]`
`  `` P[C_Int()]`
`  `` (∀fields:(Atom × C_TYPE()) List. ((∀ct∈map(λp.(snd(p));fields).P[ct]) `` P[C_Struct(fields)]))`
`  `` (∀length:ℕ. ∀elems:C_TYPE().  (P[elems] `` P[C_Array(length;elems)]))`
`  `` (∀to:C_TYPE(). (P[to] `` P[C_Pointer(to)]))`
`  `` {∀x:C_TYPE(). P[x]})`

Lemma: C_TYPE-valueall-type
`valueall-type(C_TYPE())`

Definition: C_TYPE-rank
`C_TYPE-rank(ctyp) ==`
`  C_TYPE_ind(ctyp`
`  Void=>0`
`  Int=>0`
`  Struct(fields)=>recL.Σ(recL j | j < ||fields||)`
`  Array(length,elems)=>recA.recA + 1`
`  Pointer(to)=>recP.recP + 1)`

Lemma: C_TYPE-rank_wf
`∀[ctyp:C_TYPE()]. (C_TYPE-rank(ctyp) ∈ ℕ)`

Definition: C_LOCATION
`C_LOCATION() ==  ℤ`

Lemma: C_LOCATION_wf
`C_LOCATION() ∈ Type`

Definition: C_LVALUEco
`C_LVALUEco() ==`
`  corec(X.lbl:Atom × if lbl =a "Ground" then C_LOCATION()`
`                     if lbl =a "Index" then lval:X × ℤ`
`                     if lbl =a "Scomp" then lval:X × Atom`
`                     else Void`
`                     fi )`

Lemma: C_LVALUEco_wf
`C_LVALUEco() ∈ Type`

Lemma: C_LVALUEco-ext
`C_LVALUEco() ≡ lbl:Atom × if lbl =a "Ground" then C_LOCATION()`
`                          if lbl =a "Index" then lval:C_LVALUEco() × ℤ`
`                          if lbl =a "Scomp" then lval:C_LVALUEco() × Atom`
`                          else Void`
`                          fi `

Definition: C_LVALUEco_size
`C_LVALUEco_size(p) ==`
`  fix((λsize,p. let lbl,x = p `
`                in if lbl =a "Ground" then 0`
`                   if lbl =a "Index" then let lval,z = x in 1 + (size lval)`
`                   if lbl =a "Scomp" then let lval,z = x in 1 + (size lval)`
`                   else 0`
`                   fi )) `
`  p`

Lemma: C_LVALUEco_size_wf
`∀[p:C_LVALUEco()]. (C_LVALUEco_size(p) ∈ partial(ℕ))`

Definition: C_LVALUE
`C_LVALUE() ==  {p:C_LVALUEco()| (C_LVALUEco_size(p))↓} `

Lemma: C_LVALUE_wf
`C_LVALUE() ∈ Type`

Definition: C_LVALUE_size
`C_LVALUE_size(p) ==`
`  fix((λsize,p. let lbl,x = p `
`                in if lbl =a "Ground" then 0`
`                   if lbl =a "Index" then let lval,z = x in 1 + (size lval)`
`                   if lbl =a "Scomp" then let lval,z = x in 1 + (size lval)`
`                   else 0`
`                   fi )) `
`  p`

Lemma: C_LVALUE_size_wf
`∀[p:C_LVALUE()]. (C_LVALUE_size(p) ∈ ℕ)`

Lemma: C_LVALUE-ext
`C_LVALUE() ≡ lbl:Atom × if lbl =a "Ground" then C_LOCATION()`
`                        if lbl =a "Index" then lval:C_LVALUE() × ℤ`
`                        if lbl =a "Scomp" then lval:C_LVALUE() × Atom`
`                        else Void`
`                        fi `

Definition: LV_Ground
`LV_Ground(loc) ==  <"Ground", loc>`

Lemma: LV_Ground_wf
`∀[loc:C_LOCATION()]. (LV_Ground(loc) ∈ C_LVALUE())`

Definition: LV_Index
`LV_Index(lval;idx) ==  <"Index", lval, idx>`

Lemma: LV_Index_wf
`∀[lval:C_LVALUE()]. ∀[idx:ℤ].  (LV_Index(lval;idx) ∈ C_LVALUE())`

Definition: LV_Scomp
`LV_Scomp(lval;comp) ==  <"Scomp", lval, comp>`

Lemma: LV_Scomp_wf
`∀[lval:C_LVALUE()]. ∀[comp:Atom].  (LV_Scomp(lval;comp) ∈ C_LVALUE())`

Definition: LV_Ground?
`LV_Ground?(v) ==  fst(v) =a "Ground"`

Lemma: LV_Ground?_wf
`∀[v:C_LVALUE()]. (LV_Ground?(v) ∈ 𝔹)`

Definition: LV_Ground-loc
`LV_Ground-loc(v) ==  snd(v)`

Lemma: LV_Ground-loc_wf
`∀[v:C_LVALUE()]. LV_Ground-loc(v) ∈ C_LOCATION() supposing ↑LV_Ground?(v)`

Definition: LV_Index?
`LV_Index?(v) ==  fst(v) =a "Index"`

Lemma: LV_Index?_wf
`∀[v:C_LVALUE()]. (LV_Index?(v) ∈ 𝔹)`

Definition: LV_Index-lval
`LV_Index-lval(v) ==  fst(snd(v))`

Lemma: LV_Index-lval_wf
`∀[v:C_LVALUE()]. LV_Index-lval(v) ∈ C_LVALUE() supposing ↑LV_Index?(v)`

Definition: LV_Index-idx
`LV_Index-idx(v) ==  snd(snd(v))`

Lemma: LV_Index-idx_wf
`∀[v:C_LVALUE()]. LV_Index-idx(v) ∈ ℤ supposing ↑LV_Index?(v)`

Definition: LV_Scomp?
`LV_Scomp?(v) ==  fst(v) =a "Scomp"`

Lemma: LV_Scomp?_wf
`∀[v:C_LVALUE()]. (LV_Scomp?(v) ∈ 𝔹)`

Definition: LV_Scomp-lval
`LV_Scomp-lval(v) ==  fst(snd(v))`

Lemma: LV_Scomp-lval_wf
`∀[v:C_LVALUE()]. LV_Scomp-lval(v) ∈ C_LVALUE() supposing ↑LV_Scomp?(v)`

Definition: LV_Scomp-comp
`LV_Scomp-comp(v) ==  snd(snd(v))`

Lemma: LV_Scomp-comp_wf
`∀[v:C_LVALUE()]. LV_Scomp-comp(v) ∈ Atom supposing ↑LV_Scomp?(v)`

Lemma: C_LVALUE-induction
`∀[P:C_LVALUE() ─→ ℙ]`
`  ((∀loc:C_LOCATION(). P[LV_Ground(loc)])`
`  `` (∀lval:C_LVALUE(). ∀idx:ℤ.  (P[lval] `` P[LV_Index(lval;idx)]))`
`  `` (∀lval:C_LVALUE(). ∀comp:Atom.  (P[lval] `` P[LV_Scomp(lval;comp)]))`
`  `` {∀v:C_LVALUE(). P[v]})`

Lemma: C_LVALUE-definition
`∀[A:Type]. ∀[R:A ─→ C_LVALUE() ─→ ℙ].`
`  ((∀loc:C_LOCATION(). {x:A| R[x;LV_Ground(loc)]} )`
`  `` (∀lval:C_LVALUE(). ∀idx:ℤ.  ({x:A| R[x;lval]}  `` {x:A| R[x;LV_Index(lval;idx)]} ))`
`  `` (∀lval:C_LVALUE(). ∀comp:Atom.  ({x:A| R[x;lval]}  `` {x:A| R[x;LV_Scomp(lval;comp)]} ))`
`  `` {∀v:C_LVALUE(). {x:A| R[x;v]} })`

Definition: C_LVALUE_ind
`C_LVALUE_ind(v;`
`             LV_Ground(loc)`` Ground[loc];`
`             LV_Index(lval,idx)`` rec1.Index[lval; idx; rec1];`
`             LV_Scomp(lval,comp)`` rec2.Scomp[lval; comp; rec2])  ==`
`  fix((λC_LVALUE_ind,v. let lbl,v1 = v `
`                        in if lbl="Ground" then Ground[v1]`
`                           if lbl="Index" then let lval,v2 = v1 in Index[lval; v2; C_LVALUE_ind lval]`
`                           if lbl="Scomp" then let lval,v2 = v1 in Scomp[lval; v2; C_LVALUE_ind lval]`
`                           else ⊥`
`                           fi )) `
`  v`

Lemma: C_LVALUE_ind_wf
`∀[A:Type]. ∀[R:A ─→ C_LVALUE() ─→ ℙ]. ∀[v:C_LVALUE()]. ∀[Ground:loc:C_LOCATION() ─→ {x:A| R[x;LV_Ground(loc)]} ].`
`∀[Index:lval:C_LVALUE() ─→ idx:ℤ ─→ {x:A| R[x;lval]}  ─→ {x:A| R[x;LV_Index(lval;idx)]} ].`
`∀[Scomp:lval:C_LVALUE() ─→ comp:Atom ─→ {x:A| R[x;lval]}  ─→ {x:A| R[x;LV_Scomp(lval;comp)]} ].`
`  (C_LVALUE_ind(v;`
`                LV_Ground(loc)`` Ground[loc];`
`                LV_Index(lval,idx)`` rec1.Index[lval;idx;rec1];`
`                LV_Scomp(lval,comp)`` rec2.Scomp[lval;comp;rec2])  ∈ {x:A| R[x;v]} )`

Lemma: C_LVALUE_ind_wf_simple
`∀[A:Type]. ∀[v:C_LVALUE()]. ∀[Ground:loc:C_LOCATION() ─→ A]. ∀[Index:lval:C_LVALUE() ─→ idx:ℤ ─→ A ─→ A].`
`∀[Scomp:lval:C_LVALUE() ─→ comp:Atom ─→ A ─→ A].`
`  (C_LVALUE_ind(v;`
`                LV_Ground(loc)`` Ground[loc];`
`                LV_Index(lval,idx)`` rec1.Index[lval;idx;rec1];`
`                LV_Scomp(lval,comp)`` rec2.Scomp[lval;comp;rec2])  ∈ A)`

Definition: C_field_of
`C_field_of(a;ctyp) ==  a ∈b map(λx.(fst(x));C_Struct-fields(ctyp)))`

Lemma: C_field_of_wf
`∀[a:Atom]. ∀[ctyp:{t:C_TYPE()| ↑C_Struct?(t)} ].  (C_field_of(a;ctyp) ∈ 𝔹)`

Definition: C_type_of_field
`C_type_of_field(a;ctyp) ==  outl(apply-alist(AtomDeq;C_Struct-fields(ctyp);a))`

Lemma: C_type_of_field_wf
`∀[ctyp:{t:C_TYPE()| ↑C_Struct?(t)} ]. ∀[a:{c:Atom| ↑C_field_of(c;ctyp)} ].  (C_type_of_field(a;ctyp) ∈ C_TYPE())`

Definition: C_TYPE_env
`C_TYPE_env() ==  C_LOCATION() ─→ (C_TYPE()?)`

Lemma: C_TYPE_env_wf
`C_TYPE_env() ∈ Type`

Definition: C_TYPE-of-LVALUE
`C_TYPE-of-LVALUE(env;lval) ==`
`  case lval is  `
`  Ground(loc) => env loc  `
`  aval[idx] => let r = case of aval in if isl(r)`
`               then if C_Array?(outl(r))`
`                    then if 0 ≤z idx ∧b idx <z C_Array-length(outl(r)) then inl C_Array-elems(outl(r)) else inr ⋅  fi `
`                    else inr ⋅ `
`                    fi `
`               else inr ⋅ `
`               fi   `
`  sval.comp =>  let r2 = case of sval in if isl(r2)`
`               then if C_Struct?(outl(r2)) then apply-alist(AtomDeq;C_Struct-fields(outl(r2));comp) else inr ⋅  fi `
`               else inr ⋅ `
`               fi )`

Lemma: C_TYPE-of-LVALUE_wf
`∀env:C_TYPE_env(). ∀lval:C_LVALUE().  (C_TYPE-of-LVALUE(env;lval) ∈ C_TYPE()?)`

Definition: C_LVALUE-proper
`C_LVALUE-proper(env;lval) ==  isl(C_TYPE-of-LVALUE(env;lval))`

Lemma: C_LVALUE-proper_wf
`∀env:C_TYPE_env(). ∀lval:C_LVALUE().  (C_LVALUE-proper(env;lval) ∈ 𝔹)`

Lemma: C_LVALUE-proper-Ground
`∀env:C_TYPE_env(). ∀lval:C_LVALUE().`
`  ((↑LV_Ground?(lval)) `` (↑C_LVALUE-proper(env;lval)) `` (↑isl(env LV_Ground-loc(lval))))`

Lemma: C_LVALUE-proper-Index
`∀env:C_TYPE_env(). ∀lval:C_LVALUE().`
`  ((↑LV_Index?(lval))`
`  `` (↑C_LVALUE-proper(env;lval))`
`  `` let lval' = LV_Index-lval(lval) in`
`      let i = LV_Index-idx(lval) in`
`      let typ = outl(C_TYPE-of-LVALUE(env;lval')) in`
`      (↑C_LVALUE-proper(env;lval')) ∧ (↑C_Array?(typ)) ∧ (0 ≤ i) ∧ i < C_Array-length(typ))`

Lemma: C_LVALUE-proper-Indexed
`∀env:C_TYPE_env(). ∀lval:C_LVALUE(). ∀i:ℤ.`
`  ((↑C_LVALUE-proper(env;LV_Index(lval;i))) `` (↑C_Array?(outl(C_TYPE-of-LVALUE(env;lval)))))`

Lemma: C_LVALUE-proper-Scomp
`∀env:C_TYPE_env(). ∀lval:C_LVALUE().`
`  ((↑LV_Scomp?(lval))`
`  `` (↑C_LVALUE-proper(env;lval))`
`  `` let lval' = LV_Scomp-lval(lval) in`
`      let a = LV_Scomp-comp(lval) in`
`      let typ = outl(C_TYPE-of-LVALUE(env;lval')) in`
`      (↑C_LVALUE-proper(env;lval')) ∧ (↑C_Struct?(typ)) ∧ (↑C_field_of(a;typ)))`

Lemma: C_LVALUE-proper-Scomped
`∀env:C_TYPE_env(). ∀lval:C_LVALUE(). ∀a:Atom.`
`  ((↑C_LVALUE-proper(env;LV_Scomp(lval;a))) `` (↑C_Struct?(outl(C_TYPE-of-LVALUE(env;lval)))))`

Definition: C_DVALUEpco
`C_DVALUEpco() ==`
`  corec(X.lbl:Atom × if lbl =a "Null" then Unit`
`                     if lbl =a "Int" then ℤ`
`                     if lbl =a "Pointer" then C_LVALUE()?`
`                     if lbl =a "Array" then lower:ℤ × upper:ℤ × ({lower..upper-} ─→ X)`
`                     if lbl =a "Struct" then lbls:Atom List × ({a:Atom| (a ∈ lbls)}  ─→ X)`
`                     else Void`
`                     fi )`

Lemma: C_DVALUEpco_wf
`C_DVALUEpco() ∈ Type`

Lemma: C_DVALUEpco-ext
`C_DVALUEpco() ≡ lbl:Atom × if lbl =a "Null" then Unit`
`                           if lbl =a "Int" then ℤ`
`                           if lbl =a "Pointer" then C_LVALUE()?`
`                           if lbl =a "Array" then lower:ℤ × upper:ℤ × ({lower..upper-} ─→ C_DVALUEpco())`
`                           if lbl =a "Struct" then lbls:Atom List × ({a:Atom| (a ∈ lbls)}  ─→ C_DVALUEpco())`
`                           else Void`
`                           fi `

Definition: C_DVALUEpco_size
`C_DVALUEpco_size(p) ==`
`  fix((λsize,p. let lbl,x = p `
`                in if lbl =a "Null" then 0`
`                   if lbl =a "Int" then 0`
`                   if lbl =a "Pointer" then 0`
`                   if lbl =a "Array"`
`                     then 1`
`                          + Σ(size ((snd(snd(x))) ((fst(x)) + i)) | i < if fst(x) ≤z fst(snd(x))`
`                            then (fst(snd(x))) - fst(x)`
`                            else 0`
`                            fi )`
`                   if lbl =a "Struct" then 1 + Σ(size ((snd(x)) fst(x)[a]) | a < ||fst(x)||)`
`                   else 0`
`                   fi )) `
`  p`

Lemma: C_DVALUEpco_size_wf
`∀[p:C_DVALUEpco()]. (C_DVALUEpco_size(p) ∈ partial(ℕ))`

Definition: C_DVALUEp
`C_DVALUEp() ==  {p:C_DVALUEpco()| (C_DVALUEpco_size(p))↓} `

Lemma: C_DVALUEp_wf
`C_DVALUEp() ∈ Type`

Definition: C_DVALUEp_size
`C_DVALUEp_size(p) ==`
`  fix((λsize,p. let lbl,x = p `
`                in if lbl =a "Null" then 0`
`                   if lbl =a "Int" then 0`
`                   if lbl =a "Pointer" then 0`
`                   if lbl =a "Array"`
`                     then 1`
`                          + Σ(size ((snd(snd(x))) ((fst(x)) + i)) | i < if fst(x) ≤z fst(snd(x))`
`                            then (fst(snd(x))) - fst(x)`
`                            else 0`
`                            fi )`
`                   if lbl =a "Struct" then 1 + Σ(size ((snd(x)) fst(x)[a]) | a < ||fst(x)||)`
`                   else 0`
`                   fi )) `
`  p`

Lemma: C_DVALUEp_size_wf
`∀[p:C_DVALUEp()]. (C_DVALUEp_size(p) ∈ ℕ)`

Lemma: C_DVALUEp-ext
`C_DVALUEp() ≡ lbl:Atom × if lbl =a "Null" then Unit`
`                         if lbl =a "Int" then ℤ`
`                         if lbl =a "Pointer" then C_LVALUE()?`
`                         if lbl =a "Array" then lower:ℤ × upper:ℤ × ({lower..upper-} ─→ C_DVALUEp())`
`                         if lbl =a "Struct" then lbls:Atom List × ({a:Atom| (a ∈ lbls)}  ─→ C_DVALUEp())`
`                         else Void`
`                         fi `

Definition: DVp_Null
`DVp_Null(x) ==  <"Null", x>`

Lemma: DVp_Null_wf
`∀[x:Unit]. (DVp_Null(x) ∈ C_DVALUEp())`

Definition: DVp_Int
`DVp_Int(int) ==  <"Int", int>`

Lemma: DVp_Int_wf
`∀[int:ℤ]. (DVp_Int(int) ∈ C_DVALUEp())`

Definition: DVp_Pointer
`DVp_Pointer(ptr) ==  <"Pointer", ptr>`

Lemma: DVp_Pointer_wf
`∀[ptr:C_LVALUE()?]. (DVp_Pointer(ptr) ∈ C_DVALUEp())`

Definition: DVp_Array
`DVp_Array(lower;upper;arr) ==  <"Array", lower, upper, arr>`

Lemma: DVp_Array_wf
`∀[lower,upper:ℤ]. ∀[arr:{lower..upper-} ─→ C_DVALUEp()].  (DVp_Array(lower;upper;arr) ∈ C_DVALUEp())`

Definition: DVp_Struct
`DVp_Struct(lbls;struct) ==  <"Struct", lbls, struct>`

Lemma: DVp_Struct_wf
`∀[lbls:Atom List]. ∀[struct:{a:Atom| (a ∈ lbls)}  ─→ C_DVALUEp()].  (DVp_Struct(lbls;struct) ∈ C_DVALUEp())`

Definition: DVp_Null?
`DVp_Null?(v) ==  fst(v) =a "Null"`

Lemma: DVp_Null?_wf
`∀[v:C_DVALUEp()]. (DVp_Null?(v) ∈ 𝔹)`

Definition: DVp_Null-x
`DVp_Null-x(v) ==  snd(v)`

Lemma: DVp_Null-x_wf
`∀[v:C_DVALUEp()]. DVp_Null-x(v) ∈ Unit supposing ↑DVp_Null?(v)`

Definition: DVp_Int?
`DVp_Int?(v) ==  fst(v) =a "Int"`

Lemma: DVp_Int?_wf
`∀[v:C_DVALUEp()]. (DVp_Int?(v) ∈ 𝔹)`

Definition: DVp_Int-int
`DVp_Int-int(v) ==  snd(v)`

Lemma: DVp_Int-int_wf
`∀[v:C_DVALUEp()]. DVp_Int-int(v) ∈ ℤ supposing ↑DVp_Int?(v)`

Definition: DVp_Pointer?
`DVp_Pointer?(v) ==  fst(v) =a "Pointer"`

Lemma: DVp_Pointer?_wf
`∀[v:C_DVALUEp()]. (DVp_Pointer?(v) ∈ 𝔹)`

Definition: DVp_Pointer-ptr
`DVp_Pointer-ptr(v) ==  snd(v)`

Lemma: DVp_Pointer-ptr_wf
`∀[v:C_DVALUEp()]. DVp_Pointer-ptr(v) ∈ C_LVALUE()? supposing ↑DVp_Pointer?(v)`

Definition: DVp_Array?
`DVp_Array?(v) ==  fst(v) =a "Array"`

Lemma: DVp_Array?_wf
`∀[v:C_DVALUEp()]. (DVp_Array?(v) ∈ 𝔹)`

Definition: DVp_Array-lower
`DVp_Array-lower(v) ==  fst(snd(v))`

Lemma: DVp_Array-lower_wf
`∀[v:C_DVALUEp()]. DVp_Array-lower(v) ∈ ℤ supposing ↑DVp_Array?(v)`

Definition: DVp_Array-upper
`DVp_Array-upper(v) ==  fst(snd(snd(v)))`

Lemma: DVp_Array-upper_wf
`∀[v:C_DVALUEp()]. DVp_Array-upper(v) ∈ ℤ supposing ↑DVp_Array?(v)`

Definition: DVp_Array-arr
`DVp_Array-arr(v) ==  snd(snd(snd(v)))`

Lemma: DVp_Array-arr_wf
`∀[v:C_DVALUEp()]. DVp_Array-arr(v) ∈ {DVp_Array-lower(v)..DVp_Array-upper(v)-} ─→ C_DVALUEp() supposing ↑DVp_Array?(v)`

Definition: DVp_Struct?
`DVp_Struct?(v) ==  fst(v) =a "Struct"`

Lemma: DVp_Struct?_wf
`∀[v:C_DVALUEp()]. (DVp_Struct?(v) ∈ 𝔹)`

Definition: DVp_Struct-lbls
`DVp_Struct-lbls(v) ==  fst(snd(v))`

Lemma: DVp_Struct-lbls_wf
`∀[v:C_DVALUEp()]. DVp_Struct-lbls(v) ∈ Atom List supposing ↑DVp_Struct?(v)`

Definition: DVp_Struct-struct
`DVp_Struct-struct(v) ==  snd(snd(v))`

Lemma: DVp_Struct-struct_wf
`∀[v:C_DVALUEp()]. DVp_Struct-struct(v) ∈ {a:Atom| (a ∈ DVp_Struct-lbls(v))}  ─→ C_DVALUEp() supposing ↑DVp_Struct?(v)`

Lemma: C_DVALUEp-induction
`∀[P:C_DVALUEp() ─→ ℙ]`
`  ((∀x:Unit. P[DVp_Null(x)])`
`  `` (∀int:ℤ. P[DVp_Int(int)])`
`  `` (∀ptr:C_LVALUE()?. P[DVp_Pointer(ptr)])`
`  `` (∀lower,upper:ℤ. ∀arr:{lower..upper-} ─→ C_DVALUEp().`
`        ((∀u:{lower..upper-}. P[arr u]) `` P[DVp_Array(lower;upper;arr)]))`
`  `` (∀lbls:Atom List. ∀struct:{a:Atom| (a ∈ lbls)}  ─→ C_DVALUEp().`
`        ((∀u:{a:Atom| (a ∈ lbls)} . P[struct u]) `` P[DVp_Struct(lbls;struct)]))`
`  `` {∀v:C_DVALUEp(). P[v]})`

Lemma: C_DVALUEp-definition
`∀[A:Type]. ∀[R:A ─→ C_DVALUEp() ─→ ℙ].`
`  ((∀x:Unit. {x1:A| R[x1;DVp_Null(x)]} )`
`  `` (∀int:ℤ. {x:A| R[x;DVp_Int(int)]} )`
`  `` (∀ptr:C_LVALUE()?. {x:A| R[x;DVp_Pointer(ptr)]} )`
`  `` (∀lower,upper:ℤ. ∀arr:{lower..upper-} ─→ C_DVALUEp().`
`        ((∀u:{lower..upper-}. {x:A| R[x;arr u]} ) `` {x:A| R[x;DVp_Array(lower;upper;arr)]} ))`
`  `` (∀lbls:Atom List. ∀struct:{a:Atom| (a ∈ lbls)}  ─→ C_DVALUEp().`
`        ((∀u:{a:Atom| (a ∈ lbls)} . {x:A| R[x;struct u]} ) `` {x:A| R[x;DVp_Struct(lbls;struct)]} ))`
`  `` {∀v:C_DVALUEp(). {x:A| R[x;v]} })`

Definition: C_DVALUEp_ind
`C_DVALUEp_ind(v;`
`              DVp_Null(x)`` Null[x];`
`              DVp_Int(int)`` Int[int];`
`              DVp_Pointer(ptr)`` Pointer[ptr];`
`              DVp_Array(lower,upper,arr)`` rec1.Array[lower; upper; arr; rec1];`
`              DVp_Struct(lbls,struct)`` rec2.Struct[lbls; struct; rec2])  ==`
`  fix((λC_DVALUEp_ind,v. let lbl,v1 = v `
`                         in if lbl="Null" then Null[Ax]`
`                            if lbl="Int" then Int[v1]`
`                            if lbl="Pointer" then case v1 of inl(x) => Pointer[inl x] | inr(y) => Pointer[inr Ax ]`
`                            if lbl="Array"`
`                              then let lower,v2 = v1 `
`                                   in let upper,v3 = v2 `
`                                      in Array[lower; upper; v3; λu.(C_DVALUEp_ind (v3 u))]`
`                            if lbl="Struct" then let lbls,v2 = v1 in Struct[lbls; v2; λu.(C_DVALUEp_ind (v2 u))]`
`                            else ⊥`
`                            fi )) `
`  v`

Lemma: C_DVALUEp_ind_wf
`∀[A:Type]. ∀[R:A ─→ C_DVALUEp() ─→ ℙ]. ∀[v:C_DVALUEp()]. ∀[Null:x:Unit ─→ {x1:A| R[x1;DVp_Null(x)]} ].`
`∀[Int:int:ℤ ─→ {x:A| R[x;DVp_Int(int)]} ]. ∀[Pointer:ptr:(C_LVALUE()?) ─→ {x:A| R[x;DVp_Pointer(ptr)]} ].`
`∀[Array:lower:ℤ`
`        ─→ upper:ℤ`
`        ─→ arr:({lower..upper-} ─→ C_DVALUEp())`
`        ─→ (u:{lower..upper-} ─→ {x:A| R[x;arr u]} )`
`        ─→ {x:A| R[x;DVp_Array(lower;upper;arr)]} ]. ∀[Struct:lbls:(Atom List)`
`                                                             ─→ struct:({a:Atom| (a ∈ lbls)}  ─→ C_DVALUEp())`
`                                                             ─→ (u:{a:Atom| (a ∈ lbls)}  ─→ {x:A| R[x;struct u]} )`
`                                                             ─→ {x:A| R[x;DVp_Struct(lbls;struct)]} ].`
`  (C_DVALUEp_ind(v;`
`                 DVp_Null(x)`` Null[x];`
`                 DVp_Int(int)`` Int[int];`
`                 DVp_Pointer(ptr)`` Pointer[ptr];`
`                 DVp_Array(lower,upper,arr)`` rec1.Array[lower;upper;arr;rec1];`
`                 DVp_Struct(lbls,struct)`` rec2.Struct[lbls;struct;rec2])  ∈ {x:A| R[x;v]} )`

Lemma: C_DVALUEp_ind_wf_simple
`∀[A:Type]. ∀[v:C_DVALUEp()]. ∀[Null:x:Unit ─→ A]. ∀[Int:int:ℤ ─→ A]. ∀[Pointer:ptr:(C_LVALUE()?) ─→ A].`
`∀[Array:lower:ℤ ─→ upper:ℤ ─→ arr:({lower..upper-} ─→ C_DVALUEp()) ─→ (u:{lower..upper-} ─→ A) ─→ A].`
`∀[Struct:lbls:(Atom List) ─→ struct:({a:Atom| (a ∈ lbls)}  ─→ C_DVALUEp()) ─→ (u:{a:Atom| (a ∈ lbls)}  ─→ A) ─→ A].`
`  (C_DVALUEp_ind(v;`
`                 DVp_Null(x)`` Null[x];`
`                 DVp_Int(int)`` Int[int];`
`                 DVp_Pointer(ptr)`` Pointer[ptr];`
`                 DVp_Array(lower,upper,arr)`` rec1.Array[lower;upper;arr;rec1];`
`                 DVp_Struct(lbls,struct)`` rec2.Struct[lbls;struct;rec2])  ∈ A)`

Definition: C_TYPE_vs_DVALp
`C_TYPE_vs_DVALp(env;ctyp) ==`
`  C_TYPE_ind(ctyp`
`  Void=>λdval.ff`
`  Int=>λdval.DVp_Int?(dval)`
`  Struct(fields)=>r.λdval.if DVp_Struct?(dval)`
`                          then let lbls = DVp_Struct-lbls(dval) in`
`                                let g = DVp_Struct-struct(dval) in`
`                                bdd-all(||fields||;i.eval a = fst(fields[i]) in`
`                                                     a ∈b lbls) ∧b (r i (g a)))`
`                          else ff`
`                          fi `
`  Array(n,elems)=>recA.λdval.if DVp_Array?(dval)`
`                             then let a = DVp_Array-lower(dval) in`
`                                   let b = DVp_Array-upper(dval) in`
`                                   let f = DVp_Array-arr(dval) in`
`                                   (n =z b - a) ∧b (∀i∈upto(n).recA (f (a + i)))_b`
`                             else ff`
`                             fi `
`  Pointer(typ)=>recP.λdval.if DVp_Pointer?(dval)`
`                           then let ptr = DVp_Pointer-ptr(dval) in`
`                                    if isl(ptr)`
`                                    then let lval = outl(ptr) in`
`                                             if isl(C_TYPE-of-LVALUE(env;lval))`
`                                             then C_TYPE_eq(outl(C_TYPE-of-LVALUE(env;lval));typ)`
`                                             else ff`
`                                             fi `
`                                    else tt`
`                                    fi `
`                           else ff`
`                           fi )`

Lemma: C_TYPE_vs_DVALp_wf
`∀env:C_TYPE_env(). ∀ctyp:C_TYPE().  (C_TYPE_vs_DVALp(env;ctyp) ∈ C_DVALUEp() ─→ 𝔹)`

Definition: C_STOREp
`C_STOREp() ==  C_LOCATION() ─→ (C_DVALUEp()?)`

Lemma: C_STOREp_wf
`C_STOREp() ∈ Type`

Definition: C_STOREp-welltyped
`C_STOREp-welltyped(env;store) ==`
`  ∀loc:C_LOCATION()`
`    if isl(env loc)`
`    then ↑(isl(store loc) ∧b (C_TYPE_vs_DVALp(env;outl(env loc)) outl(store loc)))`
`    else ↑isr(store loc)`
`    fi `

Lemma: C_STOREp-welltyped_wf
`∀env:C_TYPE_env(). ∀store:C_STOREp().  (C_STOREp-welltyped(env;store) ∈ ℙ)`

Lemma: C_Array_vs_DVALp
`∀store:C_STOREp(). ∀ctyp:C_TYPE(). ∀env:C_TYPE_env(). ∀dval:C_DVALUEp().`
`  (C_STOREp-welltyped(env;store)`
`  `` (↑C_Array?(ctyp))`
`  `` C_TYPE_vs_DVALp(env;ctyp) dval `
`     = if DVp_Array?(dval)`
`       then let a = DVp_Array-lower(dval) in`
`             let b = DVp_Array-upper(dval) in`
`             let f = DVp_Array-arr(dval) in`
`             (C_Array-length(ctyp) =z b - a)`
`             ∧b (∀i∈upto(C_Array-length(ctyp)).C_TYPE_vs_DVALp(env;C_Array-elems(ctyp)) (f (a + i)))_b`
`       else ff`
`       fi )`

Lemma: C_Array-elem_vs_DVALp
`∀store:C_STOREp(). ∀ctyp:C_TYPE(). ∀env:C_TYPE_env(). ∀dval:C_DVALUEp(). ∀n:ℤ.`
`  (C_STOREp-welltyped(env;store)`
`  `` (↑C_Array?(ctyp))`
`  `` (0 ≤ n)`
`  `` n < C_Array-length(ctyp)`
`  `` (↑(C_TYPE_vs_DVALp(env;ctyp) dval))`
`  `` (↑(C_TYPE_vs_DVALp(env;C_Array-elems(ctyp)) (DVp_Array-arr(dval) (DVp_Array-lower(dval) + n)))))`

Lemma: C_Struct_vs_DVALp
`∀store:C_STOREp(). ∀ctyp:C_TYPE(). ∀env:C_TYPE_env(). ∀dval:C_DVALUEp().`
`  (C_STOREp-welltyped(env;store)`
`  `` (↑C_Struct?(ctyp))`
`  `` C_TYPE_vs_DVALp(env;ctyp) dval `
`     = if DVp_Struct?(dval)`
`       then let r = map(λp.<fst(p), C_TYPE_vs_DVALp(env;snd(p))>;C_Struct-fields(ctyp)) in`
`             let lbls = DVp_Struct-lbls(dval) in`
`             let g = DVp_Struct-struct(dval) in`
`             (∀p∈r.let a,wt = p `
`                   in a ∈b lbls) ∧b (wt (g a)))_b`
`       else ff`
`       fi )`

Definition: C_the_value_p
`C_the_value_p(store;lval) ==`
`  case lval is  `
`  Ground(loc) => store loc  `
`  a[idx] => let val_a = case of a in if isl(val_a) then DVp_Array-arr(outl(val_a)) idx else inr ⋅  fi   `
`  sval.comp =>  let val_s = case of sval in if isl(val_s) then DVp_Struct-struct(outl(val_s)) comp else inr ⋅  fi )`

Definition: memb22
`memb22(T;t) ==  eq22(T; t; t)`

Lemma: BNF-list-case0
`∀ms:ℤ List. (imax-list([0 / ms]) ∈ ℕ)`

Lemma: BNF-list-case1
`∀ms:ℤ List. ∀n:ℕ.  (imax-list([0 / ms]) + n ∈ ℕ)`

Definition: MultiTreeco
`MultiTreeco(T) ==`
`  corec(X.lbl:Atom × if lbl =a "Node" then labels:{L:Atom List| 0 < ||L||}  × ({a:Atom| (a ∈ labels)}  ─→ X)`
`                     if lbl =a "Leaf" then T`
`                     else Void`
`                     fi )`

Lemma: MultiTreeco_wf
`∀[T:Type]. (MultiTreeco(T) ∈ Type)`

Lemma: MultiTreeco-ext
`∀[T:Type]`
`  MultiTreeco(T) ≡ lbl:Atom × if lbl =a "Node" then labels:{L:Atom List| 0 < ||L||}  × ({a:Atom| (a ∈ labels)}  ─→ Multi\000CTreeco(T))`
`                              if lbl =a "Leaf" then T`
`                              else Void`
`                              fi `

Definition: MultiTreeco_size
`MultiTreeco_size(p) ==`
`  fix((λsize,p. let lbl,x = p `
`                in if lbl =a "Node" then 1 + Σ(size ((snd(x)) fst(x)[a]) | a < ||fst(x)||)`
`                   if lbl =a "Leaf" then 0`
`                   else 0`
`                   fi )) `
`  p`

Lemma: MultiTreeco_size_wf
`∀[T:Type]. ∀[p:MultiTreeco(T)].  (MultiTreeco_size(p) ∈ partial(ℕ))`

Definition: MultiTree
`MultiTree(T) ==  {p:MultiTreeco(T)| (MultiTreeco_size(p))↓} `

Lemma: MultiTree_wf
`∀[T:Type]. (MultiTree(T) ∈ Type)`

Definition: MultiTree_size
`MultiTree_size(p) ==`
`  fix((λsize,p. let lbl,x = p `
`                in if lbl =a "Node" then 1 + Σ(size ((snd(x)) fst(x)[a]) | a < ||fst(x)||)`
`                   if lbl =a "Leaf" then 0`
`                   else 0`
`                   fi )) `
`  p`

Lemma: MultiTree_size_wf
`∀[T:Type]. ∀[p:MultiTree(T)].  (MultiTree_size(p) ∈ ℕ)`

Lemma: MultiTree-ext
`∀[T:Type]`
`  MultiTree(T) ≡ lbl:Atom × if lbl =a "Node" then labels:{L:Atom List| 0 < ||L||}  × ({a:Atom| (a ∈ labels)}  ─→ MultiTr\000Cee(T))`
`                            if lbl =a "Leaf" then T`
`                            else Void`
`                            fi `

Definition: MTree_Node
`MTree_Node(labels;children) ==  <"Node", labels, children>`

Lemma: MTree_Node_wf
`∀[T:Type]. ∀[labels:{L:Atom List| 0 < ||L||} ]. ∀[children:{a:Atom| (a ∈ labels)}  ─→ MultiTree(T)].`
`  (MTree_Node(labels;children) ∈ MultiTree(T))`

Definition: MTree_Leaf
`MTree_Leaf(val) ==  <"Leaf", val>`

Lemma: MTree_Leaf_wf
`∀[T:Type]. ∀[val:T].  (MTree_Leaf(val) ∈ MultiTree(T))`

Definition: MTree_Node?
`MTree_Node?(v) ==  fst(v) =a "Node"`

Lemma: MTree_Node?_wf
`∀[T:Type]. ∀[v:MultiTree(T)].  (MTree_Node?(v) ∈ 𝔹)`

Definition: MTree_Node-labels
`MTree_Node-labels(v) ==  fst(snd(v))`

Lemma: MTree_Node-labels_wf
`∀[T:Type]. ∀[v:MultiTree(T)].  MTree_Node-labels(v) ∈ {L:Atom List| 0 < ||L||}  supposing ↑MTree_Node?(v)`

Definition: MTree_Node-children
`MTree_Node-children(v) ==  snd(snd(v))`

Lemma: MTree_Node-children_wf
`∀[T:Type]. ∀[v:MultiTree(T)].  MTree_Node-children(v) ∈ {a:Atom| (a ∈ MTree_Node-labels(v))}  ─→ MultiTree(T) supposing \000C↑MTree_Node?(v)`

Definition: MTree_Leaf?
`MTree_Leaf?(v) ==  fst(v) =a "Leaf"`

Lemma: MTree_Leaf?_wf
`∀[T:Type]. ∀[v:MultiTree(T)].  (MTree_Leaf?(v) ∈ 𝔹)`

Definition: MTree_Leaf-val
`MTree_Leaf-val(v) ==  snd(v)`

Lemma: MTree_Leaf-val_wf
`∀[T:Type]. ∀[v:MultiTree(T)].  MTree_Leaf-val(v) ∈ T supposing ↑MTree_Leaf?(v)`

Lemma: MultiTree-induction
`∀[T:Type]. ∀[P:MultiTree(T) ─→ ℙ].`
`  ((∀labels:{L:Atom List| 0 < ||L||} . ∀children:{a:Atom| (a ∈ labels)}  ─→ MultiTree(T).`
`      ((∀u:{a:Atom| (a ∈ labels)} . P[children u]) `` P[MTree_Node(labels;children)]))`
`  `` (∀val:T. P[MTree_Leaf(val)])`
`  `` {∀v:MultiTree(T). P[v]})`

Lemma: MultiTree-definition
`∀[T,A:Type]. ∀[R:A ─→ MultiTree(T) ─→ ℙ].`
`  ((∀labels:{L:Atom List| 0 < ||L||} . ∀children:{a:Atom| (a ∈ labels)}  ─→ MultiTree(T).`
`      ((∀u:{a:Atom| (a ∈ labels)} . {x:A| R[x;children u]} ) `` {x:A| R[x;MTree_Node(labels;children)]} ))`
`  `` (∀val:T. {x:A| R[x;MTree_Leaf(val)]} )`
`  `` {∀v:MultiTree(T). {x:A| R[x;v]} })`

Definition: MultiTree_ind
`MultiTree_ind(v;`
`              MTree_Node(labels,children)`` rec1.Node[labels; children; rec1];`
`              MTree_Leaf(val)`` Leaf[val])  ==`
`  fix((λMultiTree_ind,v. let lbl,v1 = v `
`                         in if lbl="Node" then let labels,v2 = v1 in Node[labels; v2; λu.(MultiTree_ind (v2 u))]`
`                            if lbl="Leaf" then Leaf[v1]`
`                            else ⊥`
`                            fi )) `
`  v`

Lemma: MultiTree_ind_wf
`∀[T,A:Type]. ∀[R:A ─→ MultiTree(T) ─→ ℙ]. ∀[v:MultiTree(T)]. ∀[Node:labels:{L:Atom List| 0 < ||L||} `
`                                                                    ─→ children:({a:Atom| (a ∈ labels)}  ─→ MultiTree(T)\000C)`
`                                                                    ─→ (u:{a:Atom| (a ∈ labels)}  ─→ {x:A| R[x;children \000Cu]} )`
`                                                                    ─→ {x:A| R[x;MTree_Node(labels;children)]} ].`
`∀[Leaf:val:T ─→ {x:A| R[x;MTree_Leaf(val)]} ].`
`  (MultiTree_ind(v;`
`                 MTree_Node(labels,children)`` rec1.Node[labels;children;rec1];`
`                 MTree_Leaf(val)`` Leaf[val])  ∈ {x:A| R[x;v]} )`

Lemma: MultiTree_ind_wf_simple
`∀[T,A:Type]. ∀[v:MultiTree(T)]. ∀[Node:labels:{L:Atom List| 0 < ||L||} `
`                                       ─→ children:({a:Atom| (a ∈ labels)}  ─→ MultiTree(T))`
`                                       ─→ (u:{a:Atom| (a ∈ labels)}  ─→ A)`
`                                       ─→ A]. ∀[Leaf:val:T ─→ A].`
`  (MultiTree_ind(v;`
`                 MTree_Node(labels,children)`` rec1.Node[labels;children;rec1];`
`                 MTree_Leaf(val)`` Leaf[val])  ∈ A)`

Definition: MTree-rank
`MTree-rank(t) ==`
`  fix((λMTree-rank,t. if MTree_Leaf?(t)`
`                     then 0`
`                     else imax-list(map(λa.(MTree-rank (MTree_Node-children(t) a));MTree_Node-labels(t))) + 1`
`                     fi )) `
`  t`

Lemma: MTree-rank_wf
`∀T:Type. ∀tr:MultiTree(T).  (MTree-rank(tr) ∈ ℕ)`

Lemma: MTree-induction2
`∀[T:Type]. ∀[P:MultiTree(T) ─→ ℙ].`
`  ((∀labels:{L:Atom List| 0 < ||L||} . ∀children:{a:Atom| (a ∈ labels)}  ─→ MultiTree(T).`
`      ((∀a∈labels.P[children a]) `` P[MTree_Node(labels;children)]))`
`  `` (∀val:T. P[MTree_Leaf(val)])`
`  `` {∀x:MultiTree(T). P[x]})`

Definition: MMTreeco
`MMTreeco(T) ==  corec(X.lbl:Atom × if lbl =a "Leaf" then T if lbl =a "Node" then X List List else Void fi )`

Lemma: MMTreeco_wf
`∀[T:Type]. (MMTreeco(T) ∈ Type)`

Lemma: MMTreeco-ext
`∀[T:Type]. MMTreeco(T) ≡ lbl:Atom × if lbl =a "Leaf" then T if lbl =a "Node" then MMTreeco(T) List List else Void fi `

Definition: MMTreeco_size
`MMTreeco_size(p) ==`
`  fix((λsize,p. let lbl,x = p `
`                in if lbl =a "Leaf" then 0`
`                   if lbl =a "Node" then 1 + Σ(Σ(size x[i][i1] | i1 < ||x[i]||) | i < ||x||)`
`                   else 0`
`                   fi )) `
`  p`

Lemma: MMTreeco_size_wf
`∀[T:Type]. ∀[p:MMTreeco(T)].  (MMTreeco_size(p) ∈ partial(ℕ))`

Definition: MMTree
`MMTree(T) ==  {p:MMTreeco(T)| (MMTreeco_size(p))↓} `

Lemma: MMTree_wf
`∀[T:Type]. (MMTree(T) ∈ Type)`

Definition: MMTree_size
`MMTree_size(p) ==`
`  fix((λsize,p. let lbl,x = p `
`                in if lbl =a "Leaf" then 0`
`                   if lbl =a "Node" then 1 + Σ(Σ(size x[i][i1] | i1 < ||x[i]||) | i < ||x||)`
`                   else 0`
`                   fi )) `
`  p`

Lemma: MMTree_size_wf
`∀[T:Type]. ∀[p:MMTree(T)].  (MMTree_size(p) ∈ ℕ)`

Lemma: MMTree-ext
`∀[T:Type]. MMTree(T) ≡ lbl:Atom × if lbl =a "Leaf" then T if lbl =a "Node" then MMTree(T) List List else Void fi `

Definition: MMTree_Leaf
`MMTree_Leaf(val) ==  <"Leaf", val>`

Lemma: MMTree_Leaf_wf
`∀[T:Type]. ∀[val:T].  (MMTree_Leaf(val) ∈ MMTree(T))`

Definition: MMTree_Node
`MMTree_Node(forest) ==  <"Node", forest>`

Lemma: MMTree_Node_wf
`∀[T:Type]. ∀[forest:MMTree(T) List List].  (MMTree_Node(forest) ∈ MMTree(T))`

Definition: MMTree_Leaf?
`MMTree_Leaf?(v) ==  fst(v) =a "Leaf"`

Lemma: MMTree_Leaf?_wf
`∀[T:Type]. ∀[v:MMTree(T)].  (MMTree_Leaf?(v) ∈ 𝔹)`

Definition: MMTree_Leaf-val
`MMTree_Leaf-val(v) ==  snd(v)`

Lemma: MMTree_Leaf-val_wf
`∀[T:Type]. ∀[v:MMTree(T)].  MMTree_Leaf-val(v) ∈ T supposing ↑MMTree_Leaf?(v)`

Definition: MMTree_Node?
`MMTree_Node?(v) ==  fst(v) =a "Node"`

Lemma: MMTree_Node?_wf
`∀[T:Type]. ∀[v:MMTree(T)].  (MMTree_Node?(v) ∈ 𝔹)`

Definition: MMTree_Node-forest
`MMTree_Node-forest(v) ==  snd(v)`

Lemma: MMTree_Node-forest_wf
`∀[T:Type]. ∀[v:MMTree(T)].  MMTree_Node-forest(v) ∈ MMTree(T) List List supposing ↑MMTree_Node?(v)`

Lemma: MMTree-induction
`∀[T:Type]. ∀[P:MMTree(T) ─→ ℙ].`
`  ((∀val:T. P[MMTree_Leaf(val)])`
`  `` (∀forest:MMTree(T) List List. ((∀u∈forest.(∀u1∈u.P[u1])) `` P[MMTree_Node(forest)]))`
`  `` {∀v:MMTree(T). P[v]})`

Lemma: MMTree-definition
`∀[T,A:Type]. ∀[R:A ─→ MMTree(T) ─→ ℙ].`
`  ((∀val:T. {x:A| R[x;MMTree_Leaf(val)]} )`
`  `` (∀forest:MMTree(T) List List. ((∀u∈forest.(∀u1∈u.{x:A| R[x;u1]} )) `` {x:A| R[x;MMTree_Node(forest)]} ))`
`  `` {∀v:MMTree(T). {x:A| R[x;v]} })`

Definition: MMTree-rank
`MMTree-rank(t) ==`
`  fix((λMMTree-rank,t. if MMTree_Leaf?(t)`
`                      then 0`
`                      else imax-list([0 / map(λl.imax-list([0 / map(λs.(MMTree-rank s);l)]);MMTree_Node-forest(t))])`
`                      fi )) `
`  t`

Lemma: MMTree-rank_wf
`∀T:Type. ∀t:MMTree(T).  (MMTree-rank(t) ∈ ℕ)`

Definition: RankEx1co
`RankEx1co(T) ==`
`  corec(X.lbl:Atom × if lbl =a "Leaf" then T`
`                     if lbl =a "Prod" then X × X`
`                     if lbl =a "ProdL" then T × X`
`                     if lbl =a "ProdR" then X × T`
`                     if lbl =a "List" then X List`
`                     else Void`
`                     fi )`

Lemma: RankEx1co_wf
`∀[T:Type]. (RankEx1co(T) ∈ Type)`

Lemma: RankEx1co-ext
`∀[T:Type]`
`  RankEx1co(T) ≡ lbl:Atom × if lbl =a "Leaf" then T`
`                            if lbl =a "Prod" then RankEx1co(T) × RankEx1co(T)`
`                            if lbl =a "ProdL" then T × RankEx1co(T)`
`                            if lbl =a "ProdR" then RankEx1co(T) × T`
`                            if lbl =a "List" then RankEx1co(T) List`
`                            else Void`
`                            fi `

Definition: RankEx1co_size
`RankEx1co_size(p) ==`
`  fix((λsize,p. let lbl,x = p `
`                in if lbl =a "Leaf" then 0`
`                   if lbl =a "Prod" then 1 + (size (fst(x))) + (size (snd(x)))`
`                   if lbl =a "ProdL" then 1 + (size (snd(x)))`
`                   if lbl =a "ProdR" then 1 + (size (fst(x)))`
`                   if lbl =a "List" then 1 + Σ(size x[i] | i < ||x||)`
`                   else 0`
`                   fi )) `
`  p`

Lemma: RankEx1co_size_wf
`∀[T:Type]. ∀[p:RankEx1co(T)].  (RankEx1co_size(p) ∈ partial(ℕ))`

Definition: RankEx1
`RankEx1(T) ==  {p:RankEx1co(T)| (RankEx1co_size(p))↓} `

Lemma: RankEx1_wf
`∀[T:Type]. (RankEx1(T) ∈ Type)`

Definition: RankEx1_size
`RankEx1_size(p) ==`
`  fix((λsize,p. let lbl,x = p `
`                in if lbl =a "Leaf" then 0`
`                   if lbl =a "Prod" then 1 + (size (fst(x))) + (size (snd(x)))`
`                   if lbl =a "ProdL" then 1 + (size (snd(x)))`
`                   if lbl =a "ProdR" then 1 + (size (fst(x)))`
`                   if lbl =a "List" then 1 + Σ(size x[i] | i < ||x||)`
`                   else 0`
`                   fi )) `
`  p`

Lemma: RankEx1_size_wf
`∀[T:Type]. ∀[p:RankEx1(T)].  (RankEx1_size(p) ∈ ℕ)`

Lemma: RankEx1-ext
`∀[T:Type]`
`  RankEx1(T) ≡ lbl:Atom × if lbl =a "Leaf" then T`
`                          if lbl =a "Prod" then RankEx1(T) × RankEx1(T)`
`                          if lbl =a "ProdL" then T × RankEx1(T)`
`                          if lbl =a "ProdR" then RankEx1(T) × T`
`                          if lbl =a "List" then RankEx1(T) List`
`                          else Void`
`                          fi `

Definition: RankEx1_Leaf
`RankEx1_Leaf(leaf) ==  <"Leaf", leaf>`

Lemma: RankEx1_Leaf_wf
`∀[T:Type]. ∀[leaf:T].  (RankEx1_Leaf(leaf) ∈ RankEx1(T))`

Definition: RankEx1_Prod
`RankEx1_Prod(prod) ==  <"Prod", prod>`

Lemma: RankEx1_Prod_wf
`∀[T:Type]. ∀[prod:RankEx1(T) × RankEx1(T)].  (RankEx1_Prod(prod) ∈ RankEx1(T))`

Definition: RankEx1_ProdL
`RankEx1_ProdL(prodl) ==  <"ProdL", prodl>`

Lemma: RankEx1_ProdL_wf
`∀[T:Type]. ∀[prodl:T × RankEx1(T)].  (RankEx1_ProdL(prodl) ∈ RankEx1(T))`

Definition: RankEx1_ProdR
`RankEx1_ProdR(prodr) ==  <"ProdR", prodr>`

Lemma: RankEx1_ProdR_wf
`∀[T:Type]. ∀[prodr:RankEx1(T) × T].  (RankEx1_ProdR(prodr) ∈ RankEx1(T))`

Definition: RankEx1_List
`RankEx1_List(list) ==  <"List", list>`

Lemma: RankEx1_List_wf
`∀[T:Type]. ∀[list:RankEx1(T) List].  (RankEx1_List(list) ∈ RankEx1(T))`

Definition: RankEx1_Leaf?
`RankEx1_Leaf?(v) ==  fst(v) =a "Leaf"`

Lemma: RankEx1_Leaf?_wf
`∀[T:Type]. ∀[v:RankEx1(T)].  (RankEx1_Leaf?(v) ∈ 𝔹)`

Definition: RankEx1_Leaf-leaf
`RankEx1_Leaf-leaf(v) ==  snd(v)`

Lemma: RankEx1_Leaf-leaf_wf
`∀[T:Type]. ∀[v:RankEx1(T)].  RankEx1_Leaf-leaf(v) ∈ T supposing ↑RankEx1_Leaf?(v)`

Definition: RankEx1_Prod?
`RankEx1_Prod?(v) ==  fst(v) =a "Prod"`

Lemma: RankEx1_Prod?_wf
`∀[T:Type]. ∀[v:RankEx1(T)].  (RankEx1_Prod?(v) ∈ 𝔹)`

Definition: RankEx1_Prod-prod
`RankEx1_Prod-prod(v) ==  snd(v)`

Lemma: RankEx1_Prod-prod_wf
`∀[T:Type]. ∀[v:RankEx1(T)].  RankEx1_Prod-prod(v) ∈ RankEx1(T) × RankEx1(T) supposing ↑RankEx1_Prod?(v)`

Definition: RankEx1_ProdL?
`RankEx1_ProdL?(v) ==  fst(v) =a "ProdL"`

Lemma: RankEx1_ProdL?_wf
`∀[T:Type]. ∀[v:RankEx1(T)].  (RankEx1_ProdL?(v) ∈ 𝔹)`

Definition: RankEx1_ProdL-prodl
`RankEx1_ProdL-prodl(v) ==  snd(v)`

Lemma: RankEx1_ProdL-prodl_wf
`∀[T:Type]. ∀[v:RankEx1(T)].  RankEx1_ProdL-prodl(v) ∈ T × RankEx1(T) supposing ↑RankEx1_ProdL?(v)`

Definition: RankEx1_ProdR?
`RankEx1_ProdR?(v) ==  fst(v) =a "ProdR"`

Lemma: RankEx1_ProdR?_wf
`∀[T:Type]. ∀[v:RankEx1(T)].  (RankEx1_ProdR?(v) ∈ 𝔹)`

Definition: RankEx1_ProdR-prodr
`RankEx1_ProdR-prodr(v) ==  snd(v)`

Lemma: RankEx1_ProdR-prodr_wf
`∀[T:Type]. ∀[v:RankEx1(T)].  RankEx1_ProdR-prodr(v) ∈ RankEx1(T) × T supposing ↑RankEx1_ProdR?(v)`

Definition: RankEx1_List?
`RankEx1_List?(v) ==  fst(v) =a "List"`

Lemma: RankEx1_List?_wf
`∀[T:Type]. ∀[v:RankEx1(T)].  (RankEx1_List?(v) ∈ 𝔹)`

Definition: RankEx1_List-list
`RankEx1_List-list(v) ==  snd(v)`

Lemma: RankEx1_List-list_wf
`∀[T:Type]. ∀[v:RankEx1(T)].  RankEx1_List-list(v) ∈ RankEx1(T) List supposing ↑RankEx1_List?(v)`

Lemma: RankEx1-induction
`∀[T:Type]. ∀[P:RankEx1(T) ─→ ℙ].`
`  ((∀leaf:T. P[RankEx1_Leaf(leaf)])`
`  `` (∀prod:RankEx1(T) × RankEx1(T). (let u,u1 = prod in P[u] ∧ P[u1] `` P[RankEx1_Prod(prod)]))`
`  `` (∀prodl:T × RankEx1(T). (let u,u1 = prodl in P[u1] `` P[RankEx1_ProdL(prodl)]))`
`  `` (∀prodr:RankEx1(T) × T. (let u,u1 = prodr in P[u] `` P[RankEx1_ProdR(prodr)]))`
`  `` (∀list:RankEx1(T) List. ((∀u∈list.P[u]) `` P[RankEx1_List(list)]))`
`  `` {∀v:RankEx1(T). P[v]})`

Lemma: RankEx1-definition
`∀[T,A:Type]. ∀[R:A ─→ RankEx1(T) ─→ ℙ].`
`  ((∀leaf:T. {x:A| R[x;RankEx1_Leaf(leaf)]} )`
`  `` (∀prod:RankEx1(T) × RankEx1(T)`
`        (let u,u1 = prod in {x:A| R[x;u]}  ∧ {x:A| R[x;u1]}  `` {x:A| R[x;RankEx1_Prod(prod)]} ))`
`  `` (∀prodl:T × RankEx1(T). (let u,u1 = prodl in {x:A| R[x;u1]}  `` {x:A| R[x;RankEx1_ProdL(prodl)]} ))`
`  `` (∀prodr:RankEx1(T) × T. (let u,u1 = prodr in {x:A| R[x;u]}  `` {x:A| R[x;RankEx1_ProdR(prodr)]} ))`
`  `` (∀list:RankEx1(T) List. ((∀u∈list.{x:A| R[x;u]} ) `` {x:A| R[x;RankEx1_List(list)]} ))`
`  `` {∀v:RankEx1(T). {x:A| R[x;v]} })`

Definition: RankEx1_ind
`RankEx1_ind(v;`
`            RankEx1_Leaf(leaf)`` Leaf[leaf];`
`            RankEx1_Prod(prod)`` rec1.Prod[prod; rec1];`
`            RankEx1_ProdL(prodl)`` rec2.ProdL[prodl; rec2];`
`            RankEx1_ProdR(prodr)`` rec3.ProdR[prodr; rec3];`
`            RankEx1_List(list)`` rec4.List[list; rec4])  ==`
`  fix((λRankEx1_ind,v. let lbl,v1 = v `
`                       in if lbl="Leaf" then Leaf[v1]`
`                          if lbl="Prod" then let v2,v3 = v1 in Prod[<v2, v3>; <RankEx1_ind v2, RankEx1_ind v3>]`
`                          if lbl="ProdL" then let v2,v3 = v1 in ProdL[<v2, v3>; RankEx1_ind v3]`
`                          if lbl="ProdR" then let v2,v3 = v1 in ProdR[<v2, v3>; RankEx1_ind v2]`
`                          if lbl="List" then List[v1; λi.(RankEx1_ind v1[i])]`
`                          else ⊥`
`                          fi )) `
`  v`

Lemma: RankEx1_ind_wf
`∀[T,A:Type]. ∀[R:A ─→ RankEx1(T) ─→ ℙ]. ∀[v:RankEx1(T)]. ∀[Leaf:leaf:T ─→ {x:A| R[x;RankEx1_Leaf(leaf)]} ].`
`∀[Prod:prod:(RankEx1(T) × RankEx1(T))`
`       ─→ let u,u1 = prod `
`          in {x:A| R[x;u]}  ∧ {x:A| R[x;u1]} `
`       ─→ {x:A| R[x;RankEx1_Prod(prod)]} ]. ∀[ProdL:prodl:(T × RankEx1(T))`
`                                                   ─→ let u,u1 = prodl `
`                                                      in {x:A| R[x;u1]} `
`                                                   ─→ {x:A| R[x;RankEx1_ProdL(prodl)]} ].`
`∀[ProdR:prodr:(RankEx1(T) × T) ─→ let u,u1 = prodr in {x:A| R[x;u]}  ─→ {x:A| R[x;RankEx1_ProdR(prodr)]} ].`
`∀[List:list:(RankEx1(T) List) ─→ (∀u∈list.{x:A| R[x;u]} ) ─→ {x:A| R[x;RankEx1_List(list)]} ].`
`  (RankEx1_ind(v;`
`               RankEx1_Leaf(leaf)`` Leaf[leaf];`
`               RankEx1_Prod(prod)`` rec1.Prod[prod;rec1];`
`               RankEx1_ProdL(prodl)`` rec2.ProdL[prodl;rec2];`
`               RankEx1_ProdR(prodr)`` rec3.ProdR[prodr;rec3];`
`               RankEx1_List(list)`` rec4.List[list;rec4])  ∈ {x:A| R[x;v]} )`

Lemma: RankEx1_ind_wf_simple
`∀[T,A:Type]. ∀[v:RankEx1(T)]. ∀[Leaf:leaf:T ─→ A]. ∀[Prod:prod:(RankEx1(T) × RankEx1(T))`
`                                                          ─→ let u,u1 = prod `
`                                                             in A ∧ A`
`                                                          ─→ A]. ∀[ProdL:prodl:(T × RankEx1(T))`
`                                                                         ─→ let u,u1 = prodl `
`                                                                            in A`
`                                                                         ─→ A]. ∀[ProdR:prodr:(RankEx1(T) × T)`
`                                                                                        ─→ let u,u1 = prodr `
`                                                                                           in A`
`                                                                                        ─→ A].`
`∀[List:list:(RankEx1(T) List) ─→ (∀u∈list.A) ─→ A].`
`  (RankEx1_ind(v;`
`               RankEx1_Leaf(leaf)`` Leaf[leaf];`
`               RankEx1_Prod(prod)`` rec1.Prod[prod;rec1];`
`               RankEx1_ProdL(prodl)`` rec2.ProdL[prodl;rec2];`
`               RankEx1_ProdR(prodr)`` rec3.ProdR[prodr;rec3];`
`               RankEx1_List(list)`` rec4.List[list;rec4])  ∈ A)`

Definition: rank-Ex1
`rank-Ex1(t) ==`
`  fix((λrank-Ex1,t. if RankEx1_Leaf?(t) then 1`
`                   if RankEx1_Prod?(t)`
`                     then imax(rank-Ex1 (fst(RankEx1_Prod-prod(t)));rank-Ex1 (snd(RankEx1_Prod-prod(t)))) + 1`
`                   if RankEx1_ProdL?(t) then (rank-Ex1 (snd(RankEx1_ProdL-prodl(t)))) + 1`
`                   if RankEx1_ProdR?(t) then (rank-Ex1 (fst(RankEx1_ProdR-prodr(t)))) + 1`
`                   else imax-list([0 / map(λu.(rank-Ex1 u);RankEx1_List-list(t))]) + 1`
`                   fi )) `
`  t`

Lemma: rank-Ex1_wf
`∀[T:Type]. ∀[t:RankEx1(T)].  (rank-Ex1(t) ∈ ℕ)`

Definition: RankEx2co
`RankEx2co(S;T) ==`
`  corec(X.lbl:Atom × if lbl =a "LeafT" then T`
`                     if lbl =a "LeafS" then S`
`                     if lbl =a "Prod" then X × S × T`
`                     if lbl =a "Union" then S × X + X`
`                     if lbl =a "ListProd" then (S × X) List`
`                     if lbl =a "UnionList" then T + (X List)`
`                     else Void`
`                     fi )`

Lemma: RankEx2co_wf
`∀[S,T:Type].  (RankEx2co(S;T) ∈ Type)`

Lemma: RankEx2co-ext
`∀[S,T:Type].`
`  RankEx2co(S;T) ≡ lbl:Atom × if lbl =a "LeafT" then T`
`                              if lbl =a "LeafS" then S`
`                              if lbl =a "Prod" then RankEx2co(S;T) × S × T`
`                              if lbl =a "Union" then S × RankEx2co(S;T) + RankEx2co(S;T)`
`                              if lbl =a "ListProd" then (S × RankEx2co(S;T)) List`
`                              if lbl =a "UnionList" then T + (RankEx2co(S;T) List)`
`                              else Void`
`                              fi `

Definition: RankEx2co_size
`RankEx2co_size(p) ==`
`  fix((λsize,p. let lbl,x = p `
`                in if lbl =a "LeafT" then 0`
`                   if lbl =a "LeafS" then 0`
`                   if lbl =a "Prod" then 1 + (size (fst(fst(x))))`
`                   if lbl =a "Union" then 1 + case x of inl(a) => size (snd(a)) | inr(b) => size b`
`                   if lbl =a "ListProd" then 1 + Σ(size (snd(x[i])) | i < ||x||)`
`                   if lbl =a "UnionList" then 1 + case x of inl(a) => 0 | inr(b) => Σ(size b[i] | i < ||b||)`
`                   else 0`
`                   fi )) `
`  p`

Lemma: RankEx2co_size_wf
`∀[S,T:Type]. ∀[p:RankEx2co(S;T)].  (RankEx2co_size(p) ∈ partial(ℕ))`

Definition: RankEx2
`RankEx2(S;T) ==  {p:RankEx2co(S;T)| (RankEx2co_size(p))↓} `

Lemma: RankEx2_wf
`∀[S,T:Type].  (RankEx2(S;T) ∈ Type)`

Definition: RankEx2_size
`RankEx2_size(p) ==`
`  fix((λsize,p. let lbl,x = p `
`                in if lbl =a "LeafT" then 0`
`                   if lbl =a "LeafS" then 0`
`                   if lbl =a "Prod" then 1 + (size (fst(fst(x))))`
`                   if lbl =a "Union" then 1 + case x of inl(a) => size (snd(a)) | inr(b) => size b`
`                   if lbl =a "ListProd" then 1 + Σ(size (snd(x[i])) | i < ||x||)`
`                   if lbl =a "UnionList" then 1 + case x of inl(a) => 0 | inr(b) => Σ(size b[i] | i < ||b||)`
`                   else 0`
`                   fi )) `
`  p`

Lemma: RankEx2_size_wf
`∀[S,T:Type]. ∀[p:RankEx2(S;T)].  (RankEx2_size(p) ∈ ℕ)`

Lemma: RankEx2-ext
`∀[S,T:Type].`
`  RankEx2(S;T) ≡ lbl:Atom × if lbl =a "LeafT" then T`
`                            if lbl =a "LeafS" then S`
`                            if lbl =a "Prod" then RankEx2(S;T) × S × T`
`                            if lbl =a "Union" then S × RankEx2(S;T) + RankEx2(S;T)`
`                            if lbl =a "ListProd" then (S × RankEx2(S;T)) List`
`                            if lbl =a "UnionList" then T + (RankEx2(S;T) List)`
`                            else Void`
`                            fi `

Definition: RankEx2_LeafT
`RankEx2_LeafT(leaft) ==  <"LeafT", leaft>`

Lemma: RankEx2_LeafT_wf
`∀[S,T:Type]. ∀[leaft:T].  (RankEx2_LeafT(leaft) ∈ RankEx2(S;T))`

Definition: RankEx2_LeafS
`RankEx2_LeafS(leafs) ==  <"LeafS", leafs>`

Lemma: RankEx2_LeafS_wf
`∀[S,T:Type]. ∀[leafs:S].  (RankEx2_LeafS(leafs) ∈ RankEx2(S;T))`

Definition: RankEx2_Prod
`RankEx2_Prod(prod) ==  <"Prod", prod>`

Lemma: RankEx2_Prod_wf
`∀[S,T:Type]. ∀[prod:RankEx2(S;T) × S × T].  (RankEx2_Prod(prod) ∈ RankEx2(S;T))`

Definition: RankEx2_Union
`RankEx2_Union(union) ==  <"Union", union>`

Lemma: RankEx2_Union_wf
`∀[S,T:Type]. ∀[union:S × RankEx2(S;T) + RankEx2(S;T)].  (RankEx2_Union(union) ∈ RankEx2(S;T))`

Definition: RankEx2_ListProd
`RankEx2_ListProd(listprod) ==  <"ListProd", listprod>`

Lemma: RankEx2_ListProd_wf
`∀[S,T:Type]. ∀[listprod:(S × RankEx2(S;T)) List].  (RankEx2_ListProd(listprod) ∈ RankEx2(S;T))`

Definition: RankEx2_UnionList
`RankEx2_UnionList(unionlist) ==  <"UnionList", unionlist>`

Lemma: RankEx2_UnionList_wf
`∀[S,T:Type]. ∀[unionlist:T + (RankEx2(S;T) List)].  (RankEx2_UnionList(unionlist) ∈ RankEx2(S;T))`

Definition: RankEx2_LeafT?
`RankEx2_LeafT?(v) ==  fst(v) =a "LeafT"`

Lemma: RankEx2_LeafT?_wf
`∀[S,T:Type]. ∀[v:RankEx2(S;T)].  (RankEx2_LeafT?(v) ∈ 𝔹)`

Definition: RankEx2_LeafT-leaft
`RankEx2_LeafT-leaft(v) ==  snd(v)`

Lemma: RankEx2_LeafT-leaft_wf
`∀[S,T:Type]. ∀[v:RankEx2(S;T)].  RankEx2_LeafT-leaft(v) ∈ T supposing ↑RankEx2_LeafT?(v)`

Definition: RankEx2_LeafS?
`RankEx2_LeafS?(v) ==  fst(v) =a "LeafS"`

Lemma: RankEx2_LeafS?_wf
`∀[S,T:Type]. ∀[v:RankEx2(S;T)].  (RankEx2_LeafS?(v) ∈ 𝔹)`

Definition: RankEx2_LeafS-leafs
`RankEx2_LeafS-leafs(v) ==  snd(v)`

Lemma: RankEx2_LeafS-leafs_wf
`∀[S,T:Type]. ∀[v:RankEx2(S;T)].  RankEx2_LeafS-leafs(v) ∈ S supposing ↑RankEx2_LeafS?(v)`

Definition: RankEx2_Prod?
`RankEx2_Prod?(v) ==  fst(v) =a "Prod"`

Lemma: RankEx2_Prod?_wf
`∀[S,T:Type]. ∀[v:RankEx2(S;T)].  (RankEx2_Prod?(v) ∈ 𝔹)`

Definition: RankEx2_Prod-prod
`RankEx2_Prod-prod(v) ==  snd(v)`

Lemma: RankEx2_Prod-prod_wf
`∀[S,T:Type]. ∀[v:RankEx2(S;T)].  RankEx2_Prod-prod(v) ∈ RankEx2(S;T) × S × T supposing ↑RankEx2_Prod?(v)`

Definition: RankEx2_Union?
`RankEx2_Union?(v) ==  fst(v) =a "Union"`

Lemma: RankEx2_Union?_wf
`∀[S,T:Type]. ∀[v:RankEx2(S;T)].  (RankEx2_Union?(v) ∈ 𝔹)`

Definition: RankEx2_Union-union
`RankEx2_Union-union(v) ==  snd(v)`

Lemma: RankEx2_Union-union_wf
`∀[S,T:Type]. ∀[v:RankEx2(S;T)].  RankEx2_Union-union(v) ∈ S × RankEx2(S;T) + RankEx2(S;T) supposing ↑RankEx2_Union?(v)`

Definition: RankEx2_ListProd?
`RankEx2_ListProd?(v) ==  fst(v) =a "ListProd"`

Lemma: RankEx2_ListProd?_wf
`∀[S,T:Type]. ∀[v:RankEx2(S;T)].  (RankEx2_ListProd?(v) ∈ 𝔹)`

Definition: RankEx2_ListProd-listprod
`RankEx2_ListProd-listprod(v) ==  snd(v)`

Lemma: RankEx2_ListProd-listprod_wf
`∀[S,T:Type]. ∀[v:RankEx2(S;T)].  RankEx2_ListProd-listprod(v) ∈ (S × RankEx2(S;T)) List supposing ↑RankEx2_ListProd?(v)`

Definition: RankEx2_UnionList?
`RankEx2_UnionList?(v) ==  fst(v) =a "UnionList"`

Lemma: RankEx2_UnionList?_wf
`∀[S,T:Type]. ∀[v:RankEx2(S;T)].  (RankEx2_UnionList?(v) ∈ 𝔹)`

Definition: RankEx2_UnionList-unionlist
`RankEx2_UnionList-unionlist(v) ==  snd(v)`

Lemma: RankEx2_UnionList-unionlist_wf
`∀[S,T:Type]. ∀[v:RankEx2(S;T)].`
`  RankEx2_UnionList-unionlist(v) ∈ T + (RankEx2(S;T) List) supposing ↑RankEx2_UnionList?(v)`

Lemma: RankEx2-induction
`∀[S,T:Type]. ∀[P:RankEx2(S;T) ─→ ℙ].`
`  ((∀leaft:T. P[RankEx2_LeafT(leaft)])`
`  `` (∀leafs:S. P[RankEx2_LeafS(leafs)])`
`  `` (∀prod:RankEx2(S;T) × S × T. (let u,u1 = prod in let u1,u2 = u in P[u1] `` P[RankEx2_Prod(prod)]))`
`  `` (∀union:S × RankEx2(S;T) + RankEx2(S;T)`
`        (case union of inl(u) => let u1,u2 = u in P[u2] | inr(u1) => P[u1] `` P[RankEx2_Union(union)]))`
`  `` (∀listprod:(S × RankEx2(S;T)) List. ((∀u∈listprod.let u1,u2 = u in P[u2]) `` P[RankEx2_ListProd(listprod)]))`
`  `` (∀unionlist:T + (RankEx2(S;T) List)`
`        (case unionlist of inl(u) => True | inr(u1) => (∀u∈u1.P[u]) `` P[RankEx2_UnionList(unionlist)]))`
`  `` {∀v:RankEx2(S;T). P[v]})`

Lemma: RankEx2-definition
`∀[S,T,A:Type]. ∀[R:A ─→ RankEx2(S;T) ─→ ℙ].`
`  ((∀leaft:T. {x:A| R[x;RankEx2_LeafT(leaft)]} )`
`  `` (∀leafs:S. {x:A| R[x;RankEx2_LeafS(leafs)]} )`
`  `` (∀prod:RankEx2(S;T) × S × T`
`        (let u,u1 = prod in let u1,u2 = u in {x:A| R[x;u1]}  `` {x:A| R[x;RankEx2_Prod(prod)]} ))`
`  `` (∀union:S × RankEx2(S;T) + RankEx2(S;T)`
`        (case union of inl(u) => let u1,u2 = u in {x:A| R[x;u2]}  | inr(u1) => {x:A| R[x;u1]} `
`        `` {x:A| R[x;RankEx2_Union(union)]} ))`
`  `` (∀listprod:(S × RankEx2(S;T)) List`
`        ((∀u∈listprod.let u1,u2 = u in {x:A| R[x;u2]} ) `` {x:A| R[x;RankEx2_ListProd(listprod)]} ))`
`  `` (∀unionlist:T + (RankEx2(S;T) List)`
`        (case unionlist of inl(u) => True | inr(u1) => (∀u∈u1.{x:A| R[x;u]} ) `` {x:A| R[x;RankEx2_UnionList(unionlist)]\000C} ))`
`  `` {∀v:RankEx2(S;T). {x:A| R[x;v]} })`

Definition: RankEx2_ind
`RankEx2_ind(v;`
`            RankEx2_LeafT(leaft)`` LeafT[leaft];`
`            RankEx2_LeafS(leafs)`` LeafS[leafs];`
`            RankEx2_Prod(prod)`` rec1.Prod[prod; rec1];`
`            RankEx2_Union(union)`` rec2.Union[union; rec2];`
`            RankEx2_ListProd(listprod)`` rec3.ListProd[listprod; rec3];`
`            RankEx2_UnionList(unionlist)`` rec4.UnionList[unionlist; rec4])  ==`
`  fix((λRankEx2_ind,v. let lbl,v1 = v `
`                       in if lbl="LeafT" then LeafT[v1]`
`                          if lbl="LeafS" then LeafS[v1]`
`                          if lbl="Prod" then let v2,v3 = v1 in let v4,v5 = v2 in Prod[<<v4, v5>, v3>; RankEx2_ind v4]`
`                          if lbl="Union"`
`                            then case v1`
`                                  of inl(x) =>`
`                                  let x1,x2 = x `
`                                  in Union[inl <x1, x2>; RankEx2_ind x2]`
`                                  | inr(y) =>`
`                                  Union[inr y ; RankEx2_ind y]`
`                          if lbl="ListProd" then ListProd[v1; λi.let v2,v3 = v1[i] in RankEx2_ind v3]`
`                          if lbl="UnionList"`
`                            then case v1`
`                                  of inl(x) =>`
`                                  UnionList[inl x; Ax]`
`                                  | inr(y) =>`
`                                  UnionList[inr y ; λi.(RankEx2_ind y[i])]`
`                          else ⊥`
`                          fi )) `
`  v`

Lemma: RankEx2_ind_wf
`∀[S,T,A:Type]. ∀[R:A ─→ RankEx2(S;T) ─→ ℙ]. ∀[v:RankEx2(S;T)]. ∀[LeafT:leaft:T ─→ {x:A| R[x;RankEx2_LeafT(leaft)]} ].`
`∀[LeafS:leafs:S ─→ {x:A| R[x;RankEx2_LeafS(leafs)]} ]. ∀[Prod:prod:(RankEx2(S;T) × S × T)`
`                                                             ─→ let u,u1 = prod `
`                                                                in let u1,u2 = u `
`                                                                   in {x:A| R[x;u1]} `
`                                                             ─→ {x:A| R[x;RankEx2_Prod(prod)]} ].`
`∀[Union:union:(S × RankEx2(S;T) + RankEx2(S;T))`
`        ─→ case union of inl(u) => let u1,u2 = u in {x:A| R[x;u2]}  | inr(u1) => {x:A| R[x;u1]} `
`        ─→ {x:A| R[x;RankEx2_Union(union)]} ]. ∀[ListProd:listprod:((S × RankEx2(S;T)) List)`
`                                                         ─→ (∀u∈listprod.let u1,u2 = u `
`                                                                         in {x:A| R[x;u2]} )`
`                                                         ─→ {x:A| R[x;RankEx2_ListProd(listprod)]} ].`
`∀[UnionList:unionlist:(T + (RankEx2(S;T) List))`
`            ─→ case unionlist of inl(u) => True | inr(u1) => (∀u∈u1.{x:A| R[x;u]} )`
`            ─→ {x:A| R[x;RankEx2_UnionList(unionlist)]} ].`
`  (RankEx2_ind(v;`
`               RankEx2_LeafT(leaft)`` LeafT[leaft];`
`               RankEx2_LeafS(leafs)`` LeafS[leafs];`
`               RankEx2_Prod(prod)`` rec1.Prod[prod;rec1];`
`               RankEx2_Union(union)`` rec2.Union[union;rec2];`
`               RankEx2_ListProd(listprod)`` rec3.ListProd[listprod;rec3];`
`               RankEx2_UnionList(unionlist)`` rec4.UnionList[unionlist;rec4])  ∈ {x:A| R[x;v]} )`

Lemma: RankEx2_ind_wf_simple
`∀[S,T,A:Type]. ∀[v:RankEx2(S;T)]. ∀[LeafT:leaft:T ─→ A]. ∀[LeafS:leafs:S ─→ A]. ∀[Prod:prod:(RankEx2(S;T) × S × T)`
`                                                                                       ─→ let u,u1 = prod `
`                                                                                          in let u1,u2 = u `
`                                                                                             in A`
`                                                                                       ─→ A].`
`∀[Union:union:(S × RankEx2(S;T) + RankEx2(S;T)) ─→ case union of inl(u) => let u1,u2 = u in A | inr(u1) => A ─→ A].`
`∀[ListProd:listprod:((S × RankEx2(S;T)) List) ─→ (∀u∈listprod.let u1,u2 = u in A) ─→ A].`
`∀[UnionList:unionlist:(T + (RankEx2(S;T) List)) ─→ case unionlist of inl(u) => True | inr(u1) => (∀u∈u1.A) ─→ A].`
`  (RankEx2_ind(v;`
`               RankEx2_LeafT(leaft)`` LeafT[leaft];`
`               RankEx2_LeafS(leafs)`` LeafS[leafs];`
`               RankEx2_Prod(prod)`` rec1.Prod[prod;rec1];`
`               RankEx2_Union(union)`` rec2.Union[union;rec2];`
`               RankEx2_ListProd(listprod)`` rec3.ListProd[listprod;rec3];`
`               RankEx2_UnionList(unionlist)`` rec4.UnionList[unionlist;rec4])  ∈ A)`

Lemma: RankEx2_ind-unroll
`∀[S,T,A:Type]. ∀[R:A ─→ RankEx2(S;T) ─→ ℙ]. ∀[LeafT,LeafS,Prod,Union,ListProd,UnionList:Top]. ∀[t:RankEx2(S;T)].`
`  (RankEx2_ind(t;`
`               RankEx2_LeafT(leaft)`` LeafT[leaft];`
`               RankEx2_LeafS(leafs)`` LeafS[leafs];`
`               RankEx2_Prod(prod)`` rec1.Prod[prod;rec1];`
`               RankEx2_Union(union)`` rec2.Union[union;rec2];`
`               RankEx2_ListProd(listprod)`` rec3.ListProd[listprod;rec3];`
`               RankEx2_UnionList(unionlist)`` rec4.UnionList[unionlist;rec4])  `
`  ~ let F = λt.RankEx2_ind(t;`
`                           RankEx2_LeafT(leaft)`` LeafT[leaft];`
`                           RankEx2_LeafS(leafs)`` LeafS[leafs];`
`                           RankEx2_Prod(prod)`` rec1.Prod[prod;rec1];`
`                           RankEx2_Union(union)`` rec2.Union[union;rec2];`
`                           RankEx2_ListProd(listprod)`` rec3.ListProd[listprod;rec3];`
`                           RankEx2_UnionList(unionlist)`` rec4.UnionList[unionlist;rec4])  in`
`        if RankEx2_LeafT?(t) then LeafT RankEx2_LeafT-leaft(t)`
`        if RankEx2_LeafS?(t) then LeafS RankEx2_LeafS-leafs(t)`
`        if RankEx2_Prod?(t) then Prod RankEx2_Prod-prod(t) (F (fst(fst(RankEx2_Prod-prod(t)))))`
`        if RankEx2_Union?(t)`
`          then Union RankEx2_Union-union(t) `
`               case RankEx2_Union-union(t) of inl(x) => let x1,x2 = x in F x2 | inr(y) => F y`
`        if RankEx2_ListProd?(t)`
`          then ListProd RankEx2_ListProd-listprod(t) (λi.let u2,u3 = RankEx2_ListProd-listprod(t)[i] in F u3)`
`        else UnionList RankEx2_UnionList-unionlist(t) `
`             case RankEx2_UnionList-unionlist(t) of inl(x) => Ax | inr(y) => λi.(F y[i])`
`        fi )`

Lemma: RankEx2-defop
`∀[T,S,P:Type]. ∀[R:P ─→ RankEx2(S;T) ─→ ℙ].`
`  ((∀t:T. (∃x:{P| (R x RankEx2_LeafT(t))}))`
`  `` (∀s:S. (∃x:{P| (R x RankEx2_LeafS(s))}))`
`  `` (∀d:RankEx2(S;T). ∀s:S. ∀t:T.  ((∃x:{P| (R x d)}) `` (∃x:{P| (R x RankEx2_Prod(<<d, s>, t>))})))`
`  `` (∀z:S × RankEx2(S;T) + RankEx2(S;T)`
`        (case z of inl(p) => ∃x:{P| (R x (snd(p)))} | inr(d) => ∃x:{P| (R x d)} `` (∃x:{P| (R x RankEx2_Union(z))})))`
`  `` (∀L:(S × RankEx2(S;T)) List. ((∀p∈L.∃x:{P| (R x (snd(p)))}) `` (∃x:{P| (R x RankEx2_ListProd(L))})))`
`  `` (∀z:T + (RankEx2(S;T) List)`
`        (case z of inl(p) => True | inr(L) => (∀p∈L.∃x:{P| (R x p)}) `` (∃x:{P| (R x RankEx2_UnionList(z))})))`
`  `` {∀t:RankEx2(S;T). (∃x:{P| (R x t)})})`

Lemma: RankEx2-defop-extract
`∀[T,S,P:Type]. ∀[R:P ─→ RankEx2(S;T) ─→ ℙ].`
`  ((∀t:T. (∃x:{P| (R x RankEx2_LeafT(t))}))`
`  `` (∀s:S. (∃x:{P| (R x RankEx2_LeafS(s))}))`
`  `` (∀d:RankEx2(S;T). ∀s:S. ∀t:T.  ((∃x:{P| (R x d)}) `` (∃x:{P| (R x RankEx2_Prod(<<d, s>, t>))})))`
`  `` (∀z:S × RankEx2(S;T) + RankEx2(S;T)`
`        (case z of inl(p) => ∃x:{P| (R x (snd(p)))} | inr(d) => ∃x:{P| (R x d)} `` (∃x:{P| (R x RankEx2_Union(z))})))`
`  `` (∀L:(S × RankEx2(S;T)) List. ((∀p∈L.∃x:{P| (R x (snd(p)))}) `` (∃x:{P| (R x RankEx2_ListProd(L))})))`
`  `` (∀z:T + (RankEx2(S;T) List)`
`        (case z of inl(p) => True | inr(L) => (∀p∈L.∃x:{P| (R x p)}) `` (∃x:{P| (R x RankEx2_UnionList(z))})))`
`  `` {∀t:RankEx2(S;T). (∃x:{P| (R x t)})})`

Definition: RankEx4co
`RankEx4co() ==  corec(X.lbl:Atom × if lbl =a "Foo" then ℤ + X else Void fi )`

Lemma: RankEx4co_wf
`RankEx4co() ∈ Type`

Lemma: RankEx4co-ext
`RankEx4co() ≡ lbl:Atom × if lbl =a "Foo" then ℤ + RankEx4co() else Void fi `

Definition: RankEx4co_size
`RankEx4co_size(p) ==`
`  fix((λsize,p. let lbl,x = p in if lbl =a "Foo" then 1 + case x of inl(a) => 0 | inr(b) => size b else 0 fi )) p`

Lemma: RankEx4co_size_wf
`∀[p:RankEx4co()]. (RankEx4co_size(p) ∈ partial(ℕ))`

Definition: RankEx4
`RankEx4() ==  {p:RankEx4co()| (RankEx4co_size(p))↓} `

Lemma: RankEx4_wf
`RankEx4() ∈ Type`

Definition: RankEx4_size
`RankEx4_size(p) ==`
`  fix((λsize,p. let lbl,x = p in if lbl =a "Foo" then 1 + case x of inl(a) => 0 | inr(b) => size b else 0 fi )) p`

Lemma: RankEx4_size_wf
`∀[p:RankEx4()]. (RankEx4_size(p) ∈ ℕ)`

Lemma: RankEx4-ext
`RankEx4() ≡ lbl:Atom × if lbl =a "Foo" then ℤ + RankEx4() else Void fi `

Definition: RankEx4_Foo
`RankEx4_Foo(foo) ==  <"Foo", foo>`

Lemma: RankEx4_Foo_wf
`∀[foo:ℤ + RankEx4()]. (RankEx4_Foo(foo) ∈ RankEx4())`

Definition: RankEx4_Foo?
`RankEx4_Foo?(v) ==  fst(v) =a "Foo"`

Lemma: RankEx4_Foo?_wf
`∀[v:RankEx4()]. (RankEx4_Foo?(v) ∈ 𝔹)`

Definition: RankEx4_Foo-foo
`RankEx4_Foo-foo(v) ==  snd(v)`

Lemma: RankEx4_Foo-foo_wf
`∀[v:RankEx4()]. RankEx4_Foo-foo(v) ∈ ℤ + RankEx4() supposing ↑RankEx4_Foo?(v)`

Lemma: RankEx4-induction
`∀[P:RankEx4() ─→ ℙ]`
`  ((∀foo:ℤ + RankEx4(). (case foo of inl(u) => True | inr(u1) => P[u1] `` P[RankEx4_Foo(foo)])) `` {∀v:RankEx4(). P[v]})`

Lemma: RankEx4-definition
`∀[A:Type]. ∀[R:A ─→ RankEx4() ─→ ℙ].`
`  ((∀foo:ℤ + RankEx4(). (case foo of inl(u) => True | inr(u1) => {x:A| R[x;u1]}  `` {x:A| R[x;RankEx4_Foo(foo)]} ))`
`  `` {∀v:RankEx4(). {x:A| R[x;v]} })`

Definition: RankEx4_ind
`RankEx4_ind(v;`
`            RankEx4_Foo(foo)`` rec1.Foo[foo; rec1])  ==`
`  fix((λRankEx4_ind,v. let lbl,v1 = v `
`                       in if lbl="Foo"`
`                          then case v1 of inl(x) => Foo[inl x; Ax] | inr(y) => Foo[inr y ; RankEx4_ind y]`
`                          else ⊥`
`                          fi )) `
`  v`

Lemma: RankEx4_ind_wf
`∀[A:Type]. ∀[R:A ─→ RankEx4() ─→ ℙ]. ∀[v:RankEx4()]. ∀[Foo:foo:(ℤ + RankEx4())`
`                                                           ─→ case foo of inl(u) => True | inr(u1) => {x:A| R[x;u1]} `
`                                                           ─→ {x:A| R[x;RankEx4_Foo(foo)]} ].`
`  (RankEx4_ind(v;`
`               RankEx4_Foo(foo)`` rec1.Foo[foo;rec1])  ∈ {x:A| R[x;v]} )`

Lemma: RankEx4_ind_wf_simple
`∀[A:Type]. ∀[v:RankEx4()]. ∀[Foo:foo:(ℤ + RankEx4()) ─→ case foo of inl(u) => True | inr(u1) => A ─→ A].`
`  (RankEx4_ind(v;`
`               RankEx4_Foo(foo)`` rec1.Foo[foo;rec1])  ∈ A)`

Lemma: UallTest1
`∀F:∀[T:Type]. (T ─→ T). ∀S:Type. ∀s:S.  ((F s) = s ∈ S)`

Definition: binary-treeco
`binary-treeco() ==  corec(X.lbl:Atom × if lbl =a "Leaf" then ℤ if lbl =a "Node" then left:X × X else Void fi )`

Lemma: binary-treeco_wf
`binary-treeco() ∈ Type`

Lemma: binary-treeco-ext
`binary-treeco() ≡ lbl:Atom × if lbl =a "Leaf" then ℤ`
`                             if lbl =a "Node" then left:binary-treeco() × binary-treeco()`
`                             else Void`
`                             fi `

Definition: binary-treeco_size
`binary-treeco_size(p) ==`
`  fix((λsize,p. let lbl,x = p `
`                in if lbl =a "Leaf" then 0`
`                   if lbl =a "Node" then let left,right = x in (1 + (size left)) + (size right)`
`                   else 0`
`                   fi )) `
`  p`

Lemma: binary-treeco_size_wf
`∀[p:binary-treeco()]. (binary-treeco_size(p) ∈ partial(ℕ))`

Definition: binary-tree
`binary-tree() ==  {p:binary-treeco()| (binary-treeco_size(p))↓} `

Lemma: binary-tree_wf
`binary-tree() ∈ Type`

Definition: binary-tree_size
`binary-tree_size(p) ==`
`  fix((λsize,p. let lbl,x = p `
`                in if lbl =a "Leaf" then 0`
`                   if lbl =a "Node" then let left,right = x in (1 + (size left)) + (size right)`
`                   else 0`
`                   fi )) `
`  p`

Lemma: binary-tree_size_wf
`∀[p:binary-tree()]. (binary-tree_size(p) ∈ ℕ)`

Lemma: binary-tree-ext
`binary-tree() ≡ lbl:Atom × if lbl =a "Leaf" then ℤ`
`                           if lbl =a "Node" then left:binary-tree() × binary-tree()`
`                           else Void`
`                           fi `

Definition: btr_Leaf
`btr_Leaf(val) ==  <"Leaf", val>`

Lemma: btr_Leaf_wf
`∀[val:ℤ]. (btr_Leaf(val) ∈ binary-tree())`

Definition: btr_Node
`btr_Node(left;right) ==  <"Node", left, right>`

Lemma: btr_Node_wf
`∀[left,right:binary-tree()].  (btr_Node(left;right) ∈ binary-tree())`

Definition: btr_Leaf?
`btr_Leaf?(v) ==  fst(v) =a "Leaf"`

Lemma: btr_Leaf?_wf
`∀[v:binary-tree()]. (btr_Leaf?(v) ∈ 𝔹)`

Definition: btr_Leaf-val
`btr_Leaf-val(v) ==  snd(v)`

Lemma: btr_Leaf-val_wf
`∀[v:binary-tree()]. btr_Leaf-val(v) ∈ ℤ supposing ↑btr_Leaf?(v)`

Definition: btr_Node?
`btr_Node?(v) ==  fst(v) =a "Node"`

Lemma: btr_Node?_wf
`∀[v:binary-tree()]. (btr_Node?(v) ∈ 𝔹)`

Definition: btr_Node-left
`btr_Node-left(v) ==  fst(snd(v))`

Lemma: btr_Node-left_wf
`∀[v:binary-tree()]. btr_Node-left(v) ∈ binary-tree() supposing ↑btr_Node?(v)`

Definition: btr_Node-right
`btr_Node-right(v) ==  snd(snd(v))`

Lemma: btr_Node-right_wf
`∀[v:binary-tree()]. btr_Node-right(v) ∈ binary-tree() supposing ↑btr_Node?(v)`

Lemma: binary-tree-induction
`∀[P:binary-tree() ─→ ℙ]`
`  ((∀val:ℤ. P[btr_Leaf(val)])`
`  `` (∀left,right:binary-tree().  (P[left] `` P[right] `` P[btr_Node(left;right)]))`
`  `` {∀v:binary-tree(). P[v]})`

Lemma: binary-tree-definition
`∀[A:Type]. ∀[R:A ─→ binary-tree() ─→ ℙ].`
`  ((∀val:ℤ. {x:A| R[x;btr_Leaf(val)]} )`
`  `` (∀left,right:binary-tree().  ({x:A| R[x;left]}  `` {x:A| R[x;right]}  `` {x:A| R[x;btr_Node(left;right)]} ))`
`  `` {∀v:binary-tree(). {x:A| R[x;v]} })`

Definition: binary-tree_ind
`binary-tree_ind(v;`
`                btr_Leaf(val)`` Leaf[val];`
`                btr_Node(left,right)`` rec1,rec2.Node[left; right; rec1; rec2])  ==`
`  fix((λbinary-tree_ind,v. let lbl,v1 = v `
`                           in if lbl="Leaf" then Leaf[v1]`
`                              if lbl="Node"`
`                                then let left,v2 = v1 `
`                                     in Node[left; v2; binary-tree_ind left; binary-tree_ind v2]`
`                              else ⊥`
`                              fi )) `
`  v`

Lemma: binary-tree_ind_wf
`∀[A:Type]. ∀[R:A ─→ binary-tree() ─→ ℙ]. ∀[v:binary-tree()]. ∀[Leaf:val:ℤ ─→ {x:A| R[x;btr_Leaf(val)]} ].`
`∀[Node:left:binary-tree()`
`       ─→ right:binary-tree()`
`       ─→ {x:A| R[x;left]} `
`       ─→ {x:A| R[x;right]} `
`       ─→ {x:A| R[x;btr_Node(left;right)]} ].`
`  (binary-tree_ind(v;`
`                   btr_Leaf(val)`` Leaf[val];`
`                   btr_Node(left,right)`` rec1,rec2.Node[left;right;rec1;rec2])  ∈ {x:A| R[x;v]} )`

Lemma: binary-tree_ind_wf_simple
`∀[A:Type]. ∀[v:binary-tree()]. ∀[Leaf:val:ℤ ─→ A]. ∀[Node:left:binary-tree() ─→ right:binary-tree() ─→ A ─→ A ─→ A].`
`  (binary-tree_ind(v;`
`                   btr_Leaf(val)`` Leaf[val];`
`                   btr_Node(left,right)`` rec1,rec2.Node[left;right;rec1;rec2])  ∈ A)`

Home Index