Step
*
1
4
3
1
of Lemma
term-accum_wf_wfterm
1. opr : Type
2. P : Type
3. sort : term(opr) ⟶ ℕ
4. arity : opr ⟶ ((ℕ × ℕ) List)
5. R : P ⟶ wfterm(opr;sort;arity) ⟶ ℙ
6. 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
7. varcase : p:P ⟶ v:{v:varname()| ¬(v = nullvar() ∈ varname())} ⟶ (R p varterm(v))
8. 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))
9. t : wfterm(opr;sort;arity)
10. p : P
11. ok : ∀f:opr. ∀vs:varname() List. ∀L:(t:term(opr) × p:P × R p t supposing ↑wf-term(arity;sort;t)) List.
Dec(||L|| < ||arity f||
∧ (||vs|| = (fst(arity f[||L||])) ∈ ℤ)
∧ (∀i:ℕ||L||. ((sort (fst(L[i]))) = (snd(arity f[i])) ∈ ℤ))
∧ (∀i:ℕ||L||. (↑wf-term(arity;sort;fst(L[i])))))
12. ∀f:opr. ∀vs:varname() List. ∀L:(t:term(opr) × p:P × R p t supposing ↑wf-term(arity;sort;t)) List.
(↑isl(ok f vs L)
⇐⇒ ||L|| < ||arity f||
∧ (||vs|| = (fst(arity f[||L||])) ∈ ℤ)
∧ (∀i:ℕ||L||. ((sort (fst(L[i]))) = (snd(arity f[i])) ∈ ℤ))
∧ (∀i:ℕ||L||. (↑wf-term(arity;sort;fst(L[i])))))
13. QQ : P ⟶ opr ⟶ (varname() List) ⟶ ((t:term(opr) × p:P × R p t supposing ↑wf-term(arity;sort;t)) List) ⟶ P
14. (λp,f,vs,L. if isl(ok f vs L) then Q p f vs L else p fi )
= QQ
∈ (P ⟶ opr ⟶ (varname() List) ⟶ ((t:term(opr) × p:P × R p t supposing ↑wf-term(arity;sort;t)) List) ⟶ P)
⊢ term-accum(t with p)
p,f,vs,tr.(λp,f,vs,L. if isl(ok f vs L) then Q p f vs L else p fi ) p f vs tr
varterm(x) with p ⇒ varcase p x
mkterm(f,bts) with p ⇒ trs.mktermcase p f bts trs ~ 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
BY
{ ((Enough to prove ∀n:ℕ. ∀a:{a:wfterm(opr;sort;arity)| term-size(a) ≤ n} .
(λp.Ax ∈ ∀p:P
(term-accum(a with p)
p,f,vs,trs.(λp,f,vs,L. if isl(ok f vs L) then Q p f vs L else p fi ) p f vs trs
varterm(x) with p ⇒ varcase p x
mkterm(f,bts) with p ⇒ trs.mktermcase p f bts trs
~ term-accum(a with p)
p,f,vs,trs.Q p f vs trs
varterm(x) with p ⇒ varcase p x
mkterm(f,bts) with p ⇒ trs.mktermcase p f bts trs))
Because ((InstHyp [⌜term-size(t)⌝;⌜t⌝] (-1)⋅ THENA Auto)
THEN (Assert ∀p:P
(term-accum(t with p)
p,f,vs,trs.(λp,f,vs,L. if isl(ok f vs L) then Q p f vs L else p fi ) p f vs trs
varterm(x) with p ⇒ varcase p x
mkterm(f,bts) with p ⇒ trs.mktermcase p f bts trs
~ term-accum(t with p)
p,f,vs,trs.Q p f vs trs
varterm(x) with p ⇒ varcase p x
mkterm(f,bts) with p ⇒ trs.mktermcase p f bts trs) BY
UseWitness ⌜λp.Ax⌝⋅)
THEN BHyp -1
THEN Auto))
THEN Intro
THEN CompNatInd (-1)
THEN Intro
THEN D -1
THEN D -2
THEN RepeatFor 2 (MoveToConcl (-1))
THEN (InstLemma `term-ext` [⌜opr⌝]⋅ THENA Auto)
THEN (GenConcl ⌜a = t ∈ coterm-fun(opr;term(opr))⌝⋅ THENA Auto)
THEN ThinVar `a'
THEN (Assert t ∈ term(opr) BY
Auto)
THEN RepeatFor 2 (D -2)
THEN Folds ``varterm mkterm`` 0
THEN Reduce 0
THEN RepeatFor 2 (Intro)) }
1
1. opr : Type
2. P : Type
3. sort : term(opr) ⟶ ℕ
4. arity : opr ⟶ ((ℕ × ℕ) List)
5. R : P ⟶ wfterm(opr;sort;arity) ⟶ ℙ
6. 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
7. varcase : p:P ⟶ v:{v:varname()| ¬(v = nullvar() ∈ varname())} ⟶ (R p varterm(v))
8. 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))
9. t : wfterm(opr;sort;arity)
10. p : P
11. ok : ∀f:opr. ∀vs:varname() List. ∀L:(t:term(opr) × p:P × R p t supposing ↑wf-term(arity;sort;t)) List.
Dec(||L|| < ||arity f||
∧ (||vs|| = (fst(arity f[||L||])) ∈ ℤ)
∧ (∀i:ℕ||L||. ((sort (fst(L[i]))) = (snd(arity f[i])) ∈ ℤ))
∧ (∀i:ℕ||L||. (↑wf-term(arity;sort;fst(L[i])))))
12. ∀f:opr. ∀vs:varname() List. ∀L:(t:term(opr) × p:P × R p t supposing ↑wf-term(arity;sort;t)) List.
(↑isl(ok f vs L)
⇐⇒ ||L|| < ||arity f||
∧ (||vs|| = (fst(arity f[||L||])) ∈ ℤ)
∧ (∀i:ℕ||L||. ((sort (fst(L[i]))) = (snd(arity f[i])) ∈ ℤ))
∧ (∀i:ℕ||L||. (↑wf-term(arity;sort;fst(L[i])))))
13. QQ : P ⟶ opr ⟶ (varname() List) ⟶ ((t:term(opr) × p:P × R p t supposing ↑wf-term(arity;sort;t)) List) ⟶ P
14. (λp,f,vs,L. if isl(ok f vs L) then Q p f vs L else p fi )
= QQ
∈ (P ⟶ opr ⟶ (varname() List) ⟶ ((t:term(opr) × p:P × R p t supposing ↑wf-term(arity;sort;t)) List) ⟶ P)
15. n : ℕ
16. ∀n:ℕn. ∀a:{a:wfterm(opr;sort;arity)| term-size(a) ≤ n} .
(λp.Ax ∈ ∀p:P
(term-accum(a with p)
p,f,vs,trs.(λp,f,vs,L. if isl(ok f vs L) then Q p f vs L else p fi ) p f vs trs
varterm(x) with p ⇒ varcase p x
mkterm(f,bts) with p ⇒ trs.mktermcase p f bts trs ~ term-accum(a with p)
p,f,vs,trs.Q p f vs trs
varterm(x) with p ⇒ varcase p x
mkterm(f,bts) with p ⇒ trs.mktermcase p f bts
trs))
17. term(opr) ≡ coterm-fun(opr;term(opr))
18. x : varname()
19. [%11] : ¬(x = nullvar() ∈ varname())
20. t ∈ term(opr)
21. True
22. 1 ≤ n
⊢ λp.Ax ∈ ∀p:P. (varcase p x ~ varcase p x)
2
1. opr : Type
2. P : Type
3. sort : term(opr) ⟶ ℕ
4. arity : opr ⟶ ((ℕ × ℕ) List)
5. R : P ⟶ wfterm(opr;sort;arity) ⟶ ℙ
6. 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
7. varcase : p:P ⟶ v:{v:varname()| ¬(v = nullvar() ∈ varname())} ⟶ (R p varterm(v))
8. 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))
9. t : wfterm(opr;sort;arity)
10. p : P
11. ok : ∀f:opr. ∀vs:varname() List. ∀L:(t:term(opr) × p:P × R p t supposing ↑wf-term(arity;sort;t)) List.
Dec(||L|| < ||arity f||
∧ (||vs|| = (fst(arity f[||L||])) ∈ ℤ)
∧ (∀i:ℕ||L||. ((sort (fst(L[i]))) = (snd(arity f[i])) ∈ ℤ))
∧ (∀i:ℕ||L||. (↑wf-term(arity;sort;fst(L[i])))))
12. ∀f:opr. ∀vs:varname() List. ∀L:(t:term(opr) × p:P × R p t supposing ↑wf-term(arity;sort;t)) List.
(↑isl(ok f vs L)
⇐⇒ ||L|| < ||arity f||
∧ (||vs|| = (fst(arity f[||L||])) ∈ ℤ)
∧ (∀i:ℕ||L||. ((sort (fst(L[i]))) = (snd(arity f[i])) ∈ ℤ))
∧ (∀i:ℕ||L||. (↑wf-term(arity;sort;fst(L[i])))))
13. QQ : P ⟶ opr ⟶ (varname() List) ⟶ ((t:term(opr) × p:P × R p t supposing ↑wf-term(arity;sort;t)) List) ⟶ P
14. (λp,f,vs,L. if isl(ok f vs L) then Q p f vs L else p fi )
= QQ
∈ (P ⟶ opr ⟶ (varname() List) ⟶ ((t:term(opr) × p:P × R p t supposing ↑wf-term(arity;sort;t)) List) ⟶ P)
15. n : ℕ
16. ∀n:ℕn. ∀a:{a:wfterm(opr;sort;arity)| term-size(a) ≤ n} .
(λp.Ax ∈ ∀p:P
(term-accum(a with p)
p,f,vs,trs.(λp,f,vs,L. if isl(ok f vs L) then Q p f vs L else p fi ) p f vs trs
varterm(x) with p ⇒ varcase p x
mkterm(f,bts) with p ⇒ trs.mktermcase p f bts trs ~ term-accum(a with p)
p,f,vs,trs.Q p f vs trs
varterm(x) with p ⇒ varcase p x
mkterm(f,bts) with p ⇒ trs.mktermcase p f bts
trs))
17. term(opr) ≡ coterm-fun(opr;term(opr))
18. y1 : opr
19. y2 : (varname() List × term(opr)) List
20. t ∈ term(opr)
21. ↑wf-term(arity;sort;mkterm(y1;y2))
22. (1 + Σ(term-size(snd(bt)) | bt ∈ y2)) ≤ n
⊢ λp.Ax ∈ ∀p:P
(let trs = accumulate (with value trs and list item bt):
let p' = if isl(ok y1 (fst(bt)) trs) then Q p y1 (fst(bt)) trs else p fi in
trs
@ [<snd(bt)
, p'
, term-accum(snd(bt) with p')
p,f,vs,trs.if isl(ok f vs trs) then Q p f vs trs else p fi
varterm(x) with p ⇒ varcase p x
mkterm(f,bts) with p ⇒ trs.mktermcase p f bts trs>]
over list:
y2
with starting value:
[]) in
mktermcase p y1 y2 trs ~ let trs = accumulate (with value trs and list item bt):
let p' = Q p y1 (fst(bt)) trs in
trs
@ [<snd(bt)
, p'
, term-accum(snd(bt) with p')
p,f,vs,trs.Q p f vs trs
varterm(x) with p ⇒ varcase p x
mkterm(f,bts) with p ⇒ trs.mktermcase p f bts trs>]
over list:
y2
with starting value:
[]) in
mktermcase p y1 y2 trs)
Latex:
Latex:
1. opr : Type
2. P : Type
3. sort : term(opr) {}\mrightarrow{} \mBbbN{}
4. arity : opr {}\mrightarrow{} ((\mBbbN{} \mtimes{} \mBbbN{}) List)
5. R : P {}\mrightarrow{} wfterm(opr;sort;arity) {}\mrightarrow{} \mBbbP{}
6. Q : P
{}\mrightarrow{} f:opr
{}\mrightarrow{} vs:(varname() List)
{}\mrightarrow{} \{L:(t:wfterm(opr;sort;arity) \mtimes{} p:P \mtimes{} (R p t)) List|
||L|| < ||arity f||
\mwedge{} (||vs|| = (fst(arity f[||L||])))
\mwedge{} (\mforall{}i:\mBbbN{}||L||. ((sort (fst(L[i]))) = (snd(arity f[i]))))\}
{}\mrightarrow{} P
7. varcase : p:P {}\mrightarrow{} v:\{v:varname()| \mneg{}(v = nullvar())\} {}\mrightarrow{} (R p varterm(v))
8. mktermcase : p:P
{}\mrightarrow{} f:opr
{}\mrightarrow{} bts:wf-bound-terms(opr;sort;arity;f)
{}\mrightarrow{} L:\{L:(t:wfterm(opr;sort;arity) \mtimes{} p:P \mtimes{} (R p t)) List|
(||L|| = ||bts||)
\mwedge{} (\mforall{}i:\mBbbN{}||L||. ((fst(L[i])) = (snd(bts[i]))))
\mwedge{} (\mforall{}i:\mBbbN{}||L||. ((fst(snd(L[i]))) = (Q p f (fst(bts[i])) firstn(i;L))))\}
{}\mrightarrow{} (R p mkwfterm(f;bts))
9. t : wfterm(opr;sort;arity)
10. p : P
11. ok : \mforall{}f:opr. \mforall{}vs:varname() List.
\mforall{}L:(t:term(opr) \mtimes{} p:P \mtimes{} R p t supposing \muparrow{}wf-term(arity;sort;t)) List.
Dec(||L|| < ||arity f||
\mwedge{} (||vs|| = (fst(arity f[||L||])))
\mwedge{} (\mforall{}i:\mBbbN{}||L||. ((sort (fst(L[i]))) = (snd(arity f[i]))))
\mwedge{} (\mforall{}i:\mBbbN{}||L||. (\muparrow{}wf-term(arity;sort;fst(L[i])))))
12. \mforall{}f:opr. \mforall{}vs:varname() List.
\mforall{}L:(t:term(opr) \mtimes{} p:P \mtimes{} R p t supposing \muparrow{}wf-term(arity;sort;t)) List.
(\muparrow{}isl(ok f vs L)
\mLeftarrow{}{}\mRightarrow{} ||L|| < ||arity f||
\mwedge{} (||vs|| = (fst(arity f[||L||])))
\mwedge{} (\mforall{}i:\mBbbN{}||L||. ((sort (fst(L[i]))) = (snd(arity f[i]))))
\mwedge{} (\mforall{}i:\mBbbN{}||L||. (\muparrow{}wf-term(arity;sort;fst(L[i])))))
13. QQ : P
{}\mrightarrow{} opr
{}\mrightarrow{} (varname() List)
{}\mrightarrow{} ((t:term(opr) \mtimes{} p:P \mtimes{} R p t supposing \muparrow{}wf-term(arity;sort;t)) List)
{}\mrightarrow{} P
14. (\mlambda{}p,f,vs,L. if isl(ok f vs L) then Q p f vs L else p fi ) = QQ
\mvdash{} term-accum(t with p)
p,f,vs,tr.(\mlambda{}p,f,vs,L. if isl(ok f vs L) then Q p f vs L else p fi ) p f vs tr
varterm(x) with p {}\mRightarrow{} varcase p x
mkterm(f,bts) with p {}\mRightarrow{} trs.mktermcase p f bts trs \msim{} term-accum(t with p)
p,f,vs,tr.Q p f vs tr
varterm(x) with p {}\mRightarrow{} varcase p x
mkterm(f,bts) with p {}\mRightarrow{} trs.mktermcase p f
bts
trs
By
Latex:
((Enough to prove \mforall{}n:\mBbbN{}. \mforall{}a:\{a:wfterm(opr;sort;arity)| term-size(a) \mleq{} n\} .
(\mlambda{}p.Ax \mmember{} \mforall{}p:P
(term-accum(a with p)
p,f,vs,trs.(\mlambda{}p,f,vs,L. if isl(ok f vs L) then Q p f vs L else p fi )\000C p f vs
trs
varterm(x) with p {}\mRightarrow{} varcase p x
mkterm(f,bts) with p {}\mRightarrow{} trs.mktermcase p f bts trs
\msim{} term-accum(a with p)
p,f,vs,trs.Q p f vs trs
varterm(x) with p {}\mRightarrow{} varcase p x
mkterm(f,bts) with p {}\mRightarrow{} trs.mktermcase p f bts trs))
Because ((InstHyp [\mkleeneopen{}term-size(t)\mkleeneclose{};\mkleeneopen{}t\mkleeneclose{}] (-1)\mcdot{} THENA Auto)
THEN (Assert \mforall{}p:P
(term-accum(t with p)
p,f,vs,trs.(\mlambda{}p,f,vs,L. if isl(ok f vs L) then Q p f vs L else p fi ) p f\000C vs trs
varterm(x) with p {}\mRightarrow{} varcase p x
mkterm(f,bts) with p {}\mRightarrow{} trs.mktermcase p f bts trs
\msim{} term-accum(t with p)
p,f,vs,trs.Q p f vs trs
varterm(x) with p {}\mRightarrow{} varcase p x
mkterm(f,bts) with p {}\mRightarrow{} trs.mktermcase p f bts trs) BY
UseWitness \mkleeneopen{}\mlambda{}p.Ax\mkleeneclose{}\mcdot{})
THEN BHyp -1
THEN Auto))
THEN Intro
THEN CompNatInd (-1)
THEN Intro
THEN D -1
THEN D -2
THEN RepeatFor 2 (MoveToConcl (-1))
THEN (InstLemma `term-ext` [\mkleeneopen{}opr\mkleeneclose{}]\mcdot{} THENA Auto)
THEN (GenConcl \mkleeneopen{}a = t\mkleeneclose{}\mcdot{} THENA Auto)
THEN ThinVar `a'
THEN (Assert t \mmember{} term(opr) BY
Auto)
THEN RepeatFor 2 (D -2)
THEN Folds ``varterm mkterm`` 0
THEN Reduce 0
THEN RepeatFor 2 (Intro))
Home
Index