Step
*
of Lemma
pW-rec_wf
∀[P:Type]. ∀[A:P ⟶ Type]. ∀[B:p:P ⟶ A[p] ⟶ Type]. ∀[C:p:P ⟶ a:A[p] ⟶ B[p;a] ⟶ P]. ∀[Q:par:P ⟶ (pW par) ⟶ ℙ].
∀[ind:par:P
⟶ a:A[par]
⟶ f:(b:B[par;a] ⟶ (pW C[par;a;b]))
⟶ (b:B[par;a] ⟶ Q[C[par;a;b];f b])
⟶ Q[par;pW-sup(a;f)]]. ∀[par:P]. ∀[w:pW par].
(let ind(p,a,f,G) = ind[p;a;f;G] in
letrec F(p,w) = let a,f=w in
ind(p,a,f,λb.F(C[p;a;b],f(b)) in
F(par;w) ∈ Q[par;w])
BY
{ (InstLemma `pcw-step_wf` []
THEN RepeatFor 4 (ParallelLast')
THEN InstLemma `param-W_wf` [⌜P⌝;⌜A⌝;⌜B⌝;⌜C⌝]⋅
THEN Auto
THEN (InstLemma `param-W-rel_wf` [⌜P⌝;⌜A⌝;⌜B⌝;⌜C⌝;⌜par⌝;⌜w⌝]⋅ THENA Auto)
THEN (InstLemma `pcw-pp-barred_wf0` [⌜P⌝;⌜A⌝;⌜B⌝;⌜C⌝]⋅ THENA Auto)
THEN (Assert ⌜(λn,s. if (0) < (n)
then let q,w',d = s (n - 1) in
case d
of inl(b) =>
let a,f = w'
in let ind(p,a,f,G) = ind[p;a;f;G] in
letrec F(p,w) = let a,f=w in
ind(p,a,f,λb.F(C[p;a;b],f(b)) in
F(C[q;a;b];f b)
| inr(z) =>
Ax
else let ind(p,a,f,G) = ind[p;a;f;G] in
letrec F(p,w) = let a,f=w in
ind(p,a,f,λb.F(C[p;a;b],f(b)) in
F(par;w))
0
⊥ ∈ (λn,s. if (0) < (n)
then let q,w',d = s (n - 1) in
case d of inl(b) => let a,f = w' in Q[C[q;a;b];f b] | inr(z) => True
else Q[par;w])
0
⊥⌝⋅
THENM (Reduce (-1) THEN Trivial)
)
THEN (Strong_Bar_Induction ⌜pcw-step(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b])⌝
⌜param-W-rel(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b];par;w)⌝ ⌜λn,ss. Barred(<n, ss>)⌝⋅
THENA Auto
)
THEN All Reduce
THEN Try ((Fold `decidable` 0 THEN UsingVars [`P';`A';`B';`C'] Auto⋅))) }
1
1. P : Type
2. A : P ⟶ Type
3. B : p:P ⟶ A[p] ⟶ Type
4. C : p:P ⟶ a:A[p] ⟶ B[p;a] ⟶ P
5. pcw-step(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b]) ∈ Type
6. pW ∈ P ⟶ Type
7. Q : par:P ⟶ (pW par) ⟶ ℙ
8. ind : par:P
⟶ a:A[par]
⟶ f:(b:B[par;a] ⟶ (pW C[par;a;b]))
⟶ (b:B[par;a] ⟶ Q[C[par;a;b];f b])
⟶ Q[par;pW-sup(a;f)]
9. par : P
10. w : pW par
11. param-W-rel(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b];par;w) ∈ n:ℕ
⟶ (ℕn ⟶ pcw-step(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b]))
⟶ pcw-step(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b])
⟶ ℙ
12. ∀[pp:n:ℕ × (ℕn ⟶ pcw-step(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b]))]. (Barred(pp) ∈ ℙ)
13. alpha : ℕ ⟶ pcw-step(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b])
14. ∀n:ℕ. (param-W-rel(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b];par;w) n alpha (alpha n))
⊢ ↓∃n:ℕ. Barred(<n, alpha>)
2
1. P : Type
2. A : P ⟶ Type
3. B : p:P ⟶ A[p] ⟶ Type
4. C : p:P ⟶ a:A[p] ⟶ B[p;a] ⟶ P
5. pcw-step(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b]) ∈ Type
6. pW ∈ P ⟶ Type
7. Q : par:P ⟶ (pW par) ⟶ ℙ
8. ind : par:P
⟶ a:A[par]
⟶ f:(b:B[par;a] ⟶ (pW C[par;a;b]))
⟶ (b:B[par;a] ⟶ Q[C[par;a;b];f b])
⟶ Q[par;pW-sup(a;f)]
9. par : P
10. w : pW par
11. param-W-rel(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b];par;w) ∈ n:ℕ
⟶ (ℕn ⟶ pcw-step(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b]))
⟶ pcw-step(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b])
⟶ ℙ
12. ∀[pp:n:ℕ × (ℕn ⟶ pcw-step(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b]))]. (Barred(pp) ∈ ℙ)
13. n : ℕ
14. s : ℕn ⟶ pcw-step(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b])
15. ∀%6:ℕn. (param-W-rel(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b];par;w) %6 s (s %6))
16. m : Barred(<n, s>)
⊢ if (0) < (n)
then let q,w',d = s (n - 1) in
case d
of inl(b) =>
let a,f = w'
in let ind(p,a,f,G) = ind[p;a;f;G] in
letrec F(p,w) = let a,f=w in
ind(p,a,f,λb.F(C[p;a;b],f(b)) in
F(C[q;a;b];f b)
| inr(z) =>
Ax
else let ind(p,a,f,G) = ind[p;a;f;G] in
letrec F(p,w) = let a,f=w in
ind(p,a,f,λb.F(C[p;a;b],f(b)) in
F(par;w) ∈ if (0) < (n)
then let q,w',d = s (n - 1) in
case d of inl(b) => let a,f = w' in Q[C[q;a;b];f b] | inr(z) => True
else Q[par;w]
3
1. P : Type
2. A : P ⟶ Type
3. B : p:P ⟶ A[p] ⟶ Type
4. C : p:P ⟶ a:A[p] ⟶ B[p;a] ⟶ P
5. pcw-step(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b]) ∈ Type
6. pW ∈ P ⟶ Type
7. Q : par:P ⟶ (pW par) ⟶ ℙ
8. ind : par:P
⟶ a:A[par]
⟶ f:(b:B[par;a] ⟶ (pW C[par;a;b]))
⟶ (b:B[par;a] ⟶ Q[C[par;a;b];f b])
⟶ Q[par;pW-sup(a;f)]
9. par : P
10. w : pW par
11. param-W-rel(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b];par;w) ∈ n:ℕ
⟶ (ℕn ⟶ pcw-step(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b]))
⟶ pcw-step(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b])
⟶ ℙ
12. ∀[pp:n:ℕ × (ℕn ⟶ pcw-step(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b]))]. (Barred(pp) ∈ ℙ)
13. n : ℕ
14. s : ℕn ⟶ pcw-step(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b])
15. ∀%6:ℕn. (param-W-rel(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b];par;w) %6 s (s %6))
16. ∀t:{t:pcw-step(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b])| param-W-rel(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b];par;w) n s t}
(if (0) < (n + 1)
then let q,w',d = if (n + 1) - 1=n then t else (s ((n + 1) - 1)) in
case d
of inl(b) =>
let a,f = w'
in let ind(p,a,f,G) = ind[p;a;f;G] in
letrec F(p,w) = let a,f=w in
ind(p,a,f,λb.F(C[p;a;b],f(b)) in
F(C[q;a;b];f b)
| inr(z) =>
Ax
else let ind(p,a,f,G) = ind[p;a;f;G] in
letrec F(p,w) = let a,f=w in
ind(p,a,f,λb.F(C[p;a;b],f(b)) in
F(par;w) ∈ if (0) < (n + 1)
then let q,w',d = if (n + 1) - 1=n then t else (s ((n + 1) - 1)) in
case d of inl(b) => let a,f = w' in Q[C[q;a;b];f b] | inr(z) => True
else Q[par;w])
⊢ if (0) < (n)
then let q,w',d = s (n - 1) in
case d
of inl(b) =>
let a,f = w'
in let ind(p,a,f,G) = ind[p;a;f;G] in
letrec F(p,w) = let a,f=w in
ind(p,a,f,λb.F(C[p;a;b],f(b)) in
F(C[q;a;b];f b)
| inr(z) =>
Ax
else let ind(p,a,f,G) = ind[p;a;f;G] in
letrec F(p,w) = let a,f=w in
ind(p,a,f,λb.F(C[p;a;b],f(b)) in
F(par;w) ∈ if (0) < (n)
then let q,w',d = s (n - 1) in
case d of inl(b) => let a,f = w' in Q[C[q;a;b];f b] | inr(z) => True
else Q[par;w]
Latex:
Latex:
\mforall{}[P:Type]. \mforall{}[A:P {}\mrightarrow{} Type]. \mforall{}[B:p:P {}\mrightarrow{} A[p] {}\mrightarrow{} Type]. \mforall{}[C:p:P {}\mrightarrow{} a:A[p] {}\mrightarrow{} B[p;a] {}\mrightarrow{} P]. \mforall{}[Q:par:P
{}\mrightarrow{} (pW
par)
{}\mrightarrow{} \mBbbP{}].
\mforall{}[ind:par:P
{}\mrightarrow{} a:A[par]
{}\mrightarrow{} f:(b:B[par;a] {}\mrightarrow{} (pW C[par;a;b]))
{}\mrightarrow{} (b:B[par;a] {}\mrightarrow{} Q[C[par;a;b];f b])
{}\mrightarrow{} Q[par;pW-sup(a;f)]]. \mforall{}[par:P]. \mforall{}[w:pW par].
(let ind(p,a,f,G) = ind[p;a;f;G] in
letrec F(p,w) = let a,f=w in
ind(p,a,f,\mlambda{}b.F(C[p;a;b],f(b)) in
F(par;w) \mmember{} Q[par;w])
By
Latex:
(InstLemma `pcw-step\_wf` []
THEN RepeatFor 4 (ParallelLast')
THEN InstLemma `param-W\_wf` [\mkleeneopen{}P\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}B\mkleeneclose{};\mkleeneopen{}C\mkleeneclose{}]\mcdot{}
THEN Auto
THEN (InstLemma `param-W-rel\_wf` [\mkleeneopen{}P\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}B\mkleeneclose{};\mkleeneopen{}C\mkleeneclose{};\mkleeneopen{}par\mkleeneclose{};\mkleeneopen{}w\mkleeneclose{}]\mcdot{} THENA Auto)
THEN (InstLemma `pcw-pp-barred\_wf0` [\mkleeneopen{}P\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}B\mkleeneclose{};\mkleeneopen{}C\mkleeneclose{}]\mcdot{} THENA Auto)
THEN (Assert \mkleeneopen{}(\mlambda{}n,s. if (0) < (n)
then let q,w',d = s (n - 1) in
case d
of inl(b) =>
let a,f = w'
in let ind(p,a,f,G) = ind[p;a;f;G] in
letrec F(p,w) = let a,f=w in
ind(p,a,f,\mlambda{}b.F(C[p;a;b],f(b)) in
F(C[q;a;b];f b)
| inr(z) =>
Ax
else let ind(p,a,f,G) = ind[p;a;f;G] in
letrec F(p,w) = let a,f=w in
ind(p,a,f,\mlambda{}b.F(C[p;a;b],f(b)) in
F(par;w))
0
\mbot{} \mmember{} (\mlambda{}n,s. if (0) < (n)
then let q,w',d = s (n - 1) in
case d
of inl(b) =>
let a,f = w'
in Q[C[q;a;b];f b]
| inr(z) =>
True
else Q[par;w])
0
\mbot{}\mkleeneclose{}\mcdot{}
THENM (Reduce (-1) THEN Trivial)
)
THEN (Strong\_Bar\_Induction \mkleeneopen{}pcw-step(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b])\mkleeneclose{}
\mkleeneopen{}param-W-rel(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b];par;w)\mkleeneclose{} \mkleeneopen{}\mlambda{}n,ss. Barred(<n, ss>)\mkleeneclose{}\mcdot{}
THENA Auto
)
THEN All Reduce
THEN Try ((Fold `decidable` 0 THEN UsingVars [`P';`A';`B';`C'] Auto\mcdot{})))
Home
Index