---

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


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)]
BY
{ (BHyp 9 THEN Auto THEN InstHyp [⌜k⌝;⌜n + 1⌝;⌜s++k⌝] 12⋅ THEN 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. ∀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
19. k : T
20. k < (s' (m - 1))
21. j : ℕn + 1
22. i : ℕj
⊢ (s++k j) < (s++k i)

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
19. k : T
20. k < (s' (m - 1))
21. P[s++k ((n + 1) - 1)]
⊢ P[k]

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  [<]  :  T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}
3.  [B]  :  T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}
4.  \mforall{}x,y,z:T.    ((x  <  y)  {}\mRightarrow{}  (y  <  z)  {}\mRightarrow{}  (x  <  z))
5.  \mforall{}x,y:T.    Dec(x  B  y)
6.  \mforall{}x,y:T.    ((x  B  y)  {}\mRightarrow{}  (\mneg{}(x  <  y)))
7.  \mforall{}f:\mBbbN{}  {}\mrightarrow{}  T.  (\mdownarrow{}\mexists{}j:\mBbbN{}.  \mexists{}i:\mBbbN{}j.  ((f  j)  B  (f  i)))
8.  [P]  :  T  {}\mrightarrow{}  \mBbbP{}
9.  \mforall{}j:T.  ((\mforall{}k:T.  ((k  <  j)  {}\mRightarrow{}  P[k]))  {}\mRightarrow{}  P[j])
10.  n  :  \mBbbN{}
11.  s  :  \mBbbN{}n  {}\mrightarrow{}  T
12.  \mforall{}t:T.  \mforall{}m:\mBbbN{}.  \mforall{}s':\mBbbN{}m  {}\mrightarrow{}  T.
            (((n  +  1)  \mleq{}  m)
            {}\mRightarrow{}  (\mforall{}i:\mBbbN{}n  +  1.  ((s'  i)  =  (s++t  i)))
            {}\mRightarrow{}  (\mforall{}j:\mBbbN{}m.  \mforall{}i:\mBbbN{}j.    ((s'  j)  <  (s'  i)))
            {}\mRightarrow{}  0  <  m
            {}\mRightarrow{}  P[s'  (m  -  1)])
13.  m  :  \mBbbN{}
14.  s'  :  \mBbbN{}m  {}\mrightarrow{}  T
15.  n  \mleq{}  m
16.  \mforall{}i:\mBbbN{}n.  ((s'  i)  =  (s  i))
17.  \mforall{}j:\mBbbN{}m.  \mforall{}i:\mBbbN{}j.    ((s'  j)  <  (s'  i))
18.  0  <  m
\mvdash{}  P[s'  (m  -  1)]


By

---

Latex:
(BHyp  9  THEN  Auto  THEN  InstHyp  [\mkleeneopen{}k\mkleeneclose{};\mkleeneopen{}n  +  1\mkleeneclose{};\mkleeneopen{}s++k\mkleeneclose{}]  12\mcdot{}  THEN  Auto)\mcdot{}

---

Home Index