---

Step * 1 1 of Lemma DCC-order-type-less


1. f : ℕ ⟶ (A:Type × <:A ⟶ A ⟶ ℙ × DCC(A;<))
2. ∀i:ℕ
     ∃f@0:(fst((f (i + 1)))) ⟶ (fst((f i)))
      ∃b:fst((f i))
       (order-preserving(fst((f (i + 1)));fst((f 
                                               i));a1,a2.a1 (fst(snd((f (i + 1))))) a2;b1,b2.b1 
                                                                                             (fst(snd((f i)))) 
                                                                                             b2;f@0)
       ∧ (∀a:fst((f (i + 1))). ((f@0 a) (fst(snd((f i)))) b)))
⊢ False
BY
{ (RepUR ``order-preserving`` -1
   THEN Skolemize  (-1) `h'⋅
   THEN Auto
   THEN Skolemize  (-1) `b'⋅
   THEN Auto
   THEN Thin (-3)
   THEN Thin (-4)) }

1
1. f : ℕ ⟶ (A:Type × <:A ⟶ A ⟶ ℙ × DCC(A;<))
2. h : i:ℕ ⟶ (fst((f (i + 1)))) ⟶ (fst((f i)))
3. b : i:ℕ ⟶ (fst((f i)))
4. ∀i:ℕ
     ((∀a1,a2:fst((f (i + 1))).  ((a1 (fst(snd((f (i + 1))))) a2) ⇒ ((h i a1) (fst(snd((f i)))) (h i a2))))
     ∧ (∀a:fst((f (i + 1))). ((h i a) (fst(snd((f i)))) (b i))))
⊢ False

---

Latex:

---

Latex:

1.  f  :  \mBbbN{}  {}\mrightarrow{}  (A:Type  \mtimes{}  <:A  {}\mrightarrow{}  A  {}\mrightarrow{}  \mBbbP{}  \mtimes{}  DCC(A;<))
2.  \mforall{}i:\mBbbN{}
          \mexists{}f@0:(fst((f  (i  +  1))))  {}\mrightarrow{}  (fst((f  i)))
            \mexists{}b:fst((f  i))
              (order-preserving(fst((f  (i  +  1)));fst((f  i));a1,a2.a1 
                                                                                                                      (fst(snd((f  (i  +  1))))) 
                                                                                                                      a2;b1,b2.b1  (fst(snd((f  i))))  b2;f@0)
              \mwedge{}  (\mforall{}a:fst((f  (i  +  1))).  ((f@0  a)  (fst(snd((f  i))))  b)))
\mvdash{}  False


By

---

Latex:
(RepUR  ``order-preserving``  -1
  THEN  Skolemize    (-1)  `h'\mcdot{}
  THEN  Auto
  THEN  Skolemize    (-1)  `b'\mcdot{}
  THEN  Auto
  THEN  Thin  (-3)
  THEN  Thin  (-4))

---

Home Index