Step
*
1
of Lemma
monotone-bar-induction-strict
1. B : n:ℕ ⟶ {s:ℕn ⟶ ℕ| strictly-increasing-seq(n;s)} ⟶ ℙ
2. Q : n:ℕ ⟶ {s:ℕn ⟶ ℕ| strictly-increasing-seq(n;s)} ⟶ ℙ
3. ∀n:ℕ. ∀s:{s:ℕn ⟶ ℕ| strictly-increasing-seq(n;s)} .
(B[n;s] ⇒ (∀m:ℕ. (strictly-increasing-seq(n + 1;s.m@n) ⇒ B[n + 1;s.m@n])))
4. ∀n:ℕ. ∀s:{s:ℕn ⟶ ℕ| strictly-increasing-seq(n;s)} . (B[n;s] ⇒ (↓Q[n;s]))
5. ∀n:ℕ. ∀s:{s:ℕn ⟶ ℕ| strictly-increasing-seq(n;s)} .
((∀m:ℕ. (strictly-increasing-seq(n + 1;s.m@n) ⇒ (↓Q[n + 1;s.m@n]))) ⇒ (↓Q[n;s]))
6. ∀alpha:StrictInc. ∃m:ℕ. B[m;alpha]
⊢ ↓Q[0;λx.⊥]
BY
{ ((InstLemma `monotone-bar-induction1` [⌜λ2n s.strictly-increasing-seq(n;s) ⇒ B[n;s]⌝;
⌜λ2n s.strictly-increasing-seq(n;s) ⇒ Q[n;s]⌝]⋅
THENM (ParallelLast THEN BHyp -1 THEN D 0 THEN Auto)
)
THENA Auto
) }
1
1. B : n:ℕ ⟶ {s:ℕn ⟶ ℕ| strictly-increasing-seq(n;s)} ⟶ ℙ
2. Q : n:ℕ ⟶ {s:ℕn ⟶ ℕ| strictly-increasing-seq(n;s)} ⟶ ℙ
3. ∀n:ℕ. ∀s:{s:ℕn ⟶ ℕ| strictly-increasing-seq(n;s)} .
(B[n;s] ⇒ (∀m:ℕ. (strictly-increasing-seq(n + 1;s.m@n) ⇒ B[n + 1;s.m@n])))
4. ∀n:ℕ. ∀s:{s:ℕn ⟶ ℕ| strictly-increasing-seq(n;s)} . (B[n;s] ⇒ (↓Q[n;s]))
5. ∀n:ℕ. ∀s:{s:ℕn ⟶ ℕ| strictly-increasing-seq(n;s)} .
((∀m:ℕ. (strictly-increasing-seq(n + 1;s.m@n) ⇒ (↓Q[n + 1;s.m@n]))) ⇒ (↓Q[n;s]))
6. ∀alpha:StrictInc. ∃m:ℕ. B[m;alpha]
7. n : ℕ
8. s : ℕn ⟶ ℕ
9. strictly-increasing-seq(n;s) ⇒ B[n;s]
10. m : ℕ
11. strictly-increasing-seq(n + 1;s.m@n)
⊢ B[n + 1;s.m@n]
2
1. B : n:ℕ ⟶ {s:ℕn ⟶ ℕ| strictly-increasing-seq(n;s)} ⟶ ℙ
2. Q : n:ℕ ⟶ {s:ℕn ⟶ ℕ| strictly-increasing-seq(n;s)} ⟶ ℙ
3. ∀n:ℕ. ∀s:{s:ℕn ⟶ ℕ| strictly-increasing-seq(n;s)} .
(B[n;s] ⇒ (∀m:ℕ. (strictly-increasing-seq(n + 1;s.m@n) ⇒ B[n + 1;s.m@n])))
4. ∀n:ℕ. ∀s:{s:ℕn ⟶ ℕ| strictly-increasing-seq(n;s)} . (B[n;s] ⇒ (↓Q[n;s]))
5. ∀n:ℕ. ∀s:{s:ℕn ⟶ ℕ| strictly-increasing-seq(n;s)} .
((∀m:ℕ. (strictly-increasing-seq(n + 1;s.m@n) ⇒ (↓Q[n + 1;s.m@n]))) ⇒ (↓Q[n;s]))
6. ∀alpha:StrictInc. ∃m:ℕ. B[m;alpha]
7. n : ℕ
8. s : ℕn ⟶ ℕ
9. strictly-increasing-seq(n;s) ⇒ B[n;s]
⊢ ↓strictly-increasing-seq(n;s) ⇒ Q[n;s]
3
1. B : n:ℕ ⟶ {s:ℕn ⟶ ℕ| strictly-increasing-seq(n;s)} ⟶ ℙ
2. Q : n:ℕ ⟶ {s:ℕn ⟶ ℕ| strictly-increasing-seq(n;s)} ⟶ ℙ
3. ∀n:ℕ. ∀s:{s:ℕn ⟶ ℕ| strictly-increasing-seq(n;s)} .
(B[n;s] ⇒ (∀m:ℕ. (strictly-increasing-seq(n + 1;s.m@n) ⇒ B[n + 1;s.m@n])))
4. ∀n:ℕ. ∀s:{s:ℕn ⟶ ℕ| strictly-increasing-seq(n;s)} . (B[n;s] ⇒ (↓Q[n;s]))
5. ∀n:ℕ. ∀s:{s:ℕn ⟶ ℕ| strictly-increasing-seq(n;s)} .
((∀m:ℕ. (strictly-increasing-seq(n + 1;s.m@n) ⇒ (↓Q[n + 1;s.m@n]))) ⇒ (↓Q[n;s]))
6. ∀alpha:StrictInc. ∃m:ℕ. B[m;alpha]
7. n : ℕ
8. s : ℕn ⟶ ℕ
9. ∀m:ℕ. (↓strictly-increasing-seq(n + 1;s.m@n) ⇒ Q[n + 1;s.m@n])
⊢ ↓strictly-increasing-seq(n;s) ⇒ Q[n;s]
4
1. B : n:ℕ ⟶ {s:ℕn ⟶ ℕ| strictly-increasing-seq(n;s)} ⟶ ℙ
2. Q : n:ℕ ⟶ {s:ℕn ⟶ ℕ| strictly-increasing-seq(n;s)} ⟶ ℙ
3. ∀n:ℕ. ∀s:{s:ℕn ⟶ ℕ| strictly-increasing-seq(n;s)} .
(B[n;s] ⇒ (∀m:ℕ. (strictly-increasing-seq(n + 1;s.m@n) ⇒ B[n + 1;s.m@n])))
4. ∀n:ℕ. ∀s:{s:ℕn ⟶ ℕ| strictly-increasing-seq(n;s)} . (B[n;s] ⇒ (↓Q[n;s]))
5. ∀n:ℕ. ∀s:{s:ℕn ⟶ ℕ| strictly-increasing-seq(n;s)} .
((∀m:ℕ. (strictly-increasing-seq(n + 1;s.m@n) ⇒ (↓Q[n + 1;s.m@n]))) ⇒ (↓Q[n;s]))
6. ∀alpha:StrictInc. ∃m:ℕ. B[m;alpha]
7. alpha : ℕ ⟶ ℕ
⊢ ∃m:ℕ. (strictly-increasing-seq(m;alpha) ⇒ B[m;alpha])
Latex:
Latex:
1. B : n:\mBbbN{} {}\mrightarrow{} \{s:\mBbbN{}n {}\mrightarrow{} \mBbbN{}| strictly-increasing-seq(n;s)\} {}\mrightarrow{} \mBbbP{}
2. Q : n:\mBbbN{} {}\mrightarrow{} \{s:\mBbbN{}n {}\mrightarrow{} \mBbbN{}| strictly-increasing-seq(n;s)\} {}\mrightarrow{} \mBbbP{}
3. \mforall{}n:\mBbbN{}. \mforall{}s:\{s:\mBbbN{}n {}\mrightarrow{} \mBbbN{}| strictly-increasing-seq(n;s)\} .
(B[n;s] {}\mRightarrow{} (\mforall{}m:\mBbbN{}. (strictly-increasing-seq(n + 1;s.m@n) {}\mRightarrow{} B[n + 1;s.m@n])))
4. \mforall{}n:\mBbbN{}. \mforall{}s:\{s:\mBbbN{}n {}\mrightarrow{} \mBbbN{}| strictly-increasing-seq(n;s)\} . (B[n;s] {}\mRightarrow{} (\mdownarrow{}Q[n;s]))
5. \mforall{}n:\mBbbN{}. \mforall{}s:\{s:\mBbbN{}n {}\mrightarrow{} \mBbbN{}| strictly-increasing-seq(n;s)\} .
((\mforall{}m:\mBbbN{}. (strictly-increasing-seq(n + 1;s.m@n) {}\mRightarrow{} (\mdownarrow{}Q[n + 1;s.m@n]))) {}\mRightarrow{} (\mdownarrow{}Q[n;s]))
6. \mforall{}alpha:StrictInc. \mexists{}m:\mBbbN{}. B[m;alpha]
\mvdash{} \mdownarrow{}Q[0;\mlambda{}x.\mbot{}]
By
Latex:
((InstLemma `monotone-bar-induction1` [\mkleeneopen{}\mlambda{}\msubtwo{}n s.strictly-increasing-seq(n;s) {}\mRightarrow{} B[n;s]\mkleeneclose{};
\mkleeneopen{}\mlambda{}\msubtwo{}n s.strictly-increasing-seq(n;s) {}\mRightarrow{} Q[n;s]\mkleeneclose{}]\mcdot{}
THENM (ParallelLast THEN BHyp -1 THEN D 0 THEN Auto)
)
THENA Auto
)
Home
Index