Step
*
of Lemma
mccarthy91-sqeq
∀x:Top. (mccarthy91(x) ~ if (x) < (102) then 91 else (x - 10))
BY
{ TACTIC:(Assert ∀x:ℤ. (mccarthy91(x) = if (x) < (102) then 91 else (x - 10) ∈ ℤ) BY
(Auto
THEN (InstLemma `mccarthy91_wf1` [⌜x⌝]⋅ THEN Auto)
THEN SplitOnHypITE -1
THEN Auto
THEN MemTypeHD (-2)
THEN Auto)) }
1
1. ∀x:ℤ. (mccarthy91(x) = if (x) < (102) then 91 else (x - 10) ∈ ℤ)
⊢ ∀x:Top. (mccarthy91(x) ~ if (x) < (102) then 91 else (x - 10))
Latex:
Latex:
\mforall{}x:Top. (mccarthy91(x) \msim{} if (x) < (102) then 91 else (x - 10))
By
Latex:
TACTIC:(Assert \mforall{}x:\mBbbZ{}. (mccarthy91(x) = if (x) < (102) then 91 else (x - 10)) BY
(Auto
THEN (InstLemma `mccarthy91\_wf1` [\mkleeneopen{}x\mkleeneclose{}]\mcdot{} THEN Auto)
THEN SplitOnHypITE -1
THEN Auto
THEN MemTypeHD (-2)
THEN Auto))
Home
Index