---

Step * of Lemma num-antecedents-property

∀[Info:Type]. ∀[es:EO+(Info)]. ∀[Sys:EClass(Top)]. ∀[f:sys-antecedent(es;Sys)]. ∀[e:E(Sys)].
  {((f (f^#f(e) e)) = (f^#f(e) e) ∈ E(Sys)) ∧ (∀[i:ℕ#f(e)]. (¬((f (f^i e)) = (f^i e) ∈ E(Sys))))}
BY
{ (Auto
   THEN Try (Complete ((DVar `f' THEN Auto)))
   THEN MoveToConcl (-1)
   THEN CausalInd'
   THEN DVar `f'
   THEN RecUnfold `num-antecedents` 0
   THEN AutoSplit) }

1
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. ∀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))))})
8. (f e) = e ∈ E
⊢ {((f e) = e ∈ E(Sys)) ∧ (∀[i:ℕ0]. (¬((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. [%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))))}

---

Latex:

---

Latex:
\mforall{}[Info:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[Sys:EClass(Top)].  \mforall{}[f:sys-antecedent(es;Sys)].  \mforall{}[e:E(Sys)].
    \{((f  (f\^{}\#f(e)  e))  =  (f\^{}\#f(e)  e))  \mwedge{}  (\mforall{}[i:\mBbbN{}\#f(e)].  (\mneg{}((f  (f\^{}i  e))  =  (f\^{}i  e))))\}


By

---

Latex:
(Auto
  THEN  Try  (Complete  ((DVar  `f'  THEN  Auto)))
  THEN  MoveToConcl  (-1)
  THEN  CausalInd'
  THEN  DVar  `f'
  THEN  RecUnfold  `num-antecedents`  0
  THEN  AutoSplit)

---

Home Index