Return-Path: Delivery-Date: Received: from dworshak.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Thu, 9 Sep 1993 15:59:00 +0100 Received: by dworshak.cs.uidaho.edu (1.37.109.4/16.2) id AA25040; Thu, 9 Sep 93 07:43:28 -0700 Sender: info-hol-request@cs.uidaho.edu Errors-To: info-hol-request@cs.uidaho.edu Precedence: bulk Received: from linus.mitre.org by dworshak.cs.uidaho.edu with SMTP (1.37.109.4/16.2) id AA25036; Thu, 9 Sep 93 07:43:22 -0700 Received: from nausicaa.mitre.org by linus.mitre.org (5.61/RCF-4S) id AA09172; Thu, 9 Sep 93 10:42:07 -0400 Full-Name: Joshua D. Guttman Posted-Date: Thu, 09 Sep 1993 10:45:32 -0400 Received: by nausicaa (5.0/RCF-4C) id AA02828; Thu, 9 Sep 93 10:45:37 EDT Message-Id: <9309091445.AA02828@nausicaa> To: info-hol@cs.uidaho.edu Cc: guttman@linus.mitre.org, borm@cs.ubc.ca Subject: Re: a little proof challenge X-Postal-Address: MITRE, Mail Stop A118 X-Postal-Address: 202 Burlington Rd. X-Postal-Address: Bedford, MA 01730-1420 USA X-Telephone-Number: 617 271 2654; Fax 617 271 3816 Date: Thu, 09 Sep 1993 10:45:32 -0400 From: "Joshua D. Guttman" Content-Length: 25694 This formula is also very easy to prove with Imps. My first proof certainly took no longer than 10 minutes, including transcription, and another five minutes gave what I consider a natural and informative proof. Note that one need only instantiate one of the existentially bound variables (v), and that the obvious candidate is the conditional term if(nonvacuous_q{r}, y_$0,x_$0), where we have the assumptions that x_$0 satisfies p and y_$0 satisfies q. The Imps proof script is contained in the def-theorem form below, with the original script below it. I have also appended a postscript file which gives an Imps-generated readable description of the proof. Josh (def-theorem eric-borms-propositional-tester " forall(p,q,r:[ind,prop],x:ind, forsome(v,w:ind, forall(y,z:ind, p(x) and q(y) implies (p(v) or r(w)) and (r(z) implies q(v))))); " (theory the-kernel-theory) (proof ( simplify insistent-direct-and-antecedent-inference-strategy (instantiate-existential ("if(nonvacuous_q{r}, y_$0,x_$0)")) (move-to-ancestor 2) (case-split-on-conditionals (0))))) (comment Here's the first proof I came up with interactively. direct-and-antecedent-inference-strategy simplify direct-and-antecedent-inference-strategy auto-instantiate-existential (instantiate-existential ("if(nonvacuous_q{r}, y_$0,x)")) (contrapose "with(p:prop,not(p));") simplify (case-split-on-conditionals (0)) (contrapose "with(p:prop,p or p);") (case-split-on-conditionals (0)) (contrapose "with(p:prop,not(p));") simplify) ~~~~~~~~~~~~~~~~ %!PS-Adobe-2.0 %%Creator: dvips 5.516 Copyright 1986, 1993 Radical Eye Software %%Title: guttman-imps.dvi %%CreationDate: Thu Sep 9 10:38:29 1993 %%Pages: 2 %%PageOrder: Ascend %%BoundingBox: 0 0 612 792 %%EndComments %DVIPSCommandLine: dvips guttman-imps.dvi %DVIPSSource: TeX output 1993.09.09:1025 %%BeginProcSet: tex.pro /TeXDict 250 dict def TeXDict begin /N{def}def /B{bind def}N /S{exch}N /X{S N}B /TR{translate}N /isls false N /vsize 11 72 mul N /hsize 8.5 72 mul N /landplus90{false}def /@rigin{isls{[0 landplus90{1 -1}{-1 1} ifelse 0 0 0]concat}if 72 Resolution div 72 VResolution div neg scale isls{landplus90{VResolution 72 div vsize mul 0 exch}{Resolution -72 div hsize mul 0}ifelse TR}if Resolution VResolution vsize -72 div 1 add mul TR matrix currentmatrix dup dup 4 get round 4 exch put dup dup 5 get round 5 exch put setmatrix}N /@landscape{/isls true N}B /@manualfeed{ statusdict /manualfeed true put}B /@copies{/#copies X}B /FMat[1 0 0 -1 0 0]N /FBB[0 0 0 0]N /nn 0 N /IE 0 N /ctr 0 N /df-tail{/nn 8 dict N nn begin /FontType 3 N /FontMatrix fntrx N /FontBBox FBB N string /base X array /BitMaps X /BuildChar{CharBuilder}N /Encoding IE N end dup{/foo setfont}2 array copy cvx N load 0 nn put /ctr 0 N[}B /df{/sf 1 N /fntrx FMat N df-tail}B /dfs{div /sf X /fntrx[sf 0 0 sf neg 0 0]N df-tail}B /E{ pop nn dup definefont setfont}B /ch-width{ch-data dup length 5 sub get} B /ch-height{ch-data dup length 4 sub get}B /ch-xoff{128 ch-data dup length 3 sub get sub}B /ch-yoff{ch-data dup length 2 sub get 127 sub}B /ch-dx{ch-data dup length 1 sub get}B /ch-image{ch-data dup type /stringtype ne{ctr get /ctr ctr 1 add N}if}B /id 0 N /rw 0 N /rc 0 N /gp 0 N /cp 0 N /G 0 N /sf 0 N /CharBuilder{save 3 1 roll S dup /base get 2 index get S /BitMaps get S get /ch-data X pop /ctr 0 N ch-dx 0 ch-xoff ch-yoff ch-height sub ch-xoff ch-width add ch-yoff setcachedevice ch-width ch-height true[1 0 0 -1 -.1 ch-xoff sub ch-yoff .1 add]{ ch-image}imagemask restore}B /D{/cc X dup type /stringtype ne{]}if nn /base get cc ctr put nn /BitMaps get S ctr S sf 1 ne{dup dup length 1 sub dup 2 index S get sf div put}if put /ctr ctr 1 add N}B /I{cc 1 add D }B /bop{userdict /bop-hook known{bop-hook}if /SI save N @rigin 0 0 moveto /V matrix currentmatrix dup 1 get dup mul exch 0 get dup mul add .99 lt{/QV}{/RV}ifelse load def pop pop}N /eop{SI restore showpage userdict /eop-hook known{eop-hook}if}N /@start{userdict /start-hook known{start-hook}if pop /VResolution X /Resolution X 1000 div /DVImag X /IE 256 array N 0 1 255{IE S 1 string dup 0 3 index put cvn put}for 65781.76 div /vsize X 65781.76 div /hsize X}N /p{show}N /RMat[1 0 0 -1 0 0]N /BDot 260 string N /rulex 0 N /ruley 0 N /v{/ruley X /rulex X V}B /V {}B /RV statusdict begin /product where{pop product dup length 7 ge{0 7 getinterval dup(Display)eq exch 0 4 getinterval(NeXT)eq or}{pop false} ifelse}{false}ifelse end{{gsave TR -.1 -.1 TR 1 1 scale rulex ruley false RMat{BDot}imagemask grestore}}{{gsave TR -.1 -.1 TR rulex ruley scale 1 1 false RMat{BDot}imagemask grestore}}ifelse B /QV{gsave transform round exch round exch itransform moveto rulex 0 rlineto 0 ruley neg rlineto rulex neg 0 rlineto fill grestore}B /a{moveto}B /delta 0 N /tail{dup /delta X 0 rmoveto}B /M{S p delta add tail}B /b{S p tail} B /c{-4 M}B /d{-3 M}B /e{-2 M}B /f{-1 M}B /g{0 M}B /h{1 M}B /i{2 M}B /j{ 3 M}B /k{4 M}B /w{0 rmoveto}B /l{p -4 w}B /m{p -3 w}B /n{p -2 w}B /o{p -1 w}B /q{p 1 w}B /r{p 2 w}B /s{p 3 w}B /t{p 4 w}B /x{0 S rmoveto}B /y{ 3 2 roll p a}B /bos{/SS save N}B /eos{SS restore}B end %%EndProcSet TeXDict begin 40258437 52099154 1000 300 300 (/tmp/guttman-imps.dvi) @start /Fa 2 49 df<020002000F80326062104208C218C238C238E20072007E003FC0 1FE003F0027002384218E218E21882184210422032400F80020002000D1B7E9812>36 D<07C018303018701C600C600CE00EE00EE00EE00EE00EE00EE00EE00EE00E600C600C70 1C30181C7007C00F157F9412>48 D E /Fb 18 122 df45 D<70F8F8F870000000000000000000000070F8F8F87005157A9410>58 D80 D<00040000000E0000000E0000000E0000001F0000001F0000003F800000278000002780 000043C0000043C0000043C0000081E0000081E0000101F0000100F0000100F00003FFF8 000200780006007C0004003C0004003C000C001E000C001E003C003F00FF00FFE01B1A7F 991F>97 D<003F0201C0C603002E0E001E1C000E1C0006380006780002700002700002F0 0000F00000F00000F00000F00000F000007000027000027800023800041C00041C00080E 000803003001C0C0003F00171A7E991D>99 DIII<003F810001E063000380170006000F000C0007001C000300 38000300780001007800010070000100F0000000F0000000F0000000F0000000F0000000 F001FFE070001F0078000F0078000F0038000F001C000F000C000F0006000F0003801700 01E06300003F81001B1A7E9920>I105 D108 D110 D<007F800001C0E00007003800 0E001C001C000E003C000F0038000700780007807000038070000380F00003C0F00003C0 F00003C0F00003C0F00003C0F00003C0F00003C07800078078000780380007003C000F00 1C000E000E001C000700380001C0E000007F80001A1A7E9920>II114 D<07E100181B00300700600300600300E00100E00100E00100F00000 F800007F80003FF8001FFC000FFE0000FF00000F00000780000780800380800380800380 C00300C00700E00600DC0C0083F000111A7E9917>I<7FFFFF00701E0700601E0100401E 0100C01E0180801E0080801E0080801E0080001E0000001E0000001E0000001E0000001E 0000001E0000001E0000001E0000001E0000001E0000001E0000001E0000001E0000001E 0000001E0000001E0000003F000003FFF000191A7F991D>I121 D E /Fc 7 104 df<00C00000C00000C00000C00000C000C0C0C0F0C3C038C7000EDC00 03F00000C00003F0000EDC0038C700F0C3C0C0C0C000C00000C00000C00000C00000C000 12157D9619>3 D<03F0000FFC001C0E00300300600180600180C000C0C000C0C000C0C0 00C0C000C0C000C0C000C0C000C06001806001803003001C0E000FFC0003F00012147D95 19>14 D<03F0000FFC001FFE003FFF007FFF807FFF80FFFFC0FFFFC0FFFFC0FFFFC0FFFF C0FFFFC0FFFFC0FFFFC07FFF807FFF803FFF001FFE000FFC0003F00012147D9519>I27 D95 D<000F0038007000E001C001C001C001C001C001C001C001C001C001C001 C001C001C001C001C001C001C0038007001E00F0001E000700038001C001C001C001C001 C001C001C001C001C001C001C001C001C001C001C001C001C000E000700038000F10317C A419>102 DI E /Fd 11 123 df<00000000400000000000400000000000200000000000100000 0000001000000000000800000000000400000000000300FFFFFFFFFFC0FFFFFFFFFFC02A 0A7D9431>42 D<70F8F8F87005057C840E>58 D<70F8FCFC740404040408081010204006 0F7C840E>I<03C0F004631C04740E08780E08700708700708700F00E00F00E00F00E00F 00E00F01C01E01C01E01C01E01C03C03803803803803C07003C0E0072180071E00070000 0700000E00000E00000E00000E00001C00001C00001C0000FFC000181F819418>112 D<00782001C4600302E00601C00E01C01C01C03C01C0380380780380780380780380F007 00F00700F00700F00700F00E00700E00701E00302E0018DC000F1C00001C00001C000038 0000380000380000380000700000700000700007FF00131F7E9416>I<3C0F004630C047 41C08783C08783C08701808700000E00000E00000E00000E00001C00001C00001C00001C 000038000038000038000038000070000030000012157E9416>I<1E00C02301E04381F0 4380F08380708380308700300700200E00200E00200E00201C00401C00401C00801C0080 1C01001C01001C02000C040006080003F00014157E9418>118 D<1E0018182300383C43 80383E4380701E8380700E83807006870070060700E0040E00E0040E00E0040E00E0041C 01C0081C01C0081C01C0081C01C0101C01C0101C01C0201C03C0400C04C0C00708E10001 F03E001F157E9423>I<01E0F006310C081A1C101A3C201C3C201C18201C000038000038 0000380000380000700000700000700000700860E010F0E010F0E020E170404230803C1F 0016157E941C>I<1E00302300704380704380E08380E08380E08700E00701C00E01C00E 01C00E01C01C03801C03801C03801C03801C07001C07001C07001C0F000C3E0003CE0000 0E00000E00001C00601C00F03800F03000E0600080C0004180003E0000141F7E9418>I< 00E01003F02007F860060FC008008008010000020000040000080000100000200000C000 0100000200000400400800801001803F830061FE0040FC0080780014157E9417>I E /Fe 39 122 df<00200040008001000300060004000C000C0018001800300030003000 7000600060006000E000E000E000E000E000E000E000E000E000E000E000E000E000E000 6000600060007000300030003000180018000C000C000400060003000100008000400020 0B327CA413>40 D<800040002000100018000C0004000600060003000300018001800180 01C000C000C000C000E000E000E000E000E000E000E000E000E000E000E000E000E000E0 00C000C000C001C0018001800180030003000600060004000C0018001000200040008000 0B327DA413>I<70F8FCFC7404040404080810102040060F7C840E>44 D<70F8F8F87005057C840E>46 D<01F000071C000C06001803003803803803807001C070 01C07001C07001C0F001E0F001E0F001E0F001E0F001E0F001E0F001E0F001E0F001E0F0 01E0F001E0F001E0F001E0F001E07001C07001C07001C07803C03803803803801C07000C 0600071C0001F00013227EA018>48 D<008003800F80F380038003800380038003800380 038003800380038003800380038003800380038003800380038003800380038003800380 03800380038007C0FFFE0F217CA018>I<03F0000C1C001007002007804003C04003C080 03E0F003E0F801E0F801E0F801E02003E00003E00003C00003C0000780000700000E0000 1C0000180000300000600000C0000180000100000200200400200800201800603000403F FFC07FFFC0FFFFC013217EA018>I<01F800060E000803001001802001802000C06000C0 6000C06000C07000C07801803E01003F02001FC4000FF80003F80003FC00067F00083F80 100F803007C06001C06000E0C000E0C00060C00060C00060C000606000406000C0300080 1803000E0E0003F00013227EA018>56 D<01F000060C000C060018070038038070038070 0380F001C0F001C0F001C0F001E0F001E0F001E0F001E0F001E07001E07003E03803E018 05E00C05E00619E003E1E00001C00001C00001C000038000038030030078070078060070 0C002018001030000FC00013227EA018>I<70F8F8F870000000000000000000000070F8 F8F87005157C940E>I<07E01838201C400E800FF00FF00FF00F000F000E001C00380030 006000C000C0008000800180010001000100010001000100000000000000000000000380 07C007C007C0038010237DA217>63 D<0001800000018000000180000003C0000003C000 0003C0000005E0000005E000000DF0000008F0000008F0000010F8000010780000107800 00203C0000203C0000203C0000401E0000401E0000401E0000800F0000800F0000FFFF00 0100078001000780030007C0020003C0020003C0040003E0040001E0040001E00C0000F0 0C0000F03E0001F8FF800FFF20237EA225>65 D73 D76 D<03F0200C0C601802603001E0 7000E0600060E00060E00060E00020E00020E00020F00000F000007800007F00003FF000 1FFE000FFF0003FF80003FC00007E00001E00000F00000F0000070800070800070800070 800070C00060C00060E000C0F000C0C80180C6070081FC0014247DA21B>83 D<7FFFFFF87807807860078018400780084007800840078008C007800C80078004800780 048007800480078004000780000007800000078000000780000007800000078000000780 000007800000078000000780000007800000078000000780000007800000078000000780 000007800000078000000780000007800000078000000FC00003FFFF001E227EA123>I< FFFC07FF0FC000F807800070078000200780002007800020078000200780002007800020 078000200780002007800020078000200780002007800020078000200780002007800020 078000200780002007800020078000200780002007800020078000200780002003800040 03C0004003C0004001C0008000E000800060010000300600001C08000003F00020237EA1 25>I<0FE0001838003C0C003C0E0018070000070000070000070000FF0007C7001E0700 3C0700780700700700F00708F00708F00708F00F087817083C23900FC1E015157E9418> 97 D<01FE000703000C07801C0780380300780000700000F00000F00000F00000F00000 F00000F00000F000007000007800403800401C00800C010007060001F80012157E9416> 99 D<0000E0000FE00001E00000E00000E00000E00000E00000E00000E00000E00000E0 0000E00000E00000E001F8E00704E00C02E01C01E03800E07800E07000E0F000E0F000E0 F000E0F000E0F000E0F000E0F000E07000E07800E03800E01801E00C02E0070CF001F0FE 17237EA21B>I<01FC000707000C03801C01C03801C07801E07000E0F000E0FFFFE0F000 00F00000F00000F00000F000007000007800203800201C00400E008007030000FC001315 7F9416>I<003C00C6018F038F030F070007000700070007000700070007000700FFF807 000700070007000700070007000700070007000700070007000700070007000700070007 807FF8102380A20F>I<0E0000FE00001E00000E00000E00000E00000E00000E00000E00 000E00000E00000E00000E00000E00000E1F800E60C00E80E00F00700F00700E00700E00 700E00700E00700E00700E00700E00700E00700E00700E00700E00700E00700E00700E00 700E0070FFE7FF18237FA21B>104 D<1C001E003E001E001C0000000000000000000000 0000000000000E00FE001E000E000E000E000E000E000E000E000E000E000E000E000E00 0E000E000E000E000E00FFC00A227FA10E>I<01C003E003E003E001C000000000000000 00000000000000000001E00FE001E000E000E000E000E000E000E000E000E000E000E000 E000E000E000E000E000E000E000E000E000E000E000E000E060E0F0C0F18061803E000B 2C82A10F>I<0E00FE001E000E000E000E000E000E000E000E000E000E000E000E000E00 0E000E000E000E000E000E000E000E000E000E000E000E000E000E000E000E000E000E00 0E00FFE00B237FA20E>108 D<0E1FC07F00FE60E183801E807201C00F003C00E00F003C 00E00E003800E00E003800E00E003800E00E003800E00E003800E00E003800E00E003800 E00E003800E00E003800E00E003800E00E003800E00E003800E00E003800E00E003800E0 0E003800E0FFE3FF8FFE27157F942A>I<0E1F80FE60C01E80E00F00700F00700E00700E 00700E00700E00700E00700E00700E00700E00700E00700E00700E00700E00700E00700E 00700E0070FFE7FF18157F941B>I<01FC000707000C01801800C03800E0700070700070 F00078F00078F00078F00078F00078F00078F000787000707800F03800E01C01C00E0380 07070001FC0015157F9418>I<0E1F00FE61C00E80600F00700E00380E003C0E001C0E00 1E0E001E0E001E0E001E0E001E0E001E0E001E0E003C0E003C0E00380F00700E80E00E41 C00E3F000E00000E00000E00000E00000E00000E00000E00000E00000E0000FFE000171F 7F941B>I<01F8200704600E02601C01603801E07800E07800E0F000E0F000E0F000E0F0 00E0F000E0F000E0F000E07000E07800E03801E01C01E00C02E0070CE001F0E00000E000 00E00000E00000E00000E00000E00000E00000E00000E0000FFE171F7E941A>I<0E3CFE 461E8F0F0F0F060F000E000E000E000E000E000E000E000E000E000E000E000E000E000F 00FFF010157F9413>I<0F8830786018C018C008C008E008F0007F803FE00FF001F8003C 801C800C800CC00CC008E018D0308FC00E157E9413>I<02000200020002000600060006 000E001E003E00FFF80E000E000E000E000E000E000E000E000E000E000E000E040E040E 040E040E040E040708030801F00E1F7F9E13>I<0E0070FE07F01E00F00E00700E00700E 00700E00700E00700E00700E00700E00700E00700E00700E00700E00700E00700E00F00E 00F006017003827800FC7F18157F941B>IIIII E /Ff 15 118 df<387CFEFEFE7C3807077C8610>46 D<03FC000FFF003C1FC07007E07C07F0FE 03F0FE03F8FE03F8FE01F87C01F83803F80003F80003F00003F00007E00007C0000F8000 1F00003E0000380000700000E01801C0180380180700180E00380FFFF01FFFF03FFFF07F FFF0FFFFF0FFFFF015207D9F1C>50 D<00FE0003FFC00703E00E00F01C00F01C00783C00 783E00783F00783F80783FE0F01FF9E01FFFC00FFF8007FFC003FFE007FFF01E7FF83C1F FC7807FC7801FEF000FEF0003EF0001EF0001EF0001CF8001C7800383C00381F01F00FFF C001FF0017207E9F1C>56 D<01FE0007FF800F83E01E01F03E00F07C00F87C0078FC007C FC007CFC007CFC007EFC007EFC007EFC007E7C00FE7C00FE3E01FE1E037E0FFE7E07FC7E 00207E00007C00007C1E007C3F00F83F00F83F00F03F01E01E03C01C0F800FFE0003F800 17207E9F1C>I<01FC0407FF8C1F03FC3C007C7C003C78001C78001CF8000CF8000CFC00 0CFC0000FF0000FFE0007FFF007FFFC03FFFF01FFFF80FFFFC03FFFE003FFE0003FF0000 7F00003F00003FC0001FC0001FC0001FE0001EE0001EF0003CFC003CFF00F8C7FFE080FF 8018227DA11F>83 D<7FFFFFFF807FFFFFFF807E03F80F807803F807807003F803806003 F80180E003F801C0E003F801C0C003F800C0C003F800C0C003F800C0C003F800C00003F8 00000003F800000003F800000003F800000003F800000003F800000003F800000003F800 000003F800000003F800000003F800000003F800000003F800000003F800000003F80000 0003F800000003F800000003F800000003F800000003F8000003FFFFF80003FFFFF80022 227EA127>I<00FE0007FF800F87C01E01E03E01F07C00F07C00F8FC00F8FC00F8FFFFF8 FFFFF8FC0000FC0000FC00007C00007C00007E00003E00181F00300FC07003FFC000FF00 15167E951A>101 D104 D109 DI<00FE 0007FFC00F83E01E00F03E00F87C007C7C007C7C007CFC007EFC007EFC007EFC007EFC00 7EFC007EFC007E7C007C7C007C3E00F81F01F00F83E007FFC000FE0017167E951C>I<00 FE030007FF87000FC1C7001F006F003F003F007E003F007E001F007C001F00FC001F00FC 001F00FC001F00FC001F00FC001F00FC001F00FC001F007E001F007E001F003E003F001F 007F000FC1DF0007FF9F0001FC1F0000001F0000001F0000001F0000001F0000001F0000 001F0000001F0000001F000000FFE00000FFE01B207E951E>113 DI<0180000180000180000180000380000380000780000780000F80003F8000FFFF00FF FF000F80000F80000F80000F80000F80000F80000F80000F80000F80000F80000F80000F 81800F81800F81800F81800F81800F830007C30003FE0000F80011207F9F16>116 DI E end %%EndProlog %%BeginSetup %%Feature: *Resolution 300dpi TeXDict begin %%EndSetup %%Page: 1 1 1 0 bop 164 315 a Ff(Theorem)205 479 y Fe(for)16 b(ev)o(ery)f Fd(p;)8 b(q)r(;)g(r)15 b Fe(:)e(ind)h Fd(*)f Fc(\003)p Fd(;)8 b(x)13 b Fe(:)h(ind)65 b(for)16 b(some)f Fd(v)r(;)8 b(w)15 b Fe(:)e(ind)65 b(for)16 b(ev)o(ery)f Fd(y)r(;)8 b(z)15 b Fe(:)286 540 y(ind)48 b(implication)341 600 y Fc(\017)20 b Fe(conjunction)386 660 y Fc(\016)f Fd(p)p Fe(\()p Fd(x)p Fe(\))386 720 y Fc(\016)g Fd(q)r Fe(\()p Fd(y)r Fe(\))341 780 y Fc(\017)h Fe(conjunction)386 841 y Fc(\016)f Fd(p)p Fe(\()p Fd(v)r Fe(\))11 b Fc(_)g Fd(r)q Fe(\()p Fd(w)q Fe(\))386 901 y Fc(\016)19 b Fd(r)q Fe(\()p Fd(z)r Fe(\))14 b Fc(\033)g Fd(q)r Fe(\()p Fd(v)r Fe(\))p Fd(:)164 1065 y Fb(Pr)o(oof:)45 b Fe(Simplify)13 b(sequen)o(t)j(the)g (claim)e(of)i(the)g(theorem.)k(This)c(yields)164 1175 y Ff(Sequen)n(t)i(2.)205 1276 y Fe(for)e(ev)o(ery)f Fd(p;)8 b(q)15 b Fe(:)f(ind)f Fd(*)h Fc(\003)49 b Fe(implication)341 1337 y Fc(\017)20 b Fe(conjunction)386 1397 y Fc(\016)f Fe(non)o(v)m(acuous?)q Fc(f)p Fd(p)p Fc(g)386 1457 y(\016)g Fe(non)o(v)m(acuous?)q Fc(f)p Fd(q)r Fc(g)341 1517 y(\017)36 b Fe(for)16 b(ev)o(ery)f Fd(r)g Fe(:)f(ind)f Fd(*)h Fc(\003)65 b Fe(for)16 b(some)g Fd(v)f Fe(:)e(ind)49 b(conjunction)386 1577 y Fc(\016)19 b Fd(p)p Fe(\()p Fd(v)r Fe(\))11 b Fc(_)g Fe(non)o(v)m(acuous?)q Fc(f)p Fd(r)q Fc(g)386 1638 y(\016)19 b Fe(non)o(v)m(acuous?)q Fc(f)p Fd(r)q Fc(g)14 b(\033)g Fd(q)r Fe(\()p Fd(v)r Fe(\))p Fd(:)164 1789 y Fe(Apply)h Fb(insistent-direct-and-antecedent-inference-stra)l (tegy)e Fe(to)k(2.)164 1849 y(This)f(yields)164 1959 y Ff(Sequen)n(t)i(8.)j Fe(Let)c Fd(y)554 1967 y Fa($0)591 1959 y Fd(;)8 b(x)641 1967 y Fa($0)692 1959 y Fe(:)13 b(ind)p Fd(;)8 b(q)r(;)g(r)o(;)g(p)13 b Fe(:)g(ind)h Fd(*)f Fc(\003)p Fd(:)j Fe(Assume:)224 2123 y(0.)24 b Fd(p)p Fe(\()p Fd(x)357 2131 y Fa($0)394 2123 y Fe(\))p Fd(:)224 2225 y Fe(1.)g Fd(q)r Fe(\()p Fd(y)353 2233 y Fa($0)389 2225 y Fe(\))p Fd(:)164 2339 y Fe(Then)961 2607 y(1)p eop %%Page: 2 2 2 1 bop 205 315 a Fe(for)16 b(some)f Fd(v)h Fe(:)d(ind)48 b(conjunction)341 376 y Fc(\017)20 b Fe(disjunction)386 436 y Fc(\016)f Fd(p)p Fe(\()p Fd(v)r Fe(\))386 496 y Fc(\016)g Fe(non)o(v)m(acuous?)q Fc(f)p Fd(r)q Fc(g)341 556 y(\017)h Fe(implication)386 616 y Fc(\016)f Fe(non)o(v)m(acuous?)q Fc(f)p Fd(r)q Fc(g)386 677 y(\016)g Fd(q)r Fe(\()p Fd(v)r Fe(\))p Fd(:)164 841 y Fe(Instan)o(tiate)d(existen)o(tial)e(assertion)j (of)f(8)h(with)f(the)g(term)31 b(conditionally)219 901 y Fc(\017)36 b Fe(if)16 b(non)o(v)m(acuous?)q Fc(f)p Fd(r)q Fc(g)g Fe(then)g Fd(y)816 909 y Fa($0)219 961 y Fc(\017)36 b Fe(otherwise)16 b Fd(x)525 969 y Fa($0)562 961 y Fe(.)21 b(This)c(yields)180 1071 y Ff(Sequen)n(t)h(9.)k Fe(Let)16 b Fd(q)f Fe(:)f(ind)f Fd(*)h Fc(\003)p Fd(;)8 b(x)830 1079 y Fa($0)867 1071 y Fd(;)g(y)913 1079 y Fa($0)963 1071 y Fe(:)14 b(ind)p Fd(;)8 b(r)o(;)g(p)13 b Fe(:)h(ind)f Fd(*)h Fc(\003)p Fd(:)h Fe(Under)h(the)g(same)164 1131 y(assumptions)g(as)h(sequen)o(t)e(8,)i(w)o(e)e(ha)o(v)o(e:)188 1245 y(conjunction)341 1306 y Fc(\017)20 b Fe(disjunction)386 1366 y Fc(\016)f Fd(p)p Fe(\()e(if)e(non)o(v)m(acuous?)r Fc(f)p Fd(r)q Fc(g)h Fe(then)g Fd(y)1026 1373 y Fa($0)1080 1366 y Fe(otherwise)g Fd(x)1325 1373 y Fa($0)1362 1366 y Fe(\))386 1426 y Fc(\016)j Fe(non)o(v)m(acuous?)q Fc(f)p Fd(r)q Fc(g)341 1486 y(\017)h Fe(implication)386 1546 y Fc(\016)f Fe(non)o(v)m(acuous?)q Fc(f)p Fd(r)q Fc(g)386 1606 y(\016)g Fd(q)r Fe(\()d(if)f(non)o(v)m(acuous?)r Fc(f)p Fd(r)q Fc(g)h Fe(then)g Fd(y)1025 1614 y Fa($0)1078 1606 y Fe(otherwise)h Fd(x)1324 1614 y Fa($0)1361 1606 y Fe(\))p Fd(:)164 1770 y Fe(Apply)e Fb(case-split-on-conditionals)e Fe(to)k(9.)k(This)16 b(completes)f(the)h(pro)q(of.)961 2607 y(2)p eop %%Trailer end userdict /end-hook known{end-hook}if %%EOF