From 8f4d4c66134804bbf2d2fe65c893b68387272d31 Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Sat, 10 Jul 2010 15:57:24 +0100
Subject: Remove non-DFSG contents

---
 doc/faq/axioms.eps | 378 -----------------------------------------------------
 1 file changed, 378 deletions(-)
 delete mode 100644 doc/faq/axioms.eps

(limited to 'doc/faq/axioms.eps')

diff --git a/doc/faq/axioms.eps b/doc/faq/axioms.eps
deleted file mode 100644
index 3f3c01c4..00000000
--- a/doc/faq/axioms.eps
+++ /dev/null
@@ -1,378 +0,0 @@
-%!PS-Adobe-2.0 EPSF-2.0
-%%Title: axioms.fig
-%%Creator: fig2dev Version 3.2 Patchlevel 4
-%%CreationDate: Wed May  5 18:30:03 2004
-%%For: herbelin@limoux.polytechnique.fr (Hugo Herbelin)
-%%BoundingBox: 0 0 437 372
-%%Magnification: 1.0000
-%%EndComments
-/$F2psDict 200 dict def
-$F2psDict begin
-$F2psDict /mtrx matrix put
-/col-1 {0 setgray} bind def
-/col0 {0.000 0.000 0.000 srgb} bind def
-/col1 {0.000 0.000 1.000 srgb} bind def
-/col2 {0.000 1.000 0.000 srgb} bind def
-/col3 {0.000 1.000 1.000 srgb} bind def
-/col4 {1.000 0.000 0.000 srgb} bind def
-/col5 {1.000 0.000 1.000 srgb} bind def
-/col6 {1.000 1.000 0.000 srgb} bind def
-/col7 {1.000 1.000 1.000 srgb} bind def
-/col8 {0.000 0.000 0.560 srgb} bind def
-/col9 {0.000 0.000 0.690 srgb} bind def
-/col10 {0.000 0.000 0.820 srgb} bind def
-/col11 {0.530 0.810 1.000 srgb} bind def
-/col12 {0.000 0.560 0.000 srgb} bind def
-/col13 {0.000 0.690 0.000 srgb} bind def
-/col14 {0.000 0.820 0.000 srgb} bind def
-/col15 {0.000 0.560 0.560 srgb} bind def
-/col16 {0.000 0.690 0.690 srgb} bind def
-/col17 {0.000 0.820 0.820 srgb} bind def
-/col18 {0.560 0.000 0.000 srgb} bind def
-/col19 {0.690 0.000 0.000 srgb} bind def
-/col20 {0.820 0.000 0.000 srgb} bind def
-/col21 {0.560 0.000 0.560 srgb} bind def
-/col22 {0.690 0.000 0.690 srgb} bind def
-/col23 {0.820 0.000 0.820 srgb} bind def
-/col24 {0.500 0.190 0.000 srgb} bind def
-/col25 {0.630 0.250 0.000 srgb} bind def
-/col26 {0.750 0.380 0.000 srgb} bind def
-/col27 {1.000 0.500 0.500 srgb} bind def
-/col28 {1.000 0.630 0.630 srgb} bind def
-/col29 {1.000 0.750 0.750 srgb} bind def
-/col30 {1.000 0.880 0.880 srgb} bind def
-/col31 {1.000 0.840 0.000 srgb} bind def
-
-end
-save
-newpath 0 372 moveto 0 0 lineto 437 0 lineto 437 372 lineto closepath clip newpath
--90.0 435.2 translate
-1 -1 scale
-
-/cp {closepath} bind def
-/ef {eofill} bind def
-/gr {grestore} bind def
-/gs {gsave} bind def
-/sa {save} bind def
-/rs {restore} bind def
-/l {lineto} bind def
-/m {moveto} bind def
-/rm {rmoveto} bind def
-/n {newpath} bind def
-/s {stroke} bind def
-/sh {show} bind def
-/slc {setlinecap} bind def
-/slj {setlinejoin} bind def
-/slw {setlinewidth} bind def
-/srgb {setrgbcolor} bind def
-/rot {rotate} bind def
-/sc {scale} bind def
-/sd {setdash} bind def
-/ff {findfont} bind def
-/sf {setfont} bind def
-/scf {scalefont} bind def
-/sw {stringwidth} bind def
-/tr {translate} bind def
-/tnt {dup dup currentrgbcolor
-  4 -2 roll dup 1 exch sub 3 -1 roll mul add
-  4 -2 roll dup 1 exch sub 3 -1 roll mul add
-  4 -2 roll dup 1 exch sub 3 -1 roll mul add srgb}
-  bind def
-/shd {dup dup currentrgbcolor 4 -2 roll mul 4 -2 roll mul
-  4 -2 roll mul srgb} bind def
-/reencdict 12 dict def /ReEncode { reencdict begin
-/newcodesandnames exch def /newfontname exch def /basefontname exch def
-/basefontdict basefontname findfont def /newfont basefontdict maxlength dict def
-basefontdict { exch dup /FID ne { dup /Encoding eq
-{ exch dup length array copy newfont 3 1 roll put }
-{ exch newfont 3 1 roll put } ifelse } { pop pop } ifelse } forall
-newfont /FontName newfontname put newcodesandnames aload pop
-128 1 255 { newfont /Encoding get exch /.notdef put } for
-newcodesandnames length 2 idiv { newfont /Encoding get 3 1 roll put } repeat
-newfontname newfont definefont pop end } def
-/isovec [
-8#055 /minus 8#200 /grave 8#201 /acute 8#202 /circumflex 8#203 /tilde
-8#204 /macron 8#205 /breve 8#206 /dotaccent 8#207 /dieresis
-8#210 /ring 8#211 /cedilla 8#212 /hungarumlaut 8#213 /ogonek 8#214 /caron
-8#220 /dotlessi 8#230 /oe 8#231 /OE
-8#240 /space 8#241 /exclamdown 8#242 /cent 8#243 /sterling
-8#244 /currency 8#245 /yen 8#246 /brokenbar 8#247 /section 8#250 /dieresis
-8#251 /copyright 8#252 /ordfeminine 8#253 /guillemotleft 8#254 /logicalnot
-8#255 /hyphen 8#256 /registered 8#257 /macron 8#260 /degree 8#261 /plusminus
-8#262 /twosuperior 8#263 /threesuperior 8#264 /acute 8#265 /mu 8#266 /paragraph
-8#267 /periodcentered 8#270 /cedilla 8#271 /onesuperior 8#272 /ordmasculine
-8#273 /guillemotright 8#274 /onequarter 8#275 /onehalf
-8#276 /threequarters 8#277 /questiondown 8#300 /Agrave 8#301 /Aacute
-8#302 /Acircumflex 8#303 /Atilde 8#304 /Adieresis 8#305 /Aring
-8#306 /AE 8#307 /Ccedilla 8#310 /Egrave 8#311 /Eacute
-8#312 /Ecircumflex 8#313 /Edieresis 8#314 /Igrave 8#315 /Iacute
-8#316 /Icircumflex 8#317 /Idieresis 8#320 /Eth 8#321 /Ntilde 8#322 /Ograve
-8#323 /Oacute 8#324 /Ocircumflex 8#325 /Otilde 8#326 /Odieresis 8#327 /multiply
-8#330 /Oslash 8#331 /Ugrave 8#332 /Uacute 8#333 /Ucircumflex
-8#334 /Udieresis 8#335 /Yacute 8#336 /Thorn 8#337 /germandbls 8#340 /agrave
-8#341 /aacute 8#342 /acircumflex 8#343 /atilde 8#344 /adieresis 8#345 /aring
-8#346 /ae 8#347 /ccedilla 8#350 /egrave 8#351 /eacute
-8#352 /ecircumflex 8#353 /edieresis 8#354 /igrave 8#355 /iacute
-8#356 /icircumflex 8#357 /idieresis 8#360 /eth 8#361 /ntilde 8#362 /ograve
-8#363 /oacute 8#364 /ocircumflex 8#365 /otilde 8#366 /odieresis 8#367 /divide
-8#370 /oslash 8#371 /ugrave 8#372 /uacute 8#373 /ucircumflex
-8#374 /udieresis 8#375 /yacute 8#376 /thorn 8#377 /ydieresis] def
-/Times-Roman /Times-Roman-iso isovec ReEncode
-/$F2psBegin {$F2psDict begin /$F2psEnteredState save def} def
-/$F2psEnd {$F2psEnteredState restore end} def
-
-$F2psBegin
-10 setmiterlimit
-0 slj 0 slc
- 0.06000 0.06000 sc
-%
-% Fig objects follow
-%
-% 
-% here starts figure with depth 50
-% Arc
-7.500 slw
-gs  clippath
-3599 6933 m 3626 6879 l 3492 6812 l 3586 6893 l 3465 6865 l cp
-eoclip
-n 3600.0 6750.0 150.0 90.0 -90.0 arc
-gs col0 s gr
- gr
-
-% arrowhead
-n 3465 6865 m 3586 6893 l 3492 6812 l 3465 6865 l  cp gs 0.00 setgray ef gr  col0 s
-% Arc
-gs  clippath
-3599 6633 m 3626 6579 l 3492 6512 l 3586 6593 l 3465 6565 l cp
-eoclip
-n 3600.0 6450.0 150.0 90.0 -90.0 arc
-gs col0 s gr
- gr
-
-% arrowhead
-n 3465 6565 m 3586 6593 l 3492 6512 l 3465 6565 l  cp gs 0.00 setgray ef gr  col0 s
-% Arc
-gs  clippath
-3626 6020 m 3599 5966 l 3465 6034 l 3586 6007 l 3492 6087 l cp
-3599 6333 m 3626 6279 l 3492 6212 l 3586 6293 l 3465 6265 l cp
-eoclip
-n 3600.0 6150.0 150.0 90.0 -90.0 arc
-gs col0 s gr
- gr
-
-% arrowhead
-n 3492 6087 m 3586 6007 l 3465 6034 l 3492 6087 l  cp gs 0.00 setgray ef gr  col0 s
-% arrowhead
-n 3465 6265 m 3586 6293 l 3492 6212 l 3465 6265 l  cp gs 0.00 setgray ef gr  col0 s
-% Arc
-gs  clippath
-3626 6320 m 3599 6266 l 3465 6334 l 3586 6307 l 3492 6387 l cp
-3599 6633 m 3626 6579 l 3492 6512 l 3586 6593 l 3465 6565 l cp
-eoclip
-n 3600.0 6450.0 150.0 90.0 -90.0 arc
-gs col0 s gr
- gr
-
-% arrowhead
-n 3492 6387 m 3586 6307 l 3465 6334 l 3492 6387 l  cp gs 0.00 setgray ef gr  col0 s
-% arrowhead
-n 3465 6565 m 3586 6593 l 3492 6512 l 3465 6565 l  cp gs 0.00 setgray ef gr  col0 s
-% Arc
-gs  clippath
-3626 6620 m 3599 6566 l 3465 6634 l 3586 6607 l 3492 6687 l cp
-3599 6933 m 3626 6879 l 3492 6812 l 3586 6893 l 3465 6865 l cp
-eoclip
-n 3600.0 6750.0 150.0 90.0 -90.0 arc
-gs col0 s gr
- gr
-
-% arrowhead
-n 3492 6687 m 3586 6607 l 3465 6634 l 3492 6687 l  cp gs 0.00 setgray ef gr  col0 s
-% arrowhead
-n 3465 6865 m 3586 6893 l 3492 6812 l 3465 6865 l  cp gs 0.00 setgray ef gr  col0 s
-% Arc
-gs  clippath
-3626 6920 m 3599 6866 l 3465 6934 l 3586 6907 l 3492 6987 l cp
-3599 7233 m 3626 7179 l 3492 7112 l 3586 7193 l 3465 7165 l cp
-eoclip
-n 3600.0 7050.0 150.0 90.0 -90.0 arc
-gs col0 s gr
- gr
-
-% arrowhead
-n 3492 6987 m 3586 6907 l 3465 6934 l 3492 6987 l  cp gs 0.00 setgray ef gr  col0 s
-% arrowhead
-n 3465 7165 m 3586 7193 l 3492 7112 l 3465 7165 l  cp gs 0.00 setgray ef gr  col0 s
-% Arc
-gs  clippath
-4168 4060 m 4227 4068 l 4247 3919 l 4202 4034 l 4188 3911 l cp
-eoclip
-n 14032.5 5272.5 9908.2 -159.9 -172.9 arcn
-gs col0 s gr
- gr
-
-% arrowhead
-n 4188 3911 m 4202 4034 l 4247 3919 l 4188 3911 l  cp gs 0.00 setgray ef gr  col0 s
-% Polyline
-gs  clippath
-4170 5790 m 4230 5790 l 4230 5639 l 4200 5759 l 4170 5639 l cp
-eoclip
-n 4200 5175 m
- 4200 5775 l gs col0 s gr gr
-
-% arrowhead
-n 4170 5639 m 4200 5759 l 4230 5639 l 4170 5639 l  cp gs 0.00 setgray ef gr  col0 s
-% Polyline
-gs  clippath
-4553 5749 m 4567 5807 l 4714 5771 l 4591 5771 l 4700 5713 l cp
-eoclip
-n 7050 5175 m
- 4575 5775 l gs col0 s gr gr
-
-% arrowhead
-n 4700 5713 m 4591 5771 l 4714 5771 l 4700 5713 l  cp gs 0.00 setgray ef gr  col0 s
-% Polyline
-gs  clippath
-4170 4890 m 4230 4890 l 4230 4739 l 4200 4859 l 4170 4739 l cp
-eoclip
-n 4200 4275 m
- 4200 4875 l gs col0 s gr gr
-
-% arrowhead
-n 4170 4739 m 4200 4859 l 4230 4739 l 4170 4739 l  cp gs 0.00 setgray ef gr  col0 s
-% Polyline
-gs  clippath
-7131 4907 m 7147 4850 l 7001 4810 l 7109 4871 l 6985 4868 l cp
-eoclip
-n 4950 4275 m
- 7125 4875 l gs col0 s gr gr
-
-% arrowhead
-n 6985 4868 m 7109 4871 l 7001 4810 l 6985 4868 l  cp gs 0.00 setgray ef gr  col0 s
-% Polyline
-gs  clippath
-7167 4057 m 7225 4071 l 7262 3924 l 7204 4034 l 7204 3910 l cp
-eoclip
-n 7725 1950 m
- 7200 4050 l gs col0 s gr gr
-
-% arrowhead
-n 7204 3910 m 7204 4034 l 7262 3924 l 7204 3910 l  cp gs 0.00 setgray ef gr  col0 s
-% Polyline
-n 4350 3075 m
- 7350 1950 l gs col0 s gr 
-% Polyline
-gs  clippath
-7170 4890 m 7230 4890 l 7230 4739 l 7200 4859 l 7170 4739 l cp
-eoclip
-n 7200 4275 m
- 7200 4875 l gs col0 s gr gr
-
-% arrowhead
-n 7170 4739 m 7200 4859 l 7230 4739 l 7170 4739 l  cp gs 0.00 setgray ef gr  col0 s
-% Polyline
-n 3075 1875 m
- 3975 1875 l gs col0 s gr 
-% Polyline
-gs  clippath
-5520 4065 m 5580 4065 l 5580 3914 l 5550 4034 l 5520 3914 l cp
-5580 3660 m 5520 3660 l 5520 3811 l 5550 3691 l 5580 3811 l cp
-eoclip
-n 5550 3675 m
- 5550 4050 l gs col0 s gr gr
-
-% arrowhead
-n 5580 3811 m 5550 3691 l 5520 3811 l 5580 3811 l  cp gs 0.00 setgray ef gr  col0 s
-% arrowhead
-n 5520 3914 m 5550 4034 l 5580 3914 l 5520 3914 l  cp gs 0.00 setgray ef gr  col0 s
-% Polyline
-n 4575 4050 m
- 6450 4050 l gs col0 s gr 
-% Polyline
-gs  clippath
-3495 2265 m 3555 2265 l 3555 2114 l 3525 2234 l 3495 2114 l cp
-3555 1860 m 3495 1860 l 3495 2011 l 3525 1891 l 3555 2011 l cp
-eoclip
-n 3525 1875 m
- 3525 2250 l gs col0 s gr gr
-
-% arrowhead
-n 3555 2011 m 3525 1891 l 3495 2011 l 3555 2011 l  cp gs 0.00 setgray ef gr  col0 s
-% arrowhead
-n 3495 2114 m 3525 2234 l 3555 2114 l 3495 2114 l  cp gs 0.00 setgray ef gr  col0 s
-% Polyline
-gs  clippath
-2219 3988 m 2279 3991 l 2285 3840 l 2251 3959 l 2225 3838 l cp
-eoclip
-n 2325 1875 m
- 2250 3975 l gs col0 s gr gr
-
-% arrowhead
-n 2225 3838 m 2251 3959 l 2285 3840 l 2225 3838 l  cp gs 0.00 setgray ef gr  col0 s
-% Polyline
-n 7800 1275 m
- 2100 1275 l gs col0 s gr 
-/Times-Roman-iso ff 180.00 scf sf
-6600 5100 m
-gs 1 -1 sc (Proof-irrelevance) col0 sh gr
-/Times-Roman-iso ff 180.00 scf sf
-3675 4200 m
-gs 1 -1 sc (Excluded-middle) col0 sh gr
-/Times-Roman-iso ff 180.00 scf sf
-6900 1800 m
-gs 1 -1 sc (Predicate extensionality) col0 sh gr
-/Times-Roman-iso ff 180.00 scf sf
-3375 3525 m
-gs 1 -1 sc (\(Diaconescu\)) col0 sh gr
-/Times-Roman-iso ff 180.00 scf sf
-4650 3600 m
-gs 1 -1 sc (Propositional degeneracy) col0 sh gr
-/Times-Roman-iso ff 180.00 scf sf
-3825 1800 m
-gs 1 -1 sc (Relational choice axiom) col0 sh gr
-/Times-Roman-iso ff 180.00 scf sf
-1725 1800 m
-gs 1 -1 sc (Description principle) col0 sh gr
-/Times-Roman-iso ff 180.00 scf sf
-2550 2400 m
-gs 1 -1 sc (Functional choice axiom) col0 sh gr
-/Times-Roman-iso ff 180.00 scf sf
-3600 5100 m
-gs 1 -1 sc (Decidability of equality on $A$) col0 sh gr
-/Times-Roman-iso ff 180.00 scf sf
-4425 4575 m
-gs 1 -1 sc (\(needs Prop-impredicativity\)) col0 sh gr
-/Times-Roman-iso ff 180.00 scf sf
-5025 4725 m
-gs 1 -1 sc (\(Berardi\)) col0 sh gr
-/Times-Roman-iso ff 180.00 scf sf
-1500 3075 m
-gs 1 -1 sc (\(if Set impredicative\)) col0 sh gr
-/Times-Roman-iso ff 180.00 scf sf
-1500 4200 m
-gs 1 -1 sc (Not excluded-middle) col0 sh gr
-/Times-Roman-iso ff 180.00 scf sf
-3600 6000 m
-gs 1 -1 sc (Axiom K on A) col0 sh gr
-/Times-Roman-iso ff 180.00 scf sf
-3600 7200 m
-gs 1 -1 sc (Invariance by substitution of reflexivity proofs for equality on A) col0 sh gr
-/Times-Roman-iso ff 180.00 scf sf
-6150 4200 m
-gs 1 -1 sc (Propositional extensionality) col0 sh gr
-/Times-Roman-iso ff 180.00 scf sf
-2100 1200 m
-gs 1 -1 sc (The dependency graph of axioms in the Calculus of Inductive Constructions) col0 sh gr
-/Times-Roman-iso ff 180.00 scf sf
-3600 6900 m
-gs 1 -1 sc (Injectivity of equality on sigma-types on A) col0 sh gr
-/Times-Roman-iso ff 180.00 scf sf
-3600 6300 m
-gs 1 -1 sc (Uniqueness of reflexivity proofs for equality on A) col0 sh gr
-/Times-Roman-iso ff 180.00 scf sf
-3600 6600 m
-gs 1 -1 sc (Uniqueness of equality proofs on A) col0 sh gr
-% here ends figure;
-$F2psEnd
-rs
-showpage
-- 
cgit v1.2.3