---

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:

---

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


By

---

Latex:
((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