---

Step * 1 of Lemma partial-int-not-discrete


1. discrete-type(partial(ℤ))
⊢ False
BY
{ (Assert ⌜∀k:ℕ. (λx.(fix((λf,n. if 4 <z |x (n + 1)| then 1 else f (n + 1) fi )) k) ∈ ℝ ⟶ partial(ℤ))⌝⋅
   THENA (Intro
          THEN (MemCD THENA Auto)
          THEN (InstLemma `fixpoint-induction-bottom` [⌜ℤ⌝;⌜ℕ ⟶ partial(ℤ)⌝;⌜λF.(F k)⌝]⋅
                THENA (Try ((MemCD THENL [(MemCD THENL [Trivial; Auto]); Auto])) THEN Auto)
                )
          THEN Reduce -1
          THEN BHyp -1
          THEN Auto)
   ) }

1
1. discrete-type(partial(ℤ))
2. ∀k:ℕ. (λx.(fix((λf,n. if 4 <z |x (n + 1)| then 1 else f (n + 1) fi )) k) ∈ ℝ ⟶ partial(ℤ))
⊢ False

---

Latex:

---

Latex:

1.  discrete-type(partial(\mBbbZ{}))
\mvdash{}  False


By

---

Latex:
(Assert  \mkleeneopen{}\mforall{}k:\mBbbN{}.  (\mlambda{}x.(fix((\mlambda{}f,n.  if  4  <z  |x  (n  +  1)|  then  1  else  f  (n  +  1)  fi  ))  k)  \mmember{}  \mBbbR{}  {}\mrightarrow{}  partial(\mBbbZ{}))\000C\mkleeneclose{}\mcdot{}
  THENA  (Intro
                THEN  (MemCD  THENA  Auto)
                THEN  (InstLemma  `fixpoint-induction-bottom`  [\mkleeneopen{}\mBbbZ{}\mkleeneclose{};\mkleeneopen{}\mBbbN{}  {}\mrightarrow{}  partial(\mBbbZ{})\mkleeneclose{};\mkleeneopen{}\mlambda{}F.(F  k)\mkleeneclose{}]\mcdot{}
                            THENA  (Try  ((MemCD  THENL  [(MemCD  THENL  [Trivial;  Auto]);  Auto]))  THEN  Auto)
                            )
                THEN  Reduce  -1
                THEN  BHyp  -1
                THEN  Auto)
  )

---

Home Index