[INCLUDE TH/speedbar.blogme]
[SETFAVICON dednat4/dednat4-icon.png]
[lua: LR = R ]
[# 
(defun c () (interactive) (find-blogme3-sh0-if "2007lcccs"))
;;    http://angg.twu.net/2007lcccs.html
;; file:///home/edrx/TH/L/2007lcccs.html
#]
[lua:
  -- (eev-math-glyphs-edrx)
  eev_math_glyphs_edrx()
]

[htmlize [J Downcasing LCCCs]

[P (You are not expected to understand this!)]

[WITHINDEX
[#
 # «.rules-jacobs»	(to "rules-jacobs")
 # «.strong-sum-and-eq»	(to "strong-sum-and-eq")
 #]

[RULE ----------------------------------------]

[tsec «rules-jacobs»  (to ".rules-jacobs")
[++N]. Rules (from Jacobs's book)
=================================
From Sec. 10.1, pp.584-594.

Projection:     a|-B
               ------
               a,b|-b

Substitution:  a|-b   a,b,c|-D/d
               -----------------
                   a,c|-D/d

Contraction:   a,b,b',c|-D/d
               -------------
                a,b,c|-D/d

Weakening:     a|-B   a|-C/c
               -------------
                 a,b|-C/c

Exchange:      a,b,c,d|-E/e
               ------------
               a,c,b,d|-E/e

Unit type:               a|-*'
            ---   ---   -------
            |-1   |-*   a|-*=*'

å, Æ, Eq:   a,b|-C     a,b|-C         a|-B	      
	    -------    -------    ---------------
  	    a|-åb.C    a|-Æb.C    a,b,b'|-W[b=b']

	    a,b|-c     a|-b   a|-b|->c
	   --------    ---------------
	   a|-b|->c        a|-c

	  a,b|-C       a|-D   a,b,c|-d
       ------------    ---------------(weak)
       a,b,c|-<b,c>      a,(b,c)|-d

	    a|-B       a,b,b',c|-D   a,b,\barc|-\bard
	 ----------    ------------------------------(weak)
	 a,b|-(b=b)         a,b,b'(b=b'),c|-d

Page: 588: some conversions.
I haven't typed them yet...
]

[tsec «strong-sum-and-eq»  (to ".strong-sum-and-eq")
[++N]. Strong sums and strong equality
======================================

  a,(b,c)|-D   a,b,c|-d
  ---------------------(strong)
      a,(b,c)|-d

  a,b,b',(b=b')|-C   a,b|-\barc
  -----------------------------(strong)
       a,b,b'(b=b')|-c
  
Proposition (10.1.3, p.589):
these strong elimination rules
can be equivalently formulated as:

  a|-(b,c)    a|-(b,c)
  --------    --------
    a|-b        a|-c

  a|-(b=b')      a|-(b=b')
  ---------   ---------------(???)
   a|-b=b'    a|-(b=b')=(b=b)
]



[tsec «shorthand-seely-lccc»  (to ".shorthand-seely-lccc")
[++N]. Shorthands for LCCC notation
===================================
(From Seely's paper)

Some term formation rules:

    a|-b
  --------(=I)      Shorthand:
  a|-(b=b)          (b=b) := r(b)

     a,b|-d
  --------------(=E)
  a,b,b',e|-(d)


Some equality rules:

     a,b|-d
  --------------
  a,b,b',e|-(d)
  --------------  (= red)
    a,b|-(d)        =    a,b|-d

  a,b,b',e|-f
  -----------
     a,b|-f
  -----------     (= exp)
  a,b,b',e|-(f)     =    a,b,b',e|-f


  a|-b  a|-b'  a|-e
  -----------------(Irule1)
      a|-b=b'
  
  a|-b  a|-b'  a|-e
  -----------------(Irule2)
      a|-e=(b=b')
]



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