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