---

Step * 1 1 of Lemma mk-extended-eo_wf


1. v : eo_record{i:l}()@i'
2. eo_axioms(v)@i'
3. x : Top@i
⊢ v["info" := x] ∈ eo_record{i:l}()
BY
{ (DRecord 1 THEN Auto) }

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] ∈ eo_record{i:l}()

---

Latex:



1.  v  :  eo\_record\{i:l\}()@i'
2.  eo\_axioms(v)@i'
3.  x  :  Top@i
\mvdash{}  v["info"  :=  x]  \mmember{}  eo\_record\{i:l\}()


By

(DRecord  1  THEN  Auto)

---

Home Index