diff options
Diffstat (limited to 'etc/isar/AThousandTheorems.thy')
| -rw-r--r-- | etc/isar/AThousandTheorems.thy | 1008 |
1 files changed, 1008 insertions, 0 deletions
diff --git a/etc/isar/AThousandTheorems.thy b/etc/isar/AThousandTheorems.thy new file mode 100644 index 00000000..77be15b0 --- /dev/null +++ b/etc/isar/AThousandTheorems.thy @@ -0,0 +1,1008 @@ +theory AThousandLines imports Main +begin + +(* set global_timing *) + +lemma foo: "P --> P" by auto +lemma foo2: "P --> P" by auto +lemma foo3: "P --> P" by auto +lemma foo4: "P --> P" by auto +lemma foo5: "P --> P" by auto +lemma foo6: "P --> P" by auto +lemma foo7: "P --> P" by auto +lemma foo8: "P --> P" by auto +lemma foo9: "P --> P" by auto +lemma foo10: "P --> P" by auto +lemma foo11: "P --> P" by auto +lemma foo12: "P --> P" by auto +lemma foo13: "P --> P" by auto +lemma foo14: "P --> P" by auto +lemma foo15: "P --> P" by auto +lemma foo16: "P --> P" by auto +lemma foo17: "P --> P" by auto +lemma foo18: "P --> P" by auto +lemma foo19: "P --> P" by auto +lemma foo20: "P --> P" by auto +lemma foo21: "P --> P" by auto +lemma foo22: "P --> P" by auto +lemma foo23: "P --> P" by auto +lemma foo24: "P --> P" by auto +lemma foo25: "P --> P" by auto +lemma foo26: "P --> P" by auto +lemma foo27: "P --> P" by auto +lemma foo28: "P --> P" by auto +lemma foo29: "P --> P" by auto +lemma foo30: "P --> P" by auto +lemma foo31: "P --> P" by auto +lemma foo32: "P --> P" by auto +lemma foo33: "P --> P" by auto +lemma foo34: "P --> P" by auto +lemma foo35: "P --> P" by auto +lemma foo36: "P --> P" by auto +lemma foo37: "P --> P" by auto +lemma foo38: "P --> P" by auto +lemma foo39: "P --> P" by auto +lemma foo40: "P --> P" by auto +lemma foo41: "P --> P" by auto +lemma foo42: "P --> P" by auto +lemma foo43: "P --> P" by auto +lemma foo44: "P --> P" by auto +lemma foo45: "P --> P" by auto +lemma foo46: "P --> P" by auto +lemma foo47: "P --> P" by auto +lemma foo48: "P --> P" by auto +lemma foo49: "P --> P" by auto +lemma foo50: "P --> P" by auto +lemma foo51: "P --> P" by auto +lemma foo52: "P --> P" by auto +lemma foo53: "P --> P" by auto +lemma foo54: "P --> P" by auto +lemma foo55: "P --> P" by auto +lemma foo56: "P --> P" by auto +lemma foo57: "P --> P" by auto +lemma foo58: "P --> P" by auto +lemma foo59: "P --> P" by auto +lemma foo60: "P --> P" by auto +lemma foo61: "P --> P" by auto +lemma foo62: "P --> P" by auto +lemma foo63: "P --> P" by auto +lemma foo64: "P --> P" by auto +lemma foo65: "P --> P" by auto +lemma foo66: "P --> P" by auto +lemma foo67: "P --> P" by auto +lemma foo68: "P --> P" by auto +lemma foo69: "P --> P" by auto +lemma foo70: "P --> P" by auto +lemma foo71: "P --> P" by auto +lemma foo72: "P --> P" by auto +lemma foo73: "P --> P" by auto +lemma foo74: "P --> P" by auto +lemma foo75: "P --> P" by auto +lemma foo76: "P --> P" by auto +lemma foo77: "P --> P" by auto +lemma foo78: "P --> P" by auto +lemma foo79: "P --> P" by auto +lemma foo80: "P --> P" by auto +lemma foo81: "P --> P" by auto +lemma foo82: "P --> P" by auto +lemma foo83: "P --> P" by auto +lemma foo84: "P --> P" by auto +lemma foo85: "P --> P" by auto +lemma foo86: "P --> P" by auto +lemma foo87: "P --> P" by auto +lemma foo88: "P --> P" by auto +lemma foo89: "P --> P" by auto +lemma foo90: "P --> P" by auto +lemma foo91: "P --> P" by auto +lemma foo92: "P --> P" by auto +lemma foo93: "P --> P" by auto +lemma foo94: "P --> P" by auto +lemma foo95: "P --> P" by auto +lemma foo96: "P --> P" by auto +lemma foo97: "P --> P" by auto +lemma foo98: "P --> P" by auto +lemma foo99: "P --> P" by auto +lemma foo100: "P --> P" by auto +lemma foo101: "P --> P" by auto +lemma foo102: "P --> P" by auto +lemma foo103: "P --> P" by auto +lemma foo104: "P --> P" by auto +lemma foo105: "P --> P" by auto +lemma foo106: "P --> P" by auto +lemma foo107: "P --> P" by auto +lemma foo108: "P --> P" by auto +lemma foo109: "P --> P" by auto +lemma foo110: "P --> P" by auto +lemma foo111: "P --> P" by auto +lemma foo112: "P --> P" by auto +lemma foo113: "P --> P" by auto +lemma foo114: "P --> P" by auto +lemma foo115: "P --> P" by auto +lemma foo116: "P --> P" by auto +lemma foo117: "P --> P" by auto +lemma foo118: "P --> P" by auto +lemma foo119: "P --> P" by auto +lemma foo120: "P --> P" by auto +lemma foo121: "P --> P" by auto +lemma foo122: "P --> P" by auto +lemma foo123: "P --> P" by auto +lemma foo124: "P --> P" by auto +lemma foo125: "P --> P" by auto +lemma foo126: "P --> P" by auto +lemma foo127: "P --> P" by auto +lemma foo128: "P --> P" by auto +lemma foo129: "P --> P" by auto +lemma foo130: "P --> P" by auto +lemma foo131: "P --> P" by auto +lemma foo132: "P --> P" by auto +lemma foo133: "P --> P" by auto +lemma foo134: "P --> P" by auto +lemma foo135: "P --> P" by auto +lemma foo136: "P --> P" by auto +lemma foo137: "P --> P" by auto +lemma foo138: "P --> P" by auto +lemma foo139: "P --> P" by auto +lemma foo140: "P --> P" by auto +lemma foo141: "P --> P" by auto +lemma foo142: "P --> P" by auto +lemma foo143: "P --> P" by auto +lemma foo144: "P --> P" by auto +lemma foo145: "P --> P" by auto +lemma foo146: "P --> P" by auto +lemma foo147: "P --> P" by auto +lemma foo148: "P --> P" by auto +lemma foo149: "P --> P" by auto +lemma foo150: "P --> P" by auto +lemma foo151: "P --> P" by auto +lemma foo152: "P --> P" by auto +lemma foo153: "P --> P" by auto +lemma foo154: "P --> P" by auto +lemma foo155: "P --> P" by auto +lemma foo156: "P --> P" by auto +lemma foo157: "P --> P" by auto +lemma foo158: "P --> P" by auto +lemma foo159: "P --> P" by auto +lemma foo160: "P --> P" by auto +lemma foo161: "P --> P" by auto +lemma foo162: "P --> P" by auto +lemma foo163: "P --> P" by auto +lemma foo164: "P --> P" by auto +lemma foo165: "P --> P" by auto +lemma foo166: "P --> P" by auto +lemma foo167: "P --> P" by auto +lemma foo168: "P --> P" by auto +lemma foo169: "P --> P" by auto +lemma foo170: "P --> P" by auto +lemma foo171: "P --> P" by auto +lemma foo172: "P --> P" by auto +lemma foo173: "P --> P" by auto +lemma foo174: "P --> P" by auto +lemma foo175: "P --> P" by auto +lemma foo176: "P --> P" by auto +lemma foo177: "P --> P" by auto +lemma foo178: "P --> P" by auto +lemma foo179: "P --> P" by auto +lemma foo180: "P --> P" by auto +lemma foo181: "P --> P" by auto +lemma foo182: "P --> P" by auto +lemma foo183: "P --> P" by auto +lemma foo184: "P --> P" by auto +lemma foo185: "P --> P" by auto +lemma foo186: "P --> P" by auto +lemma foo187: "P --> P" by auto +lemma foo188: "P --> P" by auto +lemma foo189: "P --> P" by auto +lemma foo190: "P --> P" by auto +lemma foo191: "P --> P" by auto +lemma foo192: "P --> P" by auto +lemma foo193: "P --> P" by auto +lemma foo194: "P --> P" by auto +lemma foo195: "P --> P" by auto +lemma foo196: "P --> P" by auto +lemma foo197: "P --> P" by auto +lemma foo198: "P --> P" by auto +lemma foo199: "P --> P" by auto +lemma foo200: "P --> P" by auto +lemma foo201: "P --> P" by auto +lemma foo202: "P --> P" by auto +lemma foo203: "P --> P" by auto +lemma foo204: "P --> P" by auto +lemma foo205: "P --> P" by auto +lemma foo206: "P --> P" by auto +lemma foo207: "P --> P" by auto +lemma foo208: "P --> P" by auto +lemma foo209: "P --> P" by auto +lemma foo210: "P --> P" by auto +lemma foo211: "P --> P" by auto +lemma foo212: "P --> P" by auto +lemma foo213: "P --> P" by auto +lemma foo214: "P --> P" by auto +lemma foo215: "P --> P" by auto +lemma foo216: "P --> P" by auto +lemma foo217: "P --> P" by auto +lemma foo218: "P --> P" by auto +lemma foo219: "P --> P" by auto +lemma foo220: "P --> P" by auto +lemma foo221: "P --> P" by auto +lemma foo222: "P --> P" by auto +lemma foo223: "P --> P" by auto +lemma foo224: "P --> P" by auto +lemma foo225: "P --> P" by auto +lemma foo226: "P --> P" by auto +lemma foo227: "P --> P" by auto +lemma foo228: "P --> P" by auto +lemma foo229: "P --> P" by auto +lemma foo230: "P --> P" by auto +lemma foo231: "P --> P" by auto +lemma foo232: "P --> P" by auto +lemma foo233: "P --> P" by auto +lemma foo234: "P --> P" by auto +lemma foo235: "P --> P" by auto +lemma foo236: "P --> P" by auto +lemma foo237: "P --> P" by auto +lemma foo238: "P --> P" by auto +lemma foo239: "P --> P" by auto +lemma foo240: "P --> P" by auto +lemma foo241: "P --> P" by auto +lemma foo242: "P --> P" by auto +lemma foo243: "P --> P" by auto +lemma foo244: "P --> P" by auto +lemma foo245: "P --> P" by auto +lemma foo246: "P --> P" by auto +lemma foo247: "P --> P" by auto +lemma foo248: "P --> P" by auto +lemma foo249: "P --> P" by auto +lemma foo250: "P --> P" by auto +lemma foo251: "P --> P" by auto +lemma foo252: "P --> P" by auto +lemma foo253: "P --> P" by auto +lemma foo254: "P --> P" by auto +lemma foo255: "P --> P" by auto +lemma foo256: "P --> P" by auto +lemma foo257: "P --> P" by auto +lemma foo258: "P --> P" by auto +lemma foo259: "P --> P" by auto +lemma foo260: "P --> P" by auto +lemma foo261: "P --> P" by auto +lemma foo262: "P --> P" by auto +lemma foo263: "P --> P" by auto +lemma foo264: "P --> P" by auto +lemma foo265: "P --> P" by auto +lemma foo266: "P --> P" by auto +lemma foo267: "P --> P" by auto +lemma foo268: "P --> P" by auto +lemma foo269: "P --> P" by auto +lemma foo270: "P --> P" by auto +lemma foo271: "P --> P" by auto +lemma foo272: "P --> P" by auto +lemma foo273: "P --> P" by auto +lemma foo274: "P --> P" by auto +lemma foo275: "P --> P" by auto +lemma foo276: "P --> P" by auto +lemma foo277: "P --> P" by auto +lemma foo278: "P --> P" by auto +lemma foo279: "P --> P" by auto +lemma foo280: "P --> P" by auto +lemma foo281: "P --> P" by auto +lemma foo282: "P --> P" by auto +lemma foo283: "P --> P" by auto +lemma foo284: "P --> P" by auto +lemma foo285: "P --> P" by auto +lemma foo286: "P --> P" by auto +lemma foo287: "P --> P" by auto +lemma foo288: "P --> P" by auto +lemma foo289: "P --> P" by auto +lemma foo290: "P --> P" by auto +lemma foo291: "P --> P" by auto +lemma foo292: "P --> P" by auto +lemma foo293: "P --> P" by auto +lemma foo294: "P --> P" by auto +lemma foo295: "P --> P" by auto +lemma foo296: "P --> P" by auto +lemma foo297: "P --> P" by auto +lemma foo298: "P --> P" by auto +lemma foo299: "P --> P" by auto +lemma foo300: "P --> P" by auto +lemma foo301: "P --> P" by auto +lemma foo302: "P --> P" by auto +lemma foo303: "P --> P" by auto +lemma foo304: "P --> P" by auto +lemma foo305: "P --> P" by auto +lemma foo306: "P --> P" by auto +lemma foo307: "P --> P" by auto +lemma foo308: "P --> P" by auto +lemma foo309: "P --> P" by auto +lemma foo310: "P --> P" by auto +lemma foo311: "P --> P" by auto +lemma foo312: "P --> P" by auto +lemma foo313: "P --> P" by auto +lemma foo314: "P --> P" by auto +lemma foo315: "P --> P" by auto +lemma foo316: "P --> P" by auto +lemma foo317: "P --> P" by auto +lemma foo318: "P --> P" by auto +lemma foo319: "P --> P" by auto +lemma foo320: "P --> P" by auto +lemma foo321: "P --> P" by auto +lemma foo322: "P --> P" by auto +lemma foo323: "P --> P" by auto +lemma foo324: "P --> P" by auto +lemma foo325: "P --> P" by auto +lemma foo326: "P --> P" by auto +lemma foo327: "P --> P" by auto +lemma foo328: "P --> P" by auto +lemma foo329: "P --> P" by auto +lemma foo330: "P --> P" by auto +lemma foo331: "P --> P" by auto +lemma foo332: "P --> P" by auto +lemma foo333: "P --> P" by auto +lemma foo334: "P --> P" by auto +lemma foo335: "P --> P" by auto +lemma foo336: "P --> P" by auto +lemma foo337: "P --> P" by auto +lemma foo338: "P --> P" by auto +lemma foo339: "P --> P" by auto +lemma foo340: "P --> P" by auto +lemma foo341: "P --> P" by auto +lemma foo342: "P --> P" by auto +lemma foo343: "P --> P" by auto +lemma foo344: "P --> P" by auto +lemma foo345: "P --> P" by auto +lemma foo346: "P --> P" by auto +lemma foo347: "P --> P" by auto +lemma foo348: "P --> P" by auto +lemma foo349: "P --> P" by auto +lemma foo350: "P --> P" by auto +lemma foo351: "P --> P" by auto +lemma foo352: "P --> P" by auto +lemma foo353: "P --> P" by auto +lemma foo354: "P --> P" by auto +lemma foo355: "P --> P" by auto +lemma foo356: "P --> P" by auto +lemma foo357: "P --> P" by auto +lemma foo358: "P --> P" by auto +lemma foo359: "P --> P" by auto +lemma foo360: "P --> P" by auto +lemma foo361: "P --> P" by auto +lemma foo362: "P --> P" by auto +lemma foo363: "P --> P" by auto +lemma foo364: "P --> P" by auto +lemma foo365: "P --> P" by auto +lemma foo366: "P --> P" by auto +lemma foo367: "P --> P" by auto +lemma foo368: "P --> P" by auto +lemma foo369: "P --> P" by auto +lemma foo370: "P --> P" by auto +lemma foo371: "P --> P" by auto +lemma foo372: "P --> P" by auto +lemma foo373: "P --> P" by auto +lemma foo374: "P --> P" by auto +lemma foo375: "P --> P" by auto +lemma foo376: "P --> P" by auto +lemma foo377: "P --> P" by auto +lemma foo378: "P --> P" by auto +lemma foo379: "P --> P" by auto +lemma foo380: "P --> P" by auto +lemma foo381: "P --> P" by auto +lemma foo382: "P --> P" by auto +lemma foo383: "P --> P" by auto +lemma foo384: "P --> P" by auto +lemma foo385: "P --> P" by auto +lemma foo386: "P --> P" by auto +lemma foo387: "P --> P" by auto +lemma foo388: "P --> P" by auto +lemma foo389: "P --> P" by auto +lemma foo390: "P --> P" by auto +lemma foo391: "P --> P" by auto +lemma foo392: "P --> P" by auto +lemma foo393: "P --> P" by auto +lemma foo394: "P --> P" by auto +lemma foo395: "P --> P" by auto +lemma foo396: "P --> P" by auto +lemma foo397: "P --> P" by auto +lemma foo398: "P --> P" by auto +lemma foo399: "P --> P" by auto +lemma foo400: "P --> P" by auto +lemma foo401: "P --> P" by auto +lemma foo402: "P --> P" by auto +lemma foo403: "P --> P" by auto +lemma foo404: "P --> P" by auto +lemma foo405: "P --> P" by auto +lemma foo406: "P --> P" by auto +lemma foo407: "P --> P" by auto +lemma foo408: "P --> P" by auto +lemma foo409: "P --> P" by auto +lemma foo410: "P --> P" by auto +lemma foo411: "P --> P" by auto +lemma foo412: "P --> P" by auto +lemma foo413: "P --> P" by auto +lemma foo414: "P --> P" by auto +lemma foo415: "P --> P" by auto +lemma foo416: "P --> P" by auto +lemma foo417: "P --> P" by auto +lemma foo418: "P --> P" by auto +lemma foo419: "P --> P" by auto +lemma foo420: "P --> P" by auto +lemma foo421: "P --> P" by auto +lemma foo422: "P --> P" by auto +lemma foo423: "P --> P" by auto +lemma foo424: "P --> P" by auto +lemma foo425: "P --> P" by auto +lemma foo426: "P --> P" by auto +lemma foo427: "P --> P" by auto +lemma foo428: "P --> P" by auto +lemma foo429: "P --> P" by auto +lemma foo430: "P --> P" by auto +lemma foo431: "P --> P" by auto +lemma foo432: "P --> P" by auto +lemma foo433: "P --> P" by auto +lemma foo434: "P --> P" by auto +lemma foo435: "P --> P" by auto +lemma foo436: "P --> P" by auto +lemma foo437: "P --> P" by auto +lemma foo438: "P --> P" by auto +lemma foo439: "P --> P" by auto +lemma foo440: "P --> P" by auto +lemma foo441: "P --> P" by auto +lemma foo442: "P --> P" by auto +lemma foo443: "P --> P" by auto +lemma foo444: "P --> P" by auto +lemma foo445: "P --> P" by auto +lemma foo446: "P --> P" by auto +lemma foo447: "P --> P" by auto +lemma foo448: "P --> P" by auto +lemma foo449: "P --> P" by auto +lemma foo450: "P --> P" by auto +lemma foo451: "P --> P" by auto +lemma foo452: "P --> P" by auto +lemma foo453: "P --> P" by auto +lemma foo454: "P --> P" by auto +lemma foo455: "P --> P" by auto +lemma foo456: "P --> P" by auto +lemma foo457: "P --> P" by auto +lemma foo458: "P --> P" by auto +lemma foo459: "P --> P" by auto +lemma foo460: "P --> P" by auto +lemma foo461: "P --> P" by auto +lemma foo462: "P --> P" by auto +lemma foo463: "P --> P" by auto +lemma foo464: "P --> P" by auto +lemma foo465: "P --> P" by auto +lemma foo466: "P --> P" by auto +lemma foo467: "P --> P" by auto +lemma foo468: "P --> P" by auto +lemma foo469: "P --> P" by auto +lemma foo470: "P --> P" by auto +lemma foo471: "P --> P" by auto +lemma foo472: "P --> P" by auto +lemma foo473: "P --> P" by auto +lemma foo474: "P --> P" by auto +lemma foo475: "P --> P" by auto +lemma foo476: "P --> P" by auto +lemma foo477: "P --> P" by auto +lemma foo478: "P --> P" by auto +lemma foo479: "P --> P" by auto +lemma foo480: "P --> P" by auto +lemma foo481: "P --> P" by auto +lemma foo482: "P --> P" by auto +lemma foo483: "P --> P" by auto +lemma foo484: "P --> P" by auto +lemma foo485: "P --> P" by auto +lemma foo486: "P --> P" by auto +lemma foo487: "P --> P" by auto +lemma foo488: "P --> P" by auto +lemma foo489: "P --> P" by auto +lemma foo490: "P --> P" by auto +lemma foo491: "P --> P" by auto +lemma foo492: "P --> P" by auto +lemma foo493: "P --> P" by auto +lemma foo494: "P --> P" by auto +lemma foo495: "P --> P" by auto +lemma foo496: "P --> P" by auto +lemma foo497: "P --> P" by auto +lemma foo498: "P --> P" by auto +lemma foo499: "P --> P" by auto +lemma foo500: "P --> P" by auto +(*lemma foo500: "P --> P" by auto *) +lemma foo501: "P --> P" by auto +lemma foo502: "P --> P" by auto +lemma foo503: "P --> P" by auto +lemma foo504: "P --> P" by auto +lemma foo505: "P --> P" by auto +lemma foo506: "P --> P" by auto +lemma foo507: "P --> P" by auto +lemma foo508: "P --> P" by auto +lemma foo509: "P --> P" by auto +lemma foo510: "P --> P" by auto +lemma foo511: "P --> P" by auto +lemma foo512: "P --> P" by auto +lemma foo513: "P --> P" by auto +lemma foo514: "P --> P" by auto +lemma foo515: "P --> P" by auto +lemma foo516: "P --> P" by auto +lemma foo517: "P --> P" by auto +lemma foo518: "P --> P" by auto +lemma foo519: "P --> P" by auto +lemma foo520: "P --> P" by auto +lemma foo521: "P --> P" by auto +lemma foo522: "P --> P" by auto +lemma foo523: "P --> P" by auto +lemma foo524: "P --> P" by auto +lemma foo525: "P --> P" by auto +lemma foo526: "P --> P" by auto +lemma foo527: "P --> P" by auto +lemma foo528: "P --> P" by auto +lemma foo529: "P --> P" by auto +lemma foo530: "P --> P" by auto +lemma foo531: "P --> P" by auto +lemma foo532: "P --> P" by auto +lemma foo533: "P --> P" by auto +lemma foo534: "P --> P" by auto +lemma foo535: "P --> P" by auto +lemma foo536: "P --> P" by auto +lemma foo537: "P --> P" by auto +lemma foo538: "P --> P" by auto +lemma foo539: "P --> P" by auto +lemma foo540: "P --> P" by auto +lemma foo541: "P --> P" by auto +lemma foo542: "P --> P" by auto +lemma foo543: "P --> P" by auto +lemma foo544: "P --> P" by auto +lemma foo545: "P --> P" by auto +lemma foo546: "P --> P" by auto +lemma foo547: "P --> P" by auto +lemma foo548: "P --> P" by auto +lemma foo549: "P --> P" by auto +lemma foo550: "P --> P" by auto +lemma foo551: "P --> P" by auto +lemma foo552: "P --> P" by auto +lemma foo553: "P --> P" by auto +lemma foo554: "P --> P" by auto +lemma foo555: "P --> P" by auto +lemma foo556: "P --> P" by auto +lemma foo557: "P --> P" by auto +lemma foo558: "P --> P" by auto +lemma foo559: "P --> P" by auto +lemma foo560: "P --> P" by auto +lemma foo561: "P --> P" by auto +lemma foo562: "P --> P" by auto +lemma foo563: "P --> P" by auto +lemma foo564: "P --> P" by auto +lemma foo565: "P --> P" by auto +lemma foo566: "P --> P" by auto +lemma foo567: "P --> P" by auto +lemma foo568: "P --> P" by auto +lemma foo569: "P --> P" by auto +lemma foo570: "P --> P" by auto +lemma foo571: "P --> P" by auto +lemma foo572: "P --> P" by auto +lemma foo573: "P --> P" by auto +lemma foo574: "P --> P" by auto +lemma foo575: "P --> P" by auto +lemma foo576: "P --> P" by auto +lemma foo577: "P --> P" by auto +lemma foo578: "P --> P" by auto +lemma foo579: "P --> P" by auto +lemma foo580: "P --> P" by auto +lemma foo581: "P --> P" by auto +lemma foo582: "P --> P" by auto +lemma foo583: "P --> P" by auto +lemma foo584: "P --> P" by auto +lemma foo585: "P --> P" by auto +lemma foo586: "P --> P" by auto +lemma foo587: "P --> P" by auto +lemma foo588: "P --> P" by auto +lemma foo589: "P --> P" by auto +lemma foo590: "P --> P" by auto +lemma foo591: "P --> P" by auto +lemma foo592: "P --> P" by auto +lemma foo593: "P --> P" by auto +lemma foo594: "P --> P" by auto +lemma foo595: "P --> P" by auto +lemma foo596: "P --> P" by auto +lemma foo597: "P --> P" by auto +lemma foo598: "P --> P" by auto +lemma foo599: "P --> P" by auto +lemma foo600: "P --> P" by auto +lemma foo601: "P --> P" by auto +lemma foo602: "P --> P" by auto +lemma foo603: "P --> P" by auto +lemma foo604: "P --> P" by auto +lemma foo605: "P --> P" by auto +lemma foo606: "P --> P" by auto +lemma foo607: "P --> P" by auto +lemma foo608: "P --> P" by auto +lemma foo609: "P --> P" by auto +lemma foo610: "P --> P" by auto +lemma foo611: "P --> P" by auto +lemma foo612: "P --> P" by auto +lemma foo613: "P --> P" by auto +lemma foo614: "P --> P" by auto +lemma foo615: "P --> P" by auto +lemma foo616: "P --> P" by auto +lemma foo617: "P --> P" by auto +lemma foo618: "P --> P" by auto +lemma foo619: "P --> P" by auto +lemma foo620: "P --> P" by auto +lemma foo621: "P --> P" by auto +lemma foo622: "P --> P" by auto +lemma foo623: "P --> P" by auto +lemma foo624: "P --> P" by auto +lemma foo625: "P --> P" by auto +lemma foo626: "P --> P" by auto +lemma foo627: "P --> P" by auto +lemma foo628: "P --> P" by auto +lemma foo629: "P --> P" by auto +lemma foo630: "P --> P" by auto +lemma foo631: "P --> P" by auto +lemma foo632: "P --> P" by auto +lemma foo633: "P --> P" by auto +lemma foo634: "P --> P" by auto +lemma foo635: "P --> P" by auto +lemma foo636: "P --> P" by auto +lemma foo637: "P --> P" by auto +lemma foo638: "P --> P" by auto +lemma foo639: "P --> P" by auto +lemma foo640: "P --> P" by auto +lemma foo641: "P --> P" by auto +lemma foo642: "P --> P" by auto +lemma foo643: "P --> P" by auto +lemma foo644: "P --> P" by auto +lemma foo645: "P --> P" by auto +lemma foo646: "P --> P" by auto +lemma foo647: "P --> P" by auto +lemma foo648: "P --> P" by auto +lemma foo649: "P --> P" by auto +lemma foo650: "P --> P" by auto +lemma foo651: "P --> P" by auto +lemma foo652: "P --> P" by auto +lemma foo653: "P --> P" by auto +lemma foo654: "P --> P" by auto +lemma foo655: "P --> P" by auto +lemma foo656: "P --> P" by auto +lemma foo657: "P --> P" by auto +lemma foo658: "P --> P" by auto +lemma foo659: "P --> P" by auto +lemma foo660: "P --> P" by auto +lemma foo661: "P --> P" by auto +lemma foo662: "P --> P" by auto +lemma foo663: "P --> P" by auto +lemma foo664: "P --> P" by auto +lemma foo665: "P --> P" by auto +lemma foo666: "P --> P" by auto +lemma foo667: "P --> P" by auto +lemma foo668: "P --> P" by auto +lemma foo669: "P --> P" by auto +lemma foo670: "P --> P" by auto +lemma foo671: "P --> P" by auto +lemma foo672: "P --> P" by auto +lemma foo673: "P --> P" by auto +lemma foo674: "P --> P" by auto +lemma foo675: "P --> P" by auto +lemma foo676: "P --> P" by auto +lemma foo677: "P --> P" by auto +lemma foo678: "P --> P" by auto +lemma foo679: "P --> P" by auto +lemma foo680: "P --> P" by auto +lemma foo681: "P --> P" by auto +lemma foo682: "P --> P" by auto +lemma foo683: "P --> P" by auto +lemma foo684: "P --> P" by auto +lemma foo685: "P --> P" by auto +lemma foo686: "P --> P" by auto +lemma foo687: "P --> P" by auto +lemma foo688: "P --> P" by auto +lemma foo689: "P --> P" by auto +lemma foo690: "P --> P" by auto +lemma foo691: "P --> P" by auto +lemma foo692: "P --> P" by auto +lemma foo693: "P --> P" by auto +lemma foo694: "P --> P" by auto +lemma foo695: "P --> P" by auto +lemma foo696: "P --> P" by auto +lemma foo697: "P --> P" by auto +lemma foo698: "P --> P" by auto +lemma foo699: "P --> P" by auto +lemma foo700: "P --> P" by auto +lemma foo701: "P --> P" by auto +lemma foo702: "P --> P" by auto +lemma foo703: "P --> P" by auto +lemma foo704: "P --> P" by auto +lemma foo705: "P --> P" by auto +lemma foo706: "P --> P" by auto +lemma foo707: "P --> P" by auto +lemma foo708: "P --> P" by auto +lemma foo709: "P --> P" by auto +lemma foo710: "P --> P" by auto +lemma foo711: "P --> P" by auto +lemma foo712: "P --> P" by auto +lemma foo713: "P --> P" by auto +lemma foo714: "P --> P" by auto +lemma foo715: "P --> P" by auto +lemma foo716: "P --> P" by auto +lemma foo717: "P --> P" by auto +lemma foo718: "P --> P" by auto +lemma foo719: "P --> P" by auto +lemma foo720: "P --> P" by auto +lemma foo721: "P --> P" by auto +lemma foo722: "P --> P" by auto +lemma foo723: "P --> P" by auto +lemma foo724: "P --> P" by auto +lemma foo725: "P --> P" by auto +lemma foo726: "P --> P" by auto +lemma foo727: "P --> P" by auto +lemma foo728: "P --> P" by auto +lemma foo729: "P --> P" by auto +lemma foo730: "P --> P" by auto +lemma foo731: "P --> P" by auto +lemma foo732: "P --> P" by auto +lemma foo733: "P --> P" by auto +lemma foo734: "P --> P" by auto +lemma foo735: "P --> P" by auto +lemma foo736: "P --> P" by auto +lemma foo737: "P --> P" by auto +lemma foo738: "P --> P" by auto +lemma foo739: "P --> P" by auto +lemma foo740: "P --> P" by auto +lemma foo741: "P --> P" by auto +lemma foo742: "P --> P" by auto +lemma foo743: "P --> P" by auto +lemma foo744: "P --> P" by auto +lemma foo745: "P --> P" by auto +lemma foo746: "P --> P" by auto +lemma foo747: "P --> P" by auto +lemma foo748: "P --> P" by auto +lemma foo749: "P --> P" by auto +lemma foo750: "P --> P" by auto +lemma foo751: "P --> P" by auto +lemma foo752: "P --> P" by auto +lemma foo753: "P --> P" by auto +lemma foo754: "P --> P" by auto +lemma foo755: "P --> P" by auto +lemma foo756: "P --> P" by auto +lemma foo757: "P --> P" by auto +lemma foo758: "P --> P" by auto +lemma foo759: "P --> P" by auto +lemma foo760: "P --> P" by auto +lemma foo761: "P --> P" by auto +lemma foo762: "P --> P" by auto +lemma foo763: "P --> P" by auto +lemma foo764: "P --> P" by auto +lemma foo765: "P --> P" by auto +lemma foo766: "P --> P" by auto +lemma foo767: "P --> P" by auto +lemma foo768: "P --> P" by auto +lemma foo769: "P --> P" by auto +lemma foo770: "P --> P" by auto +lemma foo771: "P --> P" by auto +lemma foo772: "P --> P" by auto +lemma foo773: "P --> P" by auto +lemma foo774: "P --> P" by auto +lemma foo775: "P --> P" by auto +lemma foo776: "P --> P" by auto +lemma foo777: "P --> P" by auto +lemma foo778: "P --> P" by auto +lemma foo779: "P --> P" by auto +lemma foo780: "P --> P" by auto +lemma foo781: "P --> P" by auto +lemma foo782: "P --> P" by auto +lemma foo783: "P --> P" by auto +lemma foo784: "P --> P" by auto +lemma foo785: "P --> P" by auto +lemma foo786: "P --> P" by auto +lemma foo787: "P --> P" by auto +lemma foo788: "P --> P" by auto +lemma foo789: "P --> P" by auto +lemma foo790: "P --> P" by auto +lemma foo791: "P --> P" by auto +lemma foo792: "P --> P" by auto +lemma foo793: "P --> P" by auto +lemma foo794: "P --> P" by auto +lemma foo795: "P --> P" by auto +lemma foo796: "P --> P" by auto +lemma foo797: "P --> P" by auto +lemma foo798: "P --> P" by auto +lemma foo799: "P --> P" by auto +lemma foo800: "P --> P" by auto +lemma foo801: "P --> P" by auto +lemma foo802: "P --> P" by auto +lemma foo803: "P --> P" by auto +lemma foo804: "P --> P" by auto +lemma foo805: "P --> P" by auto +lemma foo806: "P --> P" by auto +lemma foo807: "P --> P" by auto +lemma foo808: "P --> P" by auto +lemma foo809: "P --> P" by auto +lemma foo810: "P --> P" by auto +lemma foo811: "P --> P" by auto +lemma foo812: "P --> P" by auto +lemma foo813: "P --> P" by auto +lemma foo814: "P --> P" by auto +lemma foo815: "P --> P" by auto +lemma foo816: "P --> P" by auto +lemma foo817: "P --> P" by auto +lemma foo818: "P --> P" by auto +lemma foo819: "P --> P" by auto +lemma foo820: "P --> P" by auto +lemma foo821: "P --> P" by auto +lemma foo822: "P --> P" by auto +lemma foo823: "P --> P" by auto +lemma foo824: "P --> P" by auto +lemma foo825: "P --> P" by auto +lemma foo826: "P --> P" by auto +lemma foo827: "P --> P" by auto +lemma foo828: "P --> P" by auto +lemma foo829: "P --> P" by auto +lemma foo830: "P --> P" by auto +lemma foo831: "P --> P" by auto +lemma foo832: "P --> P" by auto +lemma foo833: "P --> P" by auto +lemma foo834: "P --> P" by auto +lemma foo835: "P --> P" by auto +lemma foo836: "P --> P" by auto +lemma foo837: "P --> P" by auto +lemma foo838: "P --> P" by auto +lemma foo839: "P --> P" by auto +lemma foo840: "P --> P" by auto +lemma foo841: "P --> P" by auto +lemma foo842: "P --> P" by auto +lemma foo843: "P --> P" by auto +lemma foo844: "P --> P" by auto +lemma foo845: "P --> P" by auto +lemma foo846: "P --> P" by auto +lemma foo847: "P --> P" by auto +lemma foo848: "P --> P" by auto +lemma foo849: "P --> P" by auto +lemma foo850: "P --> P" by auto +lemma foo851: "P --> P" by auto +lemma foo852: "P --> P" by auto +lemma foo853: "P --> P" by auto +lemma foo854: "P --> P" by auto +lemma foo855: "P --> P" by auto +lemma foo856: "P --> P" by auto +lemma foo857: "P --> P" by auto +lemma foo858: "P --> P" by auto +lemma foo859: "P --> P" by auto +lemma foo860: "P --> P" by auto +lemma foo861: "P --> P" by auto +lemma foo862: "P --> P" by auto +lemma foo863: "P --> P" by auto +lemma foo864: "P --> P" by auto +lemma foo865: "P --> P" by auto +lemma foo866: "P --> P" by auto +lemma foo867: "P --> P" by auto +lemma foo868: "P --> P" by auto +lemma foo869: "P --> P" by auto +lemma foo870: "P --> P" by auto +lemma foo871: "P --> P" by auto +lemma foo872: "P --> P" by auto +lemma foo873: "P --> P" by auto +lemma foo874: "P --> P" by auto +lemma foo875: "P --> P" by auto +lemma foo876: "P --> P" by auto +lemma foo877: "P --> P" by auto +lemma foo878: "P --> P" by auto +lemma foo879: "P --> P" by auto +lemma foo880: "P --> P" by auto +lemma foo881: "P --> P" by auto +lemma foo882: "P --> P" by auto +lemma foo883: "P --> P" by auto +lemma foo884: "P --> P" by auto +lemma foo885: "P --> P" by auto +lemma foo886: "P --> P" by auto +lemma foo887: "P --> P" by auto +lemma foo888: "P --> P" by auto +lemma foo889: "P --> P" by auto +lemma foo890: "P --> P" by auto +lemma foo891: "P --> P" by auto +lemma foo892: "P --> P" by auto +lemma foo893: "P --> P" by auto +lemma foo894: "P --> P" by auto +lemma foo895: "P --> P" by auto +lemma foo896: "P --> P" by auto +lemma foo897: "P --> P" by auto +lemma foo898: "P --> P" by auto +lemma foo899: "P --> P" by auto +lemma foo900: "P --> P" by auto +lemma foo901: "P --> P" by auto +lemma foo902: "P --> P" by auto +lemma foo903: "P --> P" by auto +lemma foo904: "P --> P" by auto +lemma foo905: "P --> P" by auto +lemma foo906: "P --> P" by auto +lemma foo907: "P --> P" by auto +lemma foo908: "P --> P" by auto +lemma foo909: "P --> P" by auto +lemma foo910: "P --> P" by auto +lemma foo911: "P --> P" by auto +lemma foo912: "P --> P" by auto +lemma foo913: "P --> P" by auto +lemma foo914: "P --> P" by auto +lemma foo915: "P --> P" by auto +lemma foo916: "P --> P" by auto +lemma foo917: "P --> P" by auto +lemma foo918: "P --> P" by auto +lemma foo919: "P --> P" by auto +lemma foo920: "P --> P" by auto +lemma foo921: "P --> P" by auto +lemma foo922: "P --> P" by auto +lemma foo923: "P --> P" by auto +lemma foo924: "P --> P" by auto +lemma foo925: "P --> P" by auto +lemma foo926: "P --> P" by auto +lemma foo927: "P --> P" by auto +lemma foo928: "P --> P" by auto +lemma foo929: "P --> P" by auto +lemma foo930: "P --> P" by auto +lemma foo931: "P --> P" by auto +lemma foo932: "P --> P" by auto +lemma foo933: "P --> P" by auto +lemma foo934: "P --> P" by auto +lemma foo935: "P --> P" by auto +lemma foo936: "P --> P" by auto +lemma foo937: "P --> P" by auto +lemma foo938: "P --> P" by auto +lemma foo939: "P --> P" by auto +lemma foo940: "P --> P" by auto +lemma foo941: "P --> P" by auto +lemma foo942: "P --> P" by auto +lemma foo943: "P --> P" by auto +lemma foo944: "P --> P" by auto +lemma foo945: "P --> P" by auto +lemma foo946: "P --> P" by auto +lemma foo947: "P --> P" by auto +lemma foo948: "P --> P" by auto +lemma foo949: "P --> P" by auto +lemma foo950: "P --> P" by auto +lemma foo951: "P --> P" by auto +lemma foo952: "P --> P" by auto +lemma foo953: "P --> P" by auto +lemma foo954: "P --> P" by auto +lemma foo955: "P --> P" by auto +lemma foo956: "P --> P" by auto +lemma foo957: "P --> P" by auto +lemma foo958: "P --> P" by auto +lemma foo959: "P --> P" by auto +lemma foo960: "P --> P" by auto +lemma foo961: "P --> P" by auto +lemma foo962: "P --> P" by auto +lemma foo963: "P --> P" by auto +lemma foo964: "P --> P" by auto +lemma foo965: "P --> P" by auto +lemma foo966: "P --> P" by auto +lemma foo967: "P --> P" by auto +lemma foo968: "P --> P" by auto +lemma foo969: "P --> P" by auto +lemma foo970: "P --> P" by auto +lemma foo971: "P --> P" by auto +lemma foo972: "P --> P" by auto +lemma foo973: "P --> P" by auto +lemma foo974: "P --> P" by auto +lemma foo975: "P --> P" by auto +lemma foo976: "P --> P" by auto +lemma foo977: "P --> P" by auto +lemma foo978: "P --> P" by auto +lemma foo979: "P --> P" by auto +lemma foo980: "P --> P" by auto +lemma foo981: "P --> P" by auto +lemma foo982: "P --> P" by auto +lemma foo983: "P --> P" by auto +lemma foo984: "P --> P" by auto +lemma foo985: "P --> P" by auto +lemma foo986: "P --> P" by auto +lemma foo987: "P --> P" by auto +lemma foo988: "P --> P" by auto +lemma foo989: "P --> P" by auto +lemma foo990: "P --> P" by auto +lemma foo991: "P --> P" by auto +lemma foo992: "P --> P" by auto +lemma foo993: "P --> P" by auto +lemma foo994: "P --> P" by auto +lemma foo995: "P --> P" by auto +lemma foo996: "P --> P" by auto +lemma foo997: "P --> P" by auto +lemma foo998: "P --> P" by auto +lemma foo999: "P --> P" by auto +lemma foo1000: "P --> P" by auto + +end |