---

Step * 2 1 1 1 1 1 of Lemma eo-forward-trivial


1. v : eo_record{i:l}()@i'
2. eo_axioms(v)@i'
⊢ v["dom" := v."dom"] ∈ eo_record{i:l}()
BY
{ (DRecord 1
   THEN Auto
   THEN Unfold `eo_record` 0
   THEN RepeatFor 7 ((RecordPlusTypeCD THEN Try ((Reduce 0 THEN Trivial))))) }

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

---

Latex:



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


By

(DRecord  1
  THEN  Auto
  THEN  Unfold  `eo\_record`  0
  THEN  RepeatFor  7  ((RecordPlusTypeCD  THEN  Try  ((Reduce  0  THEN  Trivial)))))

---

Home Index