---

Step * 1 1 1 of Lemma mk-extended-eo_wf


1. v : 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. v ∈ record(x.Top)
3. eo_axioms(v)@i'
4. x : Top@i
5. v."E" ∈ Type
6. v."dom" ∈ v."E" ─→ 𝔹
7. v."<" ∈ v."E" ─→ v."E" ─→ ℙ
8. v."locless" ∈ v."E" ─→ v."E" ─→ 𝔹
9. v."loc" ∈ v."E" ─→ Id
10. v."pred" ∈ v."E" ─→ v."E"
11. v."rank" ∈ v."E" ─→ ℕ
⊢ v["info" := x] ∈ eo_record{i:l}()
BY
{ Unfold `eo_record` 0 }

1
1. v : 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. v ∈ record(x.Top)
3. eo_axioms(v)@i'
4. x : Top@i
5. v."E" ∈ Type
6. v."dom" ∈ v."E" ─→ 𝔹
7. v."<" ∈ v."E" ─→ v."E" ─→ ℙ
8. v."locless" ∈ v."E" ─→ v."E" ─→ 𝔹
9. v."loc" ∈ v."E" ─→ Id
10. v."pred" ∈ v."E" ─→ v."E"
11. v."rank" ∈ v."E" ─→ ℕ
⊢ v["info" := x] ∈ "E":Type
                   "dom":self."E" ─→ 𝔹
                   "<":self."E" ─→ self."E" ─→ ℙ
                   "locless":self."E" ─→ self."E" ─→ 𝔹
                   "loc":self."E" ─→ Id
                   "pred":self."E" ─→ self."E"
                   "rank":self."E" ─→ ℕ

---

Latex:



1.  v  :  self:"E":Type
                        "dom":self."E"  {}\mrightarrow{}  \mBbbB{}
                        "<":self."E"  {}\mrightarrow{}  self."E"  {}\mrightarrow{}  \mBbbP{}
                        "locless":self."E"  {}\mrightarrow{}  self."E"  {}\mrightarrow{}  \mBbbB{}
                        "loc":self."E"  {}\mrightarrow{}  Id
                        "pred":self."E"  {}\mrightarrow{}  self."E"  \mcap{}  x:Atom  {}\mrightarrow{}  if  x  =a  "rank"  then  self."E"  {}\mrightarrow{}  \mBbbN{}  else  Top  fi 
2.  v  \mmember{}  record(x.Top)
3.  eo\_axioms(v)@i'
4.  x  :  Top@i
5.  v."E"  \mmember{}  Type
6.  v."dom"  \mmember{}  v."E"  {}\mrightarrow{}  \mBbbB{}
7.  v."<"  \mmember{}  v."E"  {}\mrightarrow{}  v."E"  {}\mrightarrow{}  \mBbbP{}
8.  v."locless"  \mmember{}  v."E"  {}\mrightarrow{}  v."E"  {}\mrightarrow{}  \mBbbB{}
9.  v."loc"  \mmember{}  v."E"  {}\mrightarrow{}  Id
10.  v."pred"  \mmember{}  v."E"  {}\mrightarrow{}  v."E"
11.  v."rank"  \mmember{}  v."E"  {}\mrightarrow{}  \mBbbN{}
\mvdash{}  v["info"  :=  x]  \mmember{}  eo\_record\{i:l\}()


By

Unfold  `eo\_record`  0

---

Home Index