Step
*
1
of Lemma
monotone-bar-induction-strict2
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-induction2` [⌜λ2n s.strictly-increasing-seq(n;s) ⇒ B[n;s]⌝;
⌜λ2n s.strictly-increasing-seq(n;s) ⇒ Q[n;s]⌝]⋅
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])
5
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. ⇃(strictly-increasing-seq(0;λx.⊥) ⇒ Q[0;λx.⊥])
⊢ ⇃(Q[0;λx.⊥])
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{} \00D9(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{} \00D9(Q[n + 1;s.m@n]))) {}\mRightarrow{} \00D9(Q[n;s]))
6. \mforall{}alpha:StrictInc. \mexists{}m:\mBbbN{}. B[m;alpha]
\mvdash{} \00D9(Q[0;\mlambda{}x.\mbot{}])
By
Latex:
(InstLemma `monotone-bar-induction2` [\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{}
THENA Auto
)
Home
Index