%PDF-1.4 5 0 obj << /S /GoTo /D (chapter.1) >> endobj 8 0 obj (Motivation und Einleitung) endobj 9 0 obj << /S /GoTo /D (section.1.1) >> endobj 12 0 obj (\334berblick) endobj 13 0 obj << /S /GoTo /D (section.1.2) >> endobj 16 0 obj (Lesehinweise) endobj 17 0 obj << /S /GoTo /D (section.1.3) >> endobj 20 0 obj (Eine kurze Begriffs- und Notations\374bersicht) endobj 21 0 obj << /S /GoTo /D (chapter.2) >> endobj 24 0 obj (Isabelle) endobj 25 0 obj << /S /GoTo /D (section.2.1) >> endobj 28 0 obj (Isabelle/HOL und Isabelle/HOLCF in K\374rze) endobj 29 0 obj << /S /GoTo /D (section.2.2) >> endobj 32 0 obj (Isabelle/HOLCF im \334berblick) endobj 33 0 obj << /S /GoTo /D (section.2.3) >> endobj 36 0 obj (Stetigkeit von HOLCF-Funktionen) endobj 37 0 obj << /S /GoTo /D (section.2.4) >> endobj 40 0 obj (Stromverarbeitende HOLCF-Funktionen) endobj 41 0 obj << /S /GoTo /D (chapter.3) >> endobj 44 0 obj (Allgemeine Streams in HOLCF) endobj 45 0 obj << /S /GoTo /D (section.3.1) >> endobj 48 0 obj (Konstruktion von Streams) endobj 49 0 obj << /S /GoTo /D (section.3.2) >> endobj 52 0 obj (Basiseigenschaften) endobj 53 0 obj << /S /GoTo /D (section.3.3) >> endobj 56 0 obj (Take-Funktional und Take-Lemma) endobj 57 0 obj << /S /GoTo /D (section.3.4) >> endobj 60 0 obj (Weitere abgeleitete Basiseigenschaften) endobj 61 0 obj << /S /GoTo /D (chapter.4) >> endobj 64 0 obj (Fstreams - Ein formales Modell f\374r Str\366me) endobj 65 0 obj << /S /GoTo /D (section.4.1) >> endobj 68 0 obj (Grundlage f\374r die Konstruktion von Fstreams) endobj 69 0 obj << /S /GoTo /D (section.4.2) >> endobj 72 0 obj (Take-Funktional auf Fstreams und seine kleinste obere Schranke) endobj 73 0 obj << /S /GoTo /D (section.4.3) >> endobj 76 0 obj (Konkatenation) endobj 77 0 obj << /S /GoTo /D (section.4.4) >> endobj 80 0 obj (Eine konstruktive Charakterisierung von Fstreams) endobj 81 0 obj << /S /GoTo /D (section.4.5) >> endobj 84 0 obj (L\344ngenfunktion) endobj 85 0 obj << /S /GoTo /D (section.4.6) >> endobj 88 0 obj (Grundlegende Induktionsregeln f\374r Fstreams) endobj 89 0 obj << /S /GoTo /D (section.4.7) >> endobj 92 0 obj (Weitere Eigenschaften der Konkatenation) endobj 93 0 obj << /S /GoTo /D (subsection.4.7.1) >> endobj 96 0 obj (Monotonie) endobj 97 0 obj << /S /GoTo /D (subsection.4.7.2) >> endobj 100 0 obj (Stetigkeit) endobj 101 0 obj << /S /GoTo /D (subsection.4.7.3) >> endobj 104 0 obj (Assoziativit\344t) endobj 105 0 obj << /S /GoTo /D (subsection.4.7.4) >> endobj 108 0 obj (L\344nge der Konkatenation zweier endlichen Str\366me) endobj 109 0 obj << /S /GoTo /D (subsection.4.7.5) >> endobj 112 0 obj (Injektivit\344t) endobj 113 0 obj << /S /GoTo /D (section.4.8) >> endobj 116 0 obj (Weitere Eigenschaften des Take-Funktionals) endobj 117 0 obj << /S /GoTo /D (subsection.4.8.1) >> endobj 120 0 obj (Idempotenz) endobj 121 0 obj << /S /GoTo /D (subsection.4.8.2) >> endobj 124 0 obj (Komposition) endobj 125 0 obj << /S /GoTo /D (section.4.9) >> endobj 128 0 obj (Die verallgemeinerte Induktion) endobj 129 0 obj << /S /GoTo /D (section.4.10) >> endobj 132 0 obj (L\366schen beliebig langer Anfangsst\374cke und der punktweise Zugriff) endobj 133 0 obj << /S /GoTo /D (section.4.11) >> endobj 136 0 obj (Weitere grundlegende Lemmata f\374r Fstreams) endobj 137 0 obj << /S /GoTo /D (subsection.4.11.1) >> endobj 140 0 obj (Zerlegungslemma) endobj 141 0 obj << /S /GoTo /D (subsection.4.11.2) >> endobj 144 0 obj (Lemma f\374r den punktweisen Vergleich) endobj 145 0 obj << /S /GoTo /D (subsection.4.11.3) >> endobj 148 0 obj (Approximationslemma) endobj 149 0 obj << /S /GoTo /D (chapter.5) >> endobj 152 0 obj (Die Definitionsprinzipien f\374r rekursive Funktionen auf Fstreams) endobj 153 0 obj << /S /GoTo /D (section.5.1) >> endobj 156 0 obj (Ein allgemeines Definitionsmuster) endobj 157 0 obj << /S /GoTo /D (subsection.5.1.1) >> endobj 160 0 obj (Rekursive Funktionen auf Str\366men) endobj 161 0 obj << /S /GoTo /D (subsection.5.1.2) >> endobj 164 0 obj (Der Spezialfall: Stromverarbeitende Funktionen) endobj 165 0 obj << /S /GoTo /D (section.5.2) >> endobj 168 0 obj (Stromverarbeitende Funktionen als Zustandsautomaten) endobj 169 0 obj << /S /GoTo /D (section.5.3) >> endobj 172 0 obj (Stromverarbeitende Funktionen als HOLCF-Fixpunktgleichungen) endobj 173 0 obj << /S /GoTo /D (section.5.4) >> endobj 176 0 obj (Stromverarbeitende Funktionen mit Hilfe der stetigen HOL-Funktionen) endobj 177 0 obj << /S /GoTo /D (chapter.6) >> endobj 180 0 obj (Eine Bibliothek von Funktionen f\374r Fstreams) endobj 181 0 obj << /S /GoTo /D (section.6.1) >> endobj 184 0 obj (Punktweise Abbildung von Str\366men) endobj 185 0 obj << /S /GoTo /D (section.6.2) >> endobj 188 0 obj (Projektionen) endobj 189 0 obj << /S /GoTo /D (section.6.3) >> endobj 192 0 obj (Filterung von Str\366men auf der Basis einer Zeichenmenge) endobj 193 0 obj << /S /GoTo /D (section.6.4) >> endobj 196 0 obj (Zippen zweier Str\366me) endobj 197 0 obj << /S /GoTo /D (section.6.5) >> endobj 200 0 obj (Reissverschlussartiges Mergen zweier Str\366me) endobj 201 0 obj << /S /GoTo /D (section.6.6) >> endobj 204 0 obj (Selektion eines Anfangsst\374cks) endobj 205 0 obj << /S /GoTo /D (section.6.7) >> endobj 208 0 obj (L\366schen eines Anfangsst\374cks) endobj 209 0 obj << /S /GoTo /D (section.6.8) >> endobj 212 0 obj (Entfernung von unmittelbaren Zeichenwiederholungen) endobj 213 0 obj << /S /GoTo /D (section.6.9) >> endobj 216 0 obj (Verflachung von Str\366men auf Str\366men) endobj 217 0 obj << /S /GoTo /D (section.6.10) >> endobj 220 0 obj (Rekursionsmuster f\374r Str\366me) endobj 221 0 obj << /S /GoTo /D (section.6.11) >> endobj 224 0 obj (Iterierte Bildung von Str\366men) endobj 225 0 obj << /S /GoTo /D (section.6.12) >> endobj 228 0 obj (Bildung periodischer Str\366me) endobj 229 0 obj << /S /GoTo /D (section.6.13) >> endobj 232 0 obj (Mengen von Str\366men) endobj 233 0 obj << /S /GoTo /D (chapter.7) >> endobj 236 0 obj (Schlussbemerkungen) endobj 237 0 obj << /S /GoTo /D (section.7.1) >> endobj 240 0 obj (Zusammenfassung und Ausblick) endobj 241 0 obj << /S /GoTo /D (section.7.2) >> endobj 244 0 obj (Diskussion) endobj 245 0 obj << /S /GoTo /D (section.7.3) >> endobj 248 0 obj (Danksagung) endobj 249 0 obj << /S /GoTo /D (chapter*.2) >> endobj 252 0 obj (Literaturverzeichnis) endobj 253 0 obj << /S /GoTo /D [254 0 R /Fit ] >> endobj 258 0 obj << /Length 682 /Filter /FlateDecode >> stream xڍTn0+xNfiE[Ʀm6hq|}E%Z /|ˌI THKKѺNA:S%krƱ*+(jLίDTcF%Zn!*q(z)ZnL]{λm;ׯ}<[fP;c*nX\e`ByL(hju}~m:!iu/-dE>~okӻ~m1H(b%Hw뇉qH6>g4RSmŖKsCajǜ `y&:BvzYjʞ!;?0!Jm{9@H®硍XL(k \[6Pd@Lc3г~/.an&p)qa)8'!*'|T A$%,%,w9 Ezm~z*@|\#: eeykhI.f.BN^L `*x#"*X4cy:yL:8)h g7|BI\XJSD&;Ms;\MKQL>AsرF慈ޖ(_t!On(?JTӷ> [Cendstream endobj 254 0 obj << /Type /Page /Contents 258 0 R /Resources 257 0 R /MediaBox [0 0 595.276 841.89] /Parent 264 0 R >> endobj 255 0 obj << /Type /XObject /Subtype /Form /FormType 1 /PTEX.FileName (./pics/tulogo_sw.pdf) /PTEX.PageNumber 1 /PTEX.InfoDict 265 0 R /Matrix [1 0 0 1 0 0] /BBox [0 0 600 700] /Resources << /ProcSet [ /PDF /ImageB ] /ExtGState << /R4 266 0 R >>/XObject << /R8 267 0 R >>>> /Length 268 0 R /Filter /FlateDecode >> stream x+T03T0 A(Uȥd^eę\ qSKKK=3maPʕTkhdnipXY`kA֝U Qe v.X`,\ 8z'endstream endobj 265 0 obj << /Producer (GNU Ghostscript 7.07) >> endobj 266 0 obj << /Type /ExtGState /Name /R4 /TR /Identity /OPM 1 /SM 0.02 >> endobj 267 0 obj << /Subtype /Image /ImageMask true /Width 600 /Height 700 /BitsPerComponent 1 /Filter /CCITTFaxDecode /DecodeParms << /K -1 /Columns 600 >> /Length 6239 >> stream Aw-̀^WY6UuhHҸeW̐D( 89\@m y^m;)Z@`CUr膐a24i.A`+5&0 5Ll HZdX2H704(7!m(M@܈08A40ҫI0a!( D2a_pa'=AÂà `/mt pA"ש Km/:*K[A_@kIH8An_A.u/ո@\v.պ7ZpH7ID5nOwAME+tM n oV֛mt1rRl:FӵH:m l=[ta>Nn@۫ucPi$}m ;L=R kA"ccC6 @n 0U[BR ,$àB꒷ %|0LIC6az}p! [|"&mKj[NQ$o[F<2AUW Ć!0åo T&Wx zAtpD (}%wmKB KmD5 @j a6-AkoT]A@ ["& T-80aTt$ۄnp ]bK0MNn +t(%@QTtmHa(n%WA't 0XI+l JJXl5z[m0I0wH,0W:vHm!A;tm:;tX0DGMh%'M$rmMҰ,0`֭״I& dXa%Rm렖JMYmz>]B 6Zl6 6֛ti/a6Zm۪ZnwJ!p6iۺI7I`:zIAh6 V}n ^Ah0oHW/J)-0Pu[KmJZl0+ґ^Za'z@wDZZl:I^]HoUtN,8IvnPb^ޒ`KnmXuһґ hAi:mzRP V$ oJ n:EJۨV =E*"v"+vd2 (a0͵. A ' 7U_lR?;;mH&Y T\+mBӟ%H'A0W-OIXu}v&F۫I+ڰ=4۱NJ o{zO mmb,ֵ7v0l;܂zH&U٢C~WXanwH5n$:G.uy nO]vݫna;E"n!ۄޗd;k@r֘;mzWUuMTw4`L;&l}:w:4I_d4I"i 6 5R1izWzؤB.S!oV.tuw/[yA7H=vwt?%G,~JH5'a I">n 7Awoo] IV jPl&Ah0"0MkwXwvUtڡ{Mw_Z݄m7*zVD]SFavXnCQK6 [t7ۮ;A{j؎oZtްt ^h _TK^S_n&6 v&u^_÷t?~5#ino֯7>tw'mvZIo&7D3"Do_o{uAfnNI>'mn]zAO)&[[ҊߤXms_SFww_Kð}n/l7MOGPTawD jo7mߔM#@Wa߆r =ݻ ꅰnݫ6v~SA^o=CNw ZK Mdp\?a}mO8+uӸ 7&p'M.0.^.Kr&ATp R C¯;0X`?U]o_ii^=$=셅wh?vt!9&@~dB߷D5ȻgD\24@4VS_[om}Kv!߿ؠ}z5[s\0=1%Fmh nN: bh t sBgX ''z x@v\3_.4ߓxDT30ۯ\4D2Xc_i'#XSQ`~J@Ok6țxoޓowAVMk )5]5ok>=i{!w62^6D'SY}D}6TѨS` wf m?ޫ w0Z[$B|w5 U7 BOIiZ|cPZkUXhc:EZp|*~T?Z!}*QP=o _/o^]p%a/.JM3 Cao0AI.C(ᄿV¯C@4AچҮ> T0~Fr!惆\OP]ZN{M+dQ7,0\CA_+Jzi%>^.DBWeW)~%?mv~7KzKA0KSvZ<>^!u&IxdX2<*Qǫm%PǠXR^ .ӰMl]%.$5pf.hY*nׯi>Cdk5~f>; D't1hz{龗 l /Kp `z >`t.Ww 3T%BA|PMUު5.C>jZjQ b]3n{ׄ?]}tD-5>xݠjCA8w}W|Od,xTi삇0߬y<;MR|/.7;/w`d{]ڣh'H@ҫt齴ȸen{KO<_%ڥY\Vt|H `Im֤~WӴO{oTCh? w^+ÿҐQmq_(gP{ ,n:\. ᯕ0çp& 0 mj}tWȠE`LF,o#^ۭ=Fo p[ m n}o OL:6=]w~m+h07aîmUῦî7{J ||}aowik[\uG?R >-m@C#= dKi}_@> ޏ%86}<6 kDJk)=#?vտ{:kRP+_u߰]pL֚]; V/!u0}iDcΠ x> ViWE״CoPutM@ګx}ZCHK}?>zP!ې<9PVV uݵa lN jo5^A6f."1<W%@ݾApQlSEH~)&з>״{LT\' zA]I,0_җzL?ӷC[ wz GNN_ Їtiz h&Z[u#K8]/4mA4z{R5j@-W!HFw]iA]-ڭkMm9ԆǤ+a5 Zof~w_KNHM/Am0KM 0_[ n5(K(3iH=RWV}0G@`AZ^ZJnA onA:H=|-PA>[xJk!"Pzi,:!*Tl@Ą_VDRiA*)0H6u$8`iUmuOҤ[rGI }kv4tчm]^T+o_~i]iwN]-J݄$R`^d-lSn$ntmRm܁b聈nw$um6b;^xit*ޭ %T$#wkp}PT-@60oR $ ݮ}B۫@Baݲ}dL۫OpI+a밓(Ri]7$bhe۵R ҼUWJ~[a}U$Wkl[$- T CV%h&xU^M%JWaBn)Q:H)Umj't %I7I:V`8JTKmS~ɸ$$նFnK ~!xATtA64| ~H'Aߧ]%aAwMM$ꭊma+im~MWD2߭ al4 HaM$i[ mנ A[ uI6mפ +il?pL6Kn[ m[~H6i+B?h$:mI[Z$[K<5BAaoPqn$!aI][?A %nI'An?m- VߤI[oA&V~ Y 4&h60&ޭH7oWO6" nӤچ -IUkݵ ä`A[cl5 ChHtd2!V:0x AY 2PKVڰL3m IA @a-ՆAnU#ޕaCU\ TzJ0H0d6h-ҫc`2{eޒe,Э {+}% xeiV[m hH+o-ä`*`objE40ۄ B:m0ñ4h k]Xl> 4J!amKo _U4OI[jՠ Vwu6݄կKݶ֒R;WťV*]C6 N A[^-& mV4R ֿ[KDAA~%nmA[Ja%mk] Cj m-%a_ t߰%3kPKJޗ ê} aAl?,0$ ]\JaAC i{ku}0a(`+Pd\3!00nIL2*(`J[A4h 4 @kI.CUs!$(2i4 CT. ݫ +cX2 jq0'0,J )\2x0R --Ӂ$ # endstream endobj 268 0 obj 122 endobj 256 0 obj << /Type /XObject /Subtype /Form /FormType 1 /PTEX.FileName (./pics/Logo-SSEbig.pdf) /PTEX.PageNumber 1 /PTEX.InfoDict 269 0 R /Matrix [1 0 0 1 0 0] /BBox [0 0 262 67] /Resources << /ProcSet [ /PDF ] /ExtGState << /R4 270 0 R >>>> /Length 271 0 R /Filter /FlateDecode >> stream xK,gv#zKð2Ol+s."B"=z__ ^G~+3RyP^zh>_{,_@"=^xCFίXW҆};> :w|>^)}@]_S:m]+xweswSyWI\l\l1wN! ݙRK5X4n/^͖&BV0F+<5<
vbH-'&o%w%~o)iw]{d[d-ޢOb֪n}ޱ^/lY\טd{
i7YJ|k][.:wFL&mX+W瘮`;kx'{b=1%^'["e&I;OJ akiJנe8I0RuAjAuQc
Ȓ5)Dd5Wiz$T#:w}3
n}ZM
ҡ%EP.֮~bwNzsч;7o~p5_c4M.uk%{71iv,4 C?
!
=jP0.C06Iwt&Sn݅˶.Ea16'kû&1kj:
I_'Xg+;-ejK:=5g,x}[/1)Rڨ8+ڬlh-rKhKmV(1aي5H6F?0}_T/&״َrZIN:t3k~b\B%?*EH`R7'5=l:j-Wk1ؚrh;Zp2cZvRzbwNzssT^ۙwb'y`fLjXIF;r^7M!],Mg^2v>a D1d˄&0kuU·!T%g
38{4]kX.e9Iuzi DژbV)݂8t= ijg]7mmߧ>VFW>bo풂")H
O'Vz7}ls[ tn6(z'-?/3Om{c$QdAk{BZ-aՇ6}>X-62;OYq0;3Qu%Y7ifleDaDѬ=L|?[;'mٌ}Ƶf)
;W}TbmjnIV3o<:jg\DMڶ0ab8W=cN77-n3)fW7>
X~b`6-|"Ed%BgYk{D6z[Lvy0Rnɬ1㢋-i2YFP