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