%PDF-1.4 5 0 obj << /S /GoTo /D (section.0.1) >> endobj 8 0 obj (Introduction) endobj 9 0 obj << /S /GoTo /D (section.0.2) >> endobj 12 0 obj (Emacs) endobj 13 0 obj << /S /GoTo /D (section.0.3) >> endobj 16 0 obj (Tcl/Tk Interface) endobj 17 0 obj << /S /GoTo /D (section.0.4) >> endobj 20 0 obj (Prover interaction) endobj 21 0 obj << /S /GoTo /D (section.0.5) >> endobj 24 0 obj (Generating Latex, HTML, and XML) endobj 25 0 obj << /S /GoTo /D (section.0.6) >> endobj 28 0 obj (PVS as a Back-end) endobj 29 0 obj << /S /GoTo /D (section.0.7) >> endobj 32 0 obj (PVS as a Front-end) endobj 33 0 obj << /S /GoTo /D (section.0.8) >> endobj 36 0 obj (Proof discovery and maintenance) endobj 37 0 obj << /S /GoTo /D (section.0.9) >> endobj 40 0 obj (Conclusion) endobj 41 0 obj << /S /GoTo /D (section*.1) >> endobj 44 0 obj (References) endobj 45 0 obj << /S /GoTo /D [46 0 R /Fit ] >> endobj 49 0 obj << /Length 2289 /Filter /FlateDecode >> stream xڭr8Б0x$xL%٬MdE[PxۍnP,簥*l4BO-̄R-Tɢ],J1rZޭ~z@Cd2S\1[6Gzm월fs5lX `f@BlE~83R8-mGȳ]YUtK-HSfI]akb#2fmX7eKd^ M%FDvl6A~j2J@j+͙q{bVA} a>nhKcV6ʟ^κ]rzKP8qQop.pM*Zث$N"J:Qtw]U>?e?цXKvPvUʼnܵ:sbiV|\Z7F :'$8Зs|D(^JSg^4,doJi+!mۏCPCQMHH5#v>zZXYt|aS37PM^sP@Smptq}[,ڲU~~!ZmMn~d.HBe^ _hpޣ!*~bAXբR_فs_kyW:C?즡N@!ŖByZFi9(TT`;}Y'a|U, 2IuB9rg4uΏU!O\h!ܖFhhqT汌VE;xkc4\7O#dPOdQE zdqFzLXECU`ߗ%TGpfpv12ZN.Jzr6$`~j tLl,N!fI9s3 $4p"`+hZGSzhײ+l jgdm>4 G}O;)U{z^ʺSUM2+%UP` x,C&_"[y]r!Cw0E$!q~Z@*8%aw?)Hb8ik!{R*EO#CU4%<'6I;0NK#ch;f^ ~&?xjX簘OY: Q ^~ж5ZWfmheߝ z}ö-)#ׇߢ2l]燞W}B/ę[(Z]ׅ!bV^X8 xAm[_Y_V>ސLp_?}I;xP:7j:\{Qg8$9U85,x=&<#<?Ҡ-tmwMLظtfNĔ^>*%qf|.iO[zi/j?4GFB}ĵ0_{r7MELr HotR$cq*M*Xw]X9N[SYq'`MtT \ m )@@*&|V#aRsd|p/*_r/^7$Tl8]N2