---

Step * 1 of Lemma least-closed-set-inductively-defined


1. [R] : Set{i:l} ⟶ Set{i:l} ⟶ ℙ'
2. B : Set{i:l}
3. G : Set{i:l} ⟶ Set{i:l}
4. ∀x,a:Set{i:l}.  (R[x;a] ⇒ (∃b:Set{i:l}. ((b ∈ B) ∧ setimage{i:l}(x;b))))
5. ∀x,z:Set{i:l}.  ((z ∈ G x) ⇐⇒ ∃A:Set{i:l}. ((A ⊆ x) ∧ R[A;z]))
6. ∀a,b:Set{i:l}.  ((a ⊆ b) ⇒ (G a ⊆ G b))
⊢ inductively-defined{i:l}(x,a.R[x;a];least-closed-set(B;G))
BY
{ (Unfold `least-closed-set` 0
   THEN (InstLemma `regext-Regularset` [⌜setTC(B)⌝]⋅ THENA Auto)
   THEN (Assert (B ⊆ regext(setTC(B))) BY
               ((UseTrans ⌜setTC(B)⌝⋅ THEN Auto) THEN BLemma `subset-regext` ⋅ THEN Auto))
   THEN RepeatFor 2 (MoveToConcl (-1))
   THEN (GenConcl ⌜regext(setTC(B)) = r ∈ Set{i:l}⌝⋅ THENA Auto)
   THEN Thin (-1)
   THEN Auto) }

1
1. [R] : Set{i:l} ⟶ Set{i:l} ⟶ ℙ'
2. B : Set{i:l}
3. G : Set{i:l} ⟶ Set{i:l}
4. ∀x,a:Set{i:l}.  (R[x;a] ⇒ (∃b:Set{i:l}. ((b ∈ B) ∧ setimage{i:l}(x;b))))
5. ∀x,z:Set{i:l}.  ((z ∈ G x) ⇐⇒ ∃A:Set{i:l}. ((A ⊆ x) ∧ R[A;z]))
6. ∀a,b:Set{i:l}.  ((a ⊆ b) ⇒ (G a ⊆ G b))
7. r : Set{i:l}
8. Regular(r)
9. (B ⊆ r)
⊢ inductively-defined{i:l}(x,a.R[x;a]; ⋃a∈r.itersetfun(x.G x;a))

---

Latex:

---

Latex:

1.  [R]  :  Set\{i:l\}  {}\mrightarrow{}  Set\{i:l\}  {}\mrightarrow{}  \mBbbP{}'
2.  B  :  Set\{i:l\}
3.  G  :  Set\{i:l\}  {}\mrightarrow{}  Set\{i:l\}
4.  \mforall{}x,a:Set\{i:l\}.    (R[x;a]  {}\mRightarrow{}  (\mexists{}b:Set\{i:l\}.  ((b  \mmember{}  B)  \mwedge{}  setimage\{i:l\}(x;b))))
5.  \mforall{}x,z:Set\{i:l\}.    ((z  \mmember{}  G  x)  \mLeftarrow{}{}\mRightarrow{}  \mexists{}A:Set\{i:l\}.  ((A  \msubseteq{}  x)  \mwedge{}  R[A;z]))
6.  \mforall{}a,b:Set\{i:l\}.    ((a  \msubseteq{}  b)  {}\mRightarrow{}  (G  a  \msubseteq{}  G  b))
\mvdash{}  inductively-defined\{i:l\}(x,a.R[x;a];least-closed-set(B;G))


By

---

Latex:
(Unfold  `least-closed-set`  0
  THEN  (InstLemma  `regext-Regularset`  [\mkleeneopen{}setTC(B)\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (Assert  (B  \msubseteq{}  regext(setTC(B)))  BY
                          ((UseTrans  \mkleeneopen{}setTC(B)\mkleeneclose{}\mcdot{}  THEN  Auto)  THEN  BLemma  `subset-regext`  \mcdot{}  THEN  Auto))
  THEN  RepeatFor  2  (MoveToConcl  (-1))
  THEN  (GenConcl  \mkleeneopen{}regext(setTC(B))  =  r\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  Thin  (-1)
  THEN  Auto)

---

Home Index