---

Step * 1 of Lemma ss-sep-irrefl


1. ss : self:"Point":Type
        "#":{s:self."Point" ⟶ self."Point" ⟶ ℙ| ∀x:self."Point". (¬(s x x))} 
        "#symm":∀x,y:self."Point".  ((self."#" x y) ⇒ (self."#" y x)) ⋂ x:Atom ⟶ if x =a "#or"
                                                                                   then ∀x,y,z:self."Point".
                                                                                          ((self."#" x y)
                                                                                          ⇒ ((self."#" x z)
                                                                                             ∨ (self."#" y z)))
                                                                                   else Top
                                                                                   fi 
2. ss ∈ record(x.Top)
3. x : Point
4. ss."Point" ∈ Type
5. ss."#" ∈ {s:ss."Point" ⟶ ss."Point" ⟶ ℙ| ∀x:ss."Point". (¬(s x x))} 
6. ss."#symm" ∈ ∀x,y:ss."Point".  ((ss."#" x y) ⇒ (ss."#" y x))
7. ss."#or" ∈ ∀x,y,z:ss."Point".  ((ss."#" x y) ⇒ ((ss."#" x z) ∨ (ss."#" y z)))
⊢ ¬(ss."#" x x)
BY
{ At ⌜Type⌝ ((MemTypeHD (-3) THEN Auto))⋅ }

1
.....wf..... 
1. ss : self:"Point":Type
        "#":{s:self."Point" ⟶ self."Point" ⟶ ℙ| ∀x:self."Point". (¬(s x x))} 
        "#symm":∀x,y:self."Point".  ((self."#" x y) ⇒ (self."#" y x)) ⋂ x:Atom ⟶ if x =a "#or"
                                                                                   then ∀x,y,z:self."Point".
                                                                                          ((self."#" x y)
                                                                                          ⇒ ((self."#" x z)
                                                                                             ∨ (self."#" y z)))
                                                                                   else Top
                                                                                   fi 
2. ss ∈ record(x.Top)
3. x : Point
4. ss."Point" ∈ Type
5. ss."#" = ss."#" ∈ (ss."Point" ⟶ ss."Point" ⟶ ℙ)
6. ∀x:ss."Point". (¬(ss."#" x x))
7. ss."#symm" ∈ ∀x,y:ss."Point".  ((ss."#" x y) ⇒ (ss."#" y x))
8. ss."#or" ∈ ∀x,y,z:ss."Point".  ((ss."#" x y) ⇒ ((ss."#" x z) ∨ (ss."#" y z)))
⊢ ss."#" x x ∈ Type

---

Latex:

---

Latex:

1.  ss  :  self:"Point":Type
                "\#":\{s:self."Point"  {}\mrightarrow{}  self."Point"  {}\mrightarrow{}  \mBbbP{}|  \mforall{}x:self."Point".  (\mneg{}(s  x  x))\} 
                "\#symm":\mforall{}x,y:self."Point".    ((self."\#"  x  y)  {}\mRightarrow{}  (self."\#"  y  x))  \mcap{}  x:Atom
                {}\mrightarrow{}  if  x  =a  "\#or"
                      then  \mforall{}x,y,z:self."Point".    ((self."\#"  x  y)  {}\mRightarrow{}  ((self."\#"  x  z)  \mvee{}  (self."\#"  y  z)))
                      else  Top
                      fi 
2.  ss  \mmember{}  record(x.Top)
3.  x  :  Point
4.  ss."Point"  \mmember{}  Type
5.  ss."\#"  \mmember{}  \{s:ss."Point"  {}\mrightarrow{}  ss."Point"  {}\mrightarrow{}  \mBbbP{}|  \mforall{}x:ss."Point".  (\mneg{}(s  x  x))\} 
6.  ss."\#symm"  \mmember{}  \mforall{}x,y:ss."Point".    ((ss."\#"  x  y)  {}\mRightarrow{}  (ss."\#"  y  x))
7.  ss."\#or"  \mmember{}  \mforall{}x,y,z:ss."Point".    ((ss."\#"  x  y)  {}\mRightarrow{}  ((ss."\#"  x  z)  \mvee{}  (ss."\#"  y  z)))
\mvdash{}  \mneg{}(ss."\#"  x  x)


By

---

Latex:
At  \mkleeneopen{}Type\mkleeneclose{}  ((MemTypeHD  (-3)  THEN  Auto))\mcdot{}

---

Home Index