---

Step * of Lemma rec-op-bind-class_wf

∀[Info,A,B:Type]. ∀[X:A ─→ EClass(B)]. ∀[Y:A ─→ EClass(A)]. ∀[F:A ─→ bag(B) ─→ bag(B)].
  rec-op-bind-class(X;Y;F) ∈ A ─→ EClass(B) supposing not-self-starting{i:l}(Info;A;Y)
BY
{ (Auto
   THEN UnfoldTopAb (-1)
   THEN Assert ⌈∀a:A. ∀es:EO+(Info). ∀e:E.  (rec-op-bind-class(X;Y;F) a es e ∈ bag(B))⌉⋅
   THEN Try ((Unfold `eclass` 0 THEN RepeatFor 3 ((BetterExt THEN Auto)))⋅)
   THEN (Assert ⌈∀n:ℕ. ∀es:EO+(Info). ∀e:E.  (||≤loc(e)|| < n ⇒ (∀a:A. (rec-op-bind-class(X;Y;F) a es e ∈ bag(B))))⌉⋅
   THENM (Auto THEN InstHyp [⌈||≤loc(e)|| + 1⌉] (-4)⋅ THEN Auto' THEN BHyp (-1) THEN Auto')
   )
   THEN InductionOnNat 
   THEN (Complete (Auto') ORELSE (UnivCD THENA Auto))) }

1
1. Info : Type
2. A : Type
3. B : Type
4. X : A ─→ EClass(B)
5. Y : A ─→ EClass(A)
6. F : A ─→ bag(B) ─→ bag(B)
7. ∀x,a:A. ∀es:EO+(Info). ∀e:E.  (a ∈ Y x(e) ⇒ (∀w:A. (¬w ∈ Y a(e))))
8. n : ℤ
9. 0 < n
10. ∀es:EO+(Info). ∀e:E.  (||≤loc(e)|| < n - 1 ⇒ (∀a:A. (rec-op-bind-class(X;Y;F) a es e ∈ bag(B))))
11. es : EO+(Info)@i'
12. e : E@i
13. ||≤loc(e)|| < n@i
14. a : A@i
⊢ rec-op-bind-class(X;Y;F) a es e ∈ bag(B)

---

Latex:

---

Latex:
\mforall{}[Info,A,B:Type].  \mforall{}[X:A  {}\mrightarrow{}  EClass(B)].  \mforall{}[Y:A  {}\mrightarrow{}  EClass(A)].  \mforall{}[F:A  {}\mrightarrow{}  bag(B)  {}\mrightarrow{}  bag(B)].
    rec-op-bind-class(X;Y;F)  \mmember{}  A  {}\mrightarrow{}  EClass(B)  supposing  not-self-starting\{i:l\}(Info;A;Y)


By

---

Latex:
(Auto
  THEN  UnfoldTopAb  (-1)
  THEN  Assert  \mkleeneopen{}\mforall{}a:A.  \mforall{}es:EO+(Info).  \mforall{}e:E.    (rec-op-bind-class(X;Y;F)  a  es  e  \mmember{}  bag(B))\mkleeneclose{}\mcdot{}
  THEN  Try  ((Unfold  `eclass`  0  THEN  RepeatFor  3  ((BetterExt  THEN  Auto)))\mcdot{})
  THEN  (Assert  \mkleeneopen{}\mforall{}n:\mBbbN{}.  \mforall{}es:EO+(Info).  \mforall{}e:E.
                                  (||\mleq{}loc(e)||  <  n  {}\mRightarrow{}  (\mforall{}a:A.  (rec-op-bind-class(X;Y;F)  a  es  e  \mmember{}  bag(B))))\mkleeneclose{}\mcdot{}
  THENM  (Auto  THEN  InstHyp  [\mkleeneopen{}||\mleq{}loc(e)||  +  1\mkleeneclose{}]  (-4)\mcdot{}  THEN  Auto'  THEN  BHyp  (-1)  THEN  Auto')
  )
  THEN  InductionOnNat 
  THEN  (Complete  (Auto')  ORELSE  (UnivCD  THENA  Auto)))

---

Home Index