---

Step * of Lemma num-antecedents_wf

∀[Info:Type]. ∀[es:EO+(Info)]. ∀[Sys:EClass(Top)]. ∀[f:sys-antecedent(es;Sys)]. ∀[e:E(Sys)].  (#f(e) ∈ ℕ)
BY
{ ((UnivCD THENA 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. ∀x:E(Sys). f x c≤ x
6. e : E(Sys)@i
7. ¬((f e) = e ∈ E)
8. ∀e1:E(Sys). ((e1 < e) ⇒ (#f(e1) ∈ ℕ))
⊢ 1 + #f(f e) ∈ ℕ

---

Latex:


\mforall{}[Info:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[Sys:EClass(Top)].  \mforall{}[f:sys-antecedent(es;Sys)].  \mforall{}[e:E(Sys)].
    (\#f(e)  \mmember{}  \mBbbN{})


By

((UnivCD  THENA  Auto)
  THEN  MoveToConcl  (-1)
  THEN  CausalInd'\mcdot{}
  THEN  (DVar  `f'  THEN  RecUnfold  `num-antecedents`  0  THEN  AutoSplit)\mcdot{})

---

Home Index