---

Step * of Lemma rec-bind-class_wf

∀[Info,A,B:Type]. ∀[X:A ⟶ EClass(B)]. ∀[Y:A ⟶ EClass(A)].
  rec-bind-class(X;Y) ∈ 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-bind-class(X;Y) 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-bind-class(X;Y) a es e ∈ bag(B))))⌝⋅
   THENM (Auto THEN InstHyp [⌜||≤loc(e)|| + 1⌝] (-4)⋅ THEN Auto' THEN BHyp (-1) THEN Auto')⋅
   )
   THEN InductionOnNat ) }

1
.....basecase..... 
1. Info : Type
2. A : Type
3. B : Type
4. X : A ⟶ EClass(B)
5. Y : A ⟶ EClass(A)
6. ∀x,a:A. ∀es:EO+(Info). ∀e:E.  (a ∈ Y x(e) ⇒ (∀w:A. (¬w ∈ Y a(e))))
7. n : ℤ
⊢ ∀es:EO+(Info). ∀e:E.  (||≤loc(e)|| < 0 ⇒ (∀a:A. (rec-bind-class(X;Y) a es e ∈ bag(B))))

2
.....upcase..... 
1. Info : Type
2. A : Type
3. B : Type
4. X : A ⟶ EClass(B)
5. Y : A ⟶ EClass(A)
6. ∀x,a:A. ∀es:EO+(Info). ∀e:E.  (a ∈ Y x(e) ⇒ (∀w:A. (¬w ∈ Y a(e))))
7. n : ℤ
8. 0 < n
9. ∀es:EO+(Info). ∀e:E.  (||≤loc(e)|| < n - 1 ⇒ (∀a:A. (rec-bind-class(X;Y) a es e ∈ bag(B))))
⊢ ∀es:EO+(Info). ∀e:E.  (||≤loc(e)|| < n ⇒ (∀a:A. (rec-bind-class(X;Y) a es e ∈ bag(B))))

---

Latex:

---

Latex:
\mforall{}[Info,A,B:Type].  \mforall{}[X:A  {}\mrightarrow{}  EClass(B)].  \mforall{}[Y:A  {}\mrightarrow{}  EClass(A)].
    rec-bind-class(X;Y)  \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-bind-class(X;Y)  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-bind-class(X;Y)  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')\mcdot{}
  )
  THEN  InductionOnNat  )

---

Home Index