Definition: varname
varname() == Atom ⋃ (Atom × ℕ)
Lemma: varname_wf
varname() ∈ Type
Definition: num-var
t_n == <t, n>
Lemma: num-var_wf
∀[t:Atom]. ∀[n:ℕ]. (t_n ∈ varname())
Definition: eq_var
eq_var(a;b) ==
if a is an atom then if b is an atom then a =a b otherwise ff otherwise let x,n = a
in if b is an atom then ff
otherwise let y,m = b
in x =a y ∧b (n =z m)
Lemma: eq_var_wf
∀[a,b:varname()]. (eq_var(a;b) ∈ 𝔹)
Lemma: assert-eq_var
∀a,b:varname(). uiff(↑eq_var(a;b);a = b ∈ varname())
Definition: var-deq
VarDeq == λa,b. eq_var(a;b)
Lemma: var-deq_wf
VarDeq ∈ EqDecider(varname())
Definition: same-binding
same-binding(vs;ws;v;w) ==
if vs is a pair then if ws is a pair then let a,as = vs
in let b,bs = ws
in case eq_var(a;v)
of inl(_) =>
eq_var(b;w)
| inr(_) =>
(¬beq_var(b;w)) ∧b same-binding(as;bs;v;w) otherwise ff
otherwise if ws is a pair then ff otherwise eq_var(v;w)
Lemma: same-binding_wf
∀[vs,ws:varname() List]. ∀[v,w:varname()]. (same-binding(vs;ws;v;w) ∈ 𝔹)
Lemma: same-binding-not-bound
∀[vs,ws:varname() List].
∀v,w:varname().
((↑same-binding(vs;ws;v;w)) ⇒ (¬(v ∈ vs)) ⇒ {(¬(w ∈ ws)) ∧ (w = v ∈ varname()) ∧ (||vs|| = ||ws|| ∈ ℤ)})
Lemma: same-binding-refl
∀[vs:varname() List]. ∀[v:varname()]. (same-binding(vs;vs;v;v) ~ tt)
Lemma: same-binding-symm
∀[vs,ws:varname() List]. ∀[v,w:varname()]. (same-binding(vs;ws;v;w) ~ same-binding(ws;vs;w;v))
Lemma: same-binding-trans
∀[vs,ws,us:varname() List]. ∀[v,w,u:varname()].
((↑same-binding(vs;ws;v;w)) ⇒ (↑same-binding(ws;us;w;u)) ⇒ (↑same-binding(vs;us;v;u)))
Lemma: atom_subtype_varname
Atom ⊆r varname()
Lemma: atomxnat_subtype_varname
(Atom × ℕ) ⊆r varname()
Definition: var-num
var-num(t;b) ==
if b is an atom then if b =a t then 0 else -1 fi otherwise let x,n = b
in if x =a t then n + 1 else -1 fi
Lemma: var-num_wf
∀[t:Atom]. ∀[b:varname()]. (var-num(t;b) ∈ {-1...})
Definition: maybe_new_var
maybe_new_var(v;vs) ==
if null(vs)
then v
else eval t = if v is an atom then v otherwise fst(v) in
let n,x = list-max(b.var-num(t;b);vs)
in if n <z 0 then v else <t, n> fi
fi
Lemma: maybe_new_var_wf
∀[v:varname()]. ∀[vs:varname() List]. (maybe_new_var(v;vs) ∈ varname())
Lemma: maybe_new_var-distinct
∀[a:varname()]. ∀[vs:varname() List]. (∀v∈vs.¬(maybe_new_var(a;vs) = v ∈ varname()))
Definition: nullvar
nullvar() == ""
Lemma: nullvar_wf
nullvar() ∈ varname()
Lemma: maybe_new_var-is-null
∀a:varname(). ∀[vs:varname() List]. a = nullvar() ∈ varname() supposing maybe_new_var(a;vs) = nullvar() ∈ varname()
Definition: coterm-fun
coterm-fun(opr;T) == {v:varname()| ¬(v = nullvar() ∈ varname())} + (opr × ((varname() List × T) List))
Lemma: coterm-fun_wf
∀[opr,T:Type]. (coterm-fun(opr;T) ∈ Type)
Lemma: coterm-fun-continous
∀[opr:Type]. ContinuousMonotone(T.coterm-fun(opr;T))
Definition: coterm
coterm(opr) == corec(T.coterm-fun(opr;T))
Lemma: coterm_wf
∀[opr:Type]. (coterm(opr) ∈ Type)
Lemma: coterm-ext
∀[opr:Type]. coterm(opr) ≡ coterm-fun(opr;coterm(opr))
Definition: coterm-size
coterm-size(t) == fix((λsz,t. case t of inl(v) => 1 | inr(p) => let opr,bts = p in 1 + Σ(sz (snd(bt)) | bt ∈ bts))) t
Lemma: coterm-size_wf
∀[opr:Type]. ∀[t:coterm(opr)]. (coterm-size(t) ∈ partial(ℕ))
Definition: term
term(opr) == {t:coterm(opr)| (coterm-size(t))↓}
Lemma: term_wf
∀[opr:Type]. (term(opr) ∈ Type)
Lemma: term-ext
∀[opr:Type]. term(opr) ≡ coterm-fun(opr;term(opr))
Definition: isvarterm
isvarterm(t) == isl(t)
Lemma: isvarterm_wf
∀[opr:Type]. ∀[t:term(opr)]. (isvarterm(t) ∈ 𝔹)
Definition: varterm
varterm(v) == inl v
Lemma: varterm_wf
∀[opr:Type]. ∀[v:varname()]. varterm(v) ∈ term(opr) supposing ¬(v = nullvar() ∈ varname())
Definition: mkterm
mkterm(opr;bts) == inr <opr, bts>
Lemma: mkterm_wf
∀[Op:Type]. ∀[opr:Op]. ∀[bts:(varname() List × term(Op)) List]. (mkterm(opr;bts) ∈ term(Op))
Lemma: mkterm-one-one
∀[Op:Type]. ∀[f,g:Op]. ∀[as,bs:(varname() List × term(Op)) List].
((mkterm(f;as) = mkterm(g;bs) ∈ term(Op)) ⇒ {(f = g ∈ Op) ∧ (as = bs ∈ ((varname() List × term(Op)) List))})
Lemma: assert-isvarterm
∀[opr:Type]
∀t:term(opr). (↑isvarterm(t) ⇐⇒ ∃v:{v:varname()| ¬(v = nullvar() ∈ varname())} . (t = varterm(v) ∈ term(opr)))
Definition: term-size
term-size(t) == coterm-size(t)
Lemma: term-size_wf
∀[opr:Type]. ∀[t:term(opr)]. (term-size(t) ∈ ℕ)
Lemma: term_size_var_lemma
∀v:Top. (term-size(varterm(v)) ~ 1)
Lemma: term_size_mkterm_lemma
∀bts,opr:Top. (term-size(mkterm(opr;bts)) ~ 1 + Σ(term-size(snd(bt)) | bt ∈ bts))
Definition: bound-term
bound-term(opr) == varname() List × term(opr)
Lemma: bound-term_wf
∀[opr:Type]. (bound-term(opr) ∈ Type)
Lemma: assert-not-isvarterm
∀[opr:Type]. ∀t:term(opr). (¬↑isvarterm(t) ⇐⇒ ∃f:opr. ∃bts:bound-term(opr) List. (t = mkterm(f;bts) ∈ term(opr)))
Definition: term-opr
term-opr(t) == fst(outr(t))
Lemma: term-opr_wf
∀[opr:Type]. ∀[t:term(opr)]. term-opr(t) ∈ opr supposing ¬↑isvarterm(t)
Definition: term-bts
term-bts(t) == snd(outr(t))
Lemma: term-bts_wf
∀[opr:Type]. ∀[t:term(opr)]. term-bts(t) ∈ bound-term(opr) List supposing ¬↑isvarterm(t)
Lemma: not-isvarterm-implies
∀[opr:Type]. ∀t:term(opr). ((¬↑isvarterm(t)) ⇒ (t = mkterm(term-opr(t);term-bts(t)) ∈ term(opr)))
Definition: bound-term-size
bound-term-size(bt) == term-size(snd(bt))
Lemma: bound-term-size_wf
∀[opr:Type]. ∀[bt:bound-term(opr)]. (bound-term-size(bt) ∈ ℕ)
Lemma: term-cases
∀[opr:Type]
∀t:term(opr)
((∃v:varname(). ((¬(v = nullvar() ∈ varname())) ∧ (t = varterm(v) ∈ term(opr))))
∨ (∃f:opr. ∃bts:{bt:bound-term(opr)| bound-term-size(bt) < term-size(t)} List. (t = mkterm(f;bts) ∈ term(opr))))
Lemma: term-size-positive
∀[opr:Type]. ∀t:term(opr). (1 ≤ term-size(t))
Definition: immediate-subterm
s < t ==
∃f:opr. ∃bts:bound-term(opr) List. ((t = mkterm(f;bts) ∈ term(opr)) ∧ (∃i:ℕ||bts||. (s = (snd(bts[i])) ∈ term(opr))))
Lemma: immediate-subterm_wf
∀[opr:Type]. ∀[s,t:term(opr)]. (s < t ∈ ℙ)
Lemma: immediate-subterm-size
∀[opr:Type]. ∀[s,t:term(opr)]. (s < t ⇒ term-size(s) < term-size(t))
Definition: subterm-rel
subterm-rel(opr) == TC(λs,t. s < t)
Lemma: subterm-rel_wf
∀[opr:Type]. (subterm-rel(opr) ∈ term(opr) ⟶ term(opr) ⟶ ℙ)
Definition: subterm
s << t == s subterm-rel(opr) t
Lemma: subterm_wf
∀[opr:Type]. ∀[s,t:term(opr)]. (s << t ∈ ℙ)
Lemma: subterm_transitivity
∀[opr:Type]. ∀s,t,r:term(opr). (s << t ⇒ t << r ⇒ s << r)
Lemma: immediate-is-subterm
∀[opr:Type]. ∀s,t:term(opr). (s < t ⇒ s << t)
Lemma: subterm-cases
∀[opr:Type]. ∀s,t:term(opr). (s << t ⇐⇒ s < t ∨ (∃r:term(opr). (s < r ∧ r << t)))
Lemma: subterm-size
∀[opr:Type]. ∀[s,t:term(opr)]. (s << t ⇒ term-size(s) < term-size(t))
Lemma: subterm-varterm
∀[opr:Type]. ∀[s:term(opr)]. ∀[v:{v:varname()| ¬(v = nullvar() ∈ varname())} ]. (¬s << varterm(v))
Lemma: trivial-subterm
∀[opr:Type]. ∀f:opr. ∀bts:bound-term(opr) List. ∀i:ℕ||bts||. snd(bts[i]) << mkterm(f;bts)
Lemma: subterm-mkterm
∀[opr:Type]
∀s:term(opr). ∀f:opr. ∀bts:bound-term(opr) List.
(s << mkterm(f;bts) ⇐⇒ ∃i:ℕ||bts||. ((s = (snd(bts[i])) ∈ term(opr)) ∨ s << snd(bts[i])))
Lemma: bound-term-induction
∀[opr:Type]. ∀[P:bound-term(opr) ⟶ ℙ].
((∀vs:varname() List. ∀v:varname(). ((¬(v = nullvar() ∈ varname())) ⇒ P[<vs, varterm(v)>]))
⇒ (∀bts:bound-term(opr) List
((∀bt:bound-term(opr). ((bt ∈ bts) ⇒ P[bt])) ⇒ (∀f:opr. ∀vs:varname() List. P[<vs, mkterm(f;bts)>])))
⇒ (∀bt:bound-term(opr). P[bt]))
Lemma: term-induction1
∀[opr:Type]. ∀[P:term(opr) ⟶ ℙ].
((∀v:{v:varname()| ¬(v = nullvar() ∈ varname())} . P[varterm(v)])
⇒ (∀f:opr. ∀bts:bound-term(opr) List. ((∀i:ℕ||bts||. P[snd(bts[i])]) ⇒ P[mkterm(f;bts)]))
⇒ {∀t:term(opr). P[t]})
Definition: term-ind
term-ind(x.varcase[x];f,bts,r.mktermcase[f;
bts;
r];t) ==
letrec P(a)=case a
of inl(x) =>
varcase[x]
| inr(p) =>
let f,bts = p
in mktermcase[f;
bts;
λi.(P (snd(bts[i])))] in
P(t)
Lemma: term-induction1-ext
∀[opr:Type]. ∀[P:term(opr) ⟶ ℙ].
((∀v:{v:varname()| ¬(v = nullvar() ∈ varname())} . P[varterm(v)])
⇒ (∀f:opr. ∀bts:bound-term(opr) List. ((∀i:ℕ||bts||. P[snd(bts[i])]) ⇒ P[mkterm(f;bts)]))
⇒ {∀t:term(opr). P[t]})
Lemma: term-ind_wf
∀[opr:Type]. ∀[P:term(opr) ⟶ ℙ]. ∀[varcase:∀v:{v:varname()| ¬(v = nullvar() ∈ varname())} . P[varterm(v)]].
∀[mktermcase:∀f:opr. ∀bts:bound-term(opr) List. ((∀i:ℕ||bts||. P[snd(bts[i])]) ⇒ P[mkterm(f;bts)])]. ∀[t:term(opr)].
(term-ind(x.varcase[x];f,bts,r.mktermcase[f;bts;r];t) ∈ P[t])
Lemma: term-induction
∀[opr:Type]. ∀[P:term(opr) ⟶ ℙ].
((∀v:{v:varname()| ¬(v = nullvar() ∈ varname())} . P[varterm(v)])
⇒ (∀bts:bound-term(opr) List. ((∀bt:bound-term(opr). ((bt ∈ bts) ⇒ P[snd(bt)])) ⇒ (∀f:opr. P[mkterm(f;bts)])))
⇒ {∀t:term(opr). P[t]})
Definition: hereditarily
hereditarily(opr;s.P[s];t) == P[t] ∧ (∀s:term(opr). (s << t ⇒ P[s]))
Lemma: hereditarily_wf
∀[opr:Type]. ∀[P:term(opr) ⟶ ℙ]. ∀[t:term(opr)]. (hereditarily(opr;s.P[s];t) ∈ ℙ)
Lemma: hereditarily_functionality_wrt_subterm
∀[opr:Type]. ∀[P:term(opr) ⟶ ℙ]. ∀t,s:term(opr). (s << t ⇒ hereditarily(opr;s.P[s];t) ⇒ hereditarily(opr;s.P[s];s))
Lemma: hereditarily-varterm
∀[opr:Type]. ∀[P:term(opr) ⟶ ℙ]. ∀[v:{v:varname()| ¬(v = nullvar() ∈ varname())} ].
(hereditarily(opr;s.P[s];varterm(v)) ⇐⇒ P[varterm(v)])
Lemma: hereditarily-mkterm
∀[opr:Type]. ∀[P:term(opr) ⟶ ℙ].
∀f:opr. ∀bts:bound-term(opr) List.
(hereditarily(opr;s.P[s];mkterm(f;bts))
⇐⇒ P[mkterm(f;bts)] ∧ (∀bt:bound-term(opr). ((bt ∈ bts) ⇒ hereditarily(opr;s.P[s];snd(bt)))))
Definition: hered-term
hered-term(opr;t.P[t]) == {t:term(opr)| hereditarily(opr;s.P[s];t)}
Lemma: hered-term_wf
∀[opr:Type]. ∀[P:term(opr) ⟶ ℙ]. (hered-term(opr;t.P[t]) ∈ Type)
Definition: bound-terms-accum
bound-terms-accum(L,bt.f[L; bt];param,bndtrm.g[param; bndtrm];bts) == dep-accum(L,bt.f[L; bt];a,bt.g[a; bt];bts)
Lemma: bound-terms-accum_wf
∀[opr:Type]. ∀[P:term(opr) ⟶ ℙ]. ∀[Param:Type]. ∀[C:Param ⟶ (varname() List × hered-term(opr;t.P[t])) ⟶ Type].
∀[bts:(varname() List × hered-term(opr;t.P[t])) List].
∀[f:very-dep-fun(Param;varname() List × hered-term(opr;t.P[t]);a,bt.C[a;bt])]. ∀[g:a:Param
⟶ bt:{bt:varname() List
× hered-term(opr;t.P[t])|
(bt ∈ bts)}
⟶ C[a;bt]].
(bound-terms-accum(L,bt.f[L;bt];a,bt.g[a;bt];bts)
∈ {L:(a:Param × b:varname() List × hered-term(opr;t.P[t]) × C[a;b]) List|
vdf-eq(Param;f;L) ∧ (map(λx.(fst(snd(x)));L) = bts ∈ ((varname() List × hered-term(opr;t.P[t])) List))} )
Definition: hered-term-accum
hered-term-accum(par,vars,v.varcase[par;
vars;
v];
prm,vs,f,L.m[prm;
vs;
f;
L];
p0,ws,op,sofar,bt.param[p0;
ws;
op;
sofar;
bt];
param;
bndtrm) ==
let vs,t = bndtrm
in case t
of inl(v) =>
varcase[param;
vs;
v]
| inr(pr) =>
let f,bts = pr
in let L = bound-terms-accum(sofar,bt.param[param;
vs;
f;
sofar;
bt];p',bt.hered-term-accum(par,vars,v.varcase[par;
vars;
v];
prm,vs,f,L.m[prm;
vs;
f;
L];
p0,ws,op,sofar,bt.param[p0;
ws;
op;
sofar;
bt];
p';
bt);bts) in
m[param;
vs;
f;
L]
Lemma: hered-term-accum_wf
∀[opr:Type]. ∀[P:term(opr) ⟶ ℙ]. ∀[Param:Type]. ∀[C:Param ⟶ (varname() List × hered-term(opr;t.P[t])) ⟶ Type].
∀[nextp:Param ⟶ (varname() List) ⟶ opr ⟶ very-dep-fun(Param;varname() List × hered-term(opr;t.P[t]);a,bt.C[a;bt])].
∀[m:a:Param
⟶ vs:(varname() List)
⟶ f:opr
⟶ L:{L:(a:Param × bt:varname() List × hered-term(opr;t.P[t]) × C[a;bt]) List|
vdf-eq(Param;nextp a vs f;L) ∧ hereditarily(opr;s.P[s];mkterm(f;map(λx.(fst(snd(x)));L)))}
⟶ C[a;<vs, mkterm(f;map(λx.(fst(snd(x)));L))>]]. ∀[varcase:a:Param
⟶ vs:(varname() List)
⟶ v:{v:varname()|
(¬(v = nullvar() ∈ varname())) ∧ P[varterm(v)]}
⟶ C[a;<vs, varterm(v)>]]. ∀[p:Param].
∀[bt:varname() List × hered-term(opr;t.P[t])].
(hered-term-accum(p,vs,v.varcase[p;vs;v]; prm,vs,f,L.m[prm;vs;f;L]; p0,ws,op,sofar,bt.nextp[p0;ws;op;sofar;bt]; p; bt)
∈ C[p;bt])
Lemma: hered-term-accum_wf2
∀[opr:Type]. ∀[P:term(opr) ⟶ ℙ]. ∀[Param:Type]. ∀[C:Param ⟶ hered-term(opr;t.P[t]) ⟶ Type].
∀[nextp:Param
⟶ (varname() List)
⟶ opr
⟶ very-dep-fun(Param;varname() List × hered-term(opr;t.P[t]);a,bt.C[a;snd(bt)])].
∀[m:a:Param
⟶ vs:(varname() List)
⟶ f:opr
⟶ L:{L:(a:Param × bt:varname() List × hered-term(opr;t.P[t]) × C[a;snd(bt)]) List|
vdf-eq(Param;nextp a vs f;L) ∧ hereditarily(opr;s.P[s];mkterm(f;map(λx.(fst(snd(x)));L)))}
⟶ C[a;mkterm(f;map(λx.(fst(snd(x)));L))]]. ∀[varcase:a:Param
⟶ vs:(varname() List)
⟶ v:{v:varname()|
(¬(v = nullvar() ∈ varname())) ∧ P[varterm(v)]}
⟶ C[a;varterm(v)]]. ∀[p:Param]. ∀[t:hered-term(opr;t.P[t])].
(hered-term-accum(p,vs,v.varcase[p;vs;v];
prm,vs,f,L.m[prm;vs;f;L];
p0,ws,op,sofar,bt.nextp[p0;ws;op;sofar;bt];
p;
<[], t>) ∈ C[p;t])
Lemma: term-accum-induction
∀[opr,P:Type]. ∀[R:P ⟶ term(opr) ⟶ ℙ].
∀Q:P ⟶ opr ⟶ (varname() List) ⟶ ((t:term(opr) × p:P × R[p;t]) List) ⟶ P
((∀p:P. ∀v:{v:varname()| ¬(v = nullvar() ∈ varname())} . R[p;varterm(v)])
⇒ (∀p:P. ∀f:opr. ∀bts:bound-term(opr) List. ∀L:{L:(t:term(opr) × p:P × R[p;t]) List|
(||L|| = ||bts|| ∈ ℤ)
∧ (∀i:ℕ||L||. ((fst(L[i])) = (snd(bts[i])) ∈ term(opr)))
∧ (∀i:ℕ||L||
((fst(snd(L[i]))) = Q[p;f;fst(bts[i]);firstn(i;L)] ∈ P))} .
R[p;mkterm(f;bts)])
⇒ {∀t:term(opr). ∀p:P. R[p;t]})
Definition: term-accum1
term-accum1(t)
p,f,vs,L.Q[p;
f;
vs;
L]
varterm(v) with p ⇒ varcase[p; v]
mkterm(f,bts) with p ⇒ trs.mktermcase[p;
f;
bts;
trs] ==
letrec R(a)=case a
of inl(v) =>
λp.varcase[p; v]
| inr(pr) =>
let f,bts = pr
in λp.let trs = accumulate (with value L and list item bt):
let p' = Q[p;
f;
fst(bt);
L] in
L @ [<snd(bt), p', R (snd(bt)) p'>]
over list:
bts
with starting value:
[]) in
mktermcase[p;
f;
bts;
trs] in
R(t)
Lemma: term_accum1_varterm_lemma
∀p,v,M,vcase,Q:Top.
(term-accum1(varterm(v))a,b,c,d.Q[a;b;c;d]varterm(v) with p ⇒ vcase[v;p]mkterm(f,bts) with p ⇒ L.M[p;f;bts;L] p
~ vcase[v;p])
Lemma: term-accum-induction-ext
∀[opr,P:Type]. ∀[R:P ⟶ term(opr) ⟶ ℙ].
∀Q:P ⟶ opr ⟶ (varname() List) ⟶ ((t:term(opr) × p:P × R[p;t]) List) ⟶ P
((∀p:P. ∀v:{v:varname()| ¬(v = nullvar() ∈ varname())} . R[p;varterm(v)])
⇒ (∀p:P. ∀f:opr. ∀bts:bound-term(opr) List. ∀L:{L:(t:term(opr) × p:P × R[p;t]) List|
(||L|| = ||bts|| ∈ ℤ)
∧ (∀i:ℕ||L||. ((fst(L[i])) = (snd(bts[i])) ∈ term(opr)))
∧ (∀i:ℕ||L||
((fst(snd(L[i]))) = Q[p;f;fst(bts[i]);firstn(i;L)] ∈ P))} .
R[p;mkterm(f;bts)])
⇒ {∀t:term(opr). ∀p:P. R[p;t]})
Lemma: term-accum1_wf
∀[opr,P:Type]. ∀[R:P ⟶ term(opr) ⟶ ℙ]. ∀[Q:P ⟶ opr ⟶ (varname() List) ⟶ ((t:term(opr) × p:P × R[p;t]) List) ⟶ P].
∀[varcase:∀p:P. ∀v:{v:varname()| ¬(v = nullvar() ∈ varname())} . R[p;varterm(v)]].
∀[mktermcase:∀p:P. ∀f:opr. ∀bts:bound-term(opr) List. ∀L:{L:(t:term(opr) × p:P × R[p;t]) List|
(||L|| = ||bts|| ∈ ℤ)
∧ (∀i:ℕ||L||. ((fst(L[i])) = (snd(bts[i])) ∈ term(opr)))
∧ (∀i:ℕ||L||
((fst(snd(L[i])))
= Q[p;f;fst(bts[i]);firstn(i;L)]
∈ P))} .
R[p;mkterm(f;bts)]]. ∀[t:term(opr)].
(term-accum1(t)
p,f,vs,tr.Q[p;f;vs;tr]
varterm(x) with p ⇒ varcase[p;x]
mkterm(f,bts) with p ⇒ trs.mktermcase[p;f;bts;trs] ∈ p:P ⟶ R[p;t])
Definition: term-accum
term-accum(t with parm)
p,f,vs,tr.Q[p;
f;
vs;
tr]
varterm(v) with p ⇒ varcase[p; v]
mkterm(f,bts) with p ⇒ trs.mktermcase[p;
f;
bts;
trs] ==
term-accum1(t)
p,f,vs,tr.Q[p;
f;
vs;
tr]
varterm(v) with p ⇒ varcase[p; v]
mkterm(f,bts) with p ⇒ trs.mktermcase[p;
f;
bts;
trs]
parm
Lemma: term-accum_wf
∀[opr,P:Type]. ∀[R:P ⟶ term(opr) ⟶ ℙ]. ∀[Q:P ⟶ opr ⟶ (varname() List) ⟶ ((t:term(opr) × p:P × R[p;t]) List) ⟶ P].
∀[varcase:p:P ⟶ v:{v:varname()| ¬(v = nullvar() ∈ varname())} ⟶ R[p;varterm(v)]].
∀[mktermcase:p:P
⟶ f:opr
⟶ bts:(bound-term(opr) List)
⟶ L:{L:(t:term(opr) × p:P × R[p;t]) List|
(||L|| = ||bts|| ∈ ℤ)
∧ (∀i:ℕ||L||. ((fst(L[i])) = (snd(bts[i])) ∈ term(opr)))
∧ (∀i:ℕ||L||. ((fst(snd(L[i]))) = Q[p;f;fst(bts[i]);firstn(i;L)] ∈ P))}
⟶ R[p;mkterm(f;bts)]]. ∀[t:term(opr)]. ∀[p:P].
(term-accum(t with p)
p,f,vs,tr.Q[p;f;vs;tr]
varterm(x) with p ⇒ varcase[p;x]
mkterm(f,bts) with p ⇒ trs.mktermcase[p;f;bts;trs] ∈ R[p;t])
Lemma: term_accum_varterm_lemma
∀p,M,v,varcase,Q:Top.
(term-accum(varterm(v) with p)
p,f,vs,xxx.Q[p;f;vs;xxx]
varterm(x) with p ⇒ varcase[p;x]
mkterm(f,bts) with p ⇒ xxx.M[p;f;bts;xxx] ~ varcase[p;v])
Lemma: term_accum_mkterm_lemma
∀p,bts,f,M,varcase,Q:Top.
(term-accum(mkterm(f;bts) with p)
a,b,c,d.Q[a;b;c;d]
varterm(x) with p ⇒ varcase[p;x]
mkterm(f,bts) with p ⇒ trs.M[p;f;bts;trs] ~ let trs = accumulate (with value d and list item bt):
let p' = Q[p;f;fst(bt);d] in
d
@ [<snd(bt)
, p'
, term-accum(snd(bt) with p')
a,b,c,d.Q[a;b;c;d]
varterm(x) with p ⇒ varcase[p;x]
mkterm(f,bts) with p ⇒ trs.M[p;f;bts;trs]>]
over list:
bts
with starting value:
[]) in
M[p;f;bts;trs])
Definition: alpha-aux
alpha-aux(opr;vs;ws;a;b) ==
case a
of inl(v) =>
case b of inl(w) => ↑same-binding(vs;ws;v;w) | inr(p) => False
| inr(p) =>
case b
of inl(w) =>
False
| inr(q) =>
let opa,abts = p
in let opb,bbts = q
in if abts is a pair then if bbts is a pair then let bta,morea = abts
in let btb,moreb = bbts
in let as,x = bta
in let bs,y = btb
in (||as|| = ||bs|| ∈ ℤ)
∧ alpha-aux(opr;rev(as) + vs;rev(bs) + ws;x;y)
∧ alpha-aux(opr;vs;ws;mkterm(opa;morea);mkterm(opb;moreb))
otherwise False otherwise if bbts is a pair then False otherwise opa = opb ∈ opr
Lemma: alpha-aux_wf
∀[opr:Type]. ∀[a,b:term(opr)]. ∀[vs,ws:varname() List]. (alpha-aux(opr;vs;ws;a;b) ∈ ℙ)
Lemma: sq_stable__alpha-aux
∀[opr:Type]. ∀a,b:term(opr). ∀vs,ws:varname() List. SqStable(alpha-aux(opr;vs;ws;a;b))
Lemma: alpha-aux-mkterm
∀[opr:Type]
∀a,b:opr. ∀as,bs:bound-term(opr) List. ∀vs,ws:varname() List.
(alpha-aux(opr;vs;ws;mkterm(a;as);mkterm(b;bs))
⇐⇒ (a = b ∈ opr)
∧ (||as|| = ||bs|| ∈ ℤ)
∧ (∀i:ℕ||as||
(alpha-aux(opr;rev(fst(as[i])) + vs;rev(fst(bs[i])) + ws;snd(as[i]);snd(bs[i]))
∧ (||fst(as[i])|| = ||fst(bs[i])|| ∈ ℤ))))
Lemma: alpha-aux-refl
∀[opr:Type]. ∀a:term(opr). ∀vs:varname() List. alpha-aux(opr;vs;vs;a;a)
Lemma: alpha-aux-symm
∀[opr:Type]. ∀a,b:term(opr). ∀vs,ws:varname() List. (alpha-aux(opr;vs;ws;a;b) ⇐⇒ alpha-aux(opr;ws;vs;b;a))
Lemma: alpha-aux-trans
∀[opr:Type]
∀a,b,c:term(opr). ∀us,vs,ws:varname() List.
(alpha-aux(opr;us;vs;a;b) ⇒ alpha-aux(opr;vs;ws;b;c) ⇒ alpha-aux(opr;us;ws;a;c))
Definition: alpha-eq-terms
alpha-eq-terms(opr;a;b) == alpha-aux(opr;[];[];a;b)
Lemma: alpha-eq-terms_wf
∀[opr:Type]. ∀[a,b:term(opr)]. (alpha-eq-terms(opr;a;b) ∈ ℙ)
Lemma: alpha-eq-equiv-rel
∀[opr:Type]. EquivRel(term(opr);a,b.alpha-eq-terms(opr;a;b))
Lemma: alpha-eq-terms_transitivity
∀[opr:Type]. ∀a,b,c:term(opr). (alpha-eq-terms(opr;a;b) ⇒ alpha-eq-terms(opr;b;c) ⇒ alpha-eq-terms(opr;a;c))
Lemma: alpha-eq-terms_inversion
∀[opr:Type]. ∀a,b:term(opr). (alpha-eq-terms(opr;a;b) ⇒ alpha-eq-terms(opr;b;a))
Lemma: alpha-eq-terms_weakening
∀[opr:Type]. ∀a,b:term(opr). ((a = b ∈ term(opr)) ⇒ alpha-eq-terms(opr;b;a))
Lemma: alpha-eq-terms_functionality
∀[opr:Type]
∀x1,x2,y1,y2:term(opr).
(alpha-eq-terms(opr;x1;x2)
⇒ alpha-eq-terms(opr;y1;y2)
⇒ (alpha-eq-terms(opr;x1;y1) ⇐⇒ alpha-eq-terms(opr;x2;y2)))
Lemma: term-opr_functionality
∀[opr:Type]. ∀[t,t':term(opr)].
(term-opr(t) = term-opr(t') ∈ opr) supposing (alpha-eq-terms(opr;t;t') and (¬↑isvarterm(t)))
Lemma: isvarterm_functionality
∀[opr:Type]. ∀[t,t':term(opr)]. isvarterm(t) = isvarterm(t') supposing alpha-eq-terms(opr;t;t')
Lemma: alpha-equal-varterm
∀[opr:Type]. ∀[v:{v:varname()| ¬(v = nullvar() ∈ varname())} ]. ∀[t:term(opr)].
t = varterm(v) ∈ term(opr) supposing alpha-eq-terms(opr;varterm(v);t)
Definition: free-vars-aux
free-vars-aux(bnds;t) ==
case t
of inl(v) =>
if v ∈b bnds then [] else [v] fi
| inr(p) =>
let op,bts = p
in l-union-list(VarDeq;map(λbt.let vs,a = bt
in free-vars-aux(rev(vs) + bnds;a);bts))
Lemma: free-vars-aux_wf
∀[opr:Type]. ∀[t:term(opr)]. ∀[bnds:varname() List].
(free-vars-aux(bnds;t) ∈ {v:varname()| ¬(v = nullvar() ∈ varname())} List)
Lemma: member-free-vars-aux-not-bound
∀[opr:Type]. ∀t:term(opr). ∀bnds:varname() List. ∀v:varname(). ((v ∈ free-vars-aux(bnds;t)) ⇒ (¬(v ∈ bnds)))
Lemma: member-free-vars-aux
∀[opr:Type]
∀t:term(opr). ∀v:varname(). ∀bnds:varname() List.
((v ∈ free-vars-aux(bnds;t)) ⇐⇒ (v ∈ free-vars-aux([];t)) ∧ (¬(v ∈ bnds)))
Definition: free-vars
free-vars(t) == free-vars-aux([];t)
Lemma: free-vars_wf
∀[opr:Type]. ∀[t:term(opr)]. (free-vars(t) ∈ {v:varname()| ¬(v = nullvar() ∈ varname())} List)
Lemma: free-vars_functionality
∀[opr:Type]. ∀t1,t2:term(opr). (alpha-eq-terms(opr;t1;t2) ⇒ (free-vars(t1) = free-vars(t2) ∈ (varname() List)))
Definition: all-vars
all-vars(t) ==
case t
of inl(v) =>
[v]
| inr(p) =>
let op,bts = p
in accumulate (with value as and list item bt):
let vs,a = bt
in all-vars(a) ⋃ vs ⋃ as
over list:
bts
with starting value:
[])
Lemma: all-vars_wf
∀[opr:Type]. ∀[t:term(opr)]. (all-vars(t) ∈ varname() List)
Definition: binders-disjoint
binders-disjoint(opr;L;t) ==
case t
of inl(v) =>
True
| inr(p) =>
let op,bts = p
in (∀bt∈bts.l_disjoint(varname();fst(bt);L) ∧ binders-disjoint(opr;L;snd(bt)))
Lemma: binders-disjoint_wf
∀[opr:Type]. ∀[L:varname() List]. ∀[t:term(opr)]. (binders-disjoint(opr;L;t) ∈ ℙ)
Lemma: member-all-vars-mkterm
∀[opr:Type]
∀f:opr. ∀v:varname(). ∀bts:bound-term(opr) List.
((v ∈ all-vars(mkterm(f;bts))) ⇐⇒ ∃bt:bound-term(opr). ((bt ∈ bts) ∧ ((v ∈ fst(bt)) ∨ (v ∈ all-vars(snd(bt))))))
Lemma: member-free-vars-mkterm
∀[opr:Type]
∀f:opr. ∀v:varname(). ∀bts:bound-term(opr) List.
((v ∈ free-vars(mkterm(f;bts))) ⇐⇒ ∃bt:bound-term(opr). ((bt ∈ bts) ∧ (v ∈ free-vars(snd(bt))) ∧ (¬(v ∈ fst(bt)))))
Lemma: free-vars-all-vars
∀[opr:Type]. ∀t:term(opr). ∀x:varname(). ((x ∈ free-vars(t)) ⇒ (x ∈ all-vars(t)))
Definition: alpha-rename-aux
alpha-rename-aux(f;bnds;t) ==
case t
of inl(v) =>
if v ∈b bnds then varterm(f v) else t fi
| inr(p) =>
let op,bts = p
in eval bts' = eager-map(λbt.let vs,a = bt
in <map(f;vs), alpha-rename-aux(f;rev(vs) + bnds;a)>;bts) in
mkterm(op;bts')
Lemma: alpha-rename-aux_wf
∀[opr:Type]. ∀[t:term(opr)]. ∀[bnds:varname() List].
∀f:{v:varname()| (v ∈ bnds @ all-vars(t))} ⟶ varname()
alpha-rename-aux(f;bnds;t) ∈ term(opr)
supposing ∀x:{v:varname()| (v ∈ bnds @ all-vars(t))}
(((f x) = nullvar() ∈ varname()) ⇒ (x = nullvar() ∈ varname()))
Definition: alpha-rename
alpha-rename(f;t) == alpha-rename-aux(f;[];t)
Lemma: alpha-rename_wf
∀[opr:Type]. ∀[t:term(opr)].
∀f:{v:varname()| (v ∈ all-vars(t))} ⟶ varname()
alpha-rename(f;t) ∈ term(opr)
supposing ∀x:{v:varname()| (v ∈ all-vars(t))} . (((f x) = nullvar() ∈ varname()) ⇒ (x = nullvar() ∈ varname()))
Lemma: alpha-rename-equivalent
∀[opr:Type]
∀t:term(opr). ∀f:{v:varname()| (v ∈ all-vars(t))} ⟶ varname().
alpha-eq-terms(opr;alpha-rename(f;t);t)
supposing ((∀x:{v:varname()| (v ∈ all-vars(t))} . ((f x ∈ free-vars(t)) ⇒ ((f x) = x ∈ varname())))
∧ (∀x:{v:varname()| (v ∈ all-vars(t))} . (((f x) = nullvar() ∈ varname()) ⇒ (x = nullvar() ∈ varname()))))
∧ Inj({v:varname()| (v ∈ all-vars(t))} ;varname();f)
Lemma: alpha-rename-binders-disjoint
∀[opr:Type]
∀L:varname() List. ∀t:term(opr). ∀f:{v:varname()| (v ∈ all-vars(t))} ⟶ varname().
((∀x:{v:varname()| (v ∈ all-vars(t))}
((((f x) = nullvar() ∈ varname()) ⇒ (x = nullvar() ∈ varname())) ∧ (¬(f x ∈ L))))
⇒ binders-disjoint(opr;L;alpha-rename(f;t)))
Definition: alpha-rename-alist
alpha-rename-alist(t;L) ==
snd(accumulate (with value p and list item x):
let vs,tab = p
in eval x' = maybe_new_var(x;vs) in
<[x' / vs], [<x, x'> / tab]>
over list:
L
with starting value:
<L @ all-vars(t), []>))
Lemma: alpha-rename-alist_wf
∀[opr:Type]. ∀[t:term(opr)]. ∀[L:varname() List]. (alpha-rename-alist(t;L) ∈ (varname() × varname()) List)
Lemma: alpha-rename-alist-property
∀[opr:Type]
∀t:term(opr). ∀L:varname() List.
((∀x,x':varname(). ((<x, x'> ∈ alpha-rename-alist(t;L)) ⇒ ((x ∈ L) ∧ (¬(x' ∈ L @ all-vars(t))))))
∧ (∀x,x',y,y':varname().
((<x, x'> ∈ alpha-rename-alist(t;L))
⇒ (<y, y'> ∈ alpha-rename-alist(t;L))
⇒ (x' = y' ∈ varname())
⇒ (x = y ∈ varname()))))
Lemma: alpha-rename-alist-nonnullvar
∀[opr:Type]
∀t:term(opr). ∀L:varname() List. ∀x,x':varname().
((<x, x'> ∈ alpha-rename-alist(t;L)) ⇒ (x' = nullvar() ∈ varname()) ⇒ (nullvar() ∈ L))
Lemma: alpha-rename-alist-property2
∀[opr:Type]
∀t:term(opr). ∀L:varname() List. ∀x:varname(). ((x ∈ L) ⇒ (∃x':varname(). (<x, x'> ∈ alpha-rename-alist(t;L))))
Definition: alpha-avoid
alpha-avoid(L;t) == alpha-rename(alist-map(VarDeq;alpha-rename-alist(t;L));t)
Lemma: alpha-avoid_wf
∀[opr:Type]. ∀[t:term(opr)]. ∀[L:varname() List]. alpha-avoid(L;t) ∈ term(opr) supposing ¬(nullvar() ∈ L)
Lemma: alpha-avoid-binders-disjoint
∀[opr:Type]. ∀L:varname() List. ((¬(nullvar() ∈ L)) ⇒ (∀t:term(opr). binders-disjoint(opr;L;alpha-avoid(L;t))))
Lemma: alpha-avoid-equivalent
∀[opr:Type]. ∀t:term(opr). ∀L:varname() List. alpha-eq-terms(opr;alpha-avoid(L;t);t) supposing ¬(nullvar() ∈ L)
Definition: replace-vars
replace-vars(s;t) ==
case t
of inl(v) =>
case apply-alist(VarDeq;s;v) of inl(a) => a | inr(_) => t
| inr(p) =>
let op,bts = p
in eval bts' = eager-map(λbt.let vs,b = bt
in <vs, replace-vars(s;b)>;bts) in
mkterm(op;bts')
Lemma: replace-vars_wf
∀[opr:Type]. ∀[t:term(opr)]. ∀[s:(varname() × term(opr)) List]. (replace-vars(s;t) ∈ term(opr))
Definition: equiv-substs
equiv-substs(opr;s1;s2) ==
∀x:varname()
(isl(apply-alist(VarDeq;s1;x)) = isl(apply-alist(VarDeq;s2;x))
∧ ((↑isl(apply-alist(VarDeq;s1;x)))
⇒ alpha-eq-terms(opr;outl(apply-alist(VarDeq;s1;x));outl(apply-alist(VarDeq;s2;x)))))
Lemma: equiv-substs_wf
∀[opr:Type]. ∀[s1,s2:(varname() × term(opr)) List]. (equiv-substs(opr;s1;s2) ∈ ℙ)
Lemma: equiv-substs-equiv-rel
∀[opr:Type]. EquivRel((varname() × term(opr)) List;s1,s2.equiv-substs(opr;s1;s2))
Definition: vars-of-subst
vars-of-subst(s) ==
l-union-list(VarDeq;map(λvt.let v,t = vt
in if eq_var(v;nullvar()) then free-vars(t) else insert(v;free-vars(t)) fi ;s))
Lemma: vars-of-subst_wf
∀[opr:Type]. ∀[s:(varname() × term(opr)) List]. (vars-of-subst(s) ∈ {v:varname()| ¬(v = nullvar() ∈ varname())} List)
Lemma: vars-of-subst-not-nullvar
∀[opr:Type]. ∀[s:(varname() × term(opr)) List]. (¬(nullvar() ∈ vars-of-subst(s)))
Definition: subst-frame
subst-frame(s;t) == alpha-avoid(vars-of-subst(s);t)
Lemma: subst-frame_wf
∀[opr:Type]. ∀[t:term(opr)]. ∀[s:(varname() × term(opr)) List]. (subst-frame(s;t) ∈ term(opr))
Lemma: subst-frame-alpha
∀[opr:Type]. ∀t:term(opr). ∀s:(varname() × term(opr)) List. alpha-eq-terms(opr;subst-frame(s;t);t)
Lemma: subst-frame-binders-disjoint
∀[opr:Type]. ∀t:term(opr). ∀s:(varname() × term(opr)) List. binders-disjoint(opr;vars-of-subst(s);subst-frame(s;t))
Definition: subst-term
subst-term(s;t) == replace-vars(s;subst-frame(s;t))
Lemma: subst-term_wf
∀[opr:Type]. ∀[t:term(opr)]. ∀[s:(varname() × term(opr)) List]. (subst-term(s;t) ∈ term(opr))
Lemma: subst-term_functionality
∀[opr:Type]
∀t1,t2:term(opr). ∀s1,s2:(varname() × term(opr)) List.
(alpha-eq-terms(opr;t1;t2) ⇒ equiv-substs(opr;s1;s2) ⇒ alpha-eq-terms(opr;subst-term(s1;t1);subst-term(s2;t2)))
Definition: correct-sort-arity
correct-sort-arity(sort;arity;t) ==
(¬↑isvarterm(t))
⇒ let bts = term-bts(t) in
let f = term-opr(t) in
(||bts|| = ||arity f|| ∈ ℤ)
∧ (∀i:ℕ||bts||. ((||fst(bts[i])|| = (fst(arity f[i])) ∈ ℤ) ∧ ((sort (snd(bts[i]))) = (snd(arity f[i])) ∈ ℤ)))
Lemma: correct-sort-arity_wf
∀[opr:Type]. ∀[sort:term(opr) ⟶ ℕ]. ∀[arity:opr ⟶ ((ℕ × ℕ) List)]. ∀[t:term(opr)].
(correct-sort-arity(sort;arity;t) ∈ ℙ)
Definition: wf-term
wf-term(arity;sort;t) ==
case t
of inl(v) =>
tt
| inr(p) =>
let f,bts = p
in eval nms = arity f in
(||nms|| =z ||bts||)
∧b (∀nm_bt∈zip(nms;bts).let nm,bt = nm_bt
in let vs,b = bt
in (fst(nm) =z ||vs||) ∧b (sort b =z snd(nm)) ∧b wf-term(arity;sort;b))_b
Lemma: wf-term_wf
∀[opr:Type]. ∀[sort:term(opr) ⟶ ℕ]. ∀[arity:opr ⟶ ((ℕ × ℕ) List)]. ∀[t:term(opr)]. (wf-term(arity;sort;t) ∈ 𝔹)
Lemma: wf_term_var_lemma
∀v,arity,sort:Top. (wf-term(arity;sort;varterm(v)) ~ tt)
Lemma: assert-wf-mkterm
∀[opr:Type]
∀sort:term(opr) ⟶ ℕ. ∀arity:opr ⟶ ((ℕ × ℕ) List). ∀f:opr. ∀bts:(varname() List × term(opr)) List.
uiff(↑wf-term(arity;sort;mkterm(f;bts));(||bts|| = ||arity f|| ∈ ℤ)
∧ (∀i:ℕ||bts||
((||fst(bts[i])|| = (fst(arity f[i])) ∈ ℤ)
∧ ((sort (snd(bts[i]))) = (snd(arity f[i])) ∈ ℤ)
∧ (↑wf-term(arity;sort;snd(bts[i]))))))
Definition: wfterm
wfterm(opr;sort;arity) == {t:term(opr)| ↑wf-term(arity;sort;t)}
Lemma: wfterm_wf
∀[opr:Type]. ∀[sort:term(opr) ⟶ ℕ]. ∀[arity:opr ⟶ ((ℕ × ℕ) List)]. (wfterm(opr;sort;arity) ∈ Type)
Lemma: wf-term-hereditarily-correct-sort-arity
∀[opr:Type]
∀sort:term(opr) ⟶ ℕ. ∀arity:opr ⟶ ((ℕ × ℕ) List). ∀t:term(opr).
(↑wf-term(arity;sort;t) ⇐⇒ hereditarily(opr;s.correct-sort-arity(sort;arity;s);t))
Lemma: wfterm-hered-correct-sort-arity
∀[opr:Type]. ∀[sort:term(opr) ⟶ ℕ]. ∀[arity:opr ⟶ ((ℕ × ℕ) List)].
wfterm(opr;sort;arity) ≡ hered-term(opr;t.correct-sort-arity(sort;arity;t))
Definition: wf-bound-terms
wf-bound-terms(opr;sort;arity;f) ==
{bts:(varname() List × wfterm(opr;sort;arity)) List|
(||bts|| = ||arity f|| ∈ ℤ)
∧ (∀i:ℕ||bts||. ((||fst(bts[i])|| = (fst(arity f[i])) ∈ ℤ) ∧ ((sort (snd(bts[i]))) = (snd(arity f[i])) ∈ ℤ)))}
Lemma: wf-bound-terms_wf
∀[opr:Type]. ∀[sort:term(opr) ⟶ ℕ]. ∀[arity:opr ⟶ ((ℕ × ℕ) List)]. ∀[f:opr].
(wf-bound-terms(opr;sort;arity;f) ∈ Type)
Definition: mkwfterm
mkwfterm(f;bts) == mkterm(f;bts)
Lemma: mkwfterm_wf
∀[opr:Type]. ∀[sort:term(opr) ⟶ ℕ]. ∀[arity:opr ⟶ ((ℕ × ℕ) List)]. ∀[f:opr]. ∀[bts:wf-bound-terms(opr;sort;arity;f)].
(mkwfterm(f;bts) ∈ wfterm(opr;sort;arity))
Definition: wfbts
wfbts(t) == term-bts(t)
Lemma: wfbts_wf
∀[opr:Type]. ∀[sort:term(opr) ⟶ ℕ]. ∀[arity:opr ⟶ ((ℕ × ℕ) List)]. ∀[t:wfterm(opr;sort;arity)].
wfbts(t) ∈ wf-bound-terms(opr;sort;arity;term-opr(t)) supposing ¬↑isvarterm(t)
Definition: wfterm-accum
wfterm-accum(param;t)
p,vrs,v.varcase[p;
vrs;
v]
prm,vs,f,L.m[prm;
vs;
f;
L]
p0,ws,op,sofar,bt.nextp[p0;
ws;
op;
sofar;
bt] ==
hered-term-accum(p,vs,v.varcase[p;
vs;
v];
prm,vs,f,L.m[prm;
vs;
f;
L];
p0,ws,op,sofar,bt.nextp[p0;
ws;
op;
sofar;
bt];
param;
<[], t>)
Lemma: wfterm-accum_wf
∀[opr:Type]. ∀[sort:term(opr) ⟶ ℕ]. ∀[arity:opr ⟶ ((ℕ × ℕ) List)]. ∀[Param:Type]. ∀[C:Param
⟶ wfterm(opr;sort;arity)
⟶ Type].
∀[nextp:Param
⟶ (varname() List)
⟶ opr
⟶ very-dep-fun(Param;varname() List × wfterm(opr;sort;arity);a,bt.C[a;snd(bt)])].
∀[m:a:Param
⟶ vs:(varname() List)
⟶ f:opr
⟶ L:{L:(a:Param × bt:varname() List × wfterm(opr;sort;arity) × C[a;snd(bt)]) List|
vdf-eq(Param;nextp a vs f;L) ∧ (↑wf-term(arity;sort;mkterm(f;map(λx.(fst(snd(x)));L))))}
⟶ C[a;mkterm(f;map(λx.(fst(snd(x)));L))]]. ∀[varcase:a:Param
⟶ vs:(varname() List)
⟶ v:{v:varname()| ¬(v = nullvar() ∈ varname())}
⟶ C[a;varterm(v)]]. ∀[p:Param]. ∀[t:wfterm(opr;sort;arity)].
(wfterm-accum(p;t)
p,vs,v.varcase[p;vs;v]
prm,vs,f,L.m[prm;vs;f;L]
p0,ws,op,sofar,bt.nextp[p0;ws;op;sofar;bt] ∈ C[p;t])
Lemma: term-ind_wf_wfterm
∀[opr:Type]. ∀[sort:term(opr) ⟶ ℕ]. ∀[arity:opr ⟶ ((ℕ × ℕ) List)]. ∀[P:wfterm(opr;sort;arity) ⟶ ℙ].
∀[varcase:∀v:{v:varname()| ¬(v = nullvar() ∈ varname())} . P[varterm(v)]].
∀[mktermcase:∀f:opr. ∀bts:wf-bound-terms(opr;sort;arity;f). ((∀i:ℕ||bts||. P[snd(bts[i])]) ⇒ P[mkwfterm(f;bts)])].
∀[t:wfterm(opr;sort;arity)].
(term-ind(x.varcase[x];f,bts,r.mktermcase[f;bts;r];t) ∈ P[t])
Lemma: wf-term-induction
∀[opr:Type]
∀sort:term(opr) ⟶ ℕ. ∀arity:opr ⟶ ((ℕ × ℕ) List).
∀[P:wfterm(opr;sort;arity) ⟶ ℙ]
((∀v:{v:varname()| ¬(v = nullvar() ∈ varname())} . P[varterm(v)])
⇒ (∀f:opr. ∀bts:wf-bound-terms(opr;sort;arity;f). ((∀i:ℕ||bts||. P[snd(bts[i])]) ⇒ P[mkwfterm(f;bts)]))
⇒ {∀t:wfterm(opr;sort;arity). P[t]})
Lemma: term-accum_wf_wfterm_0
∀[opr,P:Type]. ∀[sort:term(opr) ⟶ ℕ]. ∀[arity:opr ⟶ ((ℕ × ℕ) List)]. ∀[R:P ⟶ wfterm(opr;sort;arity) ⟶ ℙ].
∀[Q:P ⟶ opr ⟶ (varname() List) ⟶ ((t:term(opr) × p:P × R[p;t] supposing ↑wf-term(arity;sort;t)) List) ⟶ P].
∀[varcase:p:P ⟶ v:{v:varname()| ¬(v = nullvar() ∈ varname())} ⟶ R[p;varterm(v)]].
∀[mktermcase:p:P
⟶ f:opr
⟶ bts:wf-bound-terms(opr;sort;arity;f)
⟶ L:{L:(t:wfterm(opr;sort;arity) × p:P × R[p;t]) List|
(||L|| = ||bts|| ∈ ℤ)
∧ (∀i:ℕ||L||. ((fst(L[i])) = (snd(bts[i])) ∈ term(opr)))
∧ (∀i:ℕ||L||. ((fst(snd(L[i]))) = Q[p;f;fst(bts[i]);firstn(i;L)] ∈ P))}
⟶ R[p;mkwfterm(f;bts)]]. ∀[t:wfterm(opr;sort;arity)]. ∀[p:P].
(term-accum(t with p)
p,f,vs,tr.Q[p;f;vs;tr]
varterm(x) with p ⇒ varcase[p;x]
mkterm(f,bts) with p ⇒ trs.mktermcase[p;f;bts;trs] ∈ R[p;t])
Lemma: term-accum_wf_wfterm
∀[opr,P:Type]. ∀[sort:term(opr) ⟶ ℕ]. ∀[arity:opr ⟶ ((ℕ × ℕ) List)]. ∀[R:P ⟶ wfterm(opr;sort;arity) ⟶ ℙ].
∀[Q:P
⟶ f:opr
⟶ vs:(varname() List)
⟶ {L:(t:wfterm(opr;sort;arity) × p:P × R[p;t]) List|
||L|| < ||arity f||
∧ (||vs|| = (fst(arity f[||L||])) ∈ ℤ)
∧ (∀i:ℕ||L||. ((sort (fst(L[i]))) = (snd(arity f[i])) ∈ ℤ))}
⟶ P]. ∀[varcase:p:P ⟶ v:{v:varname()| ¬(v = nullvar() ∈ varname())} ⟶ R[p;varterm(v)]].
∀[mktermcase:p:P
⟶ f:opr
⟶ bts:wf-bound-terms(opr;sort;arity;f)
⟶ L:{L:(t:wfterm(opr;sort;arity) × p:P × R[p;t]) List|
(||L|| = ||bts|| ∈ ℤ)
∧ (∀i:ℕ||L||. ((fst(L[i])) = (snd(bts[i])) ∈ term(opr)))
∧ (∀i:ℕ||L||. ((fst(snd(L[i]))) = Q[p;f;fst(bts[i]);firstn(i;L)] ∈ P))}
⟶ R[p;mkwfterm(f;bts)]]. ∀[t:wfterm(opr;sort;arity)]. ∀[p:P].
(term-accum(t with p)
p,f,vs,tr.Q[p;f;vs;tr]
varterm(x) with p ⇒ varcase[p;x]
mkterm(f,bts) with p ⇒ trs.mktermcase[p;f;bts;trs] ∈ R[p;t])
Lemma: wf-term-accum-induction
∀[opr,P:Type]. ∀[sort:term(opr) ⟶ ℕ]. ∀[arity:opr ⟶ ((ℕ × ℕ) List)]. ∀[R:P ⟶ wfterm(opr;sort;arity) ⟶ ℙ].
∀Q:P
⟶ f:opr
⟶ vs:(varname() List)
⟶ {L:(t:wfterm(opr;sort;arity) × p:P × R[p;t]) List|
||L|| < ||arity f||
∧ (||vs|| = (fst(arity f[||L||])) ∈ ℤ)
∧ (∀i:ℕ||L||. ((sort (fst(L[i]))) = (snd(arity f[i])) ∈ ℤ))}
⟶ P
((∀p:P. ∀v:{v:varname()| ¬(v = nullvar() ∈ varname())} . R[p;varterm(v)])
⇒ (∀p:P. ∀f:opr. ∀bts:wf-bound-terms(opr;sort;arity;f). ∀L:{L:(t:wfterm(opr;sort;arity) × p:P × R[p;t]) List|
(||L|| = ||bts|| ∈ ℤ)
∧ (∀i:ℕ||L||
((fst(L[i])) = (snd(bts[i])) ∈ term(opr)))
∧ (∀i:ℕ||L||
((fst(snd(L[i])))
= Q[p;f;fst(bts[i]);firstn(i;L)]
∈ P))} .
R[p;mkwfterm(f;bts)])
⇒ (∀p:P. ∀t:wfterm(opr;sort;arity). R[p;t]))
Home
Index