Step
*
1
of Lemma
cWO-induction_1
1. [T] : Type
2. [R] : T ⟶ T ⟶ ℙ
3. cWO(T;x,y.R[x;y])
4. [Q] : T ⟶ ℙ
5. ∀t:T. ((∀s:{s:T| R[t;s]} . Q[s]) ⇒ Q[t])
6. t : T
⊢ Q[t]
BY
{ InstLemma `basic_strong_bar_induction` [⌜T?⌝;⌜so_lambda(n,s,x.(0 < n ∧ (↑isl(x)))
⇒ ((↑isl(s (n - 1))) ∧ (R outl(s (n - 1)) outl(x))))⌝;⌜λ2n s.0 < n
∧ (↑isr(s
(n
- 1)))⌝;
⌜λ2n s.∀a:{a:T| 0 < n ⇒ ((↑isl(s (n - 1))) ∧ R[outl(s (n - 1));a])} . Q[a]⌝]⋅ }
1
.....wf.....
1. T : Type
2. R : T ⟶ T ⟶ ℙ
3. cWO(T;x,y.R[x;y])
4. Q : T ⟶ ℙ
5. ∀t:T. ((∀s:{s:T| R[t;s]} . Q[s]) ⇒ Q[t])
6. t : T
⊢ T? ∈ Type
2
.....wf.....
1. T : Type
2. R : T ⟶ T ⟶ ℙ
3. cWO(T;x,y.R[x;y])
4. Q : T ⟶ ℙ
5. ∀t:T. ((∀s:{s:T| R[t;s]} . Q[s]) ⇒ Q[t])
6. t : T
⊢ λn,s,x. ((0 < n ∧ (↑isl(x))) ⇒ ((↑isl(s (n - 1))) ∧ (R outl(s (n - 1)) outl(x)))) ∈ n:ℕ ⟶ (ℕn ⟶ (T?)) ⟶ (T?) ⟶ ℙ
3
.....wf.....
1. T : Type
2. R : T ⟶ T ⟶ ℙ
3. cWO(T;x,y.R[x;y])
4. Q : T ⟶ ℙ
5. ∀t:T. ((∀s:{s:T| R[t;s]} . Q[s]) ⇒ Q[t])
6. t : T
⊢ λn,s. (0 < n ∧ (↑isr(s (n - 1)))) ∈ n:ℕ
⟶ λn,s,x. ((0 < n ∧ (↑isl(x))) ⇒ ((↑isl(s (n - 1))) ∧ (R outl(s (n - 1)) outl(x))))-consistent-seq(n)
⟶ ℙ
4
.....wf.....
1. T : Type
2. R : T ⟶ T ⟶ ℙ
3. cWO(T;x,y.R[x;y])
4. Q : T ⟶ ℙ
5. ∀t:T. ((∀s:{s:T| R[t;s]} . Q[s]) ⇒ Q[t])
6. t : T
⊢ λn,s. ∀a:{a:T| 0 < n ⇒ ((↑isl(s (n - 1))) ∧ R[outl(s (n - 1));a])} . Q[a] ∈ n:ℕ
⟶ λn,s,x. ((0 < n ∧ (↑isl(x))) ⇒ ((↑isl(s (n - 1))) ∧ (R outl(s (n - 1)) outl(x))))-consistent-seq(n)
⟶ ℙ
5
.....antecedent.....
1. [T] : Type
2. [R] : T ⟶ T ⟶ ℙ
3. cWO(T;x,y.R[x;y])
4. [Q] : T ⟶ ℙ
5. ∀t:T. ((∀s:{s:T| R[t;s]} . Q[s]) ⇒ Q[t])
6. t : T
⊢ ∀n:ℕ. ∀s:so_lambda(n,s,x.(0 < n ∧ (↑isl(x))) ⇒ ((↑isl(s (n - 1))) ∧ (R outl(s (n - 1)) outl(x))))-consistent-seq(n).
Dec(0 < n ∧ (↑isr(s (n - 1))))
6
.....antecedent.....
1. [T] : Type
2. [R] : T ⟶ T ⟶ ℙ
3. cWO(T;x,y.R[x;y])
4. [Q] : T ⟶ ℙ
5. ∀t:T. ((∀s:{s:T| R[t;s]} . Q[s]) ⇒ Q[t])
6. t : T
⊢ ∀n:ℕ. ∀s:so_lambda(n,s,x.(0 < n ∧ (↑isl(x))) ⇒ ((↑isl(s (n - 1))) ∧ (R outl(s (n - 1)) outl(x))))-consistent-seq(n).
((0 < n ∧ (↑isr(s (n - 1)))) ⇒ (∀a:{a:T| 0 < n ⇒ ((↑isl(s (n - 1))) ∧ R[outl(s (n - 1));a])} . Q[a]))
7
.....antecedent.....
1. [T] : Type
2. [R] : T ⟶ T ⟶ ℙ
3. cWO(T;x,y.R[x;y])
4. [Q] : T ⟶ ℙ
5. ∀t:T. ((∀s:{s:T| R[t;s]} . Q[s]) ⇒ Q[t])
6. t : T
⊢ ∀n:ℕ. ∀s:so_lambda(n,s,x.(0 < n ∧ (↑isl(x))) ⇒ ((↑isl(s (n - 1))) ∧ (R outl(s (n - 1)) outl(x))))-consistent-seq(n).
((∀t:{t:T?| (0 < n ∧ (↑isl(t))) ⇒ ((↑isl(s (n - 1))) ∧ (R outl(s (n - 1)) outl(t)))} . ∀a:{a:T|
0 < n + 1
⇒ ((↑isl(s.t@n
((n + 1) - 1)))
∧ R[outl(s.t@n
((n + 1)
- 1));a])} .
Q[a])
⇒ (∀a:{a:T| 0 < n ⇒ ((↑isl(s (n - 1))) ∧ R[outl(s (n - 1));a])} . Q[a]))
8
.....antecedent.....
1. [T] : Type
2. [R] : T ⟶ T ⟶ ℙ
3. cWO(T;x,y.R[x;y])
4. [Q] : T ⟶ ℙ
5. ∀t:T. ((∀s:{s:T| R[t;s]} . Q[s]) ⇒ Q[t])
6. t : T
⊢ ∀alpha:{f:ℕ ⟶ (T?)| ∀x:ℕ. ((0 < x ∧ (↑isl(f x))) ⇒ ((↑isl(f (x - 1))) ∧ (R outl(f (x - 1)) outl(f x))))}
(↓∃m:ℕ. (0 < m ∧ (↑isr(alpha (m - 1)))))
9
1. [T] : Type
2. [R] : T ⟶ T ⟶ ℙ
3. cWO(T;x,y.R[x;y])
4. [Q] : T ⟶ ℙ
5. ∀t:T. ((∀s:{s:T| R[t;s]} . Q[s]) ⇒ Q[t])
6. t : T
7. ∀x:Top. ∀a:{a:T| 0 < 0 ⇒ ((↑isl(x (0 - 1))) ∧ R[outl(x (0 - 1));a])} . Q[a]
⊢ Q[t]
Latex:
Latex:
1. [T] : Type
2. [R] : T {}\mrightarrow{} T {}\mrightarrow{} \mBbbP{}
3. cWO(T;x,y.R[x;y])
4. [Q] : T {}\mrightarrow{} \mBbbP{}
5. \mforall{}t:T. ((\mforall{}s:\{s:T| R[t;s]\} . Q[s]) {}\mRightarrow{} Q[t])
6. t : T
\mvdash{} Q[t]
By
Latex:
InstLemma `basic\_strong\_bar\_induction` [\mkleeneopen{}T?\mkleeneclose{};\mkleeneopen{}so\_lambda(n,s,x.(0 < n \mwedge{} (\muparrow{}isl(x)))
{}\mRightarrow{} ((\muparrow{}isl(s (n - 1))) \mwedge{} (R outl(s (n - 1)) outl(x))))\mkleeneclose{}
;\mkleeneopen{}\mlambda{}\msubtwo{}n s.0 < n \mwedge{} (\muparrow{}isr(s (n - 1)))\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}n s.\mforall{}a:\{a:T|
0 < n {}\mRightarrow{} ((\muparrow{}isl(s (n - 1))) \mwedge{} R[outl(s (n - 1));a])\}
Q[a]\mkleeneclose{}]\mcdot{}
Home
Index