---

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


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)
BY
{ (GenConclTerm ⌈v⌉ ⋅ THEN Auto) }

---

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.  v."E"  \mmember{}  Type
5.  v."dom"  \mmember{}  v."E"  {}\mrightarrow{}  \mBbbB{}
6.  v."<"  \mmember{}  v."E"  {}\mrightarrow{}  v."E"  {}\mrightarrow{}  \mBbbP{}
7.  v."locless"  \mmember{}  v."E"  {}\mrightarrow{}  v."E"  {}\mrightarrow{}  \mBbbB{}
8.  v."loc"  \mmember{}  v."E"  {}\mrightarrow{}  Id
9.  v."pred"  \mmember{}  v."E"  {}\mrightarrow{}  v."E"
10.  v."rank"  \mmember{}  v."E"  {}\mrightarrow{}  \mBbbN{}
\mvdash{}  v["dom"  :=  v."dom"]  \mmember{}  record(x.Top)


By

(GenConclTerm  \mkleeneopen{}v\mkleeneclose{}  \mcdot{}  THEN  Auto)

---

Home Index