Step
*
2
of Lemma
num-antecedents-property
1. Info : Type
2. es : EO+(Info)
3. Sys : EClass(Top)
4. f : E(Sys) ─→ E(Sys)
5. [%7] : ∀x:E(Sys). f x c≤ x
6. e : E(Sys)@i
7. ¬((f e) = e ∈ E)
8. ∀e1:E(Sys)
((e1 < e)
⇒ {((f (f^#f(e1) e1)) = (f^#f(e1) e1) ∈ E(Sys)) ∧ (∀[i:ℕ#f(e1)]. (¬((f (f^i e1)) = (f^i e1) ∈ E(Sys))))})
⊢ {((f (f^1 + #f(f e) e)) = (f^1 + #f(f e) e) ∈ E(Sys)) ∧ (∀[i:ℕ1 + #f(f e)]. (¬((f (f^i e)) = (f^i e) ∈ E(Sys))))}
BY
{ ((Assert ↓f e c≤ e BY (Unhide THEN Auto)) THEN D -1 THEN Unfold `guard` 0 THEN (Unhide THENA Auto) THEN D -1) }
1
1. Info : Type
2. es : EO+(Info)
3. Sys : EClass(Top)
4. f : E(Sys) ─→ E(Sys)
5. ∀x:E(Sys). f x c≤ x
6. e : E(Sys)@i
7. ¬((f e) = e ∈ E)
8. ∀e1:E(Sys)
((e1 < e)
⇒ {((f (f^#f(e1) e1)) = (f^#f(e1) e1) ∈ E(Sys)) ∧ (∀[i:ℕ#f(e1)]. (¬((f (f^i e1)) = (f^i e1) ∈ E(Sys))))})
9. (f e < e)
⊢ ((f (f^1 + #f(f e) e)) = (f^1 + #f(f e) e) ∈ E(Sys)) ∧ (∀[i:ℕ1 + #f(f e)]. (¬((f (f^i e)) = (f^i e) ∈ E(Sys))))
2
1. Info : Type
2. es : EO+(Info)
3. Sys : EClass(Top)
4. f : E(Sys) ─→ E(Sys)
5. ∀x:E(Sys). f x c≤ x
6. e : E(Sys)@i
7. ¬((f e) = e ∈ E)
8. ∀e1:E(Sys)
((e1 < e)
⇒ {((f (f^#f(e1) e1)) = (f^#f(e1) e1) ∈ E(Sys)) ∧ (∀[i:ℕ#f(e1)]. (¬((f (f^i e1)) = (f^i e1) ∈ E(Sys))))})
9. (f e) = e ∈ E
⊢ ((f (f^1 + #f(f e) e)) = (f^1 + #f(f e) e) ∈ E(Sys)) ∧ (∀[i:ℕ1 + #f(f e)]. (¬((f (f^i e)) = (f^i e) ∈ E(Sys))))
Latex:
1. Info : Type
2. es : EO+(Info)
3. Sys : EClass(Top)
4. f : E(Sys) {}\mrightarrow{} E(Sys)
5. [\%7] : \mforall{}x:E(Sys). f x c\mleq{} x
6. e : E(Sys)@i
7. \mneg{}((f e) = e)
8. \mforall{}e1:E(Sys)
((e1 < e)
{}\mRightarrow{} \{((f (f\^{}\#f(e1) e1)) = (f\^{}\#f(e1) e1)) \mwedge{} (\mforall{}[i:\mBbbN{}\#f(e1)]. (\mneg{}((f (f\^{}i e1)) = (f\^{}i e1))))\})
\mvdash{} \{((f (f\^{}1 + \#f(f e) e)) = (f\^{}1 + \#f(f e) e)) \mwedge{} (\mforall{}[i:\mBbbN{}1 + \#f(f e)]. (\mneg{}((f (f\^{}i e)) = (f\^{}i e))))\}
By
((Assert \mdownarrow{}f e c\mleq{} e BY
(Unhide THEN Auto))
THEN D -1
THEN Unfold `guard` 0
THEN (Unhide THENA Auto)
THEN D -1)
Home
Index