---

Step * of Lemma descending-chain-barred-implies-wellfounded

∀[T:Type]. ∀[<,B:T ⟶ T ⟶ ℙ].
  ((∀x,y,z:T.  ((x < y) ⇒ (y < z) ⇒ (x < z)))
  ⇒ (∀x,y:T.  Dec(x B y))
  ⇒ (∀x,y:T.  ((x B y) ⇒ (¬(x < y))))
  ⇒ (∀f:ℕ ⟶ T. (↓∃j:ℕ. ∃i:ℕj. ((f j) B (f i))))
  ⇒ WellFnd{i}(T;x,y.x < y))
BY
{ (Auto
   THEN (D 0 THEN Auto)
   THEN (InstLemma `basic_bar_induction` [⌜T⌝;⌜λ2n s.∃j:ℕn. ∃i:ℕj. ((s j) B (s i))⌝;⌜λ2n s.∀m:ℕ. ∀s':ℕm ⟶ T.
                                                                                             ((n ≤ m)
                                                                                             ⇒ (∀i:ℕn
                                                                                                   ((s' i) = (s i) ∈ T))
                                                                                             ⇒ (∀j:ℕm. ∀i:ℕj.
                                                                                                   ((s' j) < (s' i)))
                                                                                             ⇒ 0 < m
                                                                                             ⇒ P[s' (m - 1)])⌝]⋅
         THENA Auto
         )) }

1
1. [T] : Type
2. [<] : T ⟶ T ⟶ ℙ
3. [B] : T ⟶ T ⟶ ℙ
4. ∀x,y,z:T.  ((x < y) ⇒ (y < z) ⇒ (x < z))
5. ∀x,y:T.  Dec(x B y)
6. ∀x,y:T.  ((x B y) ⇒ (¬(x < y)))
7. ∀f:ℕ ⟶ T. (↓∃j:ℕ. ∃i:ℕj. ((f j) B (f i)))
8. [P] : T ⟶ ℙ
9. ∀j:T. ((∀k:T. ((k < j) ⇒ P[k])) ⇒ P[j])
10. n : ℕ
11. s : ℕn ⟶ T
12. ∃j:ℕn. ∃i:ℕj. ((s j) B (s i))
13. m : ℕ
14. s' : ℕm ⟶ T
15. n ≤ m
16. ∀i:ℕn. ((s' i) = (s i) ∈ T)
17. ∀j:ℕm. ∀i:ℕj.  ((s' j) < (s' i))
18. 0 < m
⊢ P[s' (m - 1)]

2
1. [T] : Type
2. [<] : T ⟶ T ⟶ ℙ
3. [B] : T ⟶ T ⟶ ℙ
4. ∀x,y,z:T.  ((x < y) ⇒ (y < z) ⇒ (x < z))
5. ∀x,y:T.  Dec(x B y)
6. ∀x,y:T.  ((x B y) ⇒ (¬(x < y)))
7. ∀f:ℕ ⟶ T. (↓∃j:ℕ. ∃i:ℕj. ((f j) B (f i)))
8. [P] : T ⟶ ℙ
9. ∀j:T. ((∀k:T. ((k < j) ⇒ P[k])) ⇒ P[j])
10. n : ℕ
11. s : ℕn ⟶ T
12. ∀t:T. ∀m:ℕ. ∀s':ℕm ⟶ T.
      (((n + 1) ≤ m)
      ⇒ (∀i:ℕn + 1. ((s' i) = (s++t i) ∈ T))
      ⇒ (∀j:ℕm. ∀i:ℕj.  ((s' j) < (s' i)))
      ⇒ 0 < m
      ⇒ P[s' (m - 1)])
13. m : ℕ
14. s' : ℕm ⟶ T
15. n ≤ m
16. ∀i:ℕn. ((s' i) = (s i) ∈ T)
17. ∀j:ℕm. ∀i:ℕj.  ((s' j) < (s' i))
18. 0 < m
⊢ P[s' (m - 1)]

3
1. T : Type
2. < : T ⟶ T ⟶ ℙ
3. B : T ⟶ T ⟶ ℙ
4. ∀x,y,z:T.  ((x < y) ⇒ (y < z) ⇒ (x < z))
5. ∀x,y:T.  Dec(x B y)
6. ∀x,y:T.  ((x B y) ⇒ (¬(x < y)))
7. ∀f:ℕ ⟶ T. (↓∃j:ℕ. ∃i:ℕj. ((f j) B (f i)))
8. P : T ⟶ ℙ
9. ∀j:T. ((∀k:T. ((k < j) ⇒ P[k])) ⇒ P[j])
10. alpha : ℕ ⟶ T
⊢ ↓∃m:ℕ. ∃j:ℕm. ∃i:ℕj. ((alpha j) B (alpha i))

4
1. [T] : Type
2. [<] : T ⟶ T ⟶ ℙ
3. [B] : T ⟶ T ⟶ ℙ
4. ∀x,y,z:T.  ((x < y) ⇒ (y < z) ⇒ (x < z))
5. ∀x,y:T.  Dec(x B y)
6. ∀x,y:T.  ((x B y) ⇒ (¬(x < y)))
7. ∀f:ℕ ⟶ T. (↓∃j:ℕ. ∃i:ℕj. ((f j) B (f i)))
8. [P] : T ⟶ ℙ
9. ∀j:T. ((∀k:T. ((k < j) ⇒ P[k])) ⇒ P[j])
10. ∀x:Top. ∀m:ℕ. ∀s':ℕm ⟶ T.
      ((0 ≤ m) ⇒ (∀i:ℕ0. ((s' i) = (x i) ∈ T)) ⇒ (∀j:ℕm. ∀i:ℕj.  ((s' j) < (s' i))) ⇒ 0 < m ⇒ P[s' (m - 1)])
⊢ {∀n:T. P[n]}

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[<,B:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].
    ((\mforall{}x,y,z:T.    ((x  <  y)  {}\mRightarrow{}  (y  <  z)  {}\mRightarrow{}  (x  <  z)))
    {}\mRightarrow{}  (\mforall{}x,y:T.    Dec(x  B  y))
    {}\mRightarrow{}  (\mforall{}x,y:T.    ((x  B  y)  {}\mRightarrow{}  (\mneg{}(x  <  y))))
    {}\mRightarrow{}  (\mforall{}f:\mBbbN{}  {}\mrightarrow{}  T.  (\mdownarrow{}\mexists{}j:\mBbbN{}.  \mexists{}i:\mBbbN{}j.  ((f  j)  B  (f  i))))
    {}\mRightarrow{}  WellFnd\{i\}(T;x,y.x  <  y))


By

---

Latex:
(Auto
  THEN  (D  0  THEN  Auto)
  THEN  (InstLemma  `basic\_bar\_induction`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}n  s.\mexists{}j:\mBbbN{}n.  \mexists{}i:\mBbbN{}j.  ((s  j)  B  (s  i))\mkleeneclose{};
              \mkleeneopen{}\mlambda{}\msubtwo{}n  s.\mforall{}m:\mBbbN{}.  \mforall{}s':\mBbbN{}m  {}\mrightarrow{}  T.
                                ((n  \mleq{}  m)
                                {}\mRightarrow{}  (\mforall{}i:\mBbbN{}n.  ((s'  i)  =  (s  i)))
                                {}\mRightarrow{}  (\mforall{}j:\mBbbN{}m.  \mforall{}i:\mBbbN{}j.    ((s'  j)  <  (s'  i)))
                                {}\mRightarrow{}  0  <  m
                                {}\mRightarrow{}  P[s'  (m  -  1)])\mkleeneclose{}]\mcdot{}
              THENA  Auto
              ))

---

Home Index