[INCLUDE TH/speedbar.blogme]
[SETFAVICON dednat4/dednat4-icon.png]
[lua: LR = R ]
[#
(defun c () (interactive) (find-blogme3-sh0-if "2007dnc-lst"))
;;    http://angg.twu.net/2007dnc-lst.html
;; file:///home/edrx/TH/L/2007dnc-lst.html
;; (eev-math-glyphs-edrx)
;; (find-eevfile "eev-math-glyphs.el")
;; (find-glyphashtml-links "&&")
;; (find-glyphashtml-links "ku")
;; (find-glyphashtml-links "^^")
;; (find-glyphashtml-links "GG")
;; (add-to-alist 'eev-math-glyphs-name-to-char '("sqcup" . 343252))
;; (add-to-alist 'eev-math-glyphs-name-to-char '("Gamma" . 332659))
;; (eev-math-glyphs-set 'eev-glyph-face-linear "ud&"   "&&" "Ñ")
;; (eev-math-glyphs-set 'eev-glyph-face-linear "sqcup" "ku" "Ñ")
;; (eev-math-glyphs-set 'eev-glyph-face-graphic "neblock" "^^" "£")
;; (eev-math-glyphs-set 'eev-glyph-face-Greek   "Gamma"   "GG" "£")
#]
[lua:
  -- (eev-math-glyphs-edrx)
  eev_math_glyphs_edrx()
  sgmlify_table["\04"]  = "δ"
  sgmlify_table["\05"]  = "ε"
  sgmlify_table["\207"] = "ω"
  sgmlify_table["\209"] = "⊔"
  sgmlify_table["\209"] = "⊔"
  sgmlify_table["\163"] = "Γ"
  sgmlify_re = "([\1-\8\12\14-\31\128-\254])"
]

[htmlize [J Notes on other downcasings]

[P These are notes on downcasings that I have not completed yet. They
are for personal use; they contain errors.]

[WITHINDEX
[#
 # «.lst»	(to "lst")
 #]
[RULE ----------------------------------------]


[tsec «lst»  (to ".lst")
[++N]. Local Set Theories
=============================

(T1)  |-*

(T2)  a|-a

      a|-b  b|->c
(T3)  -----------
        a|-c

      a|-b_1 ... a|-b_n
(T4)  -----------------
      a|-(b_1,...,b_n)

      a|-(b_1,...,b_n)
(T5)  -----------------
          a|-b_i

      a,b|-Ï[P]
(T6)  ---------
      a|-{b|P}

      a|-b  a|-b'
(T7)  -----------
      a|-Ï[b=b']

      a|-b  a|-{b|P}
(T8)  --------------
       a|-Ï[bÝ{b|P}]


(L1)  P<=>Q := Ï[P]=Ï[Q]
(L2)      § := *=*
(L3)    P´Q := (Ï[P],Ï[Q])=(Ï[§],Ï[§])
(L4)    P¶Q := (P´Q)<=>P
(L5)   ýb.P := {b|P}={b|§}
(L6)      ® := ýÏ[P].P
(L7)     ¬P := P¶®
(L8)    PQ := ýÏ[R].(((P¶R)´(Q¶R))¶R)
(L9)   Îb.P := ýÏ[Q]. ...


(Tautology)     P|-P
(Unity)         |-*'=*
(Equality)      b'=b''|-c[b:=b']=c[b:=b'']
(Products)      |-<b,c>=b
                |-'<b,c>=c
                |-<(b,c),'(b,c)>=(b,c)
(Comprehension) |-bÝ{b|P}<=>P


                  P|-R
(Thinning)        ------
                  P,Q|-R

                  a;P|-Q   a;P,Q|-R
(Cut)             -----------------
                       a;P|-R

                    a,b;P|-Q   a|-b'
(Subst)           --------------------
                  a;P[b:=b']|-Q[b:=b']

                  a,b;P|-bÝ{b|Q}<=>bÝ{b|R}
(Extensionality)  ------------------------
                    a;P|-{b|Q}<=>{b|R}

                  P,Q|-R   P,R|-Q
(Equivalence)     ---------------
                     P|-Q<=>R

]

]
]
[#
 # Local Variables:
 # coding: raw-text-unix
 # modes: (fundamental-mode blogme-mode)
 # End:
#]