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