---

Step * of Lemma is-list-if-has-value-ext

ListLike ≡ partial(Unit ⋃ (Top × ListLike))
BY
{ (Auto
   THEN RepUR ``is-list-if-has-value`` 0
   THEN BLemma `corec-ext`
   THEN Auto
   THEN D 0
   THEN Auto
   THEN Try (Complete (((Assert ⌜(Unit ⋃ (Top × A)) ⊆r (Unit ⋃ (Top × B))⌝⋅ THENA Auto)
                        THEN (Assert ⌜value-type(Unit ⋃ (Top × A))⌝⋅ THENA Auto)
                        THEN Assert ⌜value-type(Unit ⋃ (Top × B))⌝⋅
                        THEN Auto)))) }

1
.....assertion..... 
Continuous+(L.partial(Unit ⋃ (Top × L)))

---

Latex:

---

Latex:
ListLike  \mequiv{}  partial(Unit  \mcup{}  (Top  \mtimes{}  ListLike))


By

---

Latex:
(Auto
  THEN  RepUR  ``is-list-if-has-value``  0
  THEN  BLemma  `corec-ext`
  THEN  Auto
  THEN  D  0
  THEN  Auto
  THEN  Try  (Complete  (((Assert  \mkleeneopen{}(Unit  \mcup{}  (Top  \mtimes{}  A))  \msubseteq{}r  (Unit  \mcup{}  (Top  \mtimes{}  B))\mkleeneclose{}\mcdot{}  THENA  Auto)
                                            THEN  (Assert  \mkleeneopen{}value-type(Unit  \mcup{}  (Top  \mtimes{}  A))\mkleeneclose{}\mcdot{}  THENA  Auto)
                                            THEN  Assert  \mkleeneopen{}value-type(Unit  \mcup{}  (Top  \mtimes{}  B))\mkleeneclose{}\mcdot{}
                                            THEN  Auto))))

---

Home Index