val tC8_2 = prove_goal C8cases.thy "[| dt = Der ($I |- $Y) cutr [Der IT tS [], Der TY tA [dtiy]] ; \ \ cutOnFmls {T} dt ; allDT wfb dt |] ==> \ \ allDT wfb dtiy & conclDT dtiy = ($I |- $Y)" (tacC8_2 [tA, tS]) ; val tC8'' = prove_goal C8cases.thy "[| dt = Der ($I |- $Y) cutr [Der IT tS [], Der TY tA [dtiy]] ; \ \ cutOnFmls {T} dt ; allDT wfb dt ; allDT (frb rls) dt ; \ \ allNextDTs (cutOnFmls {}) dt |] ==> \ \ EX dtn. conclDT dtn = conclDT dt & \ \ allDT wfb dtn & allDT (frb rls) dtn & allDT (cutOnFmls {}) dtn" (tacC8''con tC8_2) ; val tC8_1 = prove_goal C8cases.thy "[| dt = Der seq cutr dtl ; cutIsLRP T dt ; \ \ allDT wfb dt ; allDT (frb rls) dt |] ==> \ \ (EX dt':set dtl. conclDT dt' = seq) | \ \ (EX Y IT TY dtiy. \ \ dt = Der ($I |- $Y) cutr [Der IT tS [], Der TY tA [dtiy]])" (fn prems => [ EVERY (tacC8_1_1 prems), (EVERY (tacC8_1_2 [tA, tS] 3)), tacidf 1, tacidf 1]) ; val tC8 = prove_goal C8cases.thy "[| cutIsLRP T dt ; allDT wfb dt ; allDT (frb rls) dt ; \ \ allNextDTs (cutOnFmls {}) dt |] ==> \ \ EX dtn. conclDT dtn = conclDT dt & \ \ allDT wfb dtn & allDT (frb rls) dtn & allDT (cutOnFmls {}) dtn" (tacC8 tC8_1 (SOME tC8'')) ; val r1C8_2 = prove_goal C8cases.thy "[| dt = Der ($E |- $Y) cutr [Der IT r1S [], Der TY r1A [dtiy]] ; \ \ cutOnFmls {r1} dt ; allDT wfb dt |] ==> \ \ allDT wfb dtiy & conclDT dtiy = ($E |- $Y)" (tacC8_2 [r1A, r1S]) ; val r1C8'' = prove_goal C8cases.thy "[| dt = Der ($E |- $Y) cutr [Der IT r1S [], Der TY r1A [dtiy]] ; \ \ cutOnFmls {r1} dt ; allDT wfb dt ; allDT (frb rls) dt ; \ \ allNextDTs (cutOnFmls {}) dt |] ==> \ \ EX dtn. conclDT dtn = conclDT dt & \ \ allDT wfb dtn & allDT (frb rls) dtn & allDT (cutOnFmls {}) dtn" (tacC8''con r1C8_2) ; val r1C8_1 = prove_goal C8cases.thy "[| dt = Der seq cutr dtl ; cutIsLRP r1 dt ; \ \ allDT wfb dt ; allDT (frb rls) dt |] ==> \ \ (EX dt':set dtl. conclDT dt' = seq) | \ \ (EX Y IT TY dtiy. \ \ dt = Der ($E |- $Y) cutr [Der IT r1S [], Der TY r1A [dtiy]])" (fn prems => [ EVERY (tacC8_1_1 prems), EVERY (tacC8_1_2 [r1A, r1S] 3), tacidf 1, tacidf 1]) ; val r1C8 = prove_goal C8cases.thy "[| cutIsLRP r1 dt ; allDT wfb dt ; allDT (frb rls) dt ; \ \ allNextDTs (cutOnFmls {}) dt |] ==> \ \ EX dtn. conclDT dtn = conclDT dt & \ \ allDT wfb dtn & allDT (frb rls) dtn & allDT (cutOnFmls {}) dtn" (tacC8 r1C8_1 (SOME r1C8'')) ; val r0C8_2 = prove_goal C8cases.thy "[| dt = Der ($Y |- $E) cutr [Der IT r0S [dtiy], Der TY r0A []] ; \ \ cutOnFmls {r0} dt ; allDT wfb dt |] ==> \ \ allDT wfb dtiy & conclDT dtiy = ($Y |- $E)" (tacC8_2 [r0A, r0S]) ; val r0C8'' = prove_goal C8cases.thy "[| dt = Der ($Y |- $E) cutr [Der IT r0S [dtiy], Der TY r0A []] ; \ \ cutOnFmls {r0} dt ; allDT wfb dt ; allDT (frb rls) dt ; \ \ allNextDTs (cutOnFmls {}) dt |] ==> \ \ EX dtn. conclDT dtn = conclDT dt & \ \ allDT wfb dtn & allDT (frb rls) dtn & allDT (cutOnFmls {}) dtn" (tacC8''con r0C8_2) ; val r0C8_1 = prove_goal C8cases.thy "[| dt = Der seq cutr dtl ; cutIsLRP r0 dt ; \ \ allDT wfb dt ; allDT (frb rls) dt |] ==> \ \ (EX dt':set dtl. conclDT dt' = seq) | \ \ (EX Y IT TY dtiy. \ \ dt = Der ($Y |- $E) cutr [Der IT r0S [dtiy], Der TY r0A []])" (fn prems => [ EVERY (tacC8_1_1 prems), EVERY (tacC8_1_2 [r0A, r0S] 3), tacidf 1, tacidf 1]) ; val r0C8 = prove_goal C8cases.thy "[| cutIsLRP r0 dt ; allDT wfb dt ; allDT (frb rls) dt ; \ \ allNextDTs (cutOnFmls {}) dt |] ==> \ \ EX dtn. conclDT dtn = conclDT dt & \ \ allDT wfb dtn & allDT (frb rls) dtn & allDT (cutOnFmls {}) dtn" (tacC8 r0C8_1 (SOME r0C8'')) ; val fC8_2 = prove_goal C8cases.thy "[| dt = Der ($Y |- $I) cutr [Der IT fS [dtiy], Der TY fA []] ; \ \ cutOnFmls {F} dt ; allDT wfb dt |] ==> \ \ allDT wfb dtiy & conclDT dtiy = ($Y |- $I)" (tacC8_2 [fA, fS]) ; val fC8'' = prove_goal C8cases.thy "[| dt = Der ($Y |- $I) cutr [Der IT fS [dtiy], Der TY fA []] ; \ \ cutOnFmls {F} dt ; allDT wfb dt ; allDT (frb rls) dt ; \ \ allNextDTs (cutOnFmls {}) dt |] ==> \ \ EX dtn. conclDT dtn = conclDT dt & \ \ allDT wfb dtn & allDT (frb rls) dtn & allDT (cutOnFmls {}) dtn" (tacC8''con fC8_2) ; val fC8_1 = prove_goal C8cases.thy "[| dt = Der seq cutr dtl ; cutIsLRP F dt ; \ \ allDT wfb dt ; allDT (frb rls) dt |] ==> \ \ (EX dt':set dtl. conclDT dt' = seq) | \ \ (EX Y IT TY dtiy. \ \ dt = Der ($Y |- $I) cutr [Der IT fS [dtiy], Der TY fA []])" (fn prems => [ EVERY (tacC8_1_1 prems), (EVERY (tacC8_1_2 [fA, fS] 3)), tacidf 1, tacidf 1]) ; val fC8 = prove_goal C8cases.thy "[| cutIsLRP F dt ; allDT wfb dt ; allDT (frb rls) dt ; \ \ allNextDTs (cutOnFmls {}) dt |] ==> \ \ EX dtn. conclDT dtn = conclDT dt & \ \ allDT wfb dtn & allDT (frb rls) dtn & allDT (cutOnFmls {}) dtn" (tacC8 fC8_1 (SOME fC8'')) ; val FVC8_1 = prove_goal C8cases.thy "[| dt = Der seq cutr dtl ; cutIsLRP (FV s) dt ; \ \ allDT wfb dt ; allDT (frb rls) dt |] ==> \ \ (EX dt':set dtl. conclDT dt' = seq)" (fn prems => [ EVERY (tacC8_1_1 prems), tacidf 1]) ; val FVC8 = prove_goal C8cases.thy "[| cutIsLRP (FV s) dt ; allDT wfb dt ; allDT (frb rls) dt ; \ \ allNextDTs (cutOnFmls {}) dt |] ==> \ \ EX dtn. conclDT dtn = conclDT dt & \ \ allDT wfb dtn & allDT (frb rls) dtn & allDT (cutOnFmls {}) dtn" (tacC8 FVC8_1 NONE) ; val PPC8_1 = prove_goal C8cases.thy "[| dt = Der seq cutr dtl ; cutIsLRP (PP s) dt ; \ \ allDT wfb dt ; allDT (frb rls) dt |] ==> \ \ (EX dt':set dtl. conclDT dt' = seq)" (fn prems => [ EVERY (tacC8_1_1 prems), tacidf 1]) ; val PPC8 = prove_goal C8cases.thy "[| cutIsLRP (PP s) dt ; allDT wfb dt ; allDT (frb rls) dt ; \ \ allNextDTs (cutOnFmls {}) dt |] ==> \ \ EX dtn. conclDT dtn = conclDT dt & \ \ allDT wfb dtn & allDT (frb rls) dtn & allDT (cutOnFmls {}) dtn" (tacC8 PPC8_1 NONE) ; (* ; val prems = it ; *)