--- a/thys2/Journal/Paper.tex	Tue Jan 11 23:58:39 2022 +0000
+++ b/thys2/Journal/Paper.tex	Wed Jan 12 14:14:51 2022 +0000
@@ -225,7 +225,10 @@
   \end{tabular}
 \end{center}
 
-This rule allows us to simplify \mbox{\isa{a\ {\isacharplus}{\kern0pt}\ b\ {\isasymcdot}\ c\ {\isacharplus}{\kern0pt}\ a\ {\isasymcdot}\ c}}%
+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.%
 \end{isamarkuptext}\isamarkuptrue%
 %
 \isadelimdocument
@@ -1908,1462 +1911,1465 @@
 %:%226=287%:%
 %:%227=288%:%
 %:%228=289%:%
-%:%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%:%
+%:%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%:%

Binary file thys2/Journal/session_graph.pdf has changed

--- a/thys2/PDerivs.thy	Tue Jan 11 23:58:39 2022 +0000
+++ b/thys2/PDerivs.thy	Wed Jan 12 14:14:51 2022 +0000
@@ -333,15 +333,15 @@
 qed 
 
 text\<open>Antimirov's Corollary 3.5:\<close>
-
+(*W stands for word set*)
 corollary card_pders_set_le_awidth: 
-  shows "card (pders_Set A r) \<le> awidth r + 1"
+  shows "card (pders_Set W r) \<le> awidth r + 1"
 proof -
-  have "card (pders_Set A r) \<le> card (pders_Set UNIV r)"
+  have "card (pders_Set W r) \<le> card (pders_Set UNIV r)"
     by (simp add: card_mono finite_pders_set pders_Set_subset)
   also have "... \<le> awidth r + 1"
     by (rule card_pders_set_UNIV_le_awidth)
-  finally show "card (pders_Set A r) \<le> awidth r + 1" by simp
+  finally show "card (pders_Set W r) \<le> awidth r + 1" by simp
 qed
 
 (* other result by antimirov *)
@@ -602,6 +602,20 @@
   sledgehammer
   oops
 
+lemma pdero_result: 
+  shows "pdero  c (STAR (ALT (CH c) (SEQ (CH c) (CH c)))) =  {SEQ (CH c)(STAR (ALT (CH c) (SEQ (CH c) (CH c)))),(STAR (ALT (CH c) (SEQ (CH c) (CH c))))}"
+  apply(simp)
+  by auto
+
+fun concatLen :: "rexp \<Rightarrow> nat" where
+"concatLen ZERO = 0" |
+"concatLen ONE = 0" |
+"concatLen (CH c) = 0" |
+"concatLen (SEQ v1 v2) = Suc (max (concatLen v1) (concatLen v2))" |
+" concatLen (ALT v1 v2) =  max (concatLen v1) (concatLen v2)" |
+" concatLen (STAR v) = Suc (concatLen v)" 
+
+
 
 export_code height pders subs pderso in Scala module_name Pders 
 export_code pdero pderso in Scala module_name Pderso

Binary file thys2/journal.pdf has changed