---

Step * 1 of Lemma mccarthy91_wf1

.....assertion..... 
∀x:ℤ. ((x ≤ 101) ⇒ (mccarthy91(x) = 91 ∈ ℤ))
BY
{ xxx((Assert ⌜∀d:ℕ. ∀x:ℤ.  ((x ≤ 101) ⇒ ((101 - x) ≤ d) ⇒ (mccarthy91(x) = 91 ∈ ℤ))⌝⋅
      THENM (Auto THEN InstHyp [⌜101 - x⌝;⌜x⌝] 1⋅ THEN Auto)
      )
      THEN InductionOnNat
      THEN Auto
      THEN Unfold `mccarthy91` 0
      THEN AutoSplit
      THEN Auto')xxx }

1
1. d : ℤ
2. 0 < d
3. ∀x:ℤ. ((x ≤ 101) ⇒ ((101 - x) ≤ (d - 1)) ⇒ (mccarthy91(x) = 91 ∈ ℤ))
4. x : ℤ
5. ¬100 < x
6. x ≤ 101
7. (101 - x) ≤ d
⊢ eval y = x + 11 in eval z = mccarthy91(y) in   mccarthy91(z) = 91 ∈ ℤ

---

Latex:

---

Latex:
.....assertion..... 
\mforall{}x:\mBbbZ{}.  ((x  \mleq{}  101)  {}\mRightarrow{}  (mccarthy91(x)  =  91))


By

---

Latex:
xxx((Assert  \mkleeneopen{}\mforall{}d:\mBbbN{}.  \mforall{}x:\mBbbZ{}.    ((x  \mleq{}  101)  {}\mRightarrow{}  ((101  -  x)  \mleq{}  d)  {}\mRightarrow{}  (mccarthy91(x)  =  91))\mkleeneclose{}\mcdot{}
        THENM  (Auto  THEN  InstHyp  [\mkleeneopen{}101  -  x\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]  1\mcdot{}  THEN  Auto)
        )
        THEN  InductionOnNat
        THEN  Auto
        THEN  Unfold  `mccarthy91`  0
        THEN  AutoSplit
        THEN  Auto')xxx

---

Home Index