---

Step * of Lemma eo-record-record

∀r:eo_record{i:l}(). (r ∈ record(x.eo-record-type{i:l}(r) x))
BY
{ ((D 0 THENA Auto)
   THEN (DRecord 1 THENA Auto)
   THEN RepUR ``record eo-record-type`` 0
   THEN RepUR ``record`` 2
   THEN (ExtWith [`x'] [⌈x:Atom ─→ Top⌉]⋅ THENA Auto)) }

1
1. r : self:"E":Type
            "dom":self."E" ─→ 𝔹
            "<":self."E" ─→ self."E" ─→ ℙ
            "locless":self."E" ─→ self."E" ─→ 𝔹
            "loc":self."E" ─→ Id
            "pred":self."E" ─→ self."E" ∩ x:Atom ─→ if x =a "rank" then self."E" ─→ ℕ else Top fi 
2. r ∈ x:Atom ─→ Top
3. r."E" ∈ Type
4. r."dom" ∈ r."E" ─→ 𝔹
5. r."<" ∈ r."E" ─→ r."E" ─→ ℙ
6. r."locless" ∈ r."E" ─→ r."E" ─→ 𝔹
7. r."loc" ∈ r."E" ─→ Id
8. r."pred" ∈ r."E" ─→ r."E"
9. r."rank" ∈ r."E" ─→ ℕ
10. x : Atom
⊢ r x ∈ if x =a "E" then Type
  if x =a "dom" then r."E" ─→ 𝔹
  if x =a "<" then r."E" ─→ r."E" ─→ ℙ
  if x =a "locless" then r."E" ─→ r."E" ─→ 𝔹
  if x =a "loc" then r."E" ─→ Id
  if x =a "pred" then r."E" ─→ r."E"
  if x =a "rank" then r."E" ─→ ℕ
  else Top
  fi 

---

Latex:


\mforall{}r:eo\_record\{i:l\}().  (r  \mmember{}  record(x.eo-record-type\{i:l\}(r)  x))


By

((D  0  THENA  Auto)
  THEN  (DRecord  1  THENA  Auto)
  THEN  RepUR  ``record  eo-record-type``  0
  THEN  RepUR  ``record``  2
  THEN  (ExtWith  [`x']  [\mkleeneopen{}x:Atom  {}\mrightarrow{}  Top\mkleeneclose{}]\mcdot{}  THENA  Auto))

---

Home Index