---

Step * of Lemma tree-big-monotone

∀[T:Type]. ∀[A:(T List) ⟶ ℙ].  ∀a,b:ℕ.  ((a ≤ b) ⇒ tree-big(T;upwd-closure(T;A);a) ⇒ tree-big(T;upwd-closure(T;A);b))
BY
{ ((RepUR ``tree-big upwd-closure`` 0 THEN Auto)
   THEN (InstHyp [⌜firstn(a;as)⌝] (-3)⋅ THENA (Auto THEN RWO "length_firstn" 0 THEN Auto))
   THEN ParallelLast
   THEN Auto)⋅ }

1
1. [T] : Type
2. [A] : (T List) ⟶ ℙ
3. a : ℕ@i
4. b : ℕ@i
5. a ≤ b@i
6. ∀as:T List. ((||as|| = a ∈ ℤ) ⇒ (∃bs:T List. (bs ≤ as ∧ (A bs))))@i
7. as : T List@i
8. ||as|| = b ∈ ℤ@i
9. bs : T List
10. bs ≤ firstn(a;as)
11. A bs
⊢ bs ≤ as

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[A:(T  List)  {}\mrightarrow{}  \mBbbP{}].
    \mforall{}a,b:\mBbbN{}.    ((a  \mleq{}  b)  {}\mRightarrow{}  tree-big(T;upwd-closure(T;A);a)  {}\mRightarrow{}  tree-big(T;upwd-closure(T;A);b))


By

---

Latex:
((RepUR  ``tree-big  upwd-closure``  0  THEN  Auto)
  THEN  (InstHyp  [\mkleeneopen{}firstn(a;as)\mkleeneclose{}]  (-3)\mcdot{}  THENA  (Auto  THEN  RWO  "length\_firstn"  0  THEN  Auto))
  THEN  ParallelLast
  THEN  Auto)\mcdot{}

---

Home Index