Undergraduate Topics in Computer Science Faron Moller Georg Struth Modelling Computing Systems Mathematics for Computer Science Undergraduate Topics in Computer Science UndergraduateTopicsinComputerScience(UTiCS)delivershigh-qualityinstructionalcontentforun- dergraduatesstudyinginallareasofcomputingandinformationscience.Fromcorefoundationaland theoreticalmaterialtofinal-yeartopicsandapplications,UTiCSbookstakeafresh,concise,andmod- ernapproachandareidealforself-studyorforaone-ortwo-semestercourse.Thetextsareallauthored byestablishedexpertsintheirfields,reviewedbyaninternationaladvisoryboard,andcontainnumer- ousexamplesandproblems.Manyincludefullyworkedsolutions. Forfurthervolumes: www.springer.com/series/7592 Faron Moller (cid:2) Georg Struth Modelling Computing Systems Mathematics for Computer Science FaronMoller GeorgStruth DepartmentofComputerScience Dept.ComputerScience SwanseaUniversity UniversityofSheffield Swansea,UK Sheffield,UK Serieseditor IanMackie Advisoryboard SamsonAbramsky,UniversityofOxford,Oxford,UK KarinBreitman,PontificalCatholicUniversityofRiodeJaneiro,RiodeJaneiro,Brazil ChrisHankin,ImperialCollegeLondon,London,UK DexterKozen,CornellUniversity,Ithaca,USA AndrewPitts,UniversityofCambridge,Cambridge,UK HanneRiisNielson,TechnicalUniversityofDenmark,KongensLyngby,Denmark StevenSkiena,StonyBrookUniversity,StonyBrook,USA IainStewart,UniversityofDurham,Durham,UK ISSN1863-7310 UndergraduateTopicsinComputerScience ISBN978-1-84800-321-7 ISBN978-1-84800-322-4(eBook) DOI10.1007/978-1-84800-322-4 SpringerLondonHeidelbergNewYorkDordrecht LibraryofCongressControlNumber:2013943907 ©Springer-VerlagLondon2013 Thisworkissubjecttocopyright.AllrightsarereservedbythePublisher,whetherthewholeorpartof thematerialisconcerned,specificallytherightsoftranslation,reprinting,reuseofillustrations,recitation, broadcasting,reproductiononmicrofilmsorinanyotherphysicalway,andtransmissionorinformation storageandretrieval,electronicadaptation,computersoftware,orbysimilarordissimilarmethodology nowknownorhereafterdeveloped.Exemptedfromthislegalreservationarebriefexcerptsinconnection withreviewsorscholarlyanalysisormaterialsuppliedspecificallyforthepurposeofbeingenteredand executedonacomputersystem,forexclusiveusebythepurchaserofthework.Duplicationofthispub- licationorpartsthereofispermittedonlyundertheprovisionsoftheCopyrightLawofthePublisher’s location,initscurrentversion,andpermissionforusemustalwaysbeobtainedfromSpringer.Permis- sionsforusemaybeobtainedthroughRightsLinkattheCopyrightClearanceCenter.Violationsareliable toprosecutionundertherespectiveCopyrightLaw. Theuseofgeneraldescriptivenames,registerednames,trademarks,servicemarks,etc.inthispublication doesnotimply,evenintheabsenceofaspecificstatement,thatsuchnamesareexemptfromtherelevant protectivelawsandregulationsandthereforefreeforgeneraluse. Whiletheadviceandinformationinthisbookarebelievedtobetrueandaccurateatthedateofpublica- tion,neithertheauthorsnortheeditorsnorthepublishercanacceptanylegalresponsibilityforanyerrors oromissionsthatmaybemade.Thepublishermakesnowarranty,expressorimplied,withrespecttothe materialcontainedherein. Printedonacid-freepaper SpringerispartofSpringerScience+BusinessMedia(www.springer.com) CONTENTS v Contents (cid:0)(cid:2)(cid:3)(cid:4)(cid:4)(cid:5)(cid:6) (cid:7)(cid:5)(cid:8)(cid:2)(cid:9)(cid:10)(cid:11)(cid:7) (cid:3)(cid:4)(cid:5) (cid:10)(cid:12)(cid:2)(cid:9)(cid:10)(cid:11)(cid:3)(cid:13) (cid:3)(cid:11)(cid:6) (cid:10)(cid:14)(cid:2)(cid:5)(cid:11) (cid:4)(cid:5)(cid:12)(cid:4)(cid:5)(cid:7)(cid:5)(cid:11)(cid:2) (cid:3)(cid:6)(cid:15)(cid:3)(cid:11)(cid:8)(cid:5)(cid:6) (cid:16)(cid:3)(cid:2)(cid:5)(cid:4)(cid:9)(cid:3)(cid:13)(cid:17) Preface xiii 0 Introduction 1 (cid:0)(cid:2)(cid:3) (cid:4)(cid:5)(cid:6)(cid:7)(cid:8)(cid:9)(cid:10)(cid:11)(cid:12)(cid:13)(cid:14)(cid:15)(cid:11)(cid:16)(cid:10)(cid:7)(cid:17)(cid:6)(cid:18)(cid:9)(cid:19)(cid:20)(cid:10)(cid:11) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:21) (cid:0)(cid:2)(cid:3)(cid:2)(cid:3) (cid:22)(cid:9)(cid:6)(cid:15)(cid:16)(cid:12)(cid:23)(cid:24)(cid:19)(cid:23)(cid:23)(cid:10)(cid:9)(cid:25)(cid:26)(cid:26)(cid:18)(cid:27)(cid:10)(cid:23)(cid:16) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:21) (cid:0)(cid:2)(cid:3)(cid:2)(cid:21) (cid:28)(cid:14)(cid:14)(cid:14)(cid:26)(cid:12)(cid:20)(cid:8)(cid:18)(cid:12)(cid:23) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:29) (cid:0)(cid:2)(cid:3)(cid:2)(cid:30) (cid:24)(cid:31)(cid:10)(cid:20)(cid:6)(cid:26)(cid:21) !(cid:6)(cid:27)(cid:18)(cid:12)(cid:16)(cid:31)(cid:10)(cid:20)(cid:6)(cid:8)(cid:15)"(cid:6)(cid:26)(cid:31)(cid:18)(cid:23)(cid:10) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:29) (cid:0)(cid:2)(cid:3)(cid:2)(cid:29) #(cid:12)(cid:23)(cid:27)(cid:12)(cid:23)(cid:25)(cid:7)$(cid:19)(cid:9)(cid:6)(cid:23)(cid:26)(cid:10)(cid:14)(cid:10)(cid:20)%(cid:18)(cid:26)(cid:10) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:0)(cid:2)(cid:3)(cid:2) &(cid:23)(cid:16)(cid:10)(cid:9)’(cid:10)(cid:23)(cid:16)(cid:18)(cid:19)(cid:7) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) ( (cid:0)(cid:2)(cid:3)(cid:2)( (cid:25)(cid:20)(cid:18)(cid:6)(cid:23)(cid:10) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) ) (cid:0)(cid:2)(cid:3)(cid:2)) *(cid:10)(cid:10)(cid:27)(cid:31)(cid:6)(cid:7)+(cid:14)(cid:26)(cid:31)(cid:20)(cid:12)(cid:10)(cid:27)(cid:10)(cid:20)’(cid:20)(cid:12)(cid:16)(cid:12)(cid:26)(cid:12)(cid:9) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) ) (cid:0)(cid:2)(cid:21) (cid:14)(cid:15)(cid:11)(cid:16)(cid:10)(cid:7),"(cid:12)(cid:27)(cid:10)(cid:9),(cid:25)$(cid:11)(cid:16)(cid:20)(cid:6)(cid:26)(cid:16)(cid:18)(cid:12)(cid:23)(cid:6)(cid:23)(cid:27)*(cid:12)(cid:16)(cid:6)(cid:16)(cid:18)(cid:12)(cid:23) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) - (cid:0)(cid:2)(cid:30) (cid:14)(cid:8)(cid:10)(cid:26)(cid:18).(cid:26)(cid:6)(cid:16)(cid:18)(cid:12)(cid:23),&(cid:7)(cid:8)(cid:9)(cid:10)(cid:7)(cid:10)(cid:23)(cid:16)(cid:6)(cid:16)(cid:18)(cid:12)(cid:23)(cid:6)(cid:23)(cid:27)/(cid:10)(cid:20)(cid:18).(cid:26)(cid:6)(cid:16)(cid:18)(cid:12)(cid:23) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:3)(cid:30) Part I: Mathematics for Computer Science 15 1 Propositional Logic 17 (cid:3)(cid:2)(cid:3) ’(cid:20)(cid:12)(cid:8)(cid:12)(cid:11)(cid:18)(cid:16)(cid:18)(cid:12)(cid:23)(cid:11)(cid:6)(cid:23)(cid:27)0(cid:10)(cid:27)(cid:19)(cid:26)(cid:16)(cid:18)(cid:12)(cid:23)(cid:11) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:3)1 (cid:3)(cid:2)(cid:21) (cid:24)(cid:31)(cid:10)#(cid:6)(cid:23)2(cid:19)(cid:6)2(cid:10)(cid:12)(cid:13)’(cid:20)(cid:12)(cid:8)(cid:12)(cid:11)(cid:18)(cid:16)(cid:18)(cid:12)(cid:23)(cid:6)(cid:9)#(cid:12)2(cid:18)(cid:26) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:21)(cid:3) (cid:3)(cid:2)(cid:21)(cid:2)(cid:3) ’(cid:20)(cid:12)(cid:8)(cid:12)(cid:11)(cid:18)(cid:16)(cid:18)(cid:12)(cid:23)(cid:6)(cid:9)/(cid:6)(cid:20)(cid:18)(cid:6)$(cid:9)(cid:10)(cid:11) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:21)(cid:21) (cid:3)(cid:2)(cid:21)(cid:2)(cid:21) *(cid:10)2(cid:6)(cid:16)(cid:18)(cid:12)(cid:23) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:21)(cid:21) (cid:3)(cid:2)(cid:21)(cid:2)(cid:30) 0(cid:18)(cid:11)3(cid:19)(cid:23)(cid:26)(cid:16)(cid:18)(cid:12)(cid:23) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:21)(cid:30) (cid:3)(cid:2)(cid:21)(cid:2)(cid:29) (cid:22)(cid:12)(cid:23)3(cid:19)(cid:23)(cid:26)(cid:16)(cid:18)(cid:12)(cid:23)(cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:21) (cid:3)(cid:2)(cid:21)(cid:2) &(cid:7)(cid:8)(cid:9)(cid:18)(cid:26)(cid:6)(cid:16)(cid:18)(cid:12)(cid:23) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:21) (cid:3)(cid:2)(cid:21)(cid:2)( (cid:4)4(cid:19)(cid:18)%(cid:6)(cid:9)(cid:10)(cid:23)(cid:26)(cid:10) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:21)) (cid:3)(cid:2)(cid:21)(cid:2)) (cid:24)(cid:31)(cid:10)(cid:14)(cid:15)(cid:23)(cid:16)(cid:6)(cid:5)(cid:12)(cid:13)’(cid:20)(cid:12)(cid:8)(cid:12)(cid:11)(cid:18)(cid:16)(cid:18)(cid:12)(cid:23)(cid:6)(cid:9)#(cid:12)2(cid:18)(cid:26) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:21)) (cid:3)(cid:2)(cid:21)(cid:2)1 ’(cid:6)(cid:20)(cid:10)(cid:23)(cid:16)(cid:31)(cid:10)(cid:11)(cid:10)(cid:11) (cid:6)(cid:23)(cid:27)’(cid:20)(cid:10)(cid:26)(cid:10)(cid:27)(cid:10)(cid:23)(cid:26)(cid:10)(cid:11) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:21)1 (cid:3)(cid:2)(cid:21)(cid:2)- (cid:14)(cid:15)(cid:23)(cid:16)(cid:6)(cid:5)(cid:24)(cid:20)(cid:10)(cid:10)(cid:11) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:30)(cid:0) (cid:3)(cid:2)(cid:30) "(cid:12)(cid:27)(cid:10)(cid:9)(cid:9)(cid:18)(cid:23)25(cid:18)(cid:16)(cid:31)’(cid:20)(cid:12)(cid:8)(cid:12)(cid:11)(cid:18)(cid:16)(cid:18)(cid:12)(cid:23)(cid:6)(cid:9)#(cid:12)2(cid:18)(cid:26) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:30)(cid:21) (cid:3)(cid:2)(cid:29) (cid:25)(cid:7)$(cid:18)2(cid:19)(cid:18)(cid:16)(cid:18)(cid:10)(cid:11)(cid:12)(cid:13)*(cid:6)(cid:16)(cid:19)(cid:20)(cid:6)(cid:9)#(cid:6)(cid:23)2(cid:19)(cid:6)2(cid:10)(cid:11) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:30) (cid:3)(cid:2) (cid:24)(cid:20)(cid:19)(cid:16)(cid:31)(cid:24)(cid:6)$(cid:9)(cid:10)(cid:11) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:29)(cid:0) (cid:3)(cid:2)( (cid:4)4(cid:19)(cid:18)%(cid:6)(cid:9)(cid:10)(cid:23)(cid:26)(cid:10)(cid:11)(cid:6)(cid:23)(cid:27)/(cid:6)(cid:9)(cid:18)(cid:27)(cid:25)(cid:20)2(cid:19)(cid:7)(cid:10)(cid:23)(cid:16)(cid:11) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:29) (cid:0) (cid:3)(cid:2)) (cid:25)(cid:9)2(cid:10)$(cid:20)(cid:6)(cid:18)(cid:26)#(cid:6)5(cid:11)(cid:13)(cid:12)(cid:20)#(cid:12)2(cid:18)(cid:26)(cid:6)(cid:9)(cid:4)4(cid:19)(cid:18)%(cid:6)(cid:9)(cid:10)(cid:23)(cid:26)(cid:10)(cid:11) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:29)) (cid:3)(cid:2)1 (cid:25)(cid:27)(cid:27)(cid:18)(cid:16)(cid:18)(cid:12)(cid:23)(cid:6)(cid:9)(cid:4)(cid:5)(cid:10)(cid:20)(cid:26)(cid:18)(cid:11)(cid:10)(cid:11) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:0) 2 Sets 57 (cid:21)(cid:2)(cid:3) (cid:14)(cid:10)(cid:16)*(cid:12)(cid:16)(cid:6)(cid:16)(cid:18)(cid:12)(cid:23) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) ) (cid:21)(cid:2)(cid:21) "(cid:10)(cid:7)$(cid:10)(cid:20)(cid:11)(cid:31)(cid:18)(cid:8),(cid:4)4(cid:19)(cid:6)(cid:9)(cid:18)(cid:16)(cid:15)(cid:6)(cid:23)(cid:27)&(cid:23)(cid:26)(cid:9)(cid:19)(cid:11)(cid:18)(cid:12)(cid:23) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) - (cid:21)(cid:2)(cid:30) (cid:14)(cid:10)(cid:16)(cid:11)(cid:6)(cid:23)(cid:27)’(cid:20)(cid:12)(cid:8)(cid:10)(cid:20)(cid:16)(cid:18)(cid:10)(cid:11)(cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) ((cid:30) (cid:21)(cid:2)(cid:30)(cid:2)(cid:3) !(cid:19)(cid:11)(cid:11)(cid:10)(cid:9)(cid:9)6(cid:11)’(cid:6)(cid:20)(cid:6)(cid:27)(cid:12)(cid:5)(cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) ((cid:29) vi CONTENTS (cid:0)(cid:2)(cid:3) (cid:4)(cid:5)(cid:6)(cid:7)(cid:8)(cid:9)(cid:10)(cid:11)(cid:12)(cid:13)(cid:11)(cid:12)(cid:14)(cid:6)(cid:9)(cid:13) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:15)(cid:16) (cid:0)(cid:2)(cid:3)(cid:2)(cid:17) (cid:18)(cid:12)(cid:10)(cid:11)(cid:12) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:15)(cid:16) (cid:0)(cid:2)(cid:3)(cid:2)(cid:0) (cid:19)(cid:12)(cid:9)(cid:6)(cid:7)(cid:13)(cid:6)(cid:20)(cid:9)(cid:10)(cid:11)(cid:12) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:15)(cid:15) (cid:0)(cid:2)(cid:3)(cid:2)(cid:21) (cid:22)(cid:10)(cid:23)(cid:6)(cid:7)(cid:6)(cid:12)(cid:20)(cid:6) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:15)(cid:24) (cid:0)(cid:2)(cid:3)(cid:2)(cid:3) (cid:25)(cid:11)(cid:26)(cid:5)(cid:27)(cid:6)(cid:26)(cid:6)(cid:12)(cid:9) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:15)(cid:28) (cid:0)(cid:2)(cid:3)(cid:2)(cid:16) (cid:29)(cid:11)(cid:30)(cid:6)(cid:7)(cid:13)(cid:6)(cid:9)(cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:15)(cid:31) (cid:0) (cid:0)(cid:2)(cid:3)(cid:2)(cid:15) (cid:6)(cid:12)(cid:6)(cid:7)(cid:8)(cid:27)(cid:10)(cid:13)(cid:6)!(cid:18)(cid:12)(cid:10)(cid:11)(cid:12)(cid:8)(cid:12)!(cid:19)(cid:12)(cid:9)(cid:6)(cid:7)(cid:13)(cid:6)(cid:20)(cid:9)(cid:10)(cid:11)(cid:12)(cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:24)(cid:0) (cid:0)(cid:2)(cid:16) (cid:4)(cid:7)!(cid:6)(cid:7)(cid:6)!(cid:29)(cid:8)(cid:10)(cid:7)(cid:13)(cid:8)(cid:12)!(cid:25)(cid:8)(cid:7)(cid:9)(cid:6)(cid:13)(cid:10)(cid:8)(cid:12)(cid:29)(cid:7)(cid:11)!"(cid:20)(cid:9)(cid:13) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:24)(cid:21) (cid:0)(cid:2)(cid:15) #(cid:11)!(cid:6)(cid:27)(cid:27)(cid:10)(cid:12)$(cid:30)(cid:10)(cid:9)%(cid:14)(cid:6)(cid:9)(cid:13) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:24)(cid:15) (cid:0) (cid:0)(cid:2)(cid:24) &(cid:27)$(cid:6)’(cid:7)(cid:8)(cid:10)(cid:20)((cid:8)(cid:30)(cid:13))(cid:11)(cid:7)(cid:14)(cid:6)(cid:9)(cid:19)!(cid:6)(cid:12)(cid:9)(cid:10)(cid:9)(cid:10)(cid:6)(cid:13) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:24)(cid:31) (cid:0) (cid:0)(cid:2)(cid:28) ((cid:11)$(cid:10)(cid:20)(cid:8)(cid:27)*+"(cid:10),(cid:8)(cid:27)(cid:6)(cid:12)(cid:20)(cid:6)(cid:13),(cid:6)(cid:7)(cid:13)"(cid:13)(cid:14)(cid:6)(cid:9)(cid:19)!(cid:6)(cid:12)(cid:9)(cid:10)(cid:9)(cid:10)(cid:6)(cid:13) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:28)(cid:17) (cid:0)(cid:2)(cid:31) &!!(cid:10)(cid:9)(cid:10)(cid:11)(cid:12)(cid:8)(cid:27)*-(cid:6)(cid:7)(cid:20)(cid:10)(cid:13)(cid:6)(cid:13) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:28)(cid:21) 3 Boolean Algebras and Circuits 87 (cid:0) (cid:21)(cid:2)(cid:17) .(cid:11)(cid:11)(cid:27)(cid:6)(cid:8)(cid:12)&(cid:27)$(cid:6)’(cid:7)(cid:8)(cid:13) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:28)(cid:24) (cid:21)(cid:2)(cid:0) (cid:22)(cid:6)(cid:7)(cid:10),(cid:10)(cid:12)$(cid:19)!(cid:6)(cid:12)(cid:9)(cid:10)(cid:9)(cid:10)(cid:6)(cid:13)(cid:10)(cid:12).(cid:11)(cid:11)(cid:27)(cid:6)(cid:8)(cid:12)&(cid:27)$(cid:6)’(cid:7)(cid:8)(cid:13) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:31)/ (cid:21)(cid:2)(cid:21) 0%(cid:6)(cid:22)"(cid:8)(cid:27)(cid:10)(cid:9)1(cid:29)(cid:7)(cid:10)(cid:12)(cid:20)(cid:10)(cid:5)(cid:27)(cid:6) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:31)(cid:21) (cid:21)(cid:2)(cid:3) ((cid:11)$(cid:10)(cid:20) (cid:8)(cid:9)(cid:6)(cid:13)(cid:8)(cid:12)!(cid:22)(cid:10)$(cid:10)(cid:9)(cid:8)(cid:27)(cid:25)(cid:10)(cid:7)(cid:20)"(cid:10)(cid:9)(cid:13) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:31)(cid:16) (cid:21)(cid:2)(cid:16) #(cid:8)2(cid:10)(cid:12)$(cid:25)(cid:11)(cid:26)(cid:5)"(cid:9)(cid:6)(cid:7)(cid:13)&!! (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:17)// (cid:21)(cid:2)(cid:16)(cid:2)(cid:17) .(cid:10)(cid:12)(cid:8)(cid:7)13"(cid:26)’(cid:6)(cid:7)(cid:13) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:17)// (cid:21)(cid:2)(cid:16)(cid:2)(cid:0) &!!(cid:10)(cid:12)$.(cid:10)(cid:12)(cid:8)(cid:7)13"(cid:26)’(cid:6)(cid:7)(cid:13) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:17)/(cid:0) (cid:21)(cid:2)(cid:16)(cid:2)(cid:21) ."(cid:10)(cid:27)!(cid:10)(cid:12)$4(cid:8)(cid:27))&!!(cid:6)(cid:7)(cid:13)(cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:17)/(cid:21) (cid:21)(cid:2)(cid:16)(cid:2)(cid:3) ."(cid:10)(cid:27)!(cid:10)(cid:12)$5"(cid:27)(cid:27)&!!(cid:6)(cid:7)(cid:13) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:17)/(cid:3) (cid:21)(cid:2)(cid:16)(cid:2)(cid:16) (cid:29)"(cid:9)(cid:9)(cid:10)(cid:12)$(cid:19)(cid:9)&(cid:27)(cid:27)0(cid:11)$(cid:6)(cid:9)%(cid:6)(cid:7) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:17)/(cid:16) (cid:21)(cid:2)(cid:15) &!!(cid:10)(cid:9)(cid:10)(cid:11)(cid:12)(cid:8)(cid:27)*-(cid:6)(cid:7)(cid:20)(cid:10)(cid:13)(cid:6)(cid:13) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:17)/(cid:15) 4 Predicate Logic 109 (cid:3)(cid:2)(cid:17) (cid:29)(cid:7)(cid:6)!(cid:10)(cid:20)(cid:8)(cid:9)(cid:6)(cid:13)(cid:8)(cid:12)!5(cid:7)(cid:6)(cid:6)6(cid:8)(cid:7)(cid:10)(cid:8)’(cid:27)(cid:6)(cid:13) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:17)/(cid:31) (cid:3)(cid:2)(cid:0) 7"(cid:8)(cid:12)(cid:9)(cid:10)8(cid:6)(cid:7)(cid:13)(cid:8)(cid:12)!.(cid:11)"(cid:12)!6(cid:8)(cid:7)(cid:10)(cid:8)’(cid:27)(cid:6)(cid:13) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:17)(cid:17)(cid:17) (cid:3)(cid:2)(cid:0)(cid:2)(cid:17) (cid:18)(cid:12)(cid:10),(cid:6)(cid:7)(cid:13)(cid:8)(cid:27)7"(cid:8)(cid:12)(cid:9)(cid:10)8(cid:20)(cid:8)(cid:9)(cid:10)(cid:11)(cid:12) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:17)(cid:17)(cid:21) (cid:3)(cid:2)(cid:0)(cid:2)(cid:0) *-(cid:10)(cid:13)(cid:9)(cid:6)(cid:12)(cid:9)(cid:10)(cid:8)(cid:27)7"(cid:8)(cid:12)(cid:9)(cid:10)8(cid:20)(cid:8)(cid:9)(cid:10)(cid:11)(cid:12) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:17)(cid:17)(cid:16) (cid:3)(cid:2)(cid:0)(cid:2)(cid:21) .(cid:11)"(cid:12)!(cid:6)!7"(cid:8)(cid:12)(cid:9)(cid:10)8(cid:20)(cid:8)(cid:9)(cid:10)(cid:11)(cid:12)(cid:13)(cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:17)(cid:17)(cid:28) (cid:3)(cid:2)(cid:21) 9"(cid:27)(cid:6)(cid:13))(cid:11)(cid:7)7"(cid:8)(cid:12)(cid:9)(cid:10)8(cid:20)(cid:8)(cid:9)(cid:10)(cid:11)(cid:12) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:17)(cid:0)/ (cid:3)(cid:2)(cid:3) #(cid:11)!(cid:6)(cid:27)(cid:27)(cid:10)(cid:12)$(cid:10)(cid:12)(cid:29)(cid:7)(cid:6)!(cid:10)(cid:20)(cid:8)(cid:9)(cid:6)((cid:11)$(cid:10)(cid:20) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:17)(cid:0)(cid:3) (cid:3)(cid:2)(cid:16) &!!(cid:10)(cid:9)(cid:10)(cid:11)(cid:12)(cid:8)(cid:27)*-(cid:6)(cid:7)(cid:20)(cid:10)(cid:13)(cid:6)(cid:13) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:17)(cid:0)(cid:24) 5 Proof Strategies 131 (cid:0) (cid:16)(cid:2)(cid:17) &5(cid:10)(cid:7)(cid:13)(cid:9)*-(cid:8)(cid:26)(cid:5)(cid:27)(cid:6) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:17)(cid:21)(cid:0) (cid:16)(cid:2)(cid:0) (cid:29)(cid:7)(cid:11)(cid:11))(cid:14)(cid:9)(cid:7)(cid:8)(cid:9)(cid:6)$(cid:10)(cid:6)(cid:13))(cid:11)(cid:7)(cid:19)(cid:26)(cid:5)(cid:27)(cid:10)(cid:20)(cid:8)(cid:9)(cid:10)(cid:11)(cid:12) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:17)(cid:21)(cid:3) (cid:16)(cid:2)(cid:21) (cid:29)(cid:7)(cid:11)(cid:11))(cid:14)(cid:9)(cid:7)(cid:8)(cid:9)(cid:6)$(cid:10)(cid:6)(cid:13))(cid:11)(cid:7)3(cid:6)$(cid:8)(cid:9)(cid:10)(cid:11)(cid:12) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:17)(cid:21)(cid:28) (cid:16)(cid:2)(cid:3) (cid:29)(cid:7)(cid:11)(cid:11))(cid:14)(cid:9)(cid:7)(cid:8)(cid:9)(cid:6)$(cid:10)(cid:6)(cid:13))(cid:11)(cid:7)(cid:25)(cid:11)(cid:12):"(cid:12)(cid:20)(cid:9)(cid:10)(cid:11)(cid:12)(cid:8)(cid:12)!*+"(cid:10),(cid:8)(cid:27)(cid:6)(cid:12)(cid:20)(cid:6) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:17)(cid:3)(cid:0) (cid:16)(cid:2)(cid:16) (cid:29)(cid:7)(cid:11)(cid:11))(cid:14)(cid:9)(cid:7)(cid:8)(cid:9)(cid:6)$(cid:10)(cid:6)(cid:13))(cid:11)(cid:7)(cid:22)(cid:10)(cid:13):"(cid:12)(cid:20)(cid:9)(cid:10)(cid:11)(cid:12) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:17)(cid:3)(cid:3) (cid:16)(cid:2)(cid:15) (cid:29)(cid:7)(cid:11)(cid:11))(cid:14)(cid:9)(cid:7)(cid:8)(cid:9)(cid:6)$(cid:10)(cid:6)(cid:13))(cid:11)(cid:7)7"(cid:8)(cid:12)(cid:9)(cid:10)8(cid:6)(cid:7)(cid:13) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:17)(cid:3)(cid:24) (cid:16)(cid:2)(cid:15)(cid:2)(cid:17) (cid:18)(cid:12)(cid:10),(cid:6)(cid:7)(cid:13)(cid:8)(cid:27)7"(cid:8)(cid:12)(cid:9)(cid:10)8(cid:20)(cid:8)(cid:9)(cid:10)(cid:11)(cid:12) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:17)(cid:3)(cid:24) CONTENTS vii (cid:0)(cid:2)(cid:3)(cid:2)(cid:4) (cid:5)(cid:6)(cid:7)(cid:8)(cid:9)(cid:10)(cid:11)(cid:9)(cid:7)(cid:12)(cid:13)(cid:14)(cid:15)(cid:12)(cid:11)(cid:9)(cid:7)(cid:16)(cid:17)(cid:12)(cid:9)(cid:7)(cid:18)(cid:11) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:19)(cid:20)(cid:21) (cid:0)(cid:2)(cid:3)(cid:2)(cid:22) (cid:23)(cid:11)(cid:7)(cid:24)(cid:15)(cid:10)(cid:11)(cid:10)(cid:8)(cid:8) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:19)(cid:0)(cid:4) (cid:0)(cid:2)(cid:25) (cid:26)(cid:27)(cid:27)(cid:7)(cid:9)(cid:7)(cid:18)(cid:11)(cid:12)(cid:13)(cid:5)(cid:6)(cid:10)(cid:28)(cid:17)(cid:7)(cid:8)(cid:10)(cid:8) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:19)(cid:0)(cid:22) 6 Functions 155 (cid:3)(cid:2)(cid:19) (cid:29)(cid:12)(cid:8)(cid:7)(cid:17)(cid:30)(cid:10)(cid:16)(cid:11)(cid:7)(cid:9)(cid:7)(cid:18)(cid:11)(cid:8) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:19)(cid:0)(cid:0) (cid:3)(cid:2)(cid:4) (cid:31)(cid:11)(cid:10) !(cid:18) (cid:31)(cid:11)(cid:10)(cid:12)(cid:11)(cid:27)(cid:31)(cid:11)(cid:9)(cid:18)"(cid:15)(cid:11)(cid:17)(cid:9)(cid:7)(cid:18)(cid:11)(cid:8) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:19)(cid:3)# (cid:3)(cid:2)(cid:22) $(cid:18)%&(cid:18)(cid:8)(cid:7)(cid:11)’"(cid:15)(cid:11)(cid:17)(cid:9)(cid:7)(cid:18)(cid:11)(cid:8) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:19)(cid:3)(cid:22) (cid:0) (cid:3)(cid:2)(cid:20) $(cid:18)%&(cid:12)(cid:28)(cid:7)(cid:11)’(cid:9)((cid:10))(cid:7)*(cid:10)(cid:8)(cid:18)+)(cid:10)(cid:9)(cid:8) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:19)(cid:3)(cid:3) (cid:0) (cid:3)(cid:2)(cid:0) !((cid:10),(cid:11)(cid:12)(cid:8)(cid:9)(cid:10)(cid:28) !(cid:12)(cid:28)(cid:8)-(cid:7)!((cid:10)(cid:18)(cid:28)(cid:10)% (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:19)(cid:25)(cid:22) (cid:3)(cid:2)(cid:3) (cid:26)(cid:27)(cid:27)(cid:7)(cid:9)(cid:7)(cid:18)(cid:11)(cid:12)(cid:13)(cid:5)(cid:6)(cid:10)(cid:28)(cid:17)(cid:7)(cid:8)(cid:10)(cid:8) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:19)(cid:25)(cid:3) 7 Relations 179 (cid:25)(cid:2)(cid:19) (cid:29)(cid:12)(cid:8)(cid:7)(cid:17)(cid:30)(cid:10)(cid:16)(cid:11)(cid:7)(cid:9)(cid:7)(cid:18)(cid:11)(cid:8) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:19)(cid:25)(cid:21) (cid:25)(cid:2)(cid:4) (cid:29)(cid:7)(cid:11)(cid:12)(cid:28)./(cid:10)(cid:13)(cid:12)(cid:9)(cid:7)(cid:18)(cid:11)(cid:8) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:19)0(cid:19) (cid:25)(cid:2)(cid:4)(cid:2)(cid:19) "(cid:15)(cid:11)(cid:17)(cid:9)(cid:7)(cid:18)(cid:11)(cid:8)(cid:12)(cid:8)(cid:29)(cid:7)(cid:11)(cid:12)(cid:28)./(cid:10)(cid:13)(cid:12)(cid:9)(cid:7)(cid:18)(cid:11)(cid:8)(cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:19)0(cid:0) (cid:25)(cid:2)(cid:22) (cid:31)&(cid:10)(cid:28)(cid:12)(cid:9)(cid:7)(cid:18)(cid:11)(cid:8)(cid:18)(cid:11)(cid:29)(cid:7)(cid:11)(cid:12)(cid:28)./(cid:10)(cid:13)(cid:12)(cid:9)(cid:7)(cid:18)(cid:11)(cid:8) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:19)0(cid:3) (cid:25)(cid:2)(cid:22)(cid:2)(cid:19) (cid:29)(cid:18)(cid:18)(cid:13)(cid:10)(cid:12)(cid:11)(cid:31)&(cid:10)(cid:28)(cid:12)(cid:9)(cid:7)(cid:18)(cid:11)(cid:8) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:19)0(cid:3) (cid:25)(cid:2)(cid:22)(cid:2)(cid:4) 1(cid:11)2(cid:10)(cid:28)(cid:9)(cid:7)(cid:11)’/(cid:10)(cid:13)(cid:12)(cid:9)(cid:7)(cid:18)(cid:11)(cid:8) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:19)0(cid:25) (cid:25)(cid:2)(cid:22)(cid:2)(cid:22) $(cid:18)%&(cid:18)(cid:8)(cid:7)(cid:11)’/(cid:10)(cid:13)(cid:12)(cid:9)(cid:7)(cid:18)(cid:11)(cid:8)(cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:19)00 (cid:25)(cid:2)(cid:22)(cid:2)(cid:20) !((cid:10)(cid:30)(cid:18)%(cid:12)(cid:7)(cid:11)(cid:12)(cid:11)(cid:27)/(cid:12)(cid:11)’(cid:10)(cid:18)+(cid:12)/(cid:10)(cid:13)(cid:12)(cid:9)(cid:7)(cid:18)(cid:11) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:19)0(cid:21) (cid:25)(cid:2)(cid:20) 3(cid:28)(cid:18)&(cid:10)(cid:28)(cid:9)(cid:7)(cid:10)(cid:8)(cid:18)+(cid:29)(cid:7)(cid:11)(cid:12)(cid:28)./(cid:10)(cid:13)(cid:12)(cid:9)(cid:7)(cid:18)(cid:11)(cid:8) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:19)(cid:21)# (cid:25)(cid:2)(cid:20)(cid:2)(cid:19) /(cid:10)4(cid:10)(cid:6)(cid:7)2(cid:10)(cid:12)(cid:11)(cid:27)1(cid:28)(cid:28)(cid:10)4(cid:10)(cid:6)(cid:7)2(cid:10)/(cid:10)(cid:13)(cid:12)(cid:9)(cid:7)(cid:18)(cid:11)(cid:8) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:19)(cid:21)# (cid:25)(cid:2)(cid:20)(cid:2)(cid:4) ).%%(cid:10)(cid:9)(cid:28)(cid:7)(cid:17)(cid:12)(cid:11)(cid:27)(cid:26)(cid:11)(cid:9)(cid:7)(cid:8).%%(cid:10)(cid:9)(cid:28)(cid:7)(cid:17)/(cid:10)(cid:13)(cid:12)(cid:9)(cid:7)(cid:18)(cid:11)(cid:8) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:19)(cid:21)(cid:19) (cid:25)(cid:2)(cid:20)(cid:2)(cid:22) !(cid:28)(cid:12)(cid:11)(cid:8)(cid:7)(cid:9)(cid:7)2(cid:10)/(cid:10)(cid:13)(cid:12)(cid:9)(cid:7)(cid:18)(cid:11)(cid:8) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:19)(cid:21)(cid:19) (cid:25)(cid:2)(cid:20)(cid:2)(cid:20) (cid:31)(cid:28)(cid:27)(cid:10)(cid:28)(cid:7)(cid:11)’(cid:8)/(cid:10)(cid:13)(cid:12)(cid:9)(cid:7)(cid:18)(cid:11)(cid:8) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:19)(cid:21)(cid:4) (cid:25)(cid:2)(cid:20)(cid:2)(cid:0) (cid:5)(cid:24)(cid:15)(cid:7)2(cid:12)(cid:13)(cid:10)(cid:11)(cid:17)(cid:10)/(cid:10)(cid:13)(cid:12)(cid:9)(cid:7)(cid:18)(cid:11)(cid:8) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:19)(cid:21)(cid:22) (cid:25)(cid:2)(cid:20)(cid:2)(cid:3) (cid:5)(cid:24)(cid:15)(cid:7)2(cid:12)(cid:13)(cid:10)(cid:11)(cid:17)(cid:10)$(cid:13)(cid:12)(cid:8)(cid:8)(cid:10)(cid:8)(cid:12)(cid:11)(cid:27)3(cid:12)(cid:28)(cid:9)(cid:7)(cid:9)(cid:7)(cid:18)(cid:11)(cid:8) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:19)(cid:21)(cid:0) (cid:25)(cid:2)(cid:0) (cid:26)(cid:27)(cid:27)(cid:7)(cid:9)(cid:7)(cid:18)(cid:11)(cid:12)(cid:13)(cid:5)(cid:6)(cid:10)(cid:28)(cid:17)(cid:7)(cid:8)(cid:10)(cid:8) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:19)(cid:21)(cid:25) 8 Inductive and Recursive Definitions 201 0(cid:2)(cid:19) 1(cid:11)(cid:27)(cid:15)(cid:17)(cid:9)(cid:7)2(cid:10)(cid:13). (cid:30)(cid:10)(cid:16)(cid:11)(cid:10)(cid:27))(cid:10)(cid:9)(cid:8) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:4)#(cid:19) 0(cid:2)(cid:4) 1(cid:11)(cid:27)(cid:15)(cid:17)(cid:9)(cid:7)2(cid:10)(cid:13). (cid:30)(cid:10)(cid:16)(cid:11)(cid:10)(cid:27)).(cid:11)(cid:9)(cid:12)(cid:17)(cid:9)(cid:7)(cid:17))(cid:10)(cid:9)(cid:8) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:4)#(cid:0) 0(cid:2)(cid:22) (cid:29)(cid:12)(cid:17)-(cid:15)(cid:8) 5(cid:12)(cid:15)(cid:28)"(cid:18)(cid:28)% (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:4)#(cid:25) 0(cid:2)(cid:20) 1(cid:11)(cid:27)(cid:15)(cid:17)(cid:9)(cid:7)2(cid:10)(cid:13). (cid:30)(cid:10)(cid:16)(cid:11)(cid:10)(cid:27)(cid:30)(cid:12)(cid:9)(cid:12)!.&(cid:10)(cid:8)(cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:4)(cid:19)# 0(cid:2)(cid:0) 1(cid:11)(cid:27)(cid:15)(cid:17)(cid:9)(cid:7)2(cid:10)(cid:13). (cid:30)(cid:10)(cid:16)(cid:11)(cid:10)(cid:27)"(cid:15)(cid:11)(cid:17)(cid:9)(cid:7)(cid:18)(cid:11)(cid:8) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:4)(cid:19)(cid:4) 0(cid:2)(cid:3) /(cid:10)(cid:17)(cid:15)(cid:28)(cid:8)(cid:7)2(cid:10)"(cid:15)(cid:11)(cid:17)(cid:9)(cid:7)(cid:18)(cid:11)(cid:8) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:4)(cid:19)(cid:3) 0(cid:2)(cid:25) /(cid:10)(cid:17)(cid:15)(cid:28)(cid:8)(cid:7)2(cid:10)3(cid:28)(cid:18)(cid:17)(cid:10)(cid:27)(cid:15)(cid:28)(cid:10)(cid:8)(cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:4)(cid:19)0 0(cid:2)0 (cid:26)(cid:27)(cid:27)(cid:7)(cid:9)(cid:7)(cid:18)(cid:11)(cid:12)(cid:13)(cid:5)(cid:6)(cid:10)(cid:28)(cid:17)(cid:7)(cid:8)(cid:10)(cid:8) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:4)(cid:4)# 9 Proofs by Induction 223 (cid:21)(cid:2)(cid:19) $(cid:18)(cid:11)2(cid:7)(cid:11)(cid:17)(cid:7)(cid:11)’6(cid:15)(cid:9)1(cid:11)(cid:17)(cid:18)(cid:11)(cid:17)(cid:13)(cid:15)(cid:8)(cid:7)2(cid:10)(cid:5)2(cid:7)(cid:27)(cid:10)(cid:11)(cid:17)(cid:10) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:4)(cid:4)(cid:22) (cid:21)(cid:2)(cid:4) (cid:26)3(cid:28)(cid:7)%(cid:12)(cid:28).)(cid:17)((cid:18)(cid:18)(cid:13)1(cid:11)(cid:27)(cid:15)(cid:17)(cid:9)(cid:7)(cid:18)(cid:11)(cid:26)(cid:28)’(cid:15)%(cid:10)(cid:11)(cid:9)(cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:4)(cid:4)(cid:25) (cid:21)(cid:2)(cid:22) !((cid:10)1(cid:11)(cid:27)(cid:15)(cid:17)(cid:9)(cid:7)(cid:18)(cid:11)(cid:26)(cid:28)’(cid:15)%(cid:10)(cid:11)(cid:9) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:4)(cid:4)0 viii CONTENTS (cid:0)(cid:2)(cid:3) (cid:4)(cid:5)(cid:6)(cid:7)(cid:8)(cid:9)(cid:10)(cid:8)(cid:11)(cid:12)(cid:13)(cid:5)(cid:14)(cid:7)(cid:8) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:15)(cid:16)(cid:3) (cid:0)(cid:2)(cid:17) (cid:10)(cid:8)(cid:11)(cid:12)(cid:13)(cid:5)(cid:14)(cid:7)(cid:8)(cid:18)(cid:6)(cid:7)(cid:7)(cid:19)(cid:20)(cid:19)(cid:6)(cid:7)(cid:21)(cid:10)(cid:8)(cid:11)(cid:12)(cid:13)(cid:5)(cid:14)(cid:22)(cid:23)(cid:24)(cid:23)(cid:25)(cid:8)(cid:14)(cid:5)(cid:14)(cid:7)(cid:8)(cid:20) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:15)(cid:16)(cid:17) (cid:0) (cid:0)(cid:2)(cid:26) (cid:27)(cid:12)(cid:8)(cid:28)(cid:14)(cid:5)(cid:29)(cid:27)(cid:14)(cid:30)(cid:7)(cid:8)(cid:31)(cid:13)(cid:13)(cid:14) (cid:12)(cid:21)(cid:30)(cid:23)(cid:6)(cid:20) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:15)(cid:16)! (cid:0)(cid:2)(cid:26)(cid:2)" #(cid:27)(cid:14)(cid:30)(cid:7)(cid:8)(cid:31)(cid:13)(cid:13)(cid:14) (cid:12)(cid:21)(cid:30)(cid:23)(cid:6)$(cid:23)(cid:20)(cid:5) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:15)(cid:16)! (cid:0)(cid:2)(cid:26)(cid:2)(cid:15) #%(cid:31)(cid:6)(cid:6)(cid:7)&&(cid:23)(cid:31)(cid:8)(cid:18)(cid:31)(cid:6)(cid:31)(cid:11)(cid:7)’ (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:15)(cid:16)(cid:0) (cid:0)(cid:2)(cid:26)(cid:2)(cid:16) (cid:27)(cid:14)(cid:30)(cid:7)(cid:8)(cid:31)(cid:13)(cid:13)(cid:14)(cid:24)(cid:23)(cid:13)(cid:7)(cid:21)((cid:7)(cid:20)(cid:14)(cid:5)(cid:14)(cid:7)(cid:8)(cid:20) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:15)(cid:3)) (cid:0)(cid:2)! *(cid:29)(cid:23)(cid:8)(cid:10)(cid:8)(cid:11)(cid:12)(cid:13)(cid:5)(cid:14)(cid:7)(cid:8)(cid:20)+(cid:7)*(cid:6)(cid:7)(cid:8)(cid:9) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:15)(cid:3)" (cid:0)(cid:2), -’(cid:31)(cid:21)(&(cid:23)(cid:20)(cid:7)(cid:19)(cid:10)(cid:8)(cid:11)(cid:12)(cid:13)(cid:5)(cid:14)(cid:7)(cid:8)(cid:14)(cid:8)%(cid:7)(cid:21)((cid:12)(cid:5)(cid:23)(cid:6)(cid:4)(cid:13)(cid:14)(cid:23)(cid:8)(cid:13)(cid:23) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:15)(cid:3)(cid:3) (cid:0)(cid:2)(cid:0) #(cid:11)(cid:11)(cid:14)(cid:5)(cid:14)(cid:7)(cid:8)(cid:31)&-’(cid:23)(cid:6)(cid:13)(cid:14)(cid:20)(cid:23)(cid:20) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:15)(cid:3)(cid:26) 10 Games and Strategies 251 ")(cid:2)" (cid:4)(cid:5)(cid:6)(cid:31)(cid:5)(cid:23)(cid:9)(cid:14)(cid:23)(cid:20)(cid:19)(cid:7)(cid:6)+(cid:31)(cid:21)(cid:23)(cid:20).(cid:7)(cid:19). (cid:7).%(cid:29)(cid:31)(cid:8)(cid:13)(cid:23) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:15)(cid:17)(cid:15) ")(cid:2)(cid:15) (cid:14)(cid:21) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:15)(cid:26)) (cid:0) ")(cid:2)(cid:16) (cid:27)(cid:14)(cid:30)(cid:7)(cid:8)(cid:31)(cid:13)(cid:13)(cid:14) (cid:14)(cid:21) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:15)(cid:26)(cid:15) ")(cid:2)(cid:3) %(cid:29)(cid:7)(cid:21)((cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:15)(cid:26)(cid:3) ")(cid:2)(cid:17) /(cid:23)’ (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:15)(cid:26)(cid:26) ")(cid:2)(cid:26) 0(cid:6)(cid:14)(cid:11)(cid:9).(cid:10)(cid:5) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:15)(cid:26)(cid:0) ")(cid:2)! #(cid:11)(cid:11)(cid:14)(cid:5)(cid:14)(cid:7)(cid:8)(cid:31)&-’(cid:23)(cid:6)(cid:13)(cid:14)(cid:20)(cid:23)(cid:20) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:15)!" Part II: Modelling Computing Systems 277 11 Modelling Processes 279 ""(cid:2)" 1(cid:31)(cid:30)(cid:23)&&(cid:23)(cid:11)$(cid:6)(cid:31)(cid:8)(cid:20)(cid:14)(cid:5)(cid:14)(cid:7)(cid:8)(cid:4)2(cid:20)(cid:5)(cid:23)(cid:21)(cid:20) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:15)," ""(cid:2)(cid:15) %(cid:7)(cid:21)((cid:12)(cid:5)(cid:31)(cid:5)(cid:14)(cid:7)(cid:8)(cid:20)(cid:31)(cid:8)(cid:11)(cid:18)(cid:6)(cid:7)(cid:13)(cid:23)(cid:20)(cid:20)(cid:23)(cid:20) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:15),! ""(cid:2)(cid:16) #1(cid:31)(cid:8)(cid:9)(cid:12)(cid:31)(cid:9)(cid:23)(cid:19)(cid:7)(cid:6)(cid:24)(cid:23)(cid:20)(cid:13)(cid:6)(cid:14)(cid:30)(cid:14)(cid:8)(cid:9)(cid:18)(cid:6)(cid:7)(cid:13)(cid:23)(cid:20)(cid:20)(cid:23)(cid:20) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:15)(cid:0)(cid:15) 0 ""(cid:2)(cid:16)(cid:2)" $(cid:29)(cid:23) (cid:14)&(cid:18)(cid:6)(cid:7)(cid:13)(cid:23)(cid:20)(cid:20) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:15)(cid:0)(cid:15) ""(cid:2)(cid:16)(cid:2)(cid:15) #(cid:13)(cid:5)(cid:14)(cid:7)(cid:8)(cid:18)(cid:6)(cid:23)(cid:25)’ (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:15)(cid:0)(cid:16) ""(cid:2)(cid:16)(cid:2)(cid:16) (cid:18)(cid:6)(cid:7)(cid:13)(cid:23)(cid:20)(cid:20) (cid:24)(cid:23)(cid:25)(cid:8)(cid:14)(cid:5)(cid:14)(cid:7)(cid:8)(cid:20) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:15)(cid:0)(cid:3) ""(cid:2)(cid:16)(cid:2)(cid:3) %(cid:29)(cid:7)(cid:14)(cid:13)(cid:23) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:15)(cid:0)(cid:17) ""(cid:2)(cid:3) (cid:24)(cid:14)(cid:20)(cid:5)(cid:14)(cid:8)(cid:9)(cid:12)(cid:14)(cid:20)(cid:29)(cid:14)(cid:8)(cid:9)0(cid:23)(cid:5)(cid:28)(cid:23)(cid:23)(cid:8)0(cid:23)(cid:29)(cid:31)(cid:22)(cid:14)(cid:7)(cid:12)(cid:6)(cid:20) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:15)(cid:0)(cid:0) ""(cid:2)(cid:17) -3(cid:12)(cid:31)&(cid:14)(cid:5)20(cid:23)(cid:5)(cid:28)(cid:23)(cid:23)(cid:8)(cid:18)(cid:6)(cid:7)(cid:13)(cid:23)(cid:20)(cid:20)(cid:23)(cid:20) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:16))(cid:15) ""(cid:2)(cid:26) #(cid:11)(cid:11)(cid:14)(cid:5)(cid:14)(cid:7)(cid:8)(cid:31)&-’(cid:23)(cid:6)(cid:13)(cid:14)(cid:20)(cid:23)(cid:20) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:16))(cid:16) 12 Distinguishing Between Processes 309 "(cid:15)(cid:2)" $(cid:29)(cid:23)0(cid:14)(cid:20)(cid:14)(cid:21)(cid:12)&(cid:31)(cid:5)(cid:14)(cid:7)(cid:8)+(cid:31)(cid:21)(cid:23) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:16))(cid:0) "(cid:15)(cid:2)(cid:15) (cid:18)(cid:6)(cid:7)((cid:23)(cid:6)(cid:5)(cid:14)(cid:23)(cid:20)(cid:7)(cid:19)+(cid:31)(cid:21)(cid:23)-3(cid:12)(cid:14)(cid:22)(cid:31)&(cid:23)(cid:8)(cid:13)(cid:23)(cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:16)"(cid:16) "(cid:15)(cid:2)(cid:16) 0(cid:14)(cid:20)(cid:14)(cid:21)(cid:12)&(cid:31)(cid:5)(cid:14)(cid:7)(cid:8)4(cid:23)&(cid:31)(cid:5)(cid:14)(cid:7)(cid:8)(cid:20) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:16)"(cid:17) "(cid:15)(cid:2)(cid:3) 0(cid:14)(cid:20)(cid:14)(cid:21)(cid:12)&(cid:31)(cid:5)(cid:14)(cid:7)(cid:8)%(cid:7)&(cid:7)(cid:12)(cid:6)(cid:14)(cid:8)(cid:9)(cid:20) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:16)"(cid:0) (cid:0) "(cid:15)(cid:2)(cid:17) $(cid:29)(cid:23)0(cid:14)(cid:20)(cid:14)(cid:21)(cid:12)&(cid:31)(cid:5)(cid:14)(cid:7)(cid:8)+(cid:31)(cid:21)(cid:23)4(cid:23)(cid:22)(cid:14)(cid:20)(cid:14)(cid:5)(cid:23)(cid:11)5 $(cid:7)(cid:10)(cid:8)(cid:25)(cid:8)(cid:14)(cid:5)2(cid:31)(cid:8)(cid:11)0(cid:23)2(cid:7)(cid:8)(cid:11)6 (cid:2) (cid:16)(cid:15)(cid:15) "(cid:15)(cid:2)(cid:17)(cid:2)" 7(cid:6)(cid:11)(cid:14)(cid:8)(cid:31)& (cid:12)(cid:21)(cid:30)(cid:23)(cid:6)(cid:20) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:16)(cid:15)(cid:16) "(cid:15)(cid:2)(cid:17)(cid:2)(cid:15) 7(cid:6)(cid:11)(cid:14)(cid:8)(cid:31)&0(cid:14)(cid:20)(cid:14)(cid:21)(cid:12)&(cid:31)(cid:5)(cid:14)(cid:7)(cid:8)+(cid:31)(cid:21)(cid:23)(cid:20) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:16)(cid:15)(cid:3) "(cid:15)(cid:2)(cid:26) #(cid:11)(cid:11)(cid:14)(cid:5)(cid:14)(cid:7)(cid:8)(cid:31)&-’(cid:23)(cid:6)(cid:13)(cid:14)(cid:20)(cid:23)(cid:20) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:2) (cid:16)(cid:15), CONTENTS ix 13 Logical Properties of Processes 333 (cid:0)(cid:2)(cid:3)(cid:0) (cid:4)(cid:5)(cid:6)(cid:7)(cid:8)(cid:9)(cid:10)(cid:8)(cid:11)(cid:12)(cid:7)(cid:13)(cid:10)(cid:14)(cid:10)(cid:15)(cid:16)(cid:17)(cid:18)(cid:15)(cid:19)(cid:6)(cid:10)(cid:10)(cid:6)(cid:10)(cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:2)(cid:2)(cid:20) (cid:0)(cid:2)(cid:3)(cid:21) (cid:22)(cid:7)(cid:15)(cid:12)(cid:8)(cid:23)(cid:24)(cid:15)(cid:25)(cid:26)(cid:19)(cid:16)(cid:15)(cid:18)(cid:17)(cid:18)(cid:15)(cid:27)(cid:6)(cid:18)(cid:14)(cid:26)(cid:6)(cid:10) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:2)(cid:2)(cid:28) (cid:0)(cid:2)(cid:3)(cid:2) (cid:29)(cid:6)(cid:25)(cid:8)(cid:14)(cid:26)(cid:15)(cid:11)(cid:30)(cid:10)(cid:31)(cid:6) (cid:11)(cid:8)!(cid:23)(cid:6)(cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:2)(cid:20)(cid:0) (cid:0)(cid:2)(cid:3)(cid:20) (cid:4)(cid:5)(cid:6)"(cid:6)(cid:11)(cid:12)(cid:26)(cid:11)(cid:25)(cid:7)(cid:8)(cid:19)(cid:5)(cid:26)(cid:11)(cid:6)(cid:10)#(cid:6)$(cid:26)(cid:10)(cid:26)(cid:14)(cid:6)(cid:12) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:2)(cid:20)(cid:20) (cid:0)(cid:2)(cid:3)% (cid:7)(cid:15)(cid:12)(cid:8)(cid:23)(cid:17)(cid:18)(cid:15)(cid:27)(cid:6)(cid:18)(cid:14)(cid:26)(cid:6)(cid:10)(cid:8)(cid:11)(cid:12)&(cid:26)(cid:10)(cid:26)’(cid:13)(cid:23)(cid:8)(cid:14)(cid:26)(cid:15)(cid:11) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:2)(cid:20)(cid:28) (cid:0) (cid:0)(cid:2)(cid:3)(cid:28) ((cid:5)(cid:8)(cid:18)(cid:8)(cid:19)(cid:14)(cid:6)(cid:18)(cid:26)(cid:10)(cid:14)(cid:26)(cid:19))(cid:15)(cid:18)’(cid:13)(cid:23)* (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:2)%+ (cid:0) (cid:0)(cid:2)(cid:3), -(cid:23)(cid:15)!(cid:8)(cid:23).(cid:6)’(cid:8)(cid:11)(cid:14)(cid:26)(cid:19)(cid:10) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:2)%(cid:21) (cid:0)(cid:2)(cid:3)/ (cid:22)(cid:12)(cid:12)(cid:26)(cid:14)(cid:26)(cid:15)(cid:11)(cid:8)(cid:23)01(cid:6)(cid:18)(cid:19)(cid:26)(cid:10)(cid:6)(cid:10) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:2)%(cid:2) 14 Concurrent Processes 357 (cid:0)(cid:20)(cid:3)(cid:0) .(cid:9)(cid:11)(cid:19)(cid:5)(cid:18)(cid:15)(cid:11)(cid:26)(cid:10)(cid:8)(cid:14)(cid:26)(cid:15)(cid:11)(cid:7)(cid:6)(cid:18)(cid:25)(cid:6) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:2)%, (cid:0)(cid:20)(cid:3)(cid:21) ((cid:15)(cid:13)(cid:11)(cid:14)(cid:6)(cid:18)(cid:10)(cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:2)(cid:28)+ (cid:0)(cid:20)(cid:3)(cid:2) #(cid:8)(cid:26)(cid:23)2(cid:8)(cid:9)(cid:24)(cid:6)$(cid:6)(cid:23)((cid:18)(cid:15)(cid:10)(cid:10)(cid:26)(cid:11)(cid:25)(cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:2)(cid:28)(cid:21) (cid:0)(cid:20)(cid:3)(cid:20) (cid:7)(cid:13)(cid:14)(cid:13)(cid:8)(cid:23)01(cid:19)(cid:23)(cid:13)(cid:10)(cid:26)(cid:15)(cid:11) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:2)(cid:28)% (cid:0)(cid:20)(cid:3)(cid:20)(cid:3)(cid:0) (cid:31)(cid:26)(cid:11)(cid:26)(cid:11)(cid:25)(cid:17)(cid:5)(cid:26)(cid:23)(cid:15)(cid:10)(cid:15)(cid:27)(cid:5)(cid:6)(cid:18)(cid:10) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:2)(cid:28)% (cid:0)(cid:20)(cid:3)(cid:20)(cid:3)(cid:21) (cid:17)(cid:6)(cid:14)(cid:6)(cid:18)(cid:10)(cid:15)(cid:11)3(cid:10)(cid:22)(cid:23)(cid:25)(cid:15)(cid:18)(cid:26)(cid:14)(cid:5)’(cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:2)(cid:28)/ (cid:0)(cid:20)(cid:3)% (cid:22)(cid:7)(cid:6)(cid:10)(cid:10)(cid:8)(cid:25)(cid:6) (cid:31)(cid:6)(cid:23)(cid:26)$(cid:6)(cid:18)(cid:9).(cid:9)(cid:10)(cid:14)(cid:6)’ (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:2),(cid:0) (cid:0)(cid:20)(cid:3)(cid:28) (cid:22)(cid:23)(cid:14)(cid:6)(cid:18)(cid:11)(cid:8)(cid:14)(cid:26)(cid:11)(cid:25)&(cid:26)(cid:14)(cid:17)(cid:18)(cid:15)(cid:14)(cid:15)(cid:19)(cid:15)(cid:23) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:2),(cid:2) (cid:0)(cid:20)(cid:3), (cid:22)(cid:12)(cid:12)(cid:26)(cid:14)(cid:26)(cid:15)(cid:11)(cid:8)(cid:23)01(cid:6)(cid:18)(cid:19)(cid:26)(cid:10)(cid:6)(cid:10) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:2),, 15Temporal Properties 381 (cid:0) (cid:0)%(cid:3)(cid:0) (cid:4)(cid:5)(cid:18)(cid:6)(cid:6).(cid:14)(cid:8)(cid:11)(cid:12)(cid:8)(cid:18)(cid:12)(cid:4)(cid:6)’(cid:27)(cid:15)(cid:18)(cid:8)(cid:23)4(cid:27)(cid:6)(cid:18)(cid:8)(cid:14)(cid:15)(cid:18)(cid:10) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:2)/(cid:21) (cid:0)%(cid:3)(cid:0)(cid:3)(cid:0) (cid:22)(cid:23)2(cid:8)(cid:9)(cid:10)5 (cid:0)(cid:0) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:2)/(cid:21) (cid:0)%(cid:3)(cid:0)(cid:3)(cid:21) (cid:17)(cid:15)(cid:10)(cid:10)(cid:26)!(cid:23)(cid:9)5 (cid:2)(cid:0) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:2)/(cid:2) (cid:0)%(cid:3)(cid:0)(cid:3)(cid:2) 6(cid:11)(cid:14)(cid:26)(cid:23)5 (cid:0)6(cid:2) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:2)/(cid:20) (cid:0)%(cid:3)(cid:21) #(cid:6)(cid:19)(cid:13)(cid:18)(cid:10)(cid:26)$(cid:6)(cid:17)(cid:18)(cid:15)(cid:27)(cid:6)(cid:18)(cid:14)(cid:26)(cid:6)(cid:10) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:2)/% (cid:0)%(cid:3)(cid:21)(cid:3)(cid:0) .(cid:15)(cid:23)$(cid:26)(cid:11)(cid:25)#(cid:6)(cid:19)(cid:13)(cid:18)(cid:10)(cid:26)$(cid:6)07(cid:13)(cid:8)(cid:14)(cid:26)(cid:15)(cid:11)(cid:10) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:2)/, (cid:0)%(cid:3)(cid:21)(cid:3)(cid:21) )(cid:26)1(cid:6)(cid:12)(cid:17)(cid:15)(cid:26)(cid:11)(cid:14).(cid:15)(cid:23)(cid:13)(cid:14)(cid:26)(cid:15)(cid:11)(cid:10) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:2)// (cid:0)%(cid:3)(cid:2) (cid:4)(cid:5)(cid:6)(cid:7)(cid:15)(cid:12)(cid:8)(cid:23)(cid:7)(cid:13)8((cid:8)(cid:23)(cid:19)(cid:13)(cid:23)(cid:13)(cid:10) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:2)9+ (cid:0)%(cid:3)(cid:20) (cid:24)(cid:6)(cid:8)(cid:10)(cid:14)$(cid:6)(cid:18)(cid:10)(cid:13)(cid:10)-(cid:18)(cid:6)(cid:8)(cid:14)(cid:6)(cid:10)(cid:14))(cid:26)1(cid:6)(cid:12)(cid:17)(cid:15)(cid:26)(cid:11)(cid:14)(cid:10) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:2)9(cid:21) (cid:0)%(cid:3)(cid:20)(cid:3)(cid:0) (cid:22)(cid:27)(cid:27)(cid:18)(cid:15)1(cid:26)’(cid:8)(cid:14)(cid:26)(cid:11)(cid:25))(cid:26)1(cid:6)(cid:12)(cid:17)(cid:15)(cid:26)(cid:11)(cid:14)(cid:10) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:2)9(cid:2) (cid:0)%(cid:3)% 01(cid:27)(cid:18)(cid:6)(cid:10)(cid:10)(cid:26)(cid:11)(cid:25).(cid:14)(cid:8)(cid:11)(cid:12)(cid:8)(cid:18)(cid:12)(cid:4)(cid:6)’(cid:27)(cid:15)(cid:18)(cid:8)(cid:23)4(cid:27)(cid:6)(cid:18)(cid:8)(cid:14)(cid:15)(cid:18)(cid:10) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:2)9, (cid:0)%(cid:3)%(cid:3)(cid:0) (cid:22)(cid:23)2(cid:8)(cid:9)(cid:10)5 (cid:0)(cid:0) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:2)9/ (cid:0)%(cid:3)%(cid:3)(cid:21) (cid:17)(cid:15)(cid:10)(cid:10)(cid:26)!(cid:23)(cid:9)5 (cid:2)(cid:0) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:2)9/ (cid:0)%(cid:3)%(cid:3)(cid:2) 6(cid:11)(cid:14)(cid:26)(cid:23)5 (cid:0)6(cid:2) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:2)9/ (cid:0)%(cid:3)(cid:28) )(cid:13)(cid:18)(cid:14)(cid:5)(cid:6)(cid:18))(cid:26)1(cid:6)(cid:12)(cid:17)(cid:15)(cid:26)(cid:11)(cid:14)(cid:17)(cid:18)(cid:15)(cid:27)(cid:6)(cid:18)(cid:14)(cid:26)(cid:6)(cid:10) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:2)99 (cid:0)%(cid:3), (cid:22)(cid:12)(cid:12)(cid:26)(cid:14)(cid:26)(cid:15)(cid:11)(cid:8)(cid:23)01(cid:6)(cid:18)(cid:19)(cid:26)(cid:10)(cid:6)(cid:10) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:3) (cid:20)+(cid:0) Solutions to Exercises 405 Index 493