---

Step * 1 of Lemma eo-record-record


1. r : 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. r ∈ x:Atom ─→ Top
3. r."E" ∈ Type
4. r."dom" ∈ r."E" ─→ 𝔹
5. r."<" ∈ r."E" ─→ r."E" ─→ ℙ
6. r."locless" ∈ r."E" ─→ r."E" ─→ 𝔹
7. r."loc" ∈ r."E" ─→ Id
8. r."pred" ∈ r."E" ─→ r."E"
9. r."rank" ∈ r."E" ─→ ℕ
10. x : Atom
⊢ r x ∈ 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 
BY
{ RepeatFor 4 (AutoSplit) }

1
1. r : 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. r ∈ x:Atom ─→ Top
3. r."E" ∈ Type
4. r."dom" ∈ r."E" ─→ 𝔹
5. r."<" ∈ r."E" ─→ r."E" ─→ ℙ
6. r."locless" ∈ r."E" ─→ r."E" ─→ 𝔹
7. r."loc" ∈ r."E" ─→ Id
8. r."pred" ∈ r."E" ─→ r."E"
9. r."rank" ∈ r."E" ─→ ℕ
10. x : Atom
11. x ≠ "locless" ∈ Atom 
12. x ≠ "<" ∈ Atom 
13. x ≠ "dom" ∈ Atom 
14. x ≠ "E" ∈ Atom 
⊢ r x ∈ 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 

---

Latex:



1.  r  :  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.  r  \mmember{}  x:Atom  {}\mrightarrow{}  Top
3.  r."E"  \mmember{}  Type
4.  r."dom"  \mmember{}  r."E"  {}\mrightarrow{}  \mBbbB{}
5.  r."<"  \mmember{}  r."E"  {}\mrightarrow{}  r."E"  {}\mrightarrow{}  \mBbbP{}
6.  r."locless"  \mmember{}  r."E"  {}\mrightarrow{}  r."E"  {}\mrightarrow{}  \mBbbB{}
7.  r."loc"  \mmember{}  r."E"  {}\mrightarrow{}  Id
8.  r."pred"  \mmember{}  r."E"  {}\mrightarrow{}  r."E"
9.  r."rank"  \mmember{}  r."E"  {}\mrightarrow{}  \mBbbN{}
10.  x  :  Atom
\mvdash{}  r  x  \mmember{}  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 


By

RepeatFor  4  (AutoSplit)

---

Home Index