---

Step * 1 1 1 1 of Lemma eo-record-record-eq


1. r : eo_record{i:l}()@i'
2. r' : record(x.eo-record-type{i:l}(r) x)@i'
3. r'
= r
∈ (x:Atom ─→ 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 )@i'
4. r."E" ∈ Type
5. x:Atom ─→ 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  ∈ 𝕌'
6. r'."E" = r."E" ∈ Type
7. r ∈ eo_record{i:l}()
8. ∀z:x:Atom ─→ 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 
     (z."E" ∈ Type)
⊢ r' ∈ eo_record{i:l}()
BY
{ (Unfold `eo_record` 0
   THEN RepeatFor 7 ((RecordPlusTypeCD THENL [Id; (DoSubsume THEN RepUR ``eo-record-type`` 0 THEN Auto)]))
   ) }

1
1. r : eo_record{i:l}()@i'
2. r' : record(x.eo-record-type{i:l}(r) x)@i'
3. r'
= r
∈ (x:Atom ─→ 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 )@i'
4. r."E" ∈ Type
5. x:Atom ─→ 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  ∈ 𝕌'
6. r'."E" = r."E" ∈ Type
7. r ∈ eo_record{i:l}()
8. ∀z:x:Atom ─→ 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 
     (z."E" ∈ Type)
⊢ r' ∈ record(x.Top)

---

Latex:



1.  r  :  eo\_record\{i:l\}()@i'
2.  r'  :  record(x.eo-record-type\{i:l\}(r)  x)@i'
3.  r'  =  r@i'
4.  r."E"  \mmember{}  Type
5.  x:Atom  {}\mrightarrow{}  if  x  =a  "E"  then  Type
                          if  x  =a  "dom"  then  r."E"  {}\mrightarrow{}  \mBbbB{}
                          if  x  =a  "<"  then  r."E"  {}\mrightarrow{}  r."E"  {}\mrightarrow{}  \mBbbP{}
                          if  x  =a  "locless"  then  r."E"  {}\mrightarrow{}  r."E"  {}\mrightarrow{}  \mBbbB{}
                          if  x  =a  "loc"  then  r."E"  {}\mrightarrow{}  Id
                          if  x  =a  "pred"  then  r."E"  {}\mrightarrow{}  r."E"
                          if  x  =a  "rank"  then  r."E"  {}\mrightarrow{}  \mBbbN{}
                          else  Top
                          fi    \mmember{}  \mBbbU{}'
6.  r'."E"  =  r."E"
7.  r  \mmember{}  eo\_record\{i:l\}()
8.  \mforall{}z:x:Atom  {}\mrightarrow{}  if  x  =a  "E"  then  Type
                                if  x  =a  "dom"  then  r."E"  {}\mrightarrow{}  \mBbbB{}
                                if  x  =a  "<"  then  r."E"  {}\mrightarrow{}  r."E"  {}\mrightarrow{}  \mBbbP{}
                                if  x  =a  "locless"  then  r."E"  {}\mrightarrow{}  r."E"  {}\mrightarrow{}  \mBbbB{}
                                if  x  =a  "loc"  then  r."E"  {}\mrightarrow{}  Id
                                if  x  =a  "pred"  then  r."E"  {}\mrightarrow{}  r."E"
                                if  x  =a  "rank"  then  r."E"  {}\mrightarrow{}  \mBbbN{}
                                else  Top
                                fi 
          (z."E"  \mmember{}  Type)
\mvdash{}  r'  \mmember{}  eo\_record\{i:l\}()


By

(Unfold  `eo\_record`  0
  THEN  RepeatFor  7  ((RecordPlusTypeCD
                                        THENL  [Id;  (DoSubsume  THEN  RepUR  ``eo-record-type``  0  THEN  Auto)]
                                      ))
  )

---

Home Index