--- a/thys2/Journal/Paper.tex Sat Jan 08 15:26:33 2022 +0000
+++ b/thys2/Journal/Paper.tex Tue Jan 11 23:58:39 2022 +0000
@@ -225,10 +225,7 @@
\end{tabular}
\end{center}
-This rule allows us to simplify \mbox{\isa{{\isacharparenleft}{\kern0pt}a\ {\isacharplus}{\kern0pt}\ b{\isacharparenright}{\kern0pt}\ {\isasymcdot}\ c\ {\isacharplus}{\kern0pt}\ a\ {\isasymcdot}\ c}}
- into \mbox{\isa{a\ {\isasymcdot}\ c\ {\isacharplus}{\kern0pt}\ b\ {\isasymcdot}\ c}},
-which cannot be done under the rrewrite rule because only alternatives which are
-children of another alternative can be spilled out.%
+This rule allows us to simplify \mbox{\isa{a\ {\isacharplus}{\kern0pt}\ b\ {\isasymcdot}\ c\ {\isacharplus}{\kern0pt}\ a\ {\isasymcdot}\ c}}%
\end{isamarkuptext}\isamarkuptrue%
%
\isadelimdocument
@@ -1761,7 +1758,7 @@
%
\end{isabellebody}%
\endinput
-%:%file=~/Dropbox/Workspace/journalpaper/lexing/thys2/Journal/Paper.thy%:%
+%:%file=Paper.tex%:%
%:%50=134%:%
%:%62=136%:%
%:%63=137%:%
@@ -1911,1465 +1908,1462 @@
%:%226=287%:%
%:%227=288%:%
%:%228=289%:%
-%:%229=290%:%
-%:%230=291%:%
-%:%231=292%:%
-%:%240=299%:%
-%:%252=305%:%
-%:%253=306%:%
-%:%254=307%:%
-%:%255=308%:%
-%:%255=309%:%
-%:%256=310%:%
-%:%257=311%:%
-%:%258=312%:%
-%:%259=313%:%
-%:%260=314%:%
-%:%261=315%:%
-%:%262=316%:%
-%:%263=317%:%
-%:%264=318%:%
-%:%265=319%:%
-%:%266=320%:%
-%:%267=321%:%
-%:%268=322%:%
-%:%269=323%:%
-%:%270=324%:%
-%:%271=325%:%
-%:%272=326%:%
-%:%273=327%:%
-%:%274=328%:%
-%:%275=329%:%
-%:%276=330%:%
-%:%277=331%:%
-%:%278=332%:%
-%:%279=333%:%
-%:%280=334%:%
-%:%281=335%:%
-%:%282=336%:%
-%:%283=337%:%
-%:%284=338%:%
-%:%285=339%:%
-%:%286=340%:%
-%:%287=341%:%
-%:%288=342%:%
-%:%289=343%:%
-%:%290=344%:%
-%:%291=345%:%
-%:%292=346%:%
-%:%293=347%:%
-%:%294=348%:%
-%:%295=349%:%
-%:%296=350%:%
-%:%297=351%:%
-%:%298=352%:%
-%:%299=353%:%
-%:%300=354%:%
-%:%301=355%:%
-%:%302=356%:%
-%:%303=357%:%
-%:%304=358%:%
-%:%305=359%:%
-%:%306=360%:%
-%:%307=361%:%
-%:%308=362%:%
-%:%309=363%:%
-%:%310=364%:%
-%:%311=365%:%
-%:%312=366%:%
-%:%313=367%:%
-%:%314=368%:%
-%:%315=369%:%
-%:%316=370%:%
-%:%317=371%:%
-%:%318=372%:%
-%:%319=373%:%
-%:%319=374%:%
-%:%320=375%:%
-%:%321=376%:%
-%:%322=377%:%
-%:%323=378%:%
-%:%324=379%:%
-%:%325=380%:%
-%:%326=381%:%
-%:%327=382%:%
-%:%328=383%:%
-%:%329=384%:%
-%:%330=385%:%
-%:%331=386%:%
-%:%332=387%:%
-%:%333=388%:%
-%:%334=389%:%
-%:%335=390%:%
-%:%336=391%:%
-%:%337=392%:%
-%:%338=393%:%
-%:%339=394%:%
-%:%340=395%:%
-%:%341=396%:%
-%:%342=397%:%
-%:%343=398%:%
-%:%344=399%:%
-%:%345=400%:%
-%:%346=401%:%
-%:%347=402%:%
-%:%348=403%:%
-%:%349=404%:%
-%:%350=405%:%
-%:%351=406%:%
-%:%352=407%:%
-%:%353=408%:%
-%:%354=409%:%
-%:%355=410%:%
-%:%356=411%:%
-%:%357=412%:%
-%:%358=413%:%
-%:%359=414%:%
-%:%360=415%:%
-%:%361=416%:%
-%:%362=417%:%
-%:%363=418%:%
-%:%364=419%:%
-%:%365=420%:%
-%:%366=421%:%
-%:%367=422%:%
-%:%368=423%:%
-%:%369=424%:%
-%:%370=425%:%
-%:%371=426%:%
-%:%372=427%:%
-%:%373=428%:%
-%:%374=429%:%
-%:%375=430%:%
-%:%376=431%:%
-%:%377=432%:%
-%:%378=433%:%
-%:%379=434%:%
-%:%380=435%:%
-%:%381=436%:%
-%:%382=437%:%
-%:%383=438%:%
-%:%384=439%:%
-%:%385=440%:%
-%:%386=441%:%
-%:%387=442%:%
-%:%388=443%:%
-%:%389=444%:%
-%:%390=445%:%
-%:%391=446%:%
-%:%392=447%:%
-%:%393=448%:%
-%:%394=449%:%
-%:%395=450%:%
-%:%396=451%:%
-%:%397=452%:%
-%:%398=453%:%
-%:%399=454%:%
-%:%400=455%:%
-%:%401=456%:%
-%:%402=457%:%
-%:%403=458%:%
-%:%404=459%:%
-%:%405=460%:%
-%:%406=461%:%
-%:%407=462%:%
-%:%408=463%:%
-%:%409=464%:%
-%:%410=465%:%
-%:%411=466%:%
-%:%412=467%:%
-%:%413=468%:%
-%:%414=469%:%
-%:%415=470%:%
-%:%416=471%:%
-%:%417=472%:%
-%:%418=473%:%
-%:%419=474%:%
-%:%420=475%:%
-%:%421=476%:%
-%:%422=477%:%
-%:%423=478%:%
-%:%424=479%:%
-%:%433=486%:%
-%:%445=488%:%
-%:%446=489%:%
-%:%446=490%:%
-%:%447=491%:%
-%:%448=492%:%
-%:%449=493%:%
-%:%450=494%:%
-%:%451=495%:%
-%:%452=496%:%
-%:%453=497%:%
-%:%454=498%:%
-%:%455=499%:%
-%:%456=500%:%
-%:%457=501%:%
-%:%458=502%:%
-%:%459=503%:%
-%:%460=504%:%
-%:%461=505%:%
-%:%462=506%:%
-%:%463=507%:%
-%:%464=508%:%
-%:%465=509%:%
-%:%466=510%:%
-%:%467=511%:%
-%:%468=512%:%
-%:%469=513%:%
-%:%470=514%:%
-%:%471=515%:%
-%:%472=516%:%
-%:%473=517%:%
-%:%474=518%:%
-%:%475=519%:%
-%:%476=520%:%
-%:%477=521%:%
-%:%478=522%:%
-%:%479=523%:%
-%:%480=524%:%
-%:%481=525%:%
-%:%482=526%:%
-%:%483=527%:%
-%:%484=528%:%
-%:%485=529%:%
-%:%485=530%:%
-%:%486=531%:%
-%:%487=532%:%
-%:%488=533%:%
-%:%489=534%:%
-%:%490=535%:%
-%:%490=536%:%
-%:%491=537%:%
-%:%492=538%:%
-%:%493=539%:%
-%:%494=540%:%
-%:%495=541%:%
-%:%496=542%:%
-%:%497=543%:%
-%:%498=544%:%
-%:%499=545%:%
-%:%500=546%:%
-%:%501=547%:%
-%:%502=548%:%
-%:%503=549%:%
-%:%504=550%:%
-%:%505=551%:%
-%:%506=552%:%
-%:%507=553%:%
-%:%508=554%:%
-%:%509=555%:%
-%:%510=556%:%
-%:%511=557%:%
-%:%512=558%:%
-%:%513=559%:%
-%:%514=560%:%
-%:%515=561%:%
-%:%516=562%:%
-%:%517=563%:%
-%:%518=564%:%
-%:%519=565%:%
-%:%520=566%:%
-%:%521=567%:%
-%:%522=568%:%
-%:%523=569%:%
-%:%524=570%:%
-%:%525=571%:%
-%:%526=572%:%
-%:%527=573%:%
-%:%528=574%:%
-%:%529=575%:%
-%:%530=576%:%
-%:%531=577%:%
-%:%532=578%:%
-%:%533=579%:%
-%:%534=580%:%
-%:%535=581%:%
-%:%536=582%:%
-%:%537=583%:%
-%:%538=584%:%
-%:%539=585%:%
-%:%540=586%:%
-%:%541=587%:%
-%:%542=588%:%
-%:%543=589%:%
-%:%544=590%:%
-%:%545=591%:%
-%:%546=592%:%
-%:%547=593%:%
-%:%548=594%:%
-%:%549=595%:%
-%:%550=596%:%
-%:%551=597%:%
-%:%552=598%:%
-%:%553=599%:%
-%:%554=600%:%
-%:%555=601%:%
-%:%556=602%:%
-%:%557=603%:%
-%:%558=604%:%
-%:%559=605%:%
-%:%560=606%:%
-%:%561=607%:%
-%:%562=608%:%
-%:%563=609%:%
-%:%564=610%:%
-%:%565=611%:%
-%:%566=612%:%
-%:%567=613%:%
-%:%568=614%:%
-%:%569=615%:%
-%:%570=616%:%
-%:%571=617%:%
-%:%572=618%:%
-%:%573=619%:%
-%:%574=620%:%
-%:%575=621%:%
-%:%576=622%:%
-%:%577=623%:%
-%:%578=624%:%
-%:%579=625%:%
-%:%588=629%:%
-%:%600=633%:%
-%:%601=634%:%
-%:%602=635%:%
-%:%603=636%:%
-%:%604=637%:%
-%:%605=638%:%
-%:%606=639%:%
-%:%607=640%:%
-%:%608=641%:%
-%:%609=642%:%
-%:%610=643%:%
-%:%611=644%:%
-%:%612=645%:%
-%:%613=646%:%
-%:%614=647%:%
-%:%615=648%:%
-%:%616=649%:%
-%:%617=650%:%
-%:%618=651%:%
-%:%619=652%:%
-%:%620=653%:%
-%:%621=654%:%
-%:%622=655%:%
-%:%623=656%:%
-%:%624=657%:%
-%:%625=658%:%
-%:%626=659%:%
-%:%627=660%:%
-%:%628=661%:%
-%:%629=662%:%
-%:%630=663%:%
-%:%631=664%:%
-%:%632=665%:%
-%:%633=666%:%
-%:%634=667%:%
-%:%635=668%:%
-%:%636=669%:%
-%:%637=670%:%
-%:%638=671%:%
-%:%639=672%:%
-%:%640=673%:%
-%:%641=674%:%
-%:%642=675%:%
-%:%643=676%:%
-%:%644=677%:%
-%:%645=678%:%
-%:%646=679%:%
-%:%647=680%:%
-%:%648=681%:%
-%:%649=682%:%
-%:%650=683%:%
-%:%651=684%:%
-%:%652=685%:%
-%:%653=686%:%
-%:%654=687%:%
-%:%655=688%:%
-%:%656=689%:%
-%:%657=690%:%
-%:%658=691%:%
-%:%659=692%:%
-%:%660=693%:%
-%:%661=694%:%
-%:%662=695%:%
-%:%663=696%:%
-%:%664=697%:%
-%:%665=698%:%
-%:%666=699%:%
-%:%667=700%:%
-%:%668=701%:%
-%:%669=702%:%
-%:%670=703%:%
-%:%671=704%:%
-%:%672=705%:%
-%:%673=706%:%
-%:%674=707%:%
-%:%675=708%:%
-%:%676=709%:%
-%:%677=710%:%
-%:%678=711%:%
-%:%679=712%:%
-%:%680=713%:%
-%:%681=714%:%
-%:%682=715%:%
-%:%683=716%:%
-%:%684=717%:%
-%:%685=718%:%
-%:%686=719%:%
-%:%687=720%:%
-%:%688=721%:%
-%:%689=722%:%
-%:%690=723%:%
-%:%691=724%:%
-%:%692=725%:%
-%:%693=726%:%
-%:%694=727%:%
-%:%695=728%:%
-%:%696=729%:%
-%:%697=730%:%
-%:%698=731%:%
-%:%699=732%:%
-%:%700=733%:%
-%:%701=734%:%
-%:%702=735%:%
-%:%703=736%:%
-%:%704=737%:%
-%:%705=738%:%
-%:%706=739%:%
-%:%707=740%:%
-%:%708=741%:%
-%:%709=742%:%
-%:%710=743%:%
-%:%711=744%:%
-%:%712=745%:%
-%:%713=746%:%
-%:%714=747%:%
-%:%714=748%:%
-%:%715=749%:%
-%:%715=750%:%
-%:%716=751%:%
-%:%717=752%:%
-%:%717=753%:%
-%:%718=754%:%
-%:%719=755%:%
-%:%720=756%:%
-%:%721=757%:%
-%:%722=758%:%
-%:%723=759%:%
-%:%724=760%:%
-%:%725=761%:%
-%:%726=762%:%
-%:%727=763%:%
-%:%728=764%:%
-%:%729=765%:%
-%:%730=766%:%
-%:%731=767%:%
-%:%732=768%:%
-%:%733=769%:%
-%:%734=770%:%
-%:%735=771%:%
-%:%736=772%:%
-%:%737=773%:%
-%:%738=774%:%
-%:%739=775%:%
-%:%740=776%:%
-%:%741=777%:%
-%:%742=778%:%
-%:%743=779%:%
-%:%744=780%:%
-%:%745=781%:%
-%:%746=782%:%
-%:%747=783%:%
-%:%748=784%:%
-%:%749=785%:%
-%:%750=786%:%
-%:%751=787%:%
-%:%752=788%:%
-%:%753=789%:%
-%:%754=790%:%
-%:%755=791%:%
-%:%756=792%:%
-%:%757=793%:%
-%:%758=794%:%
-%:%759=795%:%
-%:%760=796%:%
-%:%761=797%:%
-%:%762=798%:%
-%:%763=799%:%
-%:%764=800%:%
-%:%765=801%:%
-%:%766=802%:%
-%:%767=803%:%
-%:%768=804%:%
-%:%769=805%:%
-%:%770=806%:%
-%:%771=807%:%
-%:%772=808%:%
-%:%773=809%:%
-%:%773=810%:%
-%:%773=811%:%
-%:%774=812%:%
-%:%775=813%:%
-%:%776=814%:%
-%:%777=815%:%
-%:%778=816%:%
-%:%779=817%:%
-%:%780=818%:%
-%:%781=819%:%
-%:%782=820%:%
-%:%782=821%:%
-%:%783=822%:%
-%:%784=823%:%
-%:%785=824%:%
-%:%786=825%:%
-%:%787=826%:%
-%:%788=827%:%
-%:%789=828%:%
-%:%790=829%:%
-%:%791=830%:%
-%:%792=831%:%
-%:%793=832%:%
-%:%794=833%:%
-%:%795=834%:%
-%:%796=835%:%
-%:%797=836%:%
-%:%798=837%:%
-%:%799=838%:%
-%:%800=839%:%
-%:%801=840%:%
-%:%802=841%:%
-%:%803=842%:%
-%:%804=843%:%
-%:%805=844%:%
-%:%806=845%:%
-%:%807=846%:%
-%:%808=847%:%
-%:%809=848%:%
-%:%810=849%:%
-%:%811=850%:%
-%:%812=851%:%
-%:%813=852%:%
-%:%814=853%:%
-%:%815=854%:%
-%:%816=855%:%
-%:%817=856%:%
-%:%817=857%:%
-%:%818=858%:%
-%:%819=859%:%
-%:%820=860%:%
-%:%821=861%:%
-%:%822=862%:%
-%:%823=863%:%
-%:%824=864%:%
-%:%824=865%:%
-%:%825=866%:%
-%:%826=867%:%
-%:%827=868%:%
-%:%827=869%:%
-%:%828=870%:%
-%:%829=871%:%
-%:%830=872%:%
-%:%831=873%:%
-%:%832=874%:%
-%:%833=875%:%
-%:%834=876%:%
-%:%835=877%:%
-%:%836=878%:%
-%:%837=879%:%
-%:%838=880%:%
-%:%838=881%:%
-%:%839=882%:%
-%:%840=883%:%
-%:%841=884%:%
-%:%842=885%:%
-%:%842=886%:%
-%:%843=887%:%
-%:%844=888%:%
-%:%845=889%:%
-%:%846=890%:%
-%:%847=891%:%
-%:%848=892%:%
-%:%849=893%:%
-%:%850=894%:%
-%:%851=895%:%
-%:%852=896%:%
-%:%853=897%:%
-%:%854=898%:%
-%:%855=899%:%
-%:%856=900%:%
-%:%857=901%:%
-%:%858=902%:%
-%:%859=903%:%
-%:%860=904%:%
-%:%861=905%:%
-%:%862=906%:%
-%:%863=907%:%
-%:%864=908%:%
-%:%865=909%:%
-%:%866=910%:%
-%:%867=911%:%
-%:%868=912%:%
-%:%869=913%:%
-%:%870=914%:%
-%:%871=915%:%
-%:%872=916%:%
-%:%873=917%:%
-%:%874=918%:%
-%:%875=919%:%
-%:%876=920%:%
-%:%877=921%:%
-%:%878=922%:%
-%:%879=923%:%
-%:%880=924%:%
-%:%881=925%:%
-%:%882=926%:%
-%:%883=927%:%
-%:%884=928%:%
-%:%885=929%:%
-%:%886=930%:%
-%:%887=931%:%
-%:%888=932%:%
-%:%889=933%:%
-%:%890=934%:%
-%:%891=935%:%
-%:%892=936%:%
-%:%893=937%:%
-%:%894=938%:%
-%:%895=939%:%
-%:%896=940%:%
-%:%897=941%:%
-%:%898=942%:%
-%:%899=943%:%
-%:%900=944%:%
-%:%900=945%:%
-%:%901=946%:%
-%:%902=947%:%
-%:%903=948%:%
-%:%904=949%:%
-%:%905=950%:%
-%:%906=951%:%
-%:%907=952%:%
-%:%908=953%:%
-%:%909=954%:%
-%:%910=955%:%
-%:%911=956%:%
-%:%912=957%:%
-%:%913=958%:%
-%:%914=959%:%
-%:%915=960%:%
-%:%916=961%:%
-%:%917=962%:%
-%:%918=963%:%
-%:%919=964%:%
-%:%920=965%:%
-%:%921=966%:%
-%:%922=967%:%
-%:%923=968%:%
-%:%924=969%:%
-%:%925=970%:%
-%:%926=971%:%
-%:%927=972%:%
-%:%928=973%:%
-%:%929=974%:%
-%:%930=975%:%
-%:%931=976%:%
-%:%932=977%:%
-%:%933=978%:%
-%:%933=979%:%
-%:%934=980%:%
-%:%935=981%:%
-%:%936=982%:%
-%:%937=983%:%
-%:%938=984%:%
-%:%939=985%:%
-%:%940=986%:%
-%:%941=987%:%
-%:%942=988%:%
-%:%943=989%:%
-%:%944=990%:%
-%:%945=991%:%
-%:%946=992%:%
-%:%947=993%:%
-%:%948=994%:%
-%:%949=995%:%
-%:%950=996%:%
-%:%951=997%:%
-%:%952=998%:%
-%:%953=999%:%
-%:%954=1000%:%
-%:%955=1001%:%
-%:%956=1002%:%
-%:%957=1003%:%
-%:%958=1004%:%
-%:%959=1005%:%
-%:%960=1006%:%
-%:%961=1007%:%
-%:%962=1008%:%
-%:%963=1009%:%
-%:%963=1010%:%
-%:%964=1011%:%
-%:%965=1012%:%
-%:%966=1013%:%
-%:%967=1014%:%
-%:%968=1015%:%
-%:%969=1016%:%
-%:%970=1017%:%
-%:%971=1018%:%
-%:%971=1019%:%
-%:%972=1020%:%
-%:%973=1021%:%
-%:%974=1022%:%
-%:%975=1023%:%
-%:%976=1024%:%
-%:%977=1025%:%
-%:%978=1026%:%
-%:%979=1027%:%
-%:%980=1028%:%
-%:%981=1029%:%
-%:%982=1030%:%
-%:%983=1031%:%
-%:%984=1032%:%
-%:%985=1033%:%
-%:%986=1034%:%
-%:%987=1035%:%
-%:%988=1036%:%
-%:%989=1037%:%
-%:%990=1038%:%
-%:%991=1039%:%
-%:%992=1040%:%
-%:%993=1041%:%
-%:%994=1042%:%
-%:%995=1043%:%
-%:%996=1044%:%
-%:%997=1045%:%
-%:%998=1046%:%
-%:%999=1047%:%
-%:%1000=1048%:%
-%:%1001=1049%:%
-%:%1002=1050%:%
-%:%1003=1051%:%
-%:%1004=1052%:%
-%:%1005=1053%:%
-%:%1006=1054%:%
-%:%1007=1055%:%
-%:%1008=1056%:%
-%:%1008=1057%:%
-%:%1008=1058%:%
-%:%1009=1059%:%
-%:%1009=1060%:%
-%:%1009=1061%:%
-%:%1010=1062%:%
-%:%1011=1063%:%
-%:%1011=1064%:%
-%:%1012=1065%:%
-%:%1013=1066%:%
-%:%1014=1067%:%
-%:%1015=1068%:%
-%:%1016=1069%:%
-%:%1017=1070%:%
-%:%1018=1071%:%
-%:%1019=1072%:%
-%:%1020=1073%:%
-%:%1021=1074%:%
-%:%1022=1075%:%
-%:%1023=1076%:%
-%:%1024=1077%:%
-%:%1025=1078%:%
-%:%1026=1079%:%
-%:%1027=1080%:%
-%:%1028=1081%:%
-%:%1029=1082%:%
-%:%1030=1083%:%
-%:%1031=1084%:%
-%:%1032=1085%:%
-%:%1033=1086%:%
-%:%1034=1087%:%
-%:%1035=1088%:%
-%:%1036=1089%:%
-%:%1037=1090%:%
-%:%1038=1091%:%
-%:%1039=1092%:%
-%:%1040=1093%:%
-%:%1041=1094%:%
-%:%1042=1095%:%
-%:%1043=1096%:%
-%:%1044=1097%:%
-%:%1045=1098%:%
-%:%1045=1099%:%
-%:%1046=1100%:%
-%:%1047=1101%:%
-%:%1048=1102%:%
-%:%1048=1103%:%
-%:%1048=1104%:%
-%:%1048=1105%:%
-%:%1049=1106%:%
-%:%1050=1107%:%
-%:%1051=1108%:%
-%:%1052=1109%:%
-%:%1053=1110%:%
-%:%1054=1111%:%
-%:%1055=1112%:%
-%:%1056=1113%:%
-%:%1057=1114%:%
-%:%1058=1115%:%
-%:%1059=1116%:%
-%:%1060=1117%:%
-%:%1061=1118%:%
-%:%1062=1119%:%
-%:%1063=1120%:%
-%:%1064=1121%:%
-%:%1065=1122%:%
-%:%1066=1123%:%
-%:%1067=1124%:%
-%:%1068=1125%:%
-%:%1069=1126%:%
-%:%1070=1127%:%
-%:%1071=1128%:%
-%:%1072=1129%:%
-%:%1073=1130%:%
-%:%1074=1131%:%
-%:%1075=1132%:%
-%:%1076=1133%:%
-%:%1077=1134%:%
-%:%1078=1135%:%
-%:%1079=1136%:%
-%:%1080=1137%:%
-%:%1081=1138%:%
-%:%1082=1139%:%
-%:%1083=1140%:%
-%:%1084=1141%:%
-%:%1085=1142%:%
-%:%1094=1146%:%
-%:%1106=1150%:%
-%:%1107=1151%:%
-%:%1108=1152%:%
-%:%1109=1153%:%
-%:%1110=1154%:%
-%:%1111=1155%:%
-%:%1112=1156%:%
-%:%1113=1157%:%
-%:%1114=1158%:%
-%:%1115=1159%:%
-%:%1116=1160%:%
-%:%1117=1161%:%
-%:%1118=1162%:%
-%:%1119=1163%:%
-%:%1120=1164%:%
-%:%1121=1165%:%
-%:%1122=1166%:%
-%:%1123=1167%:%
-%:%1124=1168%:%
-%:%1125=1169%:%
-%:%1126=1170%:%
-%:%1127=1171%:%
-%:%1128=1172%:%
-%:%1129=1173%:%
-%:%1130=1174%:%
-%:%1131=1175%:%
-%:%1132=1176%:%
-%:%1133=1177%:%
-%:%1134=1178%:%
-%:%1135=1179%:%
-%:%1136=1180%:%
-%:%1137=1181%:%
-%:%1138=1182%:%
-%:%1139=1183%:%
-%:%1140=1184%:%
-%:%1141=1185%:%
-%:%1142=1186%:%
-%:%1143=1187%:%
-%:%1144=1188%:%
-%:%1145=1189%:%
-%:%1146=1190%:%
-%:%1147=1191%:%
-%:%1148=1192%:%
-%:%1149=1193%:%
-%:%1150=1194%:%
-%:%1151=1195%:%
-%:%1152=1196%:%
-%:%1153=1197%:%
-%:%1154=1198%:%
-%:%1155=1199%:%
-%:%1156=1200%:%
-%:%1157=1201%:%
-%:%1158=1202%:%
-%:%1159=1203%:%
-%:%1160=1204%:%
-%:%1161=1205%:%
-%:%1162=1206%:%
-%:%1163=1207%:%
-%:%1164=1208%:%
-%:%1165=1209%:%
-%:%1166=1210%:%
-%:%1167=1211%:%
-%:%1168=1212%:%
-%:%1169=1213%:%
-%:%1170=1214%:%
-%:%1171=1215%:%
-%:%1172=1216%:%
-%:%1173=1217%:%
-%:%1174=1218%:%
-%:%1175=1219%:%
-%:%1176=1220%:%
-%:%1177=1221%:%
-%:%1178=1222%:%
-%:%1179=1223%:%
-%:%1180=1224%:%
-%:%1181=1225%:%
-%:%1182=1226%:%
-%:%1183=1227%:%
-%:%1184=1228%:%
-%:%1185=1229%:%
-%:%1186=1230%:%
-%:%1187=1231%:%
-%:%1188=1232%:%
-%:%1189=1233%:%
-%:%1190=1234%:%
-%:%1191=1235%:%
-%:%1192=1236%:%
-%:%1193=1237%:%
-%:%1194=1238%:%
-%:%1195=1239%:%
-%:%1196=1240%:%
-%:%1197=1241%:%
-%:%1198=1242%:%
-%:%1199=1243%:%
-%:%1200=1244%:%
-%:%1201=1245%:%
-%:%1202=1246%:%
-%:%1203=1247%:%
-%:%1204=1248%:%
-%:%1205=1249%:%
-%:%1206=1250%:%
-%:%1207=1251%:%
-%:%1208=1252%:%
-%:%1209=1253%:%
-%:%1210=1254%:%
-%:%1211=1255%:%
-%:%1212=1256%:%
-%:%1213=1257%:%
-%:%1214=1258%:%
-%:%1215=1259%:%
-%:%1216=1260%:%
-%:%1217=1261%:%
-%:%1218=1262%:%
-%:%1219=1263%:%
-%:%1220=1264%:%
-%:%1221=1265%:%
-%:%1221=1266%:%
-%:%1222=1267%:%
-%:%1223=1268%:%
-%:%1224=1269%:%
-%:%1225=1270%:%
-%:%1226=1271%:%
-%:%1227=1272%:%
-%:%1228=1273%:%
-%:%1229=1274%:%
-%:%1230=1275%:%
-%:%1231=1276%:%
-%:%1232=1277%:%
-%:%1232=1278%:%
-%:%1233=1279%:%
-%:%1234=1280%:%
-%:%1235=1281%:%
-%:%1236=1282%:%
-%:%1237=1283%:%
-%:%1238=1284%:%
-%:%1239=1285%:%
-%:%1240=1286%:%
-%:%1241=1287%:%
-%:%1242=1288%:%
-%:%1243=1289%:%
-%:%1244=1290%:%
-%:%1245=1291%:%
-%:%1246=1292%:%
-%:%1247=1293%:%
-%:%1248=1294%:%
-%:%1249=1295%:%
-%:%1250=1296%:%
-%:%1251=1297%:%
-%:%1252=1298%:%
-%:%1253=1299%:%
-%:%1254=1300%:%
-%:%1255=1301%:%
-%:%1256=1302%:%
-%:%1257=1303%:%
-%:%1258=1304%:%
-%:%1259=1305%:%
-%:%1260=1306%:%
-%:%1261=1307%:%
-%:%1262=1308%:%
-%:%1263=1309%:%
-%:%1264=1310%:%
-%:%1265=1311%:%
-%:%1266=1312%:%
-%:%1267=1313%:%
-%:%1268=1314%:%
-%:%1269=1315%:%
-%:%1270=1316%:%
-%:%1271=1317%:%
-%:%1272=1318%:%
-%:%1273=1319%:%
-%:%1274=1320%:%
-%:%1275=1321%:%
-%:%1276=1322%:%
-%:%1277=1323%:%
-%:%1278=1324%:%
-%:%1279=1325%:%
-%:%1280=1326%:%
-%:%1281=1327%:%
-%:%1282=1328%:%
-%:%1283=1329%:%
-%:%1284=1330%:%
-%:%1285=1331%:%
-%:%1286=1332%:%
-%:%1286=1333%:%
-%:%1286=1334%:%
-%:%1287=1335%:%
-%:%1288=1336%:%
-%:%1288=1337%:%
-%:%1288=1338%:%
-%:%1288=1339%:%
-%:%1289=1340%:%
-%:%1290=1341%:%
-%:%1291=1342%:%
-%:%1292=1343%:%
-%:%1293=1344%:%
-%:%1293=1345%:%
-%:%1294=1346%:%
-%:%1295=1347%:%
-%:%1296=1348%:%
-%:%1297=1349%:%
-%:%1298=1350%:%
-%:%1299=1351%:%
-%:%1300=1352%:%
-%:%1301=1353%:%
-%:%1302=1354%:%
-%:%1303=1355%:%
-%:%1304=1356%:%
-%:%1305=1357%:%
-%:%1306=1358%:%
-%:%1307=1359%:%
-%:%1308=1360%:%
-%:%1309=1361%:%
-%:%1310=1362%:%
-%:%1311=1363%:%
-%:%1312=1364%:%
-%:%1313=1365%:%
-%:%1314=1366%:%
-%:%1315=1367%:%
-%:%1316=1368%:%
-%:%1317=1369%:%
-%:%1318=1370%:%
-%:%1319=1371%:%
-%:%1320=1372%:%
-%:%1321=1373%:%
-%:%1322=1374%:%
-%:%1323=1375%:%
-%:%1324=1376%:%
-%:%1325=1377%:%
-%:%1326=1378%:%
-%:%1327=1379%:%
-%:%1328=1380%:%
-%:%1329=1381%:%
-%:%1330=1382%:%
-%:%1331=1383%:%
-%:%1332=1384%:%
-%:%1333=1385%:%
-%:%1334=1386%:%
-%:%1335=1387%:%
-%:%1336=1388%:%
-%:%1337=1389%:%
-%:%1338=1390%:%
-%:%1339=1391%:%
-%:%1340=1392%:%
-%:%1341=1393%:%
-%:%1341=1394%:%
-%:%1342=1395%:%
-%:%1342=1396%:%
-%:%1343=1397%:%
-%:%1343=1398%:%
-%:%1344=1399%:%
-%:%1345=1400%:%
-%:%1346=1401%:%
-%:%1347=1402%:%
-%:%1348=1403%:%
-%:%1349=1404%:%
-%:%1350=1405%:%
-%:%1350=1406%:%
-%:%1351=1407%:%
-%:%1351=1408%:%
-%:%1352=1409%:%
-%:%1352=1410%:%
-%:%1353=1411%:%
-%:%1354=1412%:%
-%:%1355=1413%:%
-%:%1356=1414%:%
-%:%1357=1415%:%
-%:%1358=1416%:%
-%:%1359=1417%:%
-%:%1360=1418%:%
-%:%1361=1419%:%
-%:%1362=1420%:%
-%:%1363=1421%:%
-%:%1364=1422%:%
-%:%1365=1423%:%
-%:%1366=1424%:%
-%:%1367=1425%:%
-%:%1368=1426%:%
-%:%1369=1427%:%
-%:%1370=1428%:%
-%:%1371=1429%:%
-%:%1372=1430%:%
-%:%1373=1431%:%
-%:%1374=1432%:%
-%:%1375=1433%:%
-%:%1376=1434%:%
-%:%1377=1435%:%
-%:%1378=1436%:%
-%:%1379=1437%:%
-%:%1380=1438%:%
-%:%1381=1439%:%
-%:%1382=1440%:%
-%:%1383=1441%:%
-%:%1383=1442%:%
-%:%1384=1443%:%
-%:%1385=1444%:%
-%:%1386=1445%:%
-%:%1387=1446%:%
-%:%1388=1447%:%
-%:%1389=1448%:%
-%:%1390=1449%:%
-%:%1390=1450%:%
-%:%1391=1451%:%
-%:%1392=1452%:%
-%:%1393=1453%:%
-%:%1393=1454%:%
-%:%1394=1455%:%
-%:%1395=1456%:%
-%:%1396=1457%:%
-%:%1396=1458%:%
-%:%1397=1459%:%
-%:%1397=1460%:%
-%:%1398=1461%:%
-%:%1398=1462%:%
-%:%1399=1463%:%
-%:%1400=1464%:%
-%:%1401=1465%:%
-%:%1401=1466%:%
-%:%1402=1467%:%
-%:%1402=1468%:%
-%:%1403=1469%:%
-%:%1403=1470%:%
-%:%1403=1471%:%
-%:%1403=1472%:%
-%:%1404=1473%:%
-%:%1404=1474%:%
-%:%1405=1475%:%
-%:%1406=1476%:%
-%:%1406=1478%:%
-%:%1406=1479%:%
-%:%1406=1480%:%
-%:%1406=1481%:%
-%:%1406=1482%:%
-%:%1407=1483%:%
-%:%1407=1484%:%
-%:%1408=1485%:%
-%:%1408=1486%:%
-%:%1409=1487%:%
-%:%1409=1488%:%
-%:%1410=1489%:%
-%:%1411=1490%:%
-%:%1412=1491%:%
-%:%1413=1492%:%
-%:%1413=1493%:%
-%:%1414=1494%:%
-%:%1414=1495%:%
-%:%1415=1496%:%
-%:%1416=1497%:%
-%:%1416=1498%:%
-%:%1417=1499%:%
-%:%1418=1500%:%
-%:%1419=1501%:%
-%:%1420=1502%:%
-%:%1421=1503%:%
-%:%1422=1504%:%
-%:%1423=1505%:%
-%:%1424=1506%:%
-%:%1425=1507%:%
-%:%1426=1508%:%
-%:%1427=1509%:%
-%:%1428=1510%:%
-%:%1429=1511%:%
-%:%1430=1512%:%
-%:%1431=1513%:%
-%:%1432=1514%:%
-%:%1433=1515%:%
-%:%1434=1516%:%
-%:%1435=1517%:%
-%:%1436=1518%:%
-%:%1437=1519%:%
-%:%1438=1520%:%
-%:%1439=1521%:%
-%:%1440=1522%:%
-%:%1441=1523%:%
-%:%1442=1524%:%
-%:%1443=1525%:%
-%:%1444=1526%:%
-%:%1445=1527%:%
-%:%1446=1528%:%
-%:%1447=1529%:%
-%:%1448=1530%:%
-%:%1449=1531%:%
-%:%1450=1532%:%
-%:%1451=1533%:%
-%:%1452=1534%:%
-%:%1453=1535%:%
-%:%1454=1536%:%
-%:%1455=1537%:%
-%:%1456=1538%:%
-%:%1457=1539%:%
-%:%1458=1540%:%
-%:%1459=1541%:%
-%:%1460=1542%:%
-%:%1461=1543%:%
-%:%1462=1544%:%
-%:%1463=1545%:%
-%:%1464=1546%:%
-%:%1465=1547%:%
-%:%1466=1548%:%
-%:%1467=1549%:%
-%:%1476=1553%:%
-%:%1488=1560%:%
-%:%1489=1561%:%
-%:%1490=1562%:%
-%:%1491=1563%:%
-%:%1492=1564%:%
-%:%1493=1565%:%
-%:%1494=1566%:%
-%:%1503=1571%:%
-%:%1515=1575%:%
-%:%1516=1576%:%
-%:%1517=1577%:%
-%:%1518=1578%:%
-%:%1519=1579%:%
-%:%1520=1580%:%
-%:%1521=1581%:%
-%:%1522=1582%:%
-%:%1523=1583%:%
-%:%1524=1584%:%
-%:%1525=1585%:%
-%:%1526=1586%:%
-%:%1527=1587%:%
-%:%1528=1588%:%
-%:%1529=1589%:%
-%:%1530=1590%:%
-%:%1531=1591%:%
-%:%1532=1592%:%
-%:%1533=1593%:%
-%:%1534=1594%:%
-%:%1535=1595%:%
-%:%1536=1596%:%
-%:%1537=1597%:%
-%:%1538=1598%:%
-%:%1539=1599%:%
-%:%1540=1600%:%
-%:%1541=1601%:%
-%:%1542=1602%:%
-%:%1543=1603%:%
-%:%1544=1604%:%
-%:%1545=1605%:%
-%:%1546=1606%:%
-%:%1547=1607%:%
-%:%1548=1608%:%
-%:%1549=1609%:%
-%:%1550=1610%:%
-%:%1551=1611%:%
-%:%1552=1612%:%
-%:%1553=1613%:%
-%:%1554=1614%:%
-%:%1555=1615%:%
-%:%1556=1616%:%
-%:%1557=1617%:%
-%:%1558=1618%:%
-%:%1559=1619%:%
-%:%1560=1620%:%
-%:%1561=1621%:%
-%:%1562=1622%:%
-%:%1563=1623%:%
-%:%1564=1624%:%
-%:%1565=1625%:%
-%:%1566=1626%:%
-%:%1567=1627%:%
-%:%1568=1628%:%
-%:%1569=1629%:%
-%:%1570=1630%:%
-%:%1571=1631%:%
-%:%1572=1632%:%
-%:%1573=1633%:%
-%:%1574=1634%:%
-%:%1575=1635%:%
-%:%1576=1636%:%
-%:%1577=1637%:%
-%:%1578=1638%:%
-%:%1579=1639%:%
-%:%1580=1640%:%
-%:%1581=1641%:%
-%:%1582=1642%:%
-%:%1583=1643%:%
-%:%1584=1644%:%
-%:%1585=1645%:%
-%:%1586=1646%:%
-%:%1587=1647%:%
-%:%1588=1648%:%
-%:%1589=1649%:%
-%:%1590=1650%:%
-%:%1591=1651%:%
-%:%1592=1652%:%
-%:%1593=1653%:%
-%:%1594=1654%:%
-%:%1595=1655%:%
-%:%1596=1656%:%
-%:%1597=1657%:%
-%:%1598=1658%:%
-%:%1599=1659%:%
-%:%1600=1660%:%
-%:%1601=1661%:%
-%:%1602=1662%:%
-%:%1603=1663%:%
-%:%1604=1664%:%
-%:%1604=1780%:%
-%:%1605=1781%:%
-%:%1606=1782%:%
-%:%1607=1783%:%
-%:%1608=1784%:%
-%:%1608=1945%:%
-%:%1609=1946%:%
-%:%1610=1947%:%
-%:%1611=1948%:%
-%:%1612=1949%:%
-%:%1613=1950%:%
-%:%1614=1951%:%
-%:%1615=1952%:%
-%:%1616=1953%:%
-%:%1617=1954%:%
-%:%1618=1955%:%
-%:%1619=1956%:%
-%:%1620=1957%:%
-%:%1621=1958%:%
-%:%1622=1959%:%
-%:%1623=1960%:%
-%:%1624=1961%:%
-%:%1625=1962%:%
-%:%1626=1963%:%
-%:%1627=1964%:%
-%:%1627=1965%:%
-%:%1628=1966%:%
-%:%1628=1967%:%
-%:%1628=1968%:%
-%:%1629=1969%:%
-%:%1629=1970%:%
-%:%1630=1971%:%
-%:%1631=1972%:%
-%:%1632=1973%:%
-%:%1633=1974%:%
-%:%1634=1975%:%
-%:%1635=1976%:%
-%:%1636=1977%:%
-%:%1637=1978%:%
-%:%1638=1979%:%
-%:%1639=1980%:%
-%:%1640=1981%:%
-%:%1641=1982%:%
-%:%1642=1983%:%
-%:%1643=1984%:%
-%:%1644=1985%:%
-%:%1645=1986%:%
-%:%1646=1987%:%
-%:%1646=1988%:%
-%:%1647=1989%:%
-%:%1648=1990%:%
-%:%1649=1991%:%
-%:%1649=1992%:%
-%:%1649=1993%:%
-%:%1650=1994%:%
-%:%1651=1995%:%
-%:%1652=1996%:%
-%:%1652=1997%:%
-%:%1653=1998%:%
-%:%1653=1999%:%
-%:%1654=2000%:%
-%:%1655=2001%:%
-%:%1656=2002%:%
-%:%1657=2003%:%
-%:%1658=2004%:%
-%:%1659=2005%:%
-%:%1660=2006%:%
-%:%1661=2007%:%
-%:%1662=2008%:%
-%:%1663=2009%:%
-%:%1664=2010%:%
-%:%1665=2011%:%
-%:%1666=2012%:%
-%:%1667=2013%:%
-%:%1668=2014%:%
-%:%1669=2015%:%
-%:%1670=2016%:%
-%:%1679=2021%:%
-%:%1691=2025%:%
-%:%1692=2026%:%
-%:%1693=2027%:%
-%:%1694=2028%:%
-%:%1695=2029%:%
-%:%1696=2030%:%
-%:%1697=2031%:%
-%:%1698=2032%:%
-%:%1699=2033%:%
-%:%1700=2034%:%
-%:%1701=2035%:%
-%:%1702=2036%:%
-%:%1703=2037%:%
-%:%1704=2038%:%
-%:%1705=2039%:%
-%:%1706=2040%:%
-%:%1707=2041%:%
-%:%1708=2042%:%
-%:%1709=2043%:%
-%:%1710=2044%:%
-%:%1711=2045%:%
-%:%1712=2046%:%
-%:%1713=2047%:%
-%:%1714=2048%:%
-%:%1715=2049%:%
-%:%1716=2050%:%
-%:%1717=2051%:%
-%:%1718=2052%:%
-%:%1719=2053%:%
-%:%1720=2054%:%
-%:%1721=2055%:%
-%:%1722=2056%:%
-%:%1723=2057%:%
-%:%1724=2058%:%
-%:%1725=2059%:%
-%:%1726=2060%:%
-%:%1727=2061%:%
-%:%1728=2062%:%
-%:%1729=2063%:%
-%:%1730=2064%:%
-%:%1731=2065%:%
-%:%1732=2066%:%
-%:%1733=2067%:%
-%:%1734=2068%:%
-%:%1735=2069%:%
-%:%1736=2070%:%
-%:%1737=2071%:%
-%:%1738=2072%:%
-%:%1739=2073%:%
-%:%1740=2074%:%
-%:%1741=2075%:%
-%:%1742=2076%:%
-%:%1743=2077%:%
-%:%1756=2083%:%
-%:%1759=2084%:%
-%:%1760=2085%:%
\ No newline at end of file
+%:%237=297%:%
+%:%249=303%:%
+%:%250=304%:%
+%:%251=305%:%
+%:%252=306%:%
+%:%252=307%:%
+%:%253=308%:%
+%:%254=309%:%
+%:%255=310%:%
+%:%256=311%:%
+%:%257=312%:%
+%:%258=313%:%
+%:%259=314%:%
+%:%260=315%:%
+%:%261=316%:%
+%:%262=317%:%
+%:%263=318%:%
+%:%264=319%:%
+%:%265=320%:%
+%:%266=321%:%
+%:%267=322%:%
+%:%268=323%:%
+%:%269=324%:%
+%:%270=325%:%
+%:%271=326%:%
+%:%272=327%:%
+%:%273=328%:%
+%:%274=329%:%
+%:%275=330%:%
+%:%276=331%:%
+%:%277=332%:%
+%:%278=333%:%
+%:%279=334%:%
+%:%280=335%:%
+%:%281=336%:%
+%:%282=337%:%
+%:%283=338%:%
+%:%284=339%:%
+%:%285=340%:%
+%:%286=341%:%
+%:%287=342%:%
+%:%288=343%:%
+%:%289=344%:%
+%:%290=345%:%
+%:%291=346%:%
+%:%292=347%:%
+%:%293=348%:%
+%:%294=349%:%
+%:%295=350%:%
+%:%296=351%:%
+%:%297=352%:%
+%:%298=353%:%
+%:%299=354%:%
+%:%300=355%:%
+%:%301=356%:%
+%:%302=357%:%
+%:%303=358%:%
+%:%304=359%:%
+%:%305=360%:%
+%:%306=361%:%
+%:%307=362%:%
+%:%308=363%:%
+%:%309=364%:%
+%:%310=365%:%
+%:%311=366%:%
+%:%312=367%:%
+%:%313=368%:%
+%:%314=369%:%
+%:%315=370%:%
+%:%316=371%:%
+%:%316=372%:%
+%:%317=373%:%
+%:%318=374%:%
+%:%319=375%:%
+%:%320=376%:%
+%:%321=377%:%
+%:%322=378%:%
+%:%323=379%:%
+%:%324=380%:%
+%:%325=381%:%
+%:%326=382%:%
+%:%327=383%:%
+%:%328=384%:%
+%:%329=385%:%
+%:%330=386%:%
+%:%331=387%:%
+%:%332=388%:%
+%:%333=389%:%
+%:%334=390%:%
+%:%335=391%:%
+%:%336=392%:%
+%:%337=393%:%
+%:%338=394%:%
+%:%339=395%:%
+%:%340=396%:%
+%:%341=397%:%
+%:%342=398%:%
+%:%343=399%:%
+%:%344=400%:%
+%:%345=401%:%
+%:%346=402%:%
+%:%347=403%:%
+%:%348=404%:%
+%:%349=405%:%
+%:%350=406%:%
+%:%351=407%:%
+%:%352=408%:%
+%:%353=409%:%
+%:%354=410%:%
+%:%355=411%:%
+%:%356=412%:%
+%:%357=413%:%
+%:%358=414%:%
+%:%359=415%:%
+%:%360=416%:%
+%:%361=417%:%
+%:%362=418%:%
+%:%363=419%:%
+%:%364=420%:%
+%:%365=421%:%
+%:%366=422%:%
+%:%367=423%:%
+%:%368=424%:%
+%:%369=425%:%
+%:%370=426%:%
+%:%371=427%:%
+%:%372=428%:%
+%:%373=429%:%
+%:%374=430%:%
+%:%375=431%:%
+%:%376=432%:%
+%:%377=433%:%
+%:%378=434%:%
+%:%379=435%:%
+%:%380=436%:%
+%:%381=437%:%
+%:%382=438%:%
+%:%383=439%:%
+%:%384=440%:%
+%:%385=441%:%
+%:%386=442%:%
+%:%387=443%:%
+%:%388=444%:%
+%:%389=445%:%
+%:%390=446%:%
+%:%391=447%:%
+%:%392=448%:%
+%:%393=449%:%
+%:%394=450%:%
+%:%395=451%:%
+%:%396=452%:%
+%:%397=453%:%
+%:%398=454%:%
+%:%399=455%:%
+%:%400=456%:%
+%:%401=457%:%
+%:%402=458%:%
+%:%403=459%:%
+%:%404=460%:%
+%:%405=461%:%
+%:%406=462%:%
+%:%407=463%:%
+%:%408=464%:%
+%:%409=465%:%
+%:%410=466%:%
+%:%411=467%:%
+%:%412=468%:%
+%:%413=469%:%
+%:%414=470%:%
+%:%415=471%:%
+%:%416=472%:%
+%:%417=473%:%
+%:%418=474%:%
+%:%419=475%:%
+%:%420=476%:%
+%:%421=477%:%
+%:%430=484%:%
+%:%442=486%:%
+%:%443=487%:%
+%:%443=488%:%
+%:%444=489%:%
+%:%445=490%:%
+%:%446=491%:%
+%:%447=492%:%
+%:%448=493%:%
+%:%449=494%:%
+%:%450=495%:%
+%:%451=496%:%
+%:%452=497%:%
+%:%453=498%:%
+%:%454=499%:%
+%:%455=500%:%
+%:%456=501%:%
+%:%457=502%:%
+%:%458=503%:%
+%:%459=504%:%
+%:%460=505%:%
+%:%461=506%:%
+%:%462=507%:%
+%:%463=508%:%
+%:%464=509%:%
+%:%465=510%:%
+%:%466=511%:%
+%:%467=512%:%
+%:%468=513%:%
+%:%469=514%:%
+%:%470=515%:%
+%:%471=516%:%
+%:%472=517%:%
+%:%473=518%:%
+%:%474=519%:%
+%:%475=520%:%
+%:%476=521%:%
+%:%477=522%:%
+%:%478=523%:%
+%:%479=524%:%
+%:%480=525%:%
+%:%481=526%:%
+%:%482=527%:%
+%:%482=528%:%
+%:%483=529%:%
+%:%484=530%:%
+%:%485=531%:%
+%:%486=532%:%
+%:%487=533%:%
+%:%487=534%:%
+%:%488=535%:%
+%:%489=536%:%
+%:%490=537%:%
+%:%491=538%:%
+%:%492=539%:%
+%:%493=540%:%
+%:%494=541%:%
+%:%495=542%:%
+%:%496=543%:%
+%:%497=544%:%
+%:%498=545%:%
+%:%499=546%:%
+%:%500=547%:%
+%:%501=548%:%
+%:%502=549%:%
+%:%503=550%:%
+%:%504=551%:%
+%:%505=552%:%
+%:%506=553%:%
+%:%507=554%:%
+%:%508=555%:%
+%:%509=556%:%
+%:%510=557%:%
+%:%511=558%:%
+%:%512=559%:%
+%:%513=560%:%
+%:%514=561%:%
+%:%515=562%:%
+%:%516=563%:%
+%:%517=564%:%
+%:%518=565%:%
+%:%519=566%:%
+%:%520=567%:%
+%:%521=568%:%
+%:%522=569%:%
+%:%523=570%:%
+%:%524=571%:%
+%:%525=572%:%
+%:%526=573%:%
+%:%527=574%:%
+%:%528=575%:%
+%:%529=576%:%
+%:%530=577%:%
+%:%531=578%:%
+%:%532=579%:%
+%:%533=580%:%
+%:%534=581%:%
+%:%535=582%:%
+%:%536=583%:%
+%:%537=584%:%
+%:%538=585%:%
+%:%539=586%:%
+%:%540=587%:%
+%:%541=588%:%
+%:%542=589%:%
+%:%543=590%:%
+%:%544=591%:%
+%:%545=592%:%
+%:%546=593%:%
+%:%547=594%:%
+%:%548=595%:%
+%:%549=596%:%
+%:%550=597%:%
+%:%551=598%:%
+%:%552=599%:%
+%:%553=600%:%
+%:%554=601%:%
+%:%555=602%:%
+%:%556=603%:%
+%:%557=604%:%
+%:%558=605%:%
+%:%559=606%:%
+%:%560=607%:%
+%:%561=608%:%
+%:%562=609%:%
+%:%563=610%:%
+%:%564=611%:%
+%:%565=612%:%
+%:%566=613%:%
+%:%567=614%:%
+%:%568=615%:%
+%:%569=616%:%
+%:%570=617%:%
+%:%571=618%:%
+%:%572=619%:%
+%:%573=620%:%
+%:%574=621%:%
+%:%575=622%:%
+%:%576=623%:%
+%:%585=627%:%
+%:%597=631%:%
+%:%598=632%:%
+%:%599=633%:%
+%:%600=634%:%
+%:%601=635%:%
+%:%602=636%:%
+%:%603=637%:%
+%:%604=638%:%
+%:%605=639%:%
+%:%606=640%:%
+%:%607=641%:%
+%:%608=642%:%
+%:%609=643%:%
+%:%610=644%:%
+%:%611=645%:%
+%:%612=646%:%
+%:%613=647%:%
+%:%614=648%:%
+%:%615=649%:%
+%:%616=650%:%
+%:%617=651%:%
+%:%618=652%:%
+%:%619=653%:%
+%:%620=654%:%
+%:%621=655%:%
+%:%622=656%:%
+%:%623=657%:%
+%:%624=658%:%
+%:%625=659%:%
+%:%626=660%:%
+%:%627=661%:%
+%:%628=662%:%
+%:%629=663%:%
+%:%630=664%:%
+%:%631=665%:%
+%:%632=666%:%
+%:%633=667%:%
+%:%634=668%:%
+%:%635=669%:%
+%:%636=670%:%
+%:%637=671%:%
+%:%638=672%:%
+%:%639=673%:%
+%:%640=674%:%
+%:%641=675%:%
+%:%642=676%:%
+%:%643=677%:%
+%:%644=678%:%
+%:%645=679%:%
+%:%646=680%:%
+%:%647=681%:%
+%:%648=682%:%
+%:%649=683%:%
+%:%650=684%:%
+%:%651=685%:%
+%:%652=686%:%
+%:%653=687%:%
+%:%654=688%:%
+%:%655=689%:%
+%:%656=690%:%
+%:%657=691%:%
+%:%658=692%:%
+%:%659=693%:%
+%:%660=694%:%
+%:%661=695%:%
+%:%662=696%:%
+%:%663=697%:%
+%:%664=698%:%
+%:%665=699%:%
+%:%666=700%:%
+%:%667=701%:%
+%:%668=702%:%
+%:%669=703%:%
+%:%670=704%:%
+%:%671=705%:%
+%:%672=706%:%
+%:%673=707%:%
+%:%674=708%:%
+%:%675=709%:%
+%:%676=710%:%
+%:%677=711%:%
+%:%678=712%:%
+%:%679=713%:%
+%:%680=714%:%
+%:%681=715%:%
+%:%682=716%:%
+%:%683=717%:%
+%:%684=718%:%
+%:%685=719%:%
+%:%686=720%:%
+%:%687=721%:%
+%:%688=722%:%
+%:%689=723%:%
+%:%690=724%:%
+%:%691=725%:%
+%:%692=726%:%
+%:%693=727%:%
+%:%694=728%:%
+%:%695=729%:%
+%:%696=730%:%
+%:%697=731%:%
+%:%698=732%:%
+%:%699=733%:%
+%:%700=734%:%
+%:%701=735%:%
+%:%702=736%:%
+%:%703=737%:%
+%:%704=738%:%
+%:%705=739%:%
+%:%706=740%:%
+%:%707=741%:%
+%:%708=742%:%
+%:%709=743%:%
+%:%710=744%:%
+%:%711=745%:%
+%:%711=746%:%
+%:%712=747%:%
+%:%712=748%:%
+%:%713=749%:%
+%:%714=750%:%
+%:%714=751%:%
+%:%715=752%:%
+%:%716=753%:%
+%:%717=754%:%
+%:%718=755%:%
+%:%719=756%:%
+%:%720=757%:%
+%:%721=758%:%
+%:%722=759%:%
+%:%723=760%:%
+%:%724=761%:%
+%:%725=762%:%
+%:%726=763%:%
+%:%727=764%:%
+%:%728=765%:%
+%:%729=766%:%
+%:%730=767%:%
+%:%731=768%:%
+%:%732=769%:%
+%:%733=770%:%
+%:%734=771%:%
+%:%735=772%:%
+%:%736=773%:%
+%:%737=774%:%
+%:%738=775%:%
+%:%739=776%:%
+%:%740=777%:%
+%:%741=778%:%
+%:%742=779%:%
+%:%743=780%:%
+%:%744=781%:%
+%:%745=782%:%
+%:%746=783%:%
+%:%747=784%:%
+%:%748=785%:%
+%:%749=786%:%
+%:%750=787%:%
+%:%751=788%:%
+%:%752=789%:%
+%:%753=790%:%
+%:%754=791%:%
+%:%755=792%:%
+%:%756=793%:%
+%:%757=794%:%
+%:%758=795%:%
+%:%759=796%:%
+%:%760=797%:%
+%:%761=798%:%
+%:%762=799%:%
+%:%763=800%:%
+%:%764=801%:%
+%:%765=802%:%
+%:%766=803%:%
+%:%767=804%:%
+%:%768=805%:%
+%:%769=806%:%
+%:%770=807%:%
+%:%770=808%:%
+%:%770=809%:%
+%:%771=810%:%
+%:%772=811%:%
+%:%773=812%:%
+%:%774=813%:%
+%:%775=814%:%
+%:%776=815%:%
+%:%777=816%:%
+%:%778=817%:%
+%:%779=818%:%
+%:%779=819%:%
+%:%780=820%:%
+%:%781=821%:%
+%:%782=822%:%
+%:%783=823%:%
+%:%784=824%:%
+%:%785=825%:%
+%:%786=826%:%
+%:%787=827%:%
+%:%788=828%:%
+%:%789=829%:%
+%:%790=830%:%
+%:%791=831%:%
+%:%792=832%:%
+%:%793=833%:%
+%:%794=834%:%
+%:%795=835%:%
+%:%796=836%:%
+%:%797=837%:%
+%:%798=838%:%
+%:%799=839%:%
+%:%800=840%:%
+%:%801=841%:%
+%:%802=842%:%
+%:%803=843%:%
+%:%804=844%:%
+%:%805=845%:%
+%:%806=846%:%
+%:%807=847%:%
+%:%808=848%:%
+%:%809=849%:%
+%:%810=850%:%
+%:%811=851%:%
+%:%812=852%:%
+%:%813=853%:%
+%:%814=854%:%
+%:%814=855%:%
+%:%815=856%:%
+%:%816=857%:%
+%:%817=858%:%
+%:%818=859%:%
+%:%819=860%:%
+%:%820=861%:%
+%:%821=862%:%
+%:%821=863%:%
+%:%822=864%:%
+%:%823=865%:%
+%:%824=866%:%
+%:%824=867%:%
+%:%825=868%:%
+%:%826=869%:%
+%:%827=870%:%
+%:%828=871%:%
+%:%829=872%:%
+%:%830=873%:%
+%:%831=874%:%
+%:%832=875%:%
+%:%833=876%:%
+%:%834=877%:%
+%:%835=878%:%
+%:%835=879%:%
+%:%836=880%:%
+%:%837=881%:%
+%:%838=882%:%
+%:%839=883%:%
+%:%839=884%:%
+%:%840=885%:%
+%:%841=886%:%
+%:%842=887%:%
+%:%843=888%:%
+%:%844=889%:%
+%:%845=890%:%
+%:%846=891%:%
+%:%847=892%:%
+%:%848=893%:%
+%:%849=894%:%
+%:%850=895%:%
+%:%851=896%:%
+%:%852=897%:%
+%:%853=898%:%
+%:%854=899%:%
+%:%855=900%:%
+%:%856=901%:%
+%:%857=902%:%
+%:%858=903%:%
+%:%859=904%:%
+%:%860=905%:%
+%:%861=906%:%
+%:%862=907%:%
+%:%863=908%:%
+%:%864=909%:%
+%:%865=910%:%
+%:%866=911%:%
+%:%867=912%:%
+%:%868=913%:%
+%:%869=914%:%
+%:%870=915%:%
+%:%871=916%:%
+%:%872=917%:%
+%:%873=918%:%
+%:%874=919%:%
+%:%875=920%:%
+%:%876=921%:%
+%:%877=922%:%
+%:%878=923%:%
+%:%879=924%:%
+%:%880=925%:%
+%:%881=926%:%
+%:%882=927%:%
+%:%883=928%:%
+%:%884=929%:%
+%:%885=930%:%
+%:%886=931%:%
+%:%887=932%:%
+%:%888=933%:%
+%:%889=934%:%
+%:%890=935%:%
+%:%891=936%:%
+%:%892=937%:%
+%:%893=938%:%
+%:%894=939%:%
+%:%895=940%:%
+%:%896=941%:%
+%:%897=942%:%
+%:%897=943%:%
+%:%898=944%:%
+%:%899=945%:%
+%:%900=946%:%
+%:%901=947%:%
+%:%902=948%:%
+%:%903=949%:%
+%:%904=950%:%
+%:%905=951%:%
+%:%906=952%:%
+%:%907=953%:%
+%:%908=954%:%
+%:%909=955%:%
+%:%910=956%:%
+%:%911=957%:%
+%:%912=958%:%
+%:%913=959%:%
+%:%914=960%:%
+%:%915=961%:%
+%:%916=962%:%
+%:%917=963%:%
+%:%918=964%:%
+%:%919=965%:%
+%:%920=966%:%
+%:%921=967%:%
+%:%922=968%:%
+%:%923=969%:%
+%:%924=970%:%
+%:%925=971%:%
+%:%926=972%:%
+%:%927=973%:%
+%:%928=974%:%
+%:%929=975%:%
+%:%930=976%:%
+%:%930=977%:%
+%:%931=978%:%
+%:%932=979%:%
+%:%933=980%:%
+%:%934=981%:%
+%:%935=982%:%
+%:%936=983%:%
+%:%937=984%:%
+%:%938=985%:%
+%:%939=986%:%
+%:%940=987%:%
+%:%941=988%:%
+%:%942=989%:%
+%:%943=990%:%
+%:%944=991%:%
+%:%945=992%:%
+%:%946=993%:%
+%:%947=994%:%
+%:%948=995%:%
+%:%949=996%:%
+%:%950=997%:%
+%:%951=998%:%
+%:%952=999%:%
+%:%953=1000%:%
+%:%954=1001%:%
+%:%955=1002%:%
+%:%956=1003%:%
+%:%957=1004%:%
+%:%958=1005%:%
+%:%959=1006%:%
+%:%960=1007%:%
+%:%960=1008%:%
+%:%961=1009%:%
+%:%962=1010%:%
+%:%963=1011%:%
+%:%964=1012%:%
+%:%965=1013%:%
+%:%966=1014%:%
+%:%967=1015%:%
+%:%968=1016%:%
+%:%968=1017%:%
+%:%969=1018%:%
+%:%970=1019%:%
+%:%971=1020%:%
+%:%972=1021%:%
+%:%973=1022%:%
+%:%974=1023%:%
+%:%975=1024%:%
+%:%976=1025%:%
+%:%977=1026%:%
+%:%978=1027%:%
+%:%979=1028%:%
+%:%980=1029%:%
+%:%981=1030%:%
+%:%982=1031%:%
+%:%983=1032%:%
+%:%984=1033%:%
+%:%985=1034%:%
+%:%986=1035%:%
+%:%987=1036%:%
+%:%988=1037%:%
+%:%989=1038%:%
+%:%990=1039%:%
+%:%991=1040%:%
+%:%992=1041%:%
+%:%993=1042%:%
+%:%994=1043%:%
+%:%995=1044%:%
+%:%996=1045%:%
+%:%997=1046%:%
+%:%998=1047%:%
+%:%999=1048%:%
+%:%1000=1049%:%
+%:%1001=1050%:%
+%:%1002=1051%:%
+%:%1003=1052%:%
+%:%1004=1053%:%
+%:%1005=1054%:%
+%:%1005=1055%:%
+%:%1005=1056%:%
+%:%1006=1057%:%
+%:%1006=1058%:%
+%:%1006=1059%:%
+%:%1007=1060%:%
+%:%1008=1061%:%
+%:%1008=1062%:%
+%:%1009=1063%:%
+%:%1010=1064%:%
+%:%1011=1065%:%
+%:%1012=1066%:%
+%:%1013=1067%:%
+%:%1014=1068%:%
+%:%1015=1069%:%
+%:%1016=1070%:%
+%:%1017=1071%:%
+%:%1018=1072%:%
+%:%1019=1073%:%
+%:%1020=1074%:%
+%:%1021=1075%:%
+%:%1022=1076%:%
+%:%1023=1077%:%
+%:%1024=1078%:%
+%:%1025=1079%:%
+%:%1026=1080%:%
+%:%1027=1081%:%
+%:%1028=1082%:%
+%:%1029=1083%:%
+%:%1030=1084%:%
+%:%1031=1085%:%
+%:%1032=1086%:%
+%:%1033=1087%:%
+%:%1034=1088%:%
+%:%1035=1089%:%
+%:%1036=1090%:%
+%:%1037=1091%:%
+%:%1038=1092%:%
+%:%1039=1093%:%
+%:%1040=1094%:%
+%:%1041=1095%:%
+%:%1042=1096%:%
+%:%1042=1097%:%
+%:%1043=1098%:%
+%:%1044=1099%:%
+%:%1045=1100%:%
+%:%1045=1101%:%
+%:%1045=1102%:%
+%:%1045=1103%:%
+%:%1046=1104%:%
+%:%1047=1105%:%
+%:%1048=1106%:%
+%:%1049=1107%:%
+%:%1050=1108%:%
+%:%1051=1109%:%
+%:%1052=1110%:%
+%:%1053=1111%:%
+%:%1054=1112%:%
+%:%1055=1113%:%
+%:%1056=1114%:%
+%:%1057=1115%:%
+%:%1058=1116%:%
+%:%1059=1117%:%
+%:%1060=1118%:%
+%:%1061=1119%:%
+%:%1062=1120%:%
+%:%1063=1121%:%
+%:%1064=1122%:%
+%:%1065=1123%:%
+%:%1066=1124%:%
+%:%1067=1125%:%
+%:%1068=1126%:%
+%:%1069=1127%:%
+%:%1070=1128%:%
+%:%1071=1129%:%
+%:%1072=1130%:%
+%:%1073=1131%:%
+%:%1074=1132%:%
+%:%1075=1133%:%
+%:%1076=1134%:%
+%:%1077=1135%:%
+%:%1078=1136%:%
+%:%1079=1137%:%
+%:%1080=1138%:%
+%:%1081=1139%:%
+%:%1082=1140%:%
+%:%1091=1144%:%
+%:%1103=1148%:%
+%:%1104=1149%:%
+%:%1105=1150%:%
+%:%1106=1151%:%
+%:%1107=1152%:%
+%:%1108=1153%:%
+%:%1109=1154%:%
+%:%1110=1155%:%
+%:%1111=1156%:%
+%:%1112=1157%:%
+%:%1113=1158%:%
+%:%1114=1159%:%
+%:%1115=1160%:%
+%:%1116=1161%:%
+%:%1117=1162%:%
+%:%1118=1163%:%
+%:%1119=1164%:%
+%:%1120=1165%:%
+%:%1121=1166%:%
+%:%1122=1167%:%
+%:%1123=1168%:%
+%:%1124=1169%:%
+%:%1125=1170%:%
+%:%1126=1171%:%
+%:%1127=1172%:%
+%:%1128=1173%:%
+%:%1129=1174%:%
+%:%1130=1175%:%
+%:%1131=1176%:%
+%:%1132=1177%:%
+%:%1133=1178%:%
+%:%1134=1179%:%
+%:%1135=1180%:%
+%:%1136=1181%:%
+%:%1137=1182%:%
+%:%1138=1183%:%
+%:%1139=1184%:%
+%:%1140=1185%:%
+%:%1141=1186%:%
+%:%1142=1187%:%
+%:%1143=1188%:%
+%:%1144=1189%:%
+%:%1145=1190%:%
+%:%1146=1191%:%
+%:%1147=1192%:%
+%:%1148=1193%:%
+%:%1149=1194%:%
+%:%1150=1195%:%
+%:%1151=1196%:%
+%:%1152=1197%:%
+%:%1153=1198%:%
+%:%1154=1199%:%
+%:%1155=1200%:%
+%:%1156=1201%:%
+%:%1157=1202%:%
+%:%1158=1203%:%
+%:%1159=1204%:%
+%:%1160=1205%:%
+%:%1161=1206%:%
+%:%1162=1207%:%
+%:%1163=1208%:%
+%:%1164=1209%:%
+%:%1165=1210%:%
+%:%1166=1211%:%
+%:%1167=1212%:%
+%:%1168=1213%:%
+%:%1169=1214%:%
+%:%1170=1215%:%
+%:%1171=1216%:%
+%:%1172=1217%:%
+%:%1173=1218%:%
+%:%1174=1219%:%
+%:%1175=1220%:%
+%:%1176=1221%:%
+%:%1177=1222%:%
+%:%1178=1223%:%
+%:%1179=1224%:%
+%:%1180=1225%:%
+%:%1181=1226%:%
+%:%1182=1227%:%
+%:%1183=1228%:%
+%:%1184=1229%:%
+%:%1185=1230%:%
+%:%1186=1231%:%
+%:%1187=1232%:%
+%:%1188=1233%:%
+%:%1189=1234%:%
+%:%1190=1235%:%
+%:%1191=1236%:%
+%:%1192=1237%:%
+%:%1193=1238%:%
+%:%1194=1239%:%
+%:%1195=1240%:%
+%:%1196=1241%:%
+%:%1197=1242%:%
+%:%1198=1243%:%
+%:%1199=1244%:%
+%:%1200=1245%:%
+%:%1201=1246%:%
+%:%1202=1247%:%
+%:%1203=1248%:%
+%:%1204=1249%:%
+%:%1205=1250%:%
+%:%1206=1251%:%
+%:%1207=1252%:%
+%:%1208=1253%:%
+%:%1209=1254%:%
+%:%1210=1255%:%
+%:%1211=1256%:%
+%:%1212=1257%:%
+%:%1213=1258%:%
+%:%1214=1259%:%
+%:%1215=1260%:%
+%:%1216=1261%:%
+%:%1217=1262%:%
+%:%1218=1263%:%
+%:%1218=1264%:%
+%:%1219=1265%:%
+%:%1220=1266%:%
+%:%1221=1267%:%
+%:%1222=1268%:%
+%:%1223=1269%:%
+%:%1224=1270%:%
+%:%1225=1271%:%
+%:%1226=1272%:%
+%:%1227=1273%:%
+%:%1228=1274%:%
+%:%1229=1275%:%
+%:%1229=1276%:%
+%:%1230=1277%:%
+%:%1231=1278%:%
+%:%1232=1279%:%
+%:%1233=1280%:%
+%:%1234=1281%:%
+%:%1235=1282%:%
+%:%1236=1283%:%
+%:%1237=1284%:%
+%:%1238=1285%:%
+%:%1239=1286%:%
+%:%1240=1287%:%
+%:%1241=1288%:%
+%:%1242=1289%:%
+%:%1243=1290%:%
+%:%1244=1291%:%
+%:%1245=1292%:%
+%:%1246=1293%:%
+%:%1247=1294%:%
+%:%1248=1295%:%
+%:%1249=1296%:%
+%:%1250=1297%:%
+%:%1251=1298%:%
+%:%1252=1299%:%
+%:%1253=1300%:%
+%:%1254=1301%:%
+%:%1255=1302%:%
+%:%1256=1303%:%
+%:%1257=1304%:%
+%:%1258=1305%:%
+%:%1259=1306%:%
+%:%1260=1307%:%
+%:%1261=1308%:%
+%:%1262=1309%:%
+%:%1263=1310%:%
+%:%1264=1311%:%
+%:%1265=1312%:%
+%:%1266=1313%:%
+%:%1267=1314%:%
+%:%1268=1315%:%
+%:%1269=1316%:%
+%:%1270=1317%:%
+%:%1271=1318%:%
+%:%1272=1319%:%
+%:%1273=1320%:%
+%:%1274=1321%:%
+%:%1275=1322%:%
+%:%1276=1323%:%
+%:%1277=1324%:%
+%:%1278=1325%:%
+%:%1279=1326%:%
+%:%1280=1327%:%
+%:%1281=1328%:%
+%:%1282=1329%:%
+%:%1283=1330%:%
+%:%1283=1331%:%
+%:%1283=1332%:%
+%:%1284=1333%:%
+%:%1285=1334%:%
+%:%1285=1335%:%
+%:%1285=1336%:%
+%:%1285=1337%:%
+%:%1286=1338%:%
+%:%1287=1339%:%
+%:%1288=1340%:%
+%:%1289=1341%:%
+%:%1290=1342%:%
+%:%1290=1343%:%
+%:%1291=1344%:%
+%:%1292=1345%:%
+%:%1293=1346%:%
+%:%1294=1347%:%
+%:%1295=1348%:%
+%:%1296=1349%:%
+%:%1297=1350%:%
+%:%1298=1351%:%
+%:%1299=1352%:%
+%:%1300=1353%:%
+%:%1301=1354%:%
+%:%1302=1355%:%
+%:%1303=1356%:%
+%:%1304=1357%:%
+%:%1305=1358%:%
+%:%1306=1359%:%
+%:%1307=1360%:%
+%:%1308=1361%:%
+%:%1309=1362%:%
+%:%1310=1363%:%
+%:%1311=1364%:%
+%:%1312=1365%:%
+%:%1313=1366%:%
+%:%1314=1367%:%
+%:%1315=1368%:%
+%:%1316=1369%:%
+%:%1317=1370%:%
+%:%1318=1371%:%
+%:%1319=1372%:%
+%:%1320=1373%:%
+%:%1321=1374%:%
+%:%1322=1375%:%
+%:%1323=1376%:%
+%:%1324=1377%:%
+%:%1325=1378%:%
+%:%1326=1379%:%
+%:%1327=1380%:%
+%:%1328=1381%:%
+%:%1329=1382%:%
+%:%1330=1383%:%
+%:%1331=1384%:%
+%:%1332=1385%:%
+%:%1333=1386%:%
+%:%1334=1387%:%
+%:%1335=1388%:%
+%:%1336=1389%:%
+%:%1337=1390%:%
+%:%1338=1391%:%
+%:%1338=1392%:%
+%:%1339=1393%:%
+%:%1339=1394%:%
+%:%1340=1395%:%
+%:%1340=1396%:%
+%:%1341=1397%:%
+%:%1342=1398%:%
+%:%1343=1399%:%
+%:%1344=1400%:%
+%:%1345=1401%:%
+%:%1346=1402%:%
+%:%1347=1403%:%
+%:%1347=1404%:%
+%:%1348=1405%:%
+%:%1348=1406%:%
+%:%1349=1407%:%
+%:%1349=1408%:%
+%:%1350=1409%:%
+%:%1351=1410%:%
+%:%1352=1411%:%
+%:%1353=1412%:%
+%:%1354=1413%:%
+%:%1355=1414%:%
+%:%1356=1415%:%
+%:%1357=1416%:%
+%:%1358=1417%:%
+%:%1359=1418%:%
+%:%1360=1419%:%
+%:%1361=1420%:%
+%:%1362=1421%:%
+%:%1363=1422%:%
+%:%1364=1423%:%
+%:%1365=1424%:%
+%:%1366=1425%:%
+%:%1367=1426%:%
+%:%1368=1427%:%
+%:%1369=1428%:%
+%:%1370=1429%:%
+%:%1371=1430%:%
+%:%1372=1431%:%
+%:%1373=1432%:%
+%:%1374=1433%:%
+%:%1375=1434%:%
+%:%1376=1435%:%
+%:%1377=1436%:%
+%:%1378=1437%:%
+%:%1379=1438%:%
+%:%1380=1439%:%
+%:%1380=1440%:%
+%:%1381=1441%:%
+%:%1382=1442%:%
+%:%1383=1443%:%
+%:%1384=1444%:%
+%:%1385=1445%:%
+%:%1386=1446%:%
+%:%1387=1447%:%
+%:%1387=1448%:%
+%:%1388=1449%:%
+%:%1389=1450%:%
+%:%1390=1451%:%
+%:%1390=1452%:%
+%:%1391=1453%:%
+%:%1392=1454%:%
+%:%1393=1455%:%
+%:%1393=1456%:%
+%:%1394=1457%:%
+%:%1394=1458%:%
+%:%1395=1459%:%
+%:%1395=1460%:%
+%:%1396=1461%:%
+%:%1397=1462%:%
+%:%1398=1463%:%
+%:%1398=1464%:%
+%:%1399=1465%:%
+%:%1399=1466%:%
+%:%1400=1467%:%
+%:%1400=1468%:%
+%:%1400=1469%:%
+%:%1400=1470%:%
+%:%1401=1471%:%
+%:%1401=1472%:%
+%:%1402=1473%:%
+%:%1403=1474%:%
+%:%1403=1476%:%
+%:%1403=1477%:%
+%:%1403=1478%:%
+%:%1403=1479%:%
+%:%1403=1480%:%
+%:%1404=1481%:%
+%:%1404=1482%:%
+%:%1405=1483%:%
+%:%1405=1484%:%
+%:%1406=1485%:%
+%:%1406=1486%:%
+%:%1407=1487%:%
+%:%1408=1488%:%
+%:%1409=1489%:%
+%:%1410=1490%:%
+%:%1410=1491%:%
+%:%1411=1492%:%
+%:%1411=1493%:%
+%:%1412=1494%:%
+%:%1413=1495%:%
+%:%1413=1496%:%
+%:%1414=1497%:%
+%:%1415=1498%:%
+%:%1416=1499%:%
+%:%1417=1500%:%
+%:%1418=1501%:%
+%:%1419=1502%:%
+%:%1420=1503%:%
+%:%1421=1504%:%
+%:%1422=1505%:%
+%:%1423=1506%:%
+%:%1424=1507%:%
+%:%1425=1508%:%
+%:%1426=1509%:%
+%:%1427=1510%:%
+%:%1428=1511%:%
+%:%1429=1512%:%
+%:%1430=1513%:%
+%:%1431=1514%:%
+%:%1432=1515%:%
+%:%1433=1516%:%
+%:%1434=1517%:%
+%:%1435=1518%:%
+%:%1436=1519%:%
+%:%1437=1520%:%
+%:%1438=1521%:%
+%:%1439=1522%:%
+%:%1440=1523%:%
+%:%1441=1524%:%
+%:%1442=1525%:%
+%:%1443=1526%:%
+%:%1444=1527%:%
+%:%1445=1528%:%
+%:%1446=1529%:%
+%:%1447=1530%:%
+%:%1448=1531%:%
+%:%1449=1532%:%
+%:%1450=1533%:%
+%:%1451=1534%:%
+%:%1452=1535%:%
+%:%1453=1536%:%
+%:%1454=1537%:%
+%:%1455=1538%:%
+%:%1456=1539%:%
+%:%1457=1540%:%
+%:%1458=1541%:%
+%:%1459=1542%:%
+%:%1460=1543%:%
+%:%1461=1544%:%
+%:%1462=1545%:%
+%:%1463=1546%:%
+%:%1464=1547%:%
+%:%1473=1551%:%
+%:%1485=1558%:%
+%:%1486=1559%:%
+%:%1487=1560%:%
+%:%1488=1561%:%
+%:%1489=1562%:%
+%:%1490=1563%:%
+%:%1491=1564%:%
+%:%1500=1569%:%
+%:%1512=1573%:%
+%:%1513=1574%:%
+%:%1514=1575%:%
+%:%1515=1576%:%
+%:%1516=1577%:%
+%:%1517=1578%:%
+%:%1518=1579%:%
+%:%1519=1580%:%
+%:%1520=1581%:%
+%:%1521=1582%:%
+%:%1522=1583%:%
+%:%1523=1584%:%
+%:%1524=1585%:%
+%:%1525=1586%:%
+%:%1526=1587%:%
+%:%1527=1588%:%
+%:%1528=1589%:%
+%:%1529=1590%:%
+%:%1530=1591%:%
+%:%1531=1592%:%
+%:%1532=1593%:%
+%:%1533=1594%:%
+%:%1534=1595%:%
+%:%1535=1596%:%
+%:%1536=1597%:%
+%:%1537=1598%:%
+%:%1538=1599%:%
+%:%1539=1600%:%
+%:%1540=1601%:%
+%:%1541=1602%:%
+%:%1542=1603%:%
+%:%1543=1604%:%
+%:%1544=1605%:%
+%:%1545=1606%:%
+%:%1546=1607%:%
+%:%1547=1608%:%
+%:%1548=1609%:%
+%:%1549=1610%:%
+%:%1550=1611%:%
+%:%1551=1612%:%
+%:%1552=1613%:%
+%:%1553=1614%:%
+%:%1554=1615%:%
+%:%1555=1616%:%
+%:%1556=1617%:%
+%:%1557=1618%:%
+%:%1558=1619%:%
+%:%1559=1620%:%
+%:%1560=1621%:%
+%:%1561=1622%:%
+%:%1562=1623%:%
+%:%1563=1624%:%
+%:%1564=1625%:%
+%:%1565=1626%:%
+%:%1566=1627%:%
+%:%1567=1628%:%
+%:%1568=1629%:%
+%:%1569=1630%:%
+%:%1570=1631%:%
+%:%1571=1632%:%
+%:%1572=1633%:%
+%:%1573=1634%:%
+%:%1574=1635%:%
+%:%1575=1636%:%
+%:%1576=1637%:%
+%:%1577=1638%:%
+%:%1578=1639%:%
+%:%1579=1640%:%
+%:%1580=1641%:%
+%:%1581=1642%:%
+%:%1582=1643%:%
+%:%1583=1644%:%
+%:%1584=1645%:%
+%:%1585=1646%:%
+%:%1586=1647%:%
+%:%1587=1648%:%
+%:%1588=1649%:%
+%:%1589=1650%:%
+%:%1590=1651%:%
+%:%1591=1652%:%
+%:%1592=1653%:%
+%:%1593=1654%:%
+%:%1594=1655%:%
+%:%1595=1656%:%
+%:%1596=1657%:%
+%:%1597=1658%:%
+%:%1598=1659%:%
+%:%1599=1660%:%
+%:%1600=1661%:%
+%:%1601=1662%:%
+%:%1601=1778%:%
+%:%1602=1779%:%
+%:%1603=1780%:%
+%:%1604=1781%:%
+%:%1605=1782%:%
+%:%1605=1943%:%
+%:%1606=1944%:%
+%:%1607=1945%:%
+%:%1608=1946%:%
+%:%1609=1947%:%
+%:%1610=1948%:%
+%:%1611=1949%:%
+%:%1612=1950%:%
+%:%1613=1951%:%
+%:%1614=1952%:%
+%:%1615=1953%:%
+%:%1616=1954%:%
+%:%1617=1955%:%
+%:%1618=1956%:%
+%:%1619=1957%:%
+%:%1620=1958%:%
+%:%1621=1959%:%
+%:%1622=1960%:%
+%:%1623=1961%:%
+%:%1624=1962%:%
+%:%1624=1963%:%
+%:%1625=1964%:%
+%:%1625=1965%:%
+%:%1625=1966%:%
+%:%1626=1967%:%
+%:%1626=1968%:%
+%:%1627=1969%:%
+%:%1628=1970%:%
+%:%1629=1971%:%
+%:%1630=1972%:%
+%:%1631=1973%:%
+%:%1632=1974%:%
+%:%1633=1975%:%
+%:%1634=1976%:%
+%:%1635=1977%:%
+%:%1636=1978%:%
+%:%1637=1979%:%
+%:%1638=1980%:%
+%:%1639=1981%:%
+%:%1640=1982%:%
+%:%1641=1983%:%
+%:%1642=1984%:%
+%:%1643=1985%:%
+%:%1643=1986%:%
+%:%1644=1987%:%
+%:%1645=1988%:%
+%:%1646=1989%:%
+%:%1646=1990%:%
+%:%1646=1991%:%
+%:%1647=1992%:%
+%:%1648=1993%:%
+%:%1649=1994%:%
+%:%1649=1995%:%
+%:%1650=1996%:%
+%:%1650=1997%:%
+%:%1651=1998%:%
+%:%1652=1999%:%
+%:%1653=2000%:%
+%:%1654=2001%:%
+%:%1655=2002%:%
+%:%1656=2003%:%
+%:%1657=2004%:%
+%:%1658=2005%:%
+%:%1659=2006%:%
+%:%1660=2007%:%
+%:%1661=2008%:%
+%:%1662=2009%:%
+%:%1663=2010%:%
+%:%1664=2011%:%
+%:%1665=2012%:%
+%:%1666=2013%:%
+%:%1667=2014%:%
+%:%1676=2019%:%
+%:%1688=2023%:%
+%:%1689=2024%:%
+%:%1690=2025%:%
+%:%1691=2026%:%
+%:%1692=2027%:%
+%:%1693=2028%:%
+%:%1694=2029%:%
+%:%1695=2030%:%
+%:%1696=2031%:%
+%:%1697=2032%:%
+%:%1698=2033%:%
+%:%1699=2034%:%
+%:%1700=2035%:%
+%:%1701=2036%:%
+%:%1702=2037%:%
+%:%1703=2038%:%
+%:%1704=2039%:%
+%:%1705=2040%:%
+%:%1706=2041%:%
+%:%1707=2042%:%
+%:%1708=2043%:%
+%:%1709=2044%:%
+%:%1710=2045%:%
+%:%1711=2046%:%
+%:%1712=2047%:%
+%:%1713=2048%:%
+%:%1714=2049%:%
+%:%1715=2050%:%
+%:%1716=2051%:%
+%:%1717=2052%:%
+%:%1718=2053%:%
+%:%1719=2054%:%
+%:%1720=2055%:%
+%:%1721=2056%:%
+%:%1722=2057%:%
+%:%1723=2058%:%
+%:%1724=2059%:%
+%:%1725=2060%:%
+%:%1726=2061%:%
+%:%1727=2062%:%
+%:%1728=2063%:%
+%:%1729=2064%:%
+%:%1730=2065%:%
+%:%1731=2066%:%
+%:%1732=2067%:%
+%:%1733=2068%:%
+%:%1734=2069%:%
+%:%1735=2070%:%
+%:%1736=2071%:%
+%:%1737=2072%:%
+%:%1738=2073%:%
+%:%1739=2074%:%
+%:%1740=2075%:%
+%:%1753=2081%:%
+%:%1756=2082%:%
+%:%1757=2083%:%
--- a/thys2/SizeBound.thy Sat Jan 08 15:26:33 2022 +0000
+++ b/thys2/SizeBound.thy Tue Jan 11 23:58:39 2022 +0000
@@ -138,6 +138,14 @@
apply(auto)
done
+lemma fuse_Nil:
+ shows "fuse [] r = r"
+ by (induct r)(simp_all)
+
+lemma map_fuse_Nil:
+ shows "map (fuse []) rs = rs"
+ by (induct rs)(simp_all add: fuse_Nil)
+
fun intern :: "rexp \<Rightarrow> arexp" where
"intern ZERO = AZERO"
@@ -737,18 +745,6 @@
done
-lemma bsimp_AALTs_qq:
- assumes "1 < length rs"
- shows "bsimp_AALTs bs rs = AALTs bs rs"
- using assms
- apply(case_tac rs)
- apply(simp)
- apply(case_tac list)
- apply(simp_all)
- done
-
-
-
lemma bbbbs1:
shows "nonalt r \<or> (\<exists>bs rs. r = AALTs bs rs)"
using nonalt.elims(3) by auto
@@ -868,23 +864,21 @@
apply(simp_all)
done
+
+
+
inductive
rrewrite:: "arexp \<Rightarrow> arexp \<Rightarrow> bool" ("_ \<leadsto> _" [99, 99] 99)
where
"ASEQ bs AZERO r2 \<leadsto> AZERO"
| "ASEQ bs r1 AZERO \<leadsto> AZERO"
-| "ASEQ bs (AONE bs1) r \<leadsto> fuse (bs@bs1) r"
+| "ASEQ bs1 (AONE bs2) r \<leadsto> fuse (bs1@bs2) r"
| "r1 \<leadsto> r2 \<Longrightarrow> ASEQ bs r1 r3 \<leadsto> ASEQ bs r2 r3"
| "r3 \<leadsto> r4 \<Longrightarrow> ASEQ bs r1 r3 \<leadsto> ASEQ bs r1 r4"
| "r \<leadsto> r' \<Longrightarrow> (AALTs bs (rs1 @ [r] @ rs2)) \<leadsto> (AALTs bs (rs1 @ [r'] @ rs2))"
(*context rule for eliminating 0, alts--corresponds to the recursive call flts r::rs = r::(flts rs)*)
| "AALTs bs (rsa@ [AZERO] @ rsb) \<leadsto> AALTs bs (rsa @ rsb)"
| "AALTs bs (rsa@ [AALTs bs1 rs1] @ rsb) \<leadsto> AALTs bs (rsa@(map (fuse bs1) rs1)@rsb)"
-(*the below rule for extracting common prefixes between a list of rexp's bitcodes*)
-(***| "AALTs bs (map (fuse bs1) rs) \<leadsto> AALTs (bs@bs1) rs"******)
-(*opposite direction also allowed, which means bits are free to be moved around
-as long as they are on the right path*)
-| "AALTs (bs@bs1) rs \<leadsto> AALTs bs (map (fuse bs1) rs)"
| "AALTs bs [] \<leadsto> AZERO"
| "AALTs bs [r] \<leadsto> fuse bs r"
| "erase a1 = erase a2 \<Longrightarrow> AALTs bs (rsa@[a1]@rsb@[a2]@rsc) \<leadsto> AALTs bs (rsa@[a1]@rsb@rsc)"
@@ -896,17 +890,22 @@
rs1[intro, simp]:"r \<leadsto>* r"
| rs2[intro]: "\<lbrakk>r1 \<leadsto>* r2; r2 \<leadsto> r3\<rbrakk> \<Longrightarrow> r1 \<leadsto>* r3"
+
inductive
srewrites:: "arexp list \<Rightarrow> arexp list \<Rightarrow> bool" (" _ s\<leadsto>* _" [100, 100] 100)
where
ss1: "[] s\<leadsto>* []"
| ss2: "\<lbrakk>r \<leadsto>* r'; rs s\<leadsto>* rs'\<rbrakk> \<Longrightarrow> (r#rs) s\<leadsto>* (r'#rs')"
-(*
-rs1 = [r1, r2, ..., rn] rs2 = [r1', r2', ..., rn']
- [r1, r2, ..., rn] \<leadsto>* [r1', r2, ..., rn] \<leadsto>* [...r2',...] \<leadsto>* [r1', r2',... rn']
-*)
+(* rewrites for lists *)
+inductive
+ frewrites:: "arexp list \<Rightarrow> arexp list \<Rightarrow> bool" (" _ f\<leadsto>* _" [100, 100] 100)
+where
+ fs1: "[] f\<leadsto>* []"
+| fs2: "\<lbrakk>rs f\<leadsto>* rs'\<rbrakk> \<Longrightarrow> (AZERO#rs) f\<leadsto>* rs'"
+| fs3: "\<lbrakk>rs f\<leadsto>* rs'\<rbrakk> \<Longrightarrow> ((AALTs bs rs1) # rs) f\<leadsto>* ((map (fuse bs) rs1) @ rs')"
+| fs4: "\<lbrakk>rs f\<leadsto>* rs'; nonalt r; nonazero r\<rbrakk> \<Longrightarrow> (r#rs) f\<leadsto>* (r#rs')"
lemma r_in_rstar : "r1 \<leadsto> r2 \<Longrightarrow> r1 \<leadsto>* r2"
@@ -952,7 +951,6 @@
apply auto
done
-
corollary srewrites_alt1:
assumes "rs1 s\<leadsto>* rs2"
shows "AALTs bs rs1 \<leadsto>* AALTs bs rs2"
@@ -992,7 +990,8 @@
and "ACHAR bs c \<leadsto>* bsimp (ACHAR bs c)"
by (simp_all)
-lemma trivialbsimpsrewrites:
+
+lemma trivialbsimp_srewrites:
"\<lbrakk>\<And>x. x \<in> set rs \<Longrightarrow> x \<leadsto>* f x \<rbrakk> \<Longrightarrow> rs s\<leadsto>* (map f rs)"
apply(induction rs)
@@ -1001,29 +1000,13 @@
by (metis insert_iff list.simps(15) list.simps(9) srewrites.simps)
-lemma bsimp_AALTsrewrites:
+lemma bsimp_AALTs_rewrites:
"AALTs bs1 rs \<leadsto>* bsimp_AALTs bs1 rs"
apply(induction rs)
apply simp
apply(rule r_in_rstar)
- apply (simp add: rrewrite.intros(10))
- apply(case_tac "rs = Nil")
- apply(simp)
- using rrewrite.intros(12) apply auto[1]
- using r_in_rstar rrewrite.intros(11) apply presburger
- apply(subgoal_tac "length (a#rs) > 1")
- apply(simp add: bsimp_AALTs_qq)
- apply(simp)
- done
-
-(* rewrites for lists *)
-inductive
- frewrites:: "arexp list \<Rightarrow> arexp list \<Rightarrow> bool" (" _ f\<leadsto>* _" [100, 100] 100)
-where
- fs1: "[] f\<leadsto>* []"
-| fs2: "\<lbrakk>rs f\<leadsto>* rs'\<rbrakk> \<Longrightarrow> (AZERO#rs) f\<leadsto>* rs'"
-| fs3: "\<lbrakk>rs f\<leadsto>* rs'\<rbrakk> \<Longrightarrow> ((AALTs bs rs1) # rs) f\<leadsto>* ((map (fuse bs) rs1) @ rs')"
-| fs4: "\<lbrakk>rs f\<leadsto>* rs'; nonalt r; nonazero r\<rbrakk> \<Longrightarrow> (r#rs) f\<leadsto>* (r#rs')"
+ using rrewrite.intros(9) apply blast
+ by (metis bsimp_AALTs.elims list.discI rrewrite.intros(10) rrewrites.simps)
@@ -1082,7 +1065,7 @@
apply auto
done
-lemma fltsrewrites: " AALTs bs1 rs \<leadsto>* AALTs bs1 (flts rs)"
+lemma flts_rewrites: " AALTs bs1 rs \<leadsto>* AALTs bs1 (flts rs)"
apply(induction rs)
apply simp
apply(case_tac "a = AZERO")
@@ -1103,13 +1086,40 @@
apply (meson fltsfrewrites fs4 nonalt.elims(3) nonazero.elims(3))
by (metis append_Cons append_Nil fltsfrewrites frewritesaalts flts_append k0a)
-lemma alts_simpalts: "\<And>bs1 rs. (\<And>x. x \<in> set rs \<Longrightarrow> x \<leadsto>* bsimp x) \<Longrightarrow>
-AALTs bs1 rs \<leadsto>* AALTs bs1 (map bsimp rs)"
- apply(subgoal_tac " rs s\<leadsto>* (map bsimp rs)")
- prefer 2
- using trivialbsimpsrewrites apply auto[1]
- using srewrites_alt1 by auto
+(* TEST *)
+lemma r:
+ assumes "AALTs bs rs1 \<leadsto> AALTs bs rs2"
+ shows "AALTs bs (x # rs1) \<leadsto>* AALTs bs (x # rs2)"
+ using assms
+ apply(erule_tac rrewrite.cases)
+ apply(auto)
+ apply (metis append_Cons append_Nil rrewrite.intros(6) r_in_rstar)
+ apply (metis append_Cons append_self_conv2 rrewrite.intros(7) r_in_rstar)
+ apply (metis Cons_eq_appendI append_eq_append_conv2 rrewrite.intros(8) self_append_conv r_in_rstar)
+ apply(case_tac rs2)
+ apply(auto)
+ apply(case_tac r)
+ apply(auto)
+ apply (metis append_Nil2 append_butlast_last_id butlast.simps(2) last.simps list.distinct(1) list.map_disc_iff r_in_rstar rrewrite.intros(8))
+ apply(case_tac r)
+ apply(auto)
+ defer
+ apply(rule r_in_rstar)
+ apply (metis append_Cons append_Nil rrewrite.intros(11))
+ apply(rule real_trans)
+ apply(rule r_in_rstar)
+ using rrewrite.intros(8)[where ?rsb = "[]", of "bs" "[x]" "[]" , simplified]
+ apply(rule_tac rrewrite.intros(8)[where ?rsb = "[]", of "bs" "[x]" "[]" , simplified])
+ apply(simp add: map_fuse_Nil fuse_Nil)
+ done
+lemma alts_simpalts:
+ "(\<And>x. x \<in> set rs \<Longrightarrow> x \<leadsto>* bsimp x) \<Longrightarrow>
+ AALTs bs1 rs \<leadsto>* AALTs bs1 (map bsimp rs)"
+ apply(induct rs)
+ apply(auto)[1]
+ using trivialbsimp_srewrites apply auto[1]
+ by (simp add: srewrites_alt1 ss2)
lemma threelistsappend: "rsa@a#rsb = (rsa@[a])@rsb"
apply auto
@@ -1149,7 +1159,7 @@
(erase `
(set rs1 \<union> set rs2)))) ")
prefer 2
- using rrewrite.intros(12) apply force
+ using rrewrite.intros(11) apply force
using r_in_rstar apply force
apply(subgoal_tac "erase ` set (rsa @ [a]) = insert (erase a) (erase ` set rsa)")
prefer 2
@@ -1161,7 +1171,7 @@
apply(subgoal_tac "AALTs bs (rsa @ a # distinctBy rs erase (insert (erase a) (erase ` set rsa))) \<leadsto>
AALTs bs (rsa @ distinctBy rs erase (insert (erase a) (erase ` set rsa)))")
apply force
- apply (smt (verit, ccfv_threshold) append_Cons append_assoc append_self_conv2 r_in_rstar rrewrite.intros(12) same_append_eq somewhereMapInside)
+ apply (smt (verit, ccfv_threshold) append_Cons append_assoc append_self_conv2 r_in_rstar rrewrite.intros(11) same_append_eq somewhereMapInside)
by force
@@ -1192,7 +1202,7 @@
next
case (2 bs1 rs)
then show "AALTs bs1 rs \<leadsto>* bsimp (AALTs bs1 rs)"
- by (metis alts_dBrewrites alts_simpalts bsimp.simps(2) bsimp_AALTsrewrites fltsrewrites real_trans)
+ by (metis alts_dBrewrites alts_simpalts bsimp.simps(2) bsimp_AALTs_rewrites flts_rewrites real_trans)
next
case "3_1"
then show "AZERO \<leadsto>* bsimp AZERO"
@@ -1262,7 +1272,7 @@
lemma third_segment_bmkeps:
"\<lbrakk>bnullable (AALTs bs (rs1@rs2@rs3)); \<not>bnullable (AALTs bs rs1); \<not>bnullable (AALTs bs rs2)\<rbrakk> \<Longrightarrow>
bmkeps (AALTs bs (rs1@rs2@rs3) ) = bmkeps (AALTs bs rs3)"
- by (metis bnullable.simps(1) bnullable.simps(4) bsimp_AALTs.simps(1) bsimp_AALTsrewrites qq2 rewritesnullable self_append_conv third_segment_bnullable)
+ by (metis bnullable.simps(1) bnullable.simps(4) bsimp_AALTs.simps(1) bsimp_AALTs_rewrites qq2 rewritesnullable self_append_conv third_segment_bnullable)
lemma rewrite_bmkepsalt:
"\<lbrakk>bnullable (AALTs bs (rsa @ AALTs bs1 rs1 # rsb)); bnullable (AALTs bs (rsa @ map (fuse bs1) rs1 @ rsb))\<rbrakk>
@@ -1302,25 +1312,21 @@
next
case (7 bs rsa rsb)
then show ?case
- by (metis bnullable.simps(1) bnullable.simps(4) bnullable_segment qq1 qq2 rewrite_nullable rrewrite.intros(10) rrewrite0away third_segment_bmkeps)
+ by (metis bnullable.simps(1) bnullable.simps(4) bnullable_segment qq1 qq2 rewrite_nullable rrewrite.intros(9) rrewrite0away third_segment_bmkeps)
next
case (8 bs rsa bs1 rs1 rsb)
then show ?case
by (simp add: rewrite_bmkepsalt)
next
- case (9 bs bs1 rs)
- then show ?case
- by (simp add: q3a)
-next
- case (10 bs)
+ case (9 bs)
then show ?case
by fastforce
next
- case (11 bs r)
+ case (10 bs r)
then show ?case
by (simp add: b2)
next
- case (12 a1 a2 bs rsa rsb rsc)
+ case (11 a1 a2 bs rsa rsb rsc)
then show ?case
by (smt (verit, ccfv_threshold) append_Cons append_eq_appendI append_self_conv2 bnullable_correctness list.set_intros(1) qq3 r1)
qed
@@ -1393,21 +1399,17 @@
then show ?case
using rrewrite.intros(8) by force
next
- case (9 bs bs1 rs)
+ case (9 bs)
then show ?case
- by (metis append.assoc fuse.simps(4) r_in_rstar rrewrite.intros(9))
-next
- case (10 bs)
- then show ?case
- by (simp add: r_in_rstar rrewrite.intros(10))
+ by (simp add: r_in_rstar rrewrite.intros(9))
next
- case (11 bs r)
+ case (10 bs r)
then show ?case
- by (metis fuse.simps(4) fuse_append r_in_rstar rrewrite.intros(11))
+ by (metis fuse.simps(4) fuse_append r_in_rstar rrewrite.intros(10))
next
- case (12 a1 a2 bs rsa rsb rsc)
+ case (11 a1 a2 bs rsa rsb rsc)
then show ?case
- using fuse.simps(4) r_in_rstar rrewrite.intros(12) by auto
+ using fuse.simps(4) r_in_rstar rrewrite.intros(11) by auto
qed
lemma rewrites_fuse:
@@ -1437,7 +1439,7 @@
bder c (AALTs bs (rsa @ [a1] @ rsb @ rsc))"
apply(simp)
- using rrewrite.intros(12) by auto
+ using rrewrite.intros(11) by auto
lemma rewrite_after_der:
assumes "r1 \<leadsto> r2"
@@ -1451,12 +1453,12 @@
case (2 bs r1)
then show "bder c (ASEQ bs r1 AZERO) \<leadsto>* bder c AZERO"
apply(simp)
- by (meson contextrewrites1 r_in_rstar real_trans rrewrite.intros(10) rrewrite.intros(2) rrewrite0away)
+ by (meson contextrewrites1 r_in_rstar real_trans rrewrite.intros(9) rrewrite.intros(2) rrewrite0away)
next
case (3 bs bs1 r)
then show "bder c (ASEQ bs (AONE bs1) r) \<leadsto>* bder c (fuse (bs @ bs1) r)"
apply(simp)
- by (metis bder_fuse fuse_append rrewrite.intros(11) rrewrite0away rrewrites.simps to_zero_in_alt)
+ by (metis bder_fuse fuse_append rrewrite.intros(10) rrewrite0away rrewrites.simps to_zero_in_alt)
next
case (4 r1 r2 bs r3)
have as: "r1 \<leadsto> r2" by fact
@@ -1467,9 +1469,8 @@
case (5 r3 r4 bs r1)
have as: "r3 \<leadsto> r4" by fact
have IH: "bder c r3 \<leadsto>* bder c r4" by fact
- from as IH show "bder c (ASEQ bs r1 r3) \<leadsto>* bder c (ASEQ bs r1 r4)"
- apply(simp)
- using r_in_rstar rewrites_fuse srewrites_alt1 ss1 ss2 star_seq2 by presburger
+ from as IH show "bder c (ASEQ bs r1 r3) \<leadsto>* bder c (ASEQ bs r1 r4)"
+ using bder.simps(5) r_in_rstar rewrites_fuse srewrites_alt1 ss1 ss2 star_seq2 by presburger
next
case (6 r r' bs rs1 rs2)
have as: "r \<leadsto> r'" by fact
@@ -1488,19 +1489,15 @@
"bder c (AALTs bs (rsa @ [AALTs bs1 rs1] @ rsb)) \<leadsto>* bder c (AALTs bs (rsa @ map (fuse bs1) rs1 @ rsb))"
using rewrite_der_altmiddle by auto
next
- case (9 bs bs1 rs)
- then show "bder c (AALTs (bs @ bs1) rs) \<leadsto>* bder c (AALTs bs (map (fuse bs1) rs))"
- by (metis bder.simps(4) bder_fuse_list list.map_comp r_in_rstar rrewrite.intros(9))
-next
- case (10 bs)
+ case (9 bs)
then show "bder c (AALTs bs []) \<leadsto>* bder c AZERO"
- by (simp add: r_in_rstar rrewrite.intros(10))
+ by (simp add: r_in_rstar rrewrite.intros(9))
next
- case (11 bs r)
+ case (10 bs r)
then show "bder c (AALTs bs [r]) \<leadsto>* bder c (fuse bs r)"
- by (simp add: bder_fuse r_in_rstar rrewrite.intros(11))
+ by (simp add: bder_fuse r_in_rstar rrewrite.intros(10))
next
- case (12 a1 a2 bs rsa rsb rsc)
+ case (11 a1 a2 bs rsa rsb rsc)
have as: "erase a1 = erase a2" by fact
then show "bder c (AALTs bs (rsa @ [a1] @ rsb @ [a2] @ rsc)) \<leadsto>* bder c (AALTs bs (rsa @ [a1] @ rsb @ rsc))"
using lock_step_der_removal by force
@@ -1533,10 +1530,13 @@
by (simp add: bders_simp_append)
qed
+
+
+
+
lemma quasi_main:
assumes "bnullable (bders r s)"
shows "bmkeps (bders r s) = bmkeps (bders_simp r s)"
- using assms central rewrites_bmkeps
proof -
have "bders r s \<leadsto>* bders_simp r s" by (rule central)
then
@@ -1545,6 +1545,8 @@
qed
+
+
theorem main_main:
shows "blexer r s = blexer_simp r s"
unfolding blexer_def blexer_simp_def