---

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

.....wf..... 
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}()
⊢ r' ∈ eo_record{i:l}()
BY
{ (Assert ∀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) BY
         ((D 0 THENA Auto) THEN Unfold `record-select` 0 THEN (DoSubsume THENL [Auto; (Reduce 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' ∈ eo_record{i:l}()

---

Latex:


.....wf..... 
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\}()
\mvdash{}  r'  \mmember{}  eo\_record\{i:l\}()


By

(Assert  \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)  BY
              ((D  0  THENA  Auto)
                THEN  Unfold  `record-select`  0
                THEN  (DoSubsume  THENL  [Auto;  (Reduce  0  THEN  Auto)])))

---

Home Index