# HG changeset patch # User Chengsong # Date 1639498665 0 # Node ID 28458dec90f8678d95247d53c357d884971a5f81 # Parent ee53acaf24205f778949891875f0f59f2dfcf857# Parent a8b4d8593bdb56e9e2537af7345cb5f15bacfc2b merged diff -r a8b4d8593bdb -r 28458dec90f8 thys2/Journal/Paper.tex --- a/thys2/Journal/Paper.tex Thu Nov 04 15:11:11 2021 +0000 +++ b/thys2/Journal/Paper.tex Tue Dec 14 16:17:45 2021 +0000 @@ -191,7 +191,44 @@ \isa{lexer\ r\ s\ {\isacharequal}{\kern0pt}\ blexer{\isacharunderscore}{\kern0pt}simp\ r\ s} \end{lemma} -The nice thing about the aove% +The nice thing about the above% +\end{isamarkuptext}\isamarkuptrue% +% +\isadelimdocument +% +\endisadelimdocument +% +\isatagdocument +% +\isamarkupsection{Additional Simp Rules?% +} +\isamarkuptrue% +% +\endisatagdocument +{\isafolddocument}% +% +\isadelimdocument +% +\endisadelimdocument +% +\begin{isamarkuptext}% +One question someone would ask is: +can we add more "atomic" simplification/rewriting rules, +so the simplification is even more aggressive, making +the intermediate results smaller, and therefore more space-efficient? +For example, one might want to do open up alternatives who is a child +of a sequence: + +\begin{center} + \begin{tabular}{lcl} + \isa{ASEQ\ bs\ {\isacharparenleft}{\kern0pt}AALTs\ bs{\isadigit{1}}\ rs{\isacharparenright}{\kern0pt}\ r\ {\isasymleadsto}{\isacharquery}{\kern0pt}\ AALTs\ {\isacharparenleft}{\kern0pt}bs\ {\isacharat}{\kern0pt}\ bs{\isadigit{1}}{\isacharparenright}{\kern0pt}\ {\isacharparenleft}{\kern0pt}map\ {\isacharparenleft}{\kern0pt}{\isasymlambda}r{\isacharprime}{\kern0pt}{\isachardot}{\kern0pt}\ ASEQ\ {\isacharbrackleft}{\kern0pt}{\isacharbrackright}{\kern0pt}\ r{\isacharprime}{\kern0pt}\ r{\isacharparenright}{\kern0pt}\ rs{\isacharparenright}{\kern0pt}}\\ + \end{tabular} +\end{center} + + +This rule allows us to simplify \mbox{\isa{a\ {\isacharplus}{\kern0pt}\ b\ {\isasymcdot}\ c\ {\isacharplus}{\kern0pt}\ a\ {\isasymcdot}\ c}} + into \mbox{\isa{a\ {\isasymcdot}\ c\ {\isacharplus}{\kern0pt}\ b\ {\isasymcdot}\ c}}, +which is not allowed under the \ rule% \end{isamarkuptext}\isamarkuptrue% % \isadelimdocument @@ -1719,6 +1756,8 @@ \isanewline % \endisadelimtheory +\isanewline +\isanewline % \end{isabellebody}% \endinput @@ -1857,1460 +1896,1480 @@ %:%192=266%:% %:%193=267%:% %:%194=268%:% -%:%203=273%:% -%:%215=279%:% -%:%216=280%:% -%:%217=281%:% -%:%218=282%:% -%:%218=283%:% -%:%219=284%:% -%:%220=285%:% -%:%221=286%:% -%:%222=287%:% -%:%223=288%:% -%:%224=289%:% -%:%225=290%:% -%:%226=291%:% -%:%227=292%:% -%:%228=293%:% -%:%229=294%:% -%:%230=295%:% -%:%231=296%:% -%:%232=297%:% -%:%233=298%:% -%:%234=299%:% -%:%235=300%:% -%:%236=301%:% -%:%237=302%:% -%:%238=303%:% -%:%239=304%:% -%:%240=305%:% -%:%241=306%:% -%:%242=307%:% -%:%243=308%:% -%:%244=309%:% -%:%245=310%:% -%:%246=311%:% -%:%247=312%:% -%:%248=313%:% -%:%249=314%:% -%:%250=315%:% -%:%251=316%:% -%:%252=317%:% -%:%253=318%:% -%:%254=319%:% -%:%255=320%:% -%:%256=321%:% -%:%257=322%:% -%:%258=323%:% -%:%259=324%:% -%:%260=325%:% -%:%261=326%:% -%:%262=327%:% -%:%263=328%:% -%:%264=329%:% -%:%265=330%:% -%:%266=331%:% -%:%267=332%:% -%:%268=333%:% -%:%269=334%:% -%:%270=335%:% -%:%271=336%:% -%:%272=337%:% -%:%273=338%:% -%:%274=339%:% -%:%275=340%:% -%:%276=341%:% -%:%277=342%:% -%:%278=343%:% -%:%279=344%:% -%:%280=345%:% -%:%281=346%:% -%:%282=347%:% -%:%282=348%:% -%:%283=349%:% -%:%284=350%:% -%:%285=351%:% -%:%286=352%:% -%:%287=353%:% -%:%288=354%:% -%:%289=355%:% -%:%290=356%:% -%:%291=357%:% -%:%292=358%:% -%:%293=359%:% -%:%294=360%:% -%:%295=361%:% -%:%296=362%:% -%:%297=363%:% -%:%298=364%:% -%:%299=365%:% -%:%300=366%:% -%:%301=367%:% -%:%302=368%:% -%:%303=369%:% -%:%304=370%:% -%:%305=371%:% -%:%306=372%:% -%:%307=373%:% -%:%308=374%:% -%:%309=375%:% -%:%310=376%:% -%:%311=377%:% -%:%312=378%:% -%:%313=379%:% -%:%314=380%:% -%:%315=381%:% -%:%316=382%:% -%:%317=383%:% -%:%318=384%:% -%:%319=385%:% -%:%320=386%:% -%:%321=387%:% -%:%322=388%:% -%:%323=389%:% -%:%324=390%:% -%:%325=391%:% -%:%326=392%:% -%:%327=393%:% -%:%328=394%:% -%:%329=395%:% -%:%330=396%:% -%:%331=397%:% -%:%332=398%:% -%:%333=399%:% -%:%334=400%:% -%:%335=401%:% -%:%336=402%:% -%:%337=403%:% -%:%338=404%:% -%:%339=405%:% -%:%340=406%:% -%:%341=407%:% -%:%342=408%:% -%:%343=409%:% -%:%344=410%:% -%:%345=411%:% -%:%346=412%:% -%:%347=413%:% -%:%348=414%:% -%:%349=415%:% -%:%350=416%:% -%:%351=417%:% -%:%352=418%:% -%:%353=419%:% -%:%354=420%:% -%:%355=421%:% -%:%356=422%:% -%:%357=423%:% -%:%358=424%:% -%:%359=425%:% -%:%360=426%:% -%:%361=427%:% -%:%362=428%:% -%:%363=429%:% -%:%364=430%:% -%:%365=431%:% -%:%366=432%:% -%:%367=433%:% -%:%368=434%:% -%:%369=435%:% -%:%370=436%:% -%:%371=437%:% -%:%372=438%:% -%:%373=439%:% -%:%374=440%:% -%:%375=441%:% -%:%376=442%:% -%:%377=443%:% -%:%378=444%:% -%:%379=445%:% -%:%380=446%:% -%:%381=447%:% -%:%382=448%:% -%:%383=449%:% -%:%384=450%:% -%:%385=451%:% -%:%386=452%:% -%:%387=453%:% -%:%396=460%:% -%:%408=462%:% -%:%409=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%:% -%:%425=480%:% -%:%426=481%:% -%:%427=482%:% -%:%428=483%:% -%:%429=484%:% -%:%430=485%:% -%:%431=486%:% -%:%432=487%:% -%:%433=488%:% -%:%434=489%:% -%:%435=490%:% -%:%436=491%:% -%:%437=492%:% -%:%438=493%:% -%:%439=494%:% -%:%440=495%:% -%:%441=496%:% -%:%442=497%:% -%:%443=498%:% -%:%444=499%:% -%:%445=500%:% -%:%446=501%:% -%:%447=502%:% -%:%448=503%:% -%:%448=504%:% -%:%449=505%:% -%:%450=506%:% -%:%451=507%:% -%:%452=508%:% -%:%453=509%:% -%:%453=510%:% -%:%454=511%:% -%:%455=512%:% -%:%456=513%:% -%:%457=514%:% -%:%458=515%:% -%:%459=516%:% -%:%460=517%:% -%:%461=518%:% -%:%462=519%:% -%:%463=520%:% -%:%464=521%:% -%:%465=522%:% -%:%466=523%:% -%:%467=524%:% -%:%468=525%:% -%:%469=526%:% -%:%470=527%:% -%:%471=528%:% -%:%472=529%:% -%:%473=530%:% -%:%474=531%:% -%:%475=532%:% -%:%476=533%:% -%:%477=534%:% -%:%478=535%:% -%:%479=536%:% -%:%480=537%:% -%:%481=538%:% -%:%482=539%:% -%:%483=540%:% -%:%484=541%:% -%:%485=542%:% -%:%486=543%:% -%:%487=544%:% -%:%488=545%:% -%:%489=546%:% -%:%490=547%:% -%:%491=548%:% -%:%492=549%:% -%:%493=550%:% -%:%494=551%:% -%:%495=552%:% -%:%496=553%:% -%:%497=554%:% -%:%498=555%:% -%:%499=556%:% -%:%500=557%:% -%:%501=558%:% -%:%502=559%:% -%:%503=560%:% -%:%504=561%:% -%:%505=562%:% -%:%506=563%:% -%:%507=564%:% -%:%508=565%:% -%:%509=566%:% -%:%510=567%:% -%:%511=568%:% -%:%512=569%:% -%:%513=570%:% -%:%514=571%:% -%:%515=572%:% -%:%516=573%:% -%:%517=574%:% -%:%518=575%:% -%:%519=576%:% -%:%520=577%:% -%:%521=578%:% -%:%522=579%:% -%:%523=580%:% -%:%524=581%:% -%:%525=582%:% -%:%526=583%:% -%:%527=584%:% -%:%528=585%:% -%:%529=586%:% -%:%530=587%:% -%:%531=588%:% -%:%532=589%:% -%:%533=590%:% -%:%534=591%:% -%:%535=592%:% -%:%536=593%:% -%:%537=594%:% -%:%538=595%:% -%:%539=596%:% -%:%540=597%:% -%:%541=598%:% -%:%542=599%:% -%:%551=603%:% -%:%563=607%:% -%:%564=608%:% -%:%565=609%:% -%:%566=610%:% -%:%567=611%:% -%:%568=612%:% -%:%569=613%:% -%:%570=614%:% -%:%571=615%:% -%:%572=616%:% -%:%573=617%:% -%:%574=618%:% -%:%575=619%:% -%:%576=620%:% -%:%577=621%:% -%:%578=622%:% -%:%579=623%:% -%:%580=624%:% -%:%581=625%:% -%:%582=626%:% -%:%583=627%:% -%:%584=628%:% -%:%585=629%:% -%:%586=630%:% -%:%587=631%:% -%:%588=632%:% -%:%589=633%:% -%:%590=634%:% -%:%591=635%:% -%:%592=636%:% -%:%593=637%:% -%:%594=638%:% -%:%595=639%:% -%:%596=640%:% -%:%597=641%:% -%:%598=642%:% -%:%599=643%:% -%:%600=644%:% -%:%601=645%:% -%:%602=646%:% -%:%603=647%:% -%:%604=648%:% -%:%605=649%:% -%:%606=650%:% -%:%607=651%:% -%:%608=652%:% -%:%609=653%:% -%:%610=654%:% -%:%611=655%:% -%:%612=656%:% -%:%613=657%:% -%:%614=658%:% -%:%615=659%:% -%:%616=660%:% -%:%617=661%:% -%:%618=662%:% -%:%619=663%:% -%:%620=664%:% -%:%621=665%:% -%:%622=666%:% -%:%623=667%:% -%:%624=668%:% -%:%625=669%:% -%:%626=670%:% -%:%627=671%:% -%:%628=672%:% -%:%629=673%:% -%:%630=674%:% -%:%631=675%:% -%:%632=676%:% -%:%633=677%:% -%:%634=678%:% -%:%635=679%:% -%:%636=680%:% -%:%637=681%:% -%:%638=682%:% -%:%639=683%:% -%:%640=684%:% -%:%641=685%:% -%:%642=686%:% -%:%643=687%:% -%:%644=688%:% -%:%645=689%:% -%:%646=690%:% -%:%647=691%:% -%:%648=692%:% -%:%649=693%:% -%:%650=694%:% -%:%651=695%:% -%:%652=696%:% -%:%653=697%:% -%:%654=698%:% -%:%655=699%:% -%:%656=700%:% -%:%657=701%:% -%:%658=702%:% -%:%659=703%:% -%:%660=704%:% -%:%661=705%:% -%:%662=706%:% -%:%663=707%:% -%:%664=708%:% -%:%665=709%:% -%:%666=710%:% -%:%667=711%:% -%:%668=712%:% -%:%669=713%:% -%:%670=714%:% -%:%671=715%:% -%:%672=716%:% -%:%673=717%:% -%:%674=718%:% -%:%675=719%:% -%:%676=720%:% -%:%677=721%:% -%:%677=722%:% -%:%678=723%:% -%:%678=724%:% -%:%679=725%:% -%:%680=726%:% -%:%680=727%:% -%:%681=728%:% -%:%682=729%:% -%:%683=730%:% -%:%684=731%:% -%:%685=732%:% -%:%686=733%:% -%:%687=734%:% -%:%688=735%:% -%:%689=736%:% -%:%690=737%:% -%:%691=738%:% -%:%692=739%:% -%:%693=740%:% -%:%694=741%:% -%:%695=742%:% -%:%696=743%:% -%:%697=744%:% -%:%698=745%:% -%:%699=746%:% -%:%700=747%:% -%:%701=748%:% -%:%702=749%:% -%:%703=750%:% -%:%704=751%:% -%:%705=752%:% -%:%706=753%:% -%:%707=754%:% -%:%708=755%:% -%:%709=756%:% -%:%710=757%:% -%:%711=758%:% -%:%712=759%:% -%:%713=760%:% -%:%714=761%:% -%:%715=762%:% -%:%716=763%:% -%:%717=764%:% -%:%718=765%:% -%:%719=766%:% -%:%720=767%:% -%:%721=768%:% -%:%722=769%:% -%:%723=770%:% -%:%724=771%:% -%:%725=772%:% -%:%726=773%:% -%:%727=774%:% -%:%728=775%:% -%:%729=776%:% -%:%730=777%:% -%:%731=778%:% -%:%732=779%:% -%:%733=780%:% -%:%734=781%:% -%:%735=782%:% -%:%736=783%:% -%:%736=784%:% -%:%736=785%:% -%:%737=786%:% -%:%738=787%:% -%:%739=788%:% -%:%740=789%:% -%:%741=790%:% -%:%742=791%:% -%:%743=792%:% -%:%744=793%:% -%:%745=794%:% -%:%745=795%:% -%:%746=796%:% -%:%747=797%:% -%:%748=798%:% -%:%749=799%:% -%:%750=800%:% -%:%751=801%:% -%:%752=802%:% -%:%753=803%:% -%:%754=804%:% -%:%755=805%:% -%:%756=806%:% -%:%757=807%:% -%:%758=808%:% -%:%759=809%:% -%:%760=810%:% -%:%761=811%:% -%:%762=812%:% -%:%763=813%:% -%:%764=814%:% -%:%765=815%:% -%:%766=816%:% -%:%767=817%:% -%:%768=818%:% -%:%769=819%:% -%:%770=820%:% -%:%771=821%:% -%:%772=822%:% -%:%773=823%:% -%:%774=824%:% -%:%775=825%:% -%:%776=826%:% -%:%777=827%:% -%:%778=828%:% -%:%779=829%:% -%:%780=830%:% -%:%780=831%:% -%:%781=832%:% -%:%782=833%:% -%:%783=834%:% -%:%784=835%:% -%:%785=836%:% -%:%786=837%:% -%:%787=838%:% -%:%787=839%:% -%:%788=840%:% -%:%789=841%:% -%:%790=842%:% -%:%790=843%:% -%:%791=844%:% -%:%792=845%:% -%:%793=846%:% -%:%794=847%:% -%:%795=848%:% -%:%796=849%:% -%:%797=850%:% -%:%798=851%:% -%:%799=852%:% -%:%800=853%:% -%:%801=854%:% -%:%801=855%:% -%:%802=856%:% -%:%803=857%:% -%:%804=858%:% -%:%805=859%:% -%:%805=860%:% -%:%806=861%:% -%:%807=862%:% -%:%808=863%:% -%:%809=864%:% -%:%810=865%:% -%:%811=866%:% -%:%812=867%:% -%:%813=868%:% -%:%814=869%:% -%:%815=870%:% -%:%816=871%:% -%:%817=872%:% -%:%818=873%:% -%:%819=874%:% -%:%820=875%:% -%:%821=876%:% -%:%822=877%:% -%:%823=878%:% -%:%824=879%:% -%:%825=880%:% -%:%826=881%:% -%:%827=882%:% -%:%828=883%:% -%:%829=884%:% -%:%830=885%:% -%:%831=886%:% -%:%832=887%:% -%:%833=888%:% -%:%834=889%:% -%:%835=890%:% -%:%836=891%:% -%:%837=892%:% -%:%838=893%:% -%:%839=894%:% -%:%840=895%:% -%:%841=896%:% -%:%842=897%:% -%:%843=898%:% -%:%844=899%:% -%:%845=900%:% -%:%846=901%:% -%:%847=902%:% -%:%848=903%:% -%:%849=904%:% -%:%850=905%:% -%:%851=906%:% -%:%852=907%:% -%:%853=908%:% -%:%854=909%:% -%:%855=910%:% -%:%856=911%:% -%:%857=912%:% -%:%858=913%:% -%:%859=914%:% -%:%860=915%:% -%:%861=916%:% -%:%862=917%:% -%:%863=918%:% -%:%863=919%:% -%:%864=920%:% -%:%865=921%:% -%:%866=922%:% -%:%867=923%:% -%:%868=924%:% -%:%869=925%:% -%:%870=926%:% -%:%871=927%:% -%:%872=928%:% -%:%873=929%:% -%:%874=930%:% -%:%875=931%:% -%:%876=932%:% -%:%877=933%:% -%:%878=934%:% -%:%879=935%:% -%:%880=936%:% -%:%881=937%:% -%:%882=938%:% -%:%883=939%:% -%:%884=940%:% -%:%885=941%:% -%:%886=942%:% -%:%887=943%:% -%:%888=944%:% -%:%889=945%:% -%:%890=946%:% -%:%891=947%:% -%:%892=948%:% -%:%893=949%:% -%:%894=950%:% -%:%895=951%:% -%:%896=952%:% -%:%896=953%:% -%:%897=954%:% -%:%898=955%:% -%:%899=956%:% -%:%900=957%:% -%:%901=958%:% -%:%902=959%:% -%:%903=960%:% -%:%904=961%:% -%:%905=962%:% -%:%906=963%:% -%:%907=964%:% -%:%908=965%:% -%:%909=966%:% -%:%910=967%:% -%:%911=968%:% -%:%912=969%:% -%:%913=970%:% -%:%914=971%:% -%:%915=972%:% -%:%916=973%:% -%:%917=974%:% -%:%918=975%:% -%:%919=976%:% -%:%920=977%:% -%:%921=978%:% -%:%922=979%:% -%:%923=980%:% -%:%924=981%:% -%:%925=982%:% -%:%926=983%:% -%:%926=984%:% -%:%927=985%:% -%:%928=986%:% -%:%929=987%:% -%:%930=988%:% -%:%931=989%:% -%:%932=990%:% -%:%933=991%:% -%:%934=992%:% -%:%934=993%:% -%:%935=994%:% -%:%936=995%:% -%:%937=996%:% -%:%938=997%:% -%:%939=998%:% -%:%940=999%:% -%:%941=1000%:% -%:%942=1001%:% -%:%943=1002%:% -%:%944=1003%:% -%:%945=1004%:% -%:%946=1005%:% -%:%947=1006%:% -%:%948=1007%:% -%:%949=1008%:% -%:%950=1009%:% -%:%951=1010%:% -%:%952=1011%:% -%:%953=1012%:% -%:%954=1013%:% -%:%955=1014%:% -%:%956=1015%:% -%:%957=1016%:% -%:%958=1017%:% -%:%959=1018%:% -%:%960=1019%:% -%:%961=1020%:% -%:%962=1021%:% -%:%963=1022%:% -%:%964=1023%:% -%:%965=1024%:% -%:%966=1025%:% -%:%967=1026%:% -%:%968=1027%:% -%:%969=1028%:% -%:%970=1029%:% -%:%971=1030%:% -%:%971=1031%:% -%:%971=1032%:% -%:%972=1033%:% -%:%972=1034%:% -%:%972=1035%:% -%:%973=1036%:% -%:%974=1037%:% -%:%974=1038%:% -%:%975=1039%:% -%:%976=1040%:% -%:%977=1041%:% -%:%978=1042%:% -%:%979=1043%:% -%:%980=1044%:% -%:%981=1045%:% -%:%982=1046%:% -%:%983=1047%:% -%:%984=1048%:% -%:%985=1049%:% -%:%986=1050%:% -%:%987=1051%:% -%:%988=1052%:% -%:%989=1053%:% -%:%990=1054%:% -%:%991=1055%:% -%:%992=1056%:% -%:%993=1057%:% -%:%994=1058%:% -%:%995=1059%:% -%:%996=1060%:% -%:%997=1061%:% -%:%998=1062%:% -%:%999=1063%:% -%:%1000=1064%:% -%:%1001=1065%:% -%:%1002=1066%:% -%:%1003=1067%:% -%:%1004=1068%:% -%:%1005=1069%:% -%:%1006=1070%:% -%:%1007=1071%:% -%:%1008=1072%:% -%:%1008=1073%:% -%:%1009=1074%:% -%:%1010=1075%:% -%:%1011=1076%:% -%:%1011=1077%:% -%:%1011=1078%:% -%:%1011=1079%:% -%:%1012=1080%:% -%:%1013=1081%:% -%:%1014=1082%:% -%:%1015=1083%:% -%:%1016=1084%:% -%:%1017=1085%:% -%:%1018=1086%:% -%:%1019=1087%:% -%:%1020=1088%:% -%:%1021=1089%:% -%:%1022=1090%:% -%:%1023=1091%:% -%:%1024=1092%:% -%:%1025=1093%:% -%:%1026=1094%:% -%:%1027=1095%:% -%:%1028=1096%:% -%:%1029=1097%:% -%:%1030=1098%:% -%:%1031=1099%:% -%:%1032=1100%:% -%:%1033=1101%:% -%:%1034=1102%:% -%:%1035=1103%:% -%:%1036=1104%:% -%:%1037=1105%:% -%:%1038=1106%:% -%:%1039=1107%:% -%:%1040=1108%:% -%:%1041=1109%:% -%:%1042=1110%:% -%:%1043=1111%:% -%:%1044=1112%:% -%:%1045=1113%:% -%:%1046=1114%:% -%:%1047=1115%:% -%:%1048=1116%:% -%:%1057=1120%:% -%:%1069=1124%:% -%:%1070=1125%:% -%:%1071=1126%:% -%:%1072=1127%:% -%:%1073=1128%:% -%:%1074=1129%:% -%:%1075=1130%:% -%:%1076=1131%:% -%:%1077=1132%:% -%:%1078=1133%:% -%:%1079=1134%:% -%:%1080=1135%:% -%:%1081=1136%:% -%:%1082=1137%:% -%:%1083=1138%:% -%:%1084=1139%:% -%:%1085=1140%:% -%:%1086=1141%:% -%:%1087=1142%:% -%:%1088=1143%:% -%:%1089=1144%:% -%:%1090=1145%:% -%:%1091=1146%:% -%:%1092=1147%:% -%:%1093=1148%:% -%:%1094=1149%:% -%:%1095=1150%:% -%:%1096=1151%:% -%:%1097=1152%:% -%:%1098=1153%:% -%:%1099=1154%:% -%:%1100=1155%:% -%:%1101=1156%:% -%:%1102=1157%:% -%:%1103=1158%:% -%:%1104=1159%:% -%:%1105=1160%:% -%:%1106=1161%:% -%:%1107=1162%:% -%:%1108=1163%:% -%:%1109=1164%:% -%:%1110=1165%:% -%:%1111=1166%:% -%:%1112=1167%:% -%:%1113=1168%:% -%:%1114=1169%:% -%:%1115=1170%:% -%:%1116=1171%:% -%:%1117=1172%:% -%:%1118=1173%:% -%:%1119=1174%:% -%:%1120=1175%:% -%:%1121=1176%:% -%:%1122=1177%:% -%:%1123=1178%:% -%:%1124=1179%:% -%:%1125=1180%:% -%:%1126=1181%:% -%:%1127=1182%:% -%:%1128=1183%:% -%:%1129=1184%:% -%:%1130=1185%:% -%:%1131=1186%:% -%:%1132=1187%:% -%:%1133=1188%:% -%:%1134=1189%:% -%:%1135=1190%:% -%:%1136=1191%:% -%:%1137=1192%:% -%:%1138=1193%:% -%:%1139=1194%:% -%:%1140=1195%:% -%:%1141=1196%:% -%:%1142=1197%:% -%:%1143=1198%:% -%:%1144=1199%:% -%:%1145=1200%:% -%:%1146=1201%:% -%:%1147=1202%:% -%:%1148=1203%:% -%:%1149=1204%:% -%:%1150=1205%:% -%:%1151=1206%:% -%:%1152=1207%:% -%:%1153=1208%:% -%:%1154=1209%:% -%:%1155=1210%:% -%:%1156=1211%:% -%:%1157=1212%:% -%:%1158=1213%:% -%:%1159=1214%:% -%:%1160=1215%:% -%:%1161=1216%:% -%:%1162=1217%:% -%:%1163=1218%:% -%:%1164=1219%:% -%:%1165=1220%:% -%:%1166=1221%:% -%:%1167=1222%:% -%:%1168=1223%:% -%:%1169=1224%:% -%:%1170=1225%:% -%:%1171=1226%:% -%:%1172=1227%:% -%:%1173=1228%:% -%:%1174=1229%:% -%:%1175=1230%:% -%:%1176=1231%:% -%:%1177=1232%:% -%:%1178=1233%:% -%:%1179=1234%:% -%:%1180=1235%:% -%:%1181=1236%:% -%:%1182=1237%:% -%:%1183=1238%:% -%:%1184=1239%:% -%:%1184=1240%:% -%:%1185=1241%:% -%:%1186=1242%:% -%:%1187=1243%:% -%:%1188=1244%:% -%:%1189=1245%:% -%:%1190=1246%:% -%:%1191=1247%:% -%:%1192=1248%:% -%:%1193=1249%:% -%:%1194=1250%:% -%:%1195=1251%:% -%:%1195=1252%:% -%:%1196=1253%:% -%:%1197=1254%:% -%:%1198=1255%:% -%:%1199=1256%:% -%:%1200=1257%:% -%:%1201=1258%:% -%:%1202=1259%:% -%:%1203=1260%:% -%:%1204=1261%:% -%:%1205=1262%:% -%:%1206=1263%:% -%:%1207=1264%:% -%:%1208=1265%:% -%:%1209=1266%:% -%:%1210=1267%:% -%:%1211=1268%:% -%:%1212=1269%:% -%:%1213=1270%:% -%:%1214=1271%:% -%:%1215=1272%:% -%:%1216=1273%:% -%:%1217=1274%:% -%:%1218=1275%:% -%:%1219=1276%:% -%:%1220=1277%:% -%:%1221=1278%:% -%:%1222=1279%:% -%:%1223=1280%:% -%:%1224=1281%:% -%:%1225=1282%:% -%:%1226=1283%:% -%:%1227=1284%:% -%:%1228=1285%:% -%:%1229=1286%:% -%:%1230=1287%:% -%:%1231=1288%:% -%:%1232=1289%:% -%:%1233=1290%:% -%:%1234=1291%:% -%:%1235=1292%:% -%:%1236=1293%:% -%:%1237=1294%:% -%:%1238=1295%:% -%:%1239=1296%:% -%:%1240=1297%:% -%:%1241=1298%:% -%:%1242=1299%:% -%:%1243=1300%:% -%:%1244=1301%:% -%:%1245=1302%:% -%:%1246=1303%:% -%:%1247=1304%:% -%:%1248=1305%:% -%:%1249=1306%:% -%:%1249=1307%:% -%:%1249=1308%:% -%:%1250=1309%:% -%:%1251=1310%:% -%:%1251=1311%:% -%:%1251=1312%:% -%:%1251=1313%:% -%:%1252=1314%:% -%:%1253=1315%:% -%:%1254=1316%:% -%:%1255=1317%:% -%:%1256=1318%:% -%:%1256=1319%:% -%:%1257=1320%:% -%:%1258=1321%:% -%:%1259=1322%:% -%:%1260=1323%:% -%:%1261=1324%:% -%:%1262=1325%:% -%:%1263=1326%:% -%:%1264=1327%:% -%:%1265=1328%:% -%:%1266=1329%:% -%:%1267=1330%:% -%:%1268=1331%:% -%:%1269=1332%:% -%:%1270=1333%:% -%:%1271=1334%:% -%:%1272=1335%:% -%:%1273=1336%:% -%:%1274=1337%:% -%:%1275=1338%:% -%:%1276=1339%:% -%:%1277=1340%:% -%:%1278=1341%:% -%:%1279=1342%:% -%:%1280=1343%:% -%:%1281=1344%:% -%:%1282=1345%:% -%:%1283=1346%:% -%:%1284=1347%:% -%:%1285=1348%:% -%:%1286=1349%:% -%:%1287=1350%:% -%:%1288=1351%:% -%:%1289=1352%:% -%:%1290=1353%:% -%:%1291=1354%:% -%:%1292=1355%:% -%:%1293=1356%:% -%:%1294=1357%:% -%:%1295=1358%:% -%:%1296=1359%:% -%:%1297=1360%:% -%:%1298=1361%:% -%:%1299=1362%:% -%:%1300=1363%:% -%:%1301=1364%:% -%:%1302=1365%:% -%:%1303=1366%:% -%:%1304=1367%:% -%:%1304=1368%:% -%:%1305=1369%:% -%:%1305=1370%:% -%:%1306=1371%:% -%:%1306=1372%:% -%:%1307=1373%:% -%:%1308=1374%:% -%:%1309=1375%:% -%:%1310=1376%:% -%:%1311=1377%:% -%:%1312=1378%:% -%:%1313=1379%:% -%:%1313=1380%:% -%:%1314=1381%:% -%:%1314=1382%:% -%:%1315=1383%:% -%:%1315=1384%:% -%:%1316=1385%:% -%:%1317=1386%:% -%:%1318=1387%:% -%:%1319=1388%:% -%:%1320=1389%:% -%:%1321=1390%:% -%:%1322=1391%:% -%:%1323=1392%:% -%:%1324=1393%:% -%:%1325=1394%:% -%:%1326=1395%:% -%:%1327=1396%:% -%:%1328=1397%:% -%:%1329=1398%:% -%:%1330=1399%:% -%:%1331=1400%:% -%:%1332=1401%:% -%:%1333=1402%:% -%:%1334=1403%:% -%:%1335=1404%:% -%:%1336=1405%:% -%:%1337=1406%:% -%:%1338=1407%:% -%:%1339=1408%:% -%:%1340=1409%:% -%:%1341=1410%:% -%:%1342=1411%:% -%:%1343=1412%:% -%:%1344=1413%:% -%:%1345=1414%:% -%:%1346=1415%:% -%:%1346=1416%:% -%:%1347=1417%:% -%:%1348=1418%:% -%:%1349=1419%:% -%:%1350=1420%:% -%:%1351=1421%:% -%:%1352=1422%:% -%:%1353=1423%:% -%:%1353=1424%:% -%:%1354=1425%:% -%:%1355=1426%:% -%:%1356=1427%:% -%:%1356=1428%:% -%:%1357=1429%:% -%:%1358=1430%:% -%:%1359=1431%:% -%:%1359=1432%:% -%:%1360=1433%:% -%:%1360=1434%:% -%:%1361=1435%:% -%:%1361=1436%:% -%:%1362=1437%:% -%:%1363=1438%:% -%:%1364=1439%:% -%:%1364=1440%:% -%:%1365=1441%:% -%:%1365=1442%:% -%:%1366=1443%:% -%:%1366=1444%:% -%:%1366=1445%:% -%:%1366=1446%:% -%:%1367=1447%:% -%:%1367=1448%:% -%:%1368=1449%:% -%:%1369=1450%:% -%:%1369=1452%:% -%:%1369=1453%:% -%:%1369=1454%:% -%:%1369=1455%:% -%:%1369=1456%:% -%:%1370=1457%:% -%:%1370=1458%:% -%:%1371=1459%:% -%:%1371=1460%:% -%:%1372=1461%:% -%:%1372=1462%:% -%:%1373=1463%:% -%:%1374=1464%:% -%:%1375=1465%:% -%:%1376=1466%:% -%:%1376=1467%:% -%:%1377=1468%:% -%:%1377=1469%:% -%:%1378=1470%:% -%:%1379=1471%:% -%:%1379=1472%:% -%:%1380=1473%:% -%:%1381=1474%:% -%:%1382=1475%:% -%:%1383=1476%:% -%:%1384=1477%:% -%:%1385=1478%:% -%:%1386=1479%:% -%:%1387=1480%:% -%:%1388=1481%:% -%:%1389=1482%:% -%:%1390=1483%:% -%:%1391=1484%:% -%:%1392=1485%:% -%:%1393=1486%:% -%:%1394=1487%:% -%:%1395=1488%:% -%:%1396=1489%:% -%:%1397=1490%:% -%:%1398=1491%:% -%:%1399=1492%:% -%:%1400=1493%:% -%:%1401=1494%:% -%:%1402=1495%:% -%:%1403=1496%:% -%:%1404=1497%:% -%:%1405=1498%:% -%:%1406=1499%:% -%:%1407=1500%:% -%:%1408=1501%:% -%:%1409=1502%:% -%:%1410=1503%:% -%:%1411=1504%:% -%:%1412=1505%:% -%:%1413=1506%:% -%:%1414=1507%:% -%:%1415=1508%:% -%:%1416=1509%:% -%:%1417=1510%:% -%:%1418=1511%:% -%:%1419=1512%:% -%:%1420=1513%:% -%:%1421=1514%:% -%:%1422=1515%:% -%:%1423=1516%:% -%:%1424=1517%:% -%:%1425=1518%:% -%:%1426=1519%:% -%:%1427=1520%:% -%:%1428=1521%:% -%:%1429=1522%:% -%:%1430=1523%:% -%:%1439=1527%:% -%:%1451=1534%:% -%:%1452=1535%:% -%:%1453=1536%:% -%:%1454=1537%:% -%:%1455=1538%:% -%:%1456=1539%:% -%:%1457=1540%:% +%:%203=272%:% +%:%215=276%:% +%:%216=277%:% +%:%217=278%:% +%:%218=279%:% +%:%219=280%:% +%:%220=281%:% +%:%221=282%:% +%:%222=283%:% +%:%223=284%:% +%:%224=285%:% +%:%225=286%:% +%:%226=287%:% +%:%227=288%:% +%:%228=289%:% +%:%229=290%:% +%:%230=291%:% +%:%231=292%:% +%:%240=296%:% +%:%252=302%:% +%:%253=303%:% +%:%254=304%:% +%:%255=305%:% +%:%255=306%:% +%:%256=307%:% +%:%257=308%:% +%:%258=309%:% +%:%259=310%:% +%:%260=311%:% +%:%261=312%:% +%:%262=313%:% +%:%263=314%:% +%:%264=315%:% +%:%265=316%:% +%:%266=317%:% +%:%267=318%:% +%:%268=319%:% +%:%269=320%:% +%:%270=321%:% +%:%271=322%:% +%:%272=323%:% +%:%273=324%:% +%:%274=325%:% +%:%275=326%:% +%:%276=327%:% +%:%277=328%:% +%:%278=329%:% +%:%279=330%:% +%:%280=331%:% +%:%281=332%:% +%:%282=333%:% +%:%283=334%:% +%:%284=335%:% +%:%285=336%:% +%:%286=337%:% +%:%287=338%:% +%:%288=339%:% +%:%289=340%:% +%:%290=341%:% +%:%291=342%:% +%:%292=343%:% +%:%293=344%:% +%:%294=345%:% +%:%295=346%:% +%:%296=347%:% +%:%297=348%:% +%:%298=349%:% +%:%299=350%:% +%:%300=351%:% +%:%301=352%:% +%:%302=353%:% +%:%303=354%:% +%:%304=355%:% +%:%305=356%:% +%:%306=357%:% +%:%307=358%:% +%:%308=359%:% +%:%309=360%:% +%:%310=361%:% +%:%311=362%:% +%:%312=363%:% +%:%313=364%:% +%:%314=365%:% +%:%315=366%:% +%:%316=367%:% +%:%317=368%:% +%:%318=369%:% +%:%319=370%:% +%:%319=371%:% +%:%320=372%:% +%:%321=373%:% +%:%322=374%:% +%:%323=375%:% +%:%324=376%:% +%:%325=377%:% +%:%326=378%:% +%:%327=379%:% +%:%328=380%:% +%:%329=381%:% +%:%330=382%:% +%:%331=383%:% +%:%332=384%:% +%:%333=385%:% +%:%334=386%:% +%:%335=387%:% +%:%336=388%:% +%:%337=389%:% +%:%338=390%:% +%:%339=391%:% +%:%340=392%:% +%:%341=393%:% +%:%342=394%:% +%:%343=395%:% +%:%344=396%:% +%:%345=397%:% +%:%346=398%:% +%:%347=399%:% +%:%348=400%:% +%:%349=401%:% +%:%350=402%:% +%:%351=403%:% +%:%352=404%:% +%:%353=405%:% +%:%354=406%:% +%:%355=407%:% +%:%356=408%:% +%:%357=409%:% +%:%358=410%:% +%:%359=411%:% +%:%360=412%:% +%:%361=413%:% +%:%362=414%:% +%:%363=415%:% +%:%364=416%:% +%:%365=417%:% +%:%366=418%:% +%:%367=419%:% +%:%368=420%:% +%:%369=421%:% +%:%370=422%:% +%:%371=423%:% +%:%372=424%:% +%:%373=425%:% +%:%374=426%:% +%:%375=427%:% +%:%376=428%:% +%:%377=429%:% +%:%378=430%:% +%:%379=431%:% +%:%380=432%:% +%:%381=433%:% +%:%382=434%:% +%:%383=435%:% +%:%384=436%:% +%:%385=437%:% +%:%386=438%:% +%:%387=439%:% +%:%388=440%:% +%:%389=441%:% +%:%390=442%:% +%:%391=443%:% +%:%392=444%:% +%:%393=445%:% +%:%394=446%:% +%:%395=447%:% +%:%396=448%:% +%:%397=449%:% +%:%398=450%:% +%:%399=451%:% +%:%400=452%:% +%:%401=453%:% +%:%402=454%:% +%:%403=455%:% +%:%404=456%:% +%:%405=457%:% +%:%406=458%:% +%:%407=459%:% +%:%408=460%:% +%:%409=461%:% +%:%410=462%:% +%:%411=463%:% +%:%412=464%:% +%:%413=465%:% +%:%414=466%:% +%:%415=467%:% +%:%416=468%:% +%:%417=469%:% +%:%418=470%:% +%:%419=471%:% +%:%420=472%:% +%:%421=473%:% +%:%422=474%:% +%:%423=475%:% +%:%424=476%:% +%:%433=483%:% +%:%445=485%:% +%:%446=486%:% +%:%446=487%:% +%:%447=488%:% +%:%448=489%:% +%:%449=490%:% +%:%450=491%:% +%:%451=492%:% +%:%452=493%:% +%:%453=494%:% +%:%454=495%:% +%:%455=496%:% +%:%456=497%:% +%:%457=498%:% +%:%458=499%:% +%:%459=500%:% +%:%460=501%:% +%:%461=502%:% +%:%462=503%:% +%:%463=504%:% +%:%464=505%:% +%:%465=506%:% +%:%466=507%:% +%:%467=508%:% +%:%468=509%:% +%:%469=510%:% +%:%470=511%:% +%:%471=512%:% +%:%472=513%:% +%:%473=514%:% +%:%474=515%:% +%:%475=516%:% +%:%476=517%:% +%:%477=518%:% +%:%478=519%:% +%:%479=520%:% +%:%480=521%:% +%:%481=522%:% +%:%482=523%:% +%:%483=524%:% +%:%484=525%:% +%:%485=526%:% +%:%485=527%:% +%:%486=528%:% +%:%487=529%:% +%:%488=530%:% +%:%489=531%:% +%:%490=532%:% +%:%490=533%:% +%:%491=534%:% +%:%492=535%:% +%:%493=536%:% +%:%494=537%:% +%:%495=538%:% +%:%496=539%:% +%:%497=540%:% +%:%498=541%:% +%:%499=542%:% +%:%500=543%:% +%:%501=544%:% +%:%502=545%:% +%:%503=546%:% +%:%504=547%:% +%:%505=548%:% +%:%506=549%:% +%:%507=550%:% +%:%508=551%:% +%:%509=552%:% +%:%510=553%:% +%:%511=554%:% +%:%512=555%:% +%:%513=556%:% +%:%514=557%:% +%:%515=558%:% +%:%516=559%:% +%:%517=560%:% +%:%518=561%:% +%:%519=562%:% +%:%520=563%:% +%:%521=564%:% +%:%522=565%:% +%:%523=566%:% +%:%524=567%:% +%:%525=568%:% +%:%526=569%:% +%:%527=570%:% +%:%528=571%:% +%:%529=572%:% +%:%530=573%:% +%:%531=574%:% +%:%532=575%:% +%:%533=576%:% +%:%534=577%:% +%:%535=578%:% +%:%536=579%:% +%:%537=580%:% +%:%538=581%:% +%:%539=582%:% +%:%540=583%:% +%:%541=584%:% +%:%542=585%:% +%:%543=586%:% +%:%544=587%:% +%:%545=588%:% +%:%546=589%:% +%:%547=590%:% +%:%548=591%:% +%:%549=592%:% +%:%550=593%:% +%:%551=594%:% +%:%552=595%:% +%:%553=596%:% +%:%554=597%:% +%:%555=598%:% +%:%556=599%:% +%:%557=600%:% +%:%558=601%:% +%:%559=602%:% +%:%560=603%:% +%:%561=604%:% +%:%562=605%:% +%:%563=606%:% +%:%564=607%:% +%:%565=608%:% +%:%566=609%:% +%:%567=610%:% +%:%568=611%:% +%:%569=612%:% +%:%570=613%:% +%:%571=614%:% +%:%572=615%:% +%:%573=616%:% +%:%574=617%:% +%:%575=618%:% +%:%576=619%:% +%:%577=620%:% +%:%578=621%:% +%:%579=622%:% +%:%588=626%:% +%:%600=630%:% +%:%601=631%:% +%:%602=632%:% +%:%603=633%:% +%:%604=634%:% +%:%605=635%:% +%:%606=636%:% +%:%607=637%:% +%:%608=638%:% +%:%609=639%:% +%:%610=640%:% +%:%611=641%:% +%:%612=642%:% +%:%613=643%:% +%:%614=644%:% +%:%615=645%:% +%:%616=646%:% +%:%617=647%:% +%:%618=648%:% +%:%619=649%:% +%:%620=650%:% +%:%621=651%:% +%:%622=652%:% +%:%623=653%:% +%:%624=654%:% +%:%625=655%:% +%:%626=656%:% +%:%627=657%:% +%:%628=658%:% +%:%629=659%:% +%:%630=660%:% +%:%631=661%:% +%:%632=662%:% +%:%633=663%:% +%:%634=664%:% +%:%635=665%:% +%:%636=666%:% +%:%637=667%:% +%:%638=668%:% +%:%639=669%:% +%:%640=670%:% +%:%641=671%:% +%:%642=672%:% +%:%643=673%:% +%:%644=674%:% +%:%645=675%:% +%:%646=676%:% +%:%647=677%:% +%:%648=678%:% +%:%649=679%:% +%:%650=680%:% +%:%651=681%:% +%:%652=682%:% +%:%653=683%:% +%:%654=684%:% +%:%655=685%:% +%:%656=686%:% +%:%657=687%:% +%:%658=688%:% +%:%659=689%:% +%:%660=690%:% +%:%661=691%:% +%:%662=692%:% +%:%663=693%:% +%:%664=694%:% +%:%665=695%:% +%:%666=696%:% +%:%667=697%:% +%:%668=698%:% +%:%669=699%:% +%:%670=700%:% +%:%671=701%:% +%:%672=702%:% +%:%673=703%:% +%:%674=704%:% +%:%675=705%:% +%:%676=706%:% +%:%677=707%:% +%:%678=708%:% +%:%679=709%:% +%:%680=710%:% +%:%681=711%:% +%:%682=712%:% +%:%683=713%:% +%:%684=714%:% +%:%685=715%:% +%:%686=716%:% +%:%687=717%:% +%:%688=718%:% +%:%689=719%:% +%:%690=720%:% +%:%691=721%:% +%:%692=722%:% +%:%693=723%:% +%:%694=724%:% +%:%695=725%:% +%:%696=726%:% +%:%697=727%:% +%:%698=728%:% +%:%699=729%:% +%:%700=730%:% +%:%701=731%:% +%:%702=732%:% +%:%703=733%:% +%:%704=734%:% +%:%705=735%:% +%:%706=736%:% +%:%707=737%:% +%:%708=738%:% +%:%709=739%:% +%:%710=740%:% +%:%711=741%:% +%:%712=742%:% +%:%713=743%:% +%:%714=744%:% +%:%714=745%:% +%:%715=746%:% +%:%715=747%:% +%:%716=748%:% +%:%717=749%:% +%:%717=750%:% +%:%718=751%:% +%:%719=752%:% +%:%720=753%:% +%:%721=754%:% +%:%722=755%:% +%:%723=756%:% +%:%724=757%:% +%:%725=758%:% +%:%726=759%:% +%:%727=760%:% +%:%728=761%:% +%:%729=762%:% +%:%730=763%:% +%:%731=764%:% +%:%732=765%:% +%:%733=766%:% +%:%734=767%:% +%:%735=768%:% +%:%736=769%:% +%:%737=770%:% +%:%738=771%:% +%:%739=772%:% +%:%740=773%:% +%:%741=774%:% +%:%742=775%:% +%:%743=776%:% +%:%744=777%:% +%:%745=778%:% +%:%746=779%:% +%:%747=780%:% +%:%748=781%:% +%:%749=782%:% +%:%750=783%:% +%:%751=784%:% +%:%752=785%:% +%:%753=786%:% +%:%754=787%:% +%:%755=788%:% +%:%756=789%:% +%:%757=790%:% +%:%758=791%:% +%:%759=792%:% +%:%760=793%:% +%:%761=794%:% +%:%762=795%:% +%:%763=796%:% +%:%764=797%:% +%:%765=798%:% +%:%766=799%:% +%:%767=800%:% +%:%768=801%:% +%:%769=802%:% +%:%770=803%:% +%:%771=804%:% +%:%772=805%:% +%:%773=806%:% +%:%773=807%:% +%:%773=808%:% +%:%774=809%:% +%:%775=810%:% +%:%776=811%:% +%:%777=812%:% +%:%778=813%:% +%:%779=814%:% +%:%780=815%:% +%:%781=816%:% +%:%782=817%:% +%:%782=818%:% +%:%783=819%:% +%:%784=820%:% +%:%785=821%:% +%:%786=822%:% +%:%787=823%:% +%:%788=824%:% +%:%789=825%:% +%:%790=826%:% +%:%791=827%:% +%:%792=828%:% +%:%793=829%:% +%:%794=830%:% +%:%795=831%:% +%:%796=832%:% +%:%797=833%:% +%:%798=834%:% +%:%799=835%:% +%:%800=836%:% +%:%801=837%:% +%:%802=838%:% +%:%803=839%:% +%:%804=840%:% +%:%805=841%:% +%:%806=842%:% +%:%807=843%:% +%:%808=844%:% +%:%809=845%:% +%:%810=846%:% +%:%811=847%:% +%:%812=848%:% +%:%813=849%:% +%:%814=850%:% +%:%815=851%:% +%:%816=852%:% +%:%817=853%:% +%:%817=854%:% +%:%818=855%:% +%:%819=856%:% +%:%820=857%:% +%:%821=858%:% +%:%822=859%:% +%:%823=860%:% +%:%824=861%:% +%:%824=862%:% +%:%825=863%:% +%:%826=864%:% +%:%827=865%:% +%:%827=866%:% +%:%828=867%:% +%:%829=868%:% +%:%830=869%:% +%:%831=870%:% +%:%832=871%:% +%:%833=872%:% +%:%834=873%:% +%:%835=874%:% +%:%836=875%:% +%:%837=876%:% +%:%838=877%:% +%:%838=878%:% +%:%839=879%:% +%:%840=880%:% +%:%841=881%:% +%:%842=882%:% +%:%842=883%:% +%:%843=884%:% +%:%844=885%:% +%:%845=886%:% +%:%846=887%:% +%:%847=888%:% +%:%848=889%:% +%:%849=890%:% +%:%850=891%:% +%:%851=892%:% +%:%852=893%:% +%:%853=894%:% +%:%854=895%:% +%:%855=896%:% +%:%856=897%:% +%:%857=898%:% +%:%858=899%:% +%:%859=900%:% +%:%860=901%:% +%:%861=902%:% +%:%862=903%:% +%:%863=904%:% +%:%864=905%:% +%:%865=906%:% +%:%866=907%:% +%:%867=908%:% +%:%868=909%:% +%:%869=910%:% +%:%870=911%:% +%:%871=912%:% +%:%872=913%:% +%:%873=914%:% +%:%874=915%:% +%:%875=916%:% +%:%876=917%:% +%:%877=918%:% +%:%878=919%:% +%:%879=920%:% +%:%880=921%:% +%:%881=922%:% +%:%882=923%:% +%:%883=924%:% +%:%884=925%:% +%:%885=926%:% +%:%886=927%:% +%:%887=928%:% +%:%888=929%:% +%:%889=930%:% +%:%890=931%:% +%:%891=932%:% +%:%892=933%:% +%:%893=934%:% +%:%894=935%:% +%:%895=936%:% +%:%896=937%:% +%:%897=938%:% +%:%898=939%:% +%:%899=940%:% +%:%900=941%:% +%:%900=942%:% +%:%901=943%:% +%:%902=944%:% +%:%903=945%:% +%:%904=946%:% +%:%905=947%:% +%:%906=948%:% +%:%907=949%:% +%:%908=950%:% +%:%909=951%:% +%:%910=952%:% +%:%911=953%:% +%:%912=954%:% +%:%913=955%:% +%:%914=956%:% +%:%915=957%:% +%:%916=958%:% +%:%917=959%:% +%:%918=960%:% +%:%919=961%:% +%:%920=962%:% +%:%921=963%:% +%:%922=964%:% +%:%923=965%:% +%:%924=966%:% +%:%925=967%:% +%:%926=968%:% +%:%927=969%:% +%:%928=970%:% +%:%929=971%:% +%:%930=972%:% +%:%931=973%:% +%:%932=974%:% +%:%933=975%:% +%:%933=976%:% +%:%934=977%:% +%:%935=978%:% +%:%936=979%:% +%:%937=980%:% +%:%938=981%:% +%:%939=982%:% +%:%940=983%:% +%:%941=984%:% +%:%942=985%:% +%:%943=986%:% +%:%944=987%:% +%:%945=988%:% +%:%946=989%:% +%:%947=990%:% +%:%948=991%:% +%:%949=992%:% +%:%950=993%:% +%:%951=994%:% +%:%952=995%:% +%:%953=996%:% +%:%954=997%:% +%:%955=998%:% +%:%956=999%:% +%:%957=1000%:% +%:%958=1001%:% +%:%959=1002%:% +%:%960=1003%:% +%:%961=1004%:% +%:%962=1005%:% +%:%963=1006%:% +%:%963=1007%:% +%:%964=1008%:% +%:%965=1009%:% +%:%966=1010%:% +%:%967=1011%:% +%:%968=1012%:% +%:%969=1013%:% +%:%970=1014%:% +%:%971=1015%:% +%:%971=1016%:% +%:%972=1017%:% +%:%973=1018%:% +%:%974=1019%:% +%:%975=1020%:% +%:%976=1021%:% +%:%977=1022%:% +%:%978=1023%:% +%:%979=1024%:% +%:%980=1025%:% +%:%981=1026%:% +%:%982=1027%:% +%:%983=1028%:% +%:%984=1029%:% +%:%985=1030%:% +%:%986=1031%:% +%:%987=1032%:% +%:%988=1033%:% +%:%989=1034%:% +%:%990=1035%:% +%:%991=1036%:% +%:%992=1037%:% +%:%993=1038%:% +%:%994=1039%:% +%:%995=1040%:% +%:%996=1041%:% +%:%997=1042%:% +%:%998=1043%:% +%:%999=1044%:% +%:%1000=1045%:% +%:%1001=1046%:% +%:%1002=1047%:% +%:%1003=1048%:% +%:%1004=1049%:% +%:%1005=1050%:% +%:%1006=1051%:% +%:%1007=1052%:% +%:%1008=1053%:% +%:%1008=1054%:% +%:%1008=1055%:% +%:%1009=1056%:% +%:%1009=1057%:% +%:%1009=1058%:% +%:%1010=1059%:% +%:%1011=1060%:% +%:%1011=1061%:% +%:%1012=1062%:% +%:%1013=1063%:% +%:%1014=1064%:% +%:%1015=1065%:% +%:%1016=1066%:% +%:%1017=1067%:% +%:%1018=1068%:% +%:%1019=1069%:% +%:%1020=1070%:% +%:%1021=1071%:% +%:%1022=1072%:% +%:%1023=1073%:% +%:%1024=1074%:% +%:%1025=1075%:% +%:%1026=1076%:% +%:%1027=1077%:% +%:%1028=1078%:% +%:%1029=1079%:% +%:%1030=1080%:% +%:%1031=1081%:% +%:%1032=1082%:% +%:%1033=1083%:% +%:%1034=1084%:% +%:%1035=1085%:% +%:%1036=1086%:% +%:%1037=1087%:% +%:%1038=1088%:% +%:%1039=1089%:% +%:%1040=1090%:% +%:%1041=1091%:% +%:%1042=1092%:% +%:%1043=1093%:% +%:%1044=1094%:% +%:%1045=1095%:% +%:%1045=1096%:% +%:%1046=1097%:% +%:%1047=1098%:% +%:%1048=1099%:% +%:%1048=1100%:% +%:%1048=1101%:% +%:%1048=1102%:% +%:%1049=1103%:% +%:%1050=1104%:% +%:%1051=1105%:% +%:%1052=1106%:% +%:%1053=1107%:% +%:%1054=1108%:% +%:%1055=1109%:% +%:%1056=1110%:% +%:%1057=1111%:% +%:%1058=1112%:% +%:%1059=1113%:% +%:%1060=1114%:% +%:%1061=1115%:% +%:%1062=1116%:% +%:%1063=1117%:% +%:%1064=1118%:% +%:%1065=1119%:% +%:%1066=1120%:% +%:%1067=1121%:% +%:%1068=1122%:% +%:%1069=1123%:% +%:%1070=1124%:% +%:%1071=1125%:% +%:%1072=1126%:% +%:%1073=1127%:% +%:%1074=1128%:% +%:%1075=1129%:% +%:%1076=1130%:% +%:%1077=1131%:% +%:%1078=1132%:% +%:%1079=1133%:% +%:%1080=1134%:% +%:%1081=1135%:% +%:%1082=1136%:% +%:%1083=1137%:% +%:%1084=1138%:% +%:%1085=1139%:% +%:%1094=1143%:% +%:%1106=1147%:% +%:%1107=1148%:% +%:%1108=1149%:% +%:%1109=1150%:% +%:%1110=1151%:% +%:%1111=1152%:% +%:%1112=1153%:% +%:%1113=1154%:% +%:%1114=1155%:% +%:%1115=1156%:% +%:%1116=1157%:% +%:%1117=1158%:% +%:%1118=1159%:% +%:%1119=1160%:% +%:%1120=1161%:% +%:%1121=1162%:% +%:%1122=1163%:% +%:%1123=1164%:% +%:%1124=1165%:% +%:%1125=1166%:% +%:%1126=1167%:% +%:%1127=1168%:% +%:%1128=1169%:% +%:%1129=1170%:% +%:%1130=1171%:% +%:%1131=1172%:% +%:%1132=1173%:% +%:%1133=1174%:% +%:%1134=1175%:% +%:%1135=1176%:% +%:%1136=1177%:% +%:%1137=1178%:% +%:%1138=1179%:% +%:%1139=1180%:% +%:%1140=1181%:% +%:%1141=1182%:% +%:%1142=1183%:% +%:%1143=1184%:% +%:%1144=1185%:% +%:%1145=1186%:% +%:%1146=1187%:% +%:%1147=1188%:% +%:%1148=1189%:% +%:%1149=1190%:% +%:%1150=1191%:% +%:%1151=1192%:% +%:%1152=1193%:% +%:%1153=1194%:% +%:%1154=1195%:% +%:%1155=1196%:% +%:%1156=1197%:% +%:%1157=1198%:% +%:%1158=1199%:% +%:%1159=1200%:% +%:%1160=1201%:% +%:%1161=1202%:% +%:%1162=1203%:% +%:%1163=1204%:% +%:%1164=1205%:% +%:%1165=1206%:% +%:%1166=1207%:% +%:%1167=1208%:% +%:%1168=1209%:% +%:%1169=1210%:% +%:%1170=1211%:% +%:%1171=1212%:% +%:%1172=1213%:% +%:%1173=1214%:% +%:%1174=1215%:% +%:%1175=1216%:% +%:%1176=1217%:% +%:%1177=1218%:% +%:%1178=1219%:% +%:%1179=1220%:% +%:%1180=1221%:% +%:%1181=1222%:% +%:%1182=1223%:% +%:%1183=1224%:% +%:%1184=1225%:% +%:%1185=1226%:% +%:%1186=1227%:% +%:%1187=1228%:% +%:%1188=1229%:% +%:%1189=1230%:% +%:%1190=1231%:% +%:%1191=1232%:% +%:%1192=1233%:% +%:%1193=1234%:% +%:%1194=1235%:% +%:%1195=1236%:% +%:%1196=1237%:% +%:%1197=1238%:% +%:%1198=1239%:% +%:%1199=1240%:% +%:%1200=1241%:% +%:%1201=1242%:% +%:%1202=1243%:% +%:%1203=1244%:% +%:%1204=1245%:% +%:%1205=1246%:% +%:%1206=1247%:% +%:%1207=1248%:% +%:%1208=1249%:% +%:%1209=1250%:% +%:%1210=1251%:% +%:%1211=1252%:% +%:%1212=1253%:% +%:%1213=1254%:% +%:%1214=1255%:% +%:%1215=1256%:% +%:%1216=1257%:% +%:%1217=1258%:% +%:%1218=1259%:% +%:%1219=1260%:% +%:%1220=1261%:% +%:%1221=1262%:% +%:%1221=1263%:% +%:%1222=1264%:% +%:%1223=1265%:% +%:%1224=1266%:% +%:%1225=1267%:% +%:%1226=1268%:% +%:%1227=1269%:% +%:%1228=1270%:% +%:%1229=1271%:% +%:%1230=1272%:% +%:%1231=1273%:% +%:%1232=1274%:% +%:%1232=1275%:% +%:%1233=1276%:% +%:%1234=1277%:% +%:%1235=1278%:% +%:%1236=1279%:% +%:%1237=1280%:% +%:%1238=1281%:% +%:%1239=1282%:% +%:%1240=1283%:% +%:%1241=1284%:% +%:%1242=1285%:% +%:%1243=1286%:% +%:%1244=1287%:% +%:%1245=1288%:% +%:%1246=1289%:% +%:%1247=1290%:% +%:%1248=1291%:% +%:%1249=1292%:% +%:%1250=1293%:% +%:%1251=1294%:% +%:%1252=1295%:% +%:%1253=1296%:% +%:%1254=1297%:% +%:%1255=1298%:% +%:%1256=1299%:% +%:%1257=1300%:% +%:%1258=1301%:% +%:%1259=1302%:% +%:%1260=1303%:% +%:%1261=1304%:% +%:%1262=1305%:% +%:%1263=1306%:% +%:%1264=1307%:% +%:%1265=1308%:% +%:%1266=1309%:% +%:%1267=1310%:% +%:%1268=1311%:% +%:%1269=1312%:% +%:%1270=1313%:% +%:%1271=1314%:% +%:%1272=1315%:% +%:%1273=1316%:% +%:%1274=1317%:% +%:%1275=1318%:% +%:%1276=1319%:% +%:%1277=1320%:% +%:%1278=1321%:% +%:%1279=1322%:% +%:%1280=1323%:% +%:%1281=1324%:% +%:%1282=1325%:% +%:%1283=1326%:% +%:%1284=1327%:% +%:%1285=1328%:% +%:%1286=1329%:% +%:%1286=1330%:% +%:%1286=1331%:% +%:%1287=1332%:% +%:%1288=1333%:% +%:%1288=1334%:% +%:%1288=1335%:% +%:%1288=1336%:% +%:%1289=1337%:% +%:%1290=1338%:% +%:%1291=1339%:% +%:%1292=1340%:% +%:%1293=1341%:% +%:%1293=1342%:% +%:%1294=1343%:% +%:%1295=1344%:% +%:%1296=1345%:% +%:%1297=1346%:% +%:%1298=1347%:% +%:%1299=1348%:% +%:%1300=1349%:% +%:%1301=1350%:% +%:%1302=1351%:% +%:%1303=1352%:% +%:%1304=1353%:% +%:%1305=1354%:% +%:%1306=1355%:% +%:%1307=1356%:% +%:%1308=1357%:% +%:%1309=1358%:% +%:%1310=1359%:% +%:%1311=1360%:% +%:%1312=1361%:% +%:%1313=1362%:% +%:%1314=1363%:% +%:%1315=1364%:% +%:%1316=1365%:% +%:%1317=1366%:% +%:%1318=1367%:% +%:%1319=1368%:% +%:%1320=1369%:% +%:%1321=1370%:% +%:%1322=1371%:% +%:%1323=1372%:% +%:%1324=1373%:% +%:%1325=1374%:% +%:%1326=1375%:% +%:%1327=1376%:% +%:%1328=1377%:% +%:%1329=1378%:% +%:%1330=1379%:% +%:%1331=1380%:% +%:%1332=1381%:% +%:%1333=1382%:% +%:%1334=1383%:% +%:%1335=1384%:% +%:%1336=1385%:% +%:%1337=1386%:% +%:%1338=1387%:% +%:%1339=1388%:% +%:%1340=1389%:% +%:%1341=1390%:% +%:%1341=1391%:% +%:%1342=1392%:% +%:%1342=1393%:% +%:%1343=1394%:% +%:%1343=1395%:% +%:%1344=1396%:% +%:%1345=1397%:% +%:%1346=1398%:% +%:%1347=1399%:% +%:%1348=1400%:% +%:%1349=1401%:% +%:%1350=1402%:% +%:%1350=1403%:% +%:%1351=1404%:% +%:%1351=1405%:% +%:%1352=1406%:% +%:%1352=1407%:% +%:%1353=1408%:% +%:%1354=1409%:% +%:%1355=1410%:% +%:%1356=1411%:% +%:%1357=1412%:% +%:%1358=1413%:% +%:%1359=1414%:% +%:%1360=1415%:% +%:%1361=1416%:% +%:%1362=1417%:% +%:%1363=1418%:% +%:%1364=1419%:% +%:%1365=1420%:% +%:%1366=1421%:% +%:%1367=1422%:% +%:%1368=1423%:% +%:%1369=1424%:% +%:%1370=1425%:% +%:%1371=1426%:% +%:%1372=1427%:% +%:%1373=1428%:% +%:%1374=1429%:% +%:%1375=1430%:% +%:%1376=1431%:% +%:%1377=1432%:% +%:%1378=1433%:% +%:%1379=1434%:% +%:%1380=1435%:% +%:%1381=1436%:% +%:%1382=1437%:% +%:%1383=1438%:% +%:%1383=1439%:% +%:%1384=1440%:% +%:%1385=1441%:% +%:%1386=1442%:% +%:%1387=1443%:% +%:%1388=1444%:% +%:%1389=1445%:% +%:%1390=1446%:% +%:%1390=1447%:% +%:%1391=1448%:% +%:%1392=1449%:% +%:%1393=1450%:% +%:%1393=1451%:% +%:%1394=1452%:% +%:%1395=1453%:% +%:%1396=1454%:% +%:%1396=1455%:% +%:%1397=1456%:% +%:%1397=1457%:% +%:%1398=1458%:% +%:%1398=1459%:% +%:%1399=1460%:% +%:%1400=1461%:% +%:%1401=1462%:% +%:%1401=1463%:% +%:%1402=1464%:% +%:%1402=1465%:% +%:%1403=1466%:% +%:%1403=1467%:% +%:%1403=1468%:% +%:%1403=1469%:% +%:%1404=1470%:% +%:%1404=1471%:% +%:%1405=1472%:% +%:%1406=1473%:% +%:%1406=1475%:% +%:%1406=1476%:% +%:%1406=1477%:% +%:%1406=1478%:% +%:%1406=1479%:% +%:%1407=1480%:% +%:%1407=1481%:% +%:%1408=1482%:% +%:%1408=1483%:% +%:%1409=1484%:% +%:%1409=1485%:% +%:%1410=1486%:% +%:%1411=1487%:% +%:%1412=1488%:% +%:%1413=1489%:% +%:%1413=1490%:% +%:%1414=1491%:% +%:%1414=1492%:% +%:%1415=1493%:% +%:%1416=1494%:% +%:%1416=1495%:% +%:%1417=1496%:% +%:%1418=1497%:% +%:%1419=1498%:% +%:%1420=1499%:% +%:%1421=1500%:% +%:%1422=1501%:% +%:%1423=1502%:% +%:%1424=1503%:% +%:%1425=1504%:% +%:%1426=1505%:% +%:%1427=1506%:% +%:%1428=1507%:% +%:%1429=1508%:% +%:%1430=1509%:% +%:%1431=1510%:% +%:%1432=1511%:% +%:%1433=1512%:% +%:%1434=1513%:% +%:%1435=1514%:% +%:%1436=1515%:% +%:%1437=1516%:% +%:%1438=1517%:% +%:%1439=1518%:% +%:%1440=1519%:% +%:%1441=1520%:% +%:%1442=1521%:% +%:%1443=1522%:% +%:%1444=1523%:% +%:%1445=1524%:% +%:%1446=1525%:% +%:%1447=1526%:% +%:%1448=1527%:% +%:%1449=1528%:% +%:%1450=1529%:% +%:%1451=1530%:% +%:%1452=1531%:% +%:%1453=1532%:% +%:%1454=1533%:% +%:%1455=1534%:% +%:%1456=1535%:% +%:%1457=1536%:% +%:%1458=1537%:% +%:%1459=1538%:% +%:%1460=1539%:% +%:%1461=1540%:% +%:%1462=1541%:% +%:%1463=1542%:% +%:%1464=1543%:% +%:%1465=1544%:% %:%1466=1545%:% -%:%1478=1549%:% -%:%1479=1550%:% -%:%1480=1551%:% -%:%1481=1552%:% -%:%1482=1553%:% -%:%1483=1554%:% -%:%1484=1555%:% -%:%1485=1556%:% -%:%1486=1557%:% -%:%1487=1558%:% -%:%1488=1559%:% -%:%1489=1560%:% -%:%1490=1561%:% -%:%1491=1562%:% -%:%1492=1563%:% -%:%1493=1564%:% -%:%1494=1565%:% -%:%1495=1566%:% -%:%1496=1567%:% -%:%1497=1568%:% -%:%1498=1569%:% -%:%1499=1570%:% -%:%1500=1571%:% -%:%1501=1572%:% -%:%1502=1573%:% -%:%1503=1574%:% -%:%1504=1575%:% -%:%1505=1576%:% -%:%1506=1577%:% -%:%1507=1578%:% -%:%1508=1579%:% -%:%1509=1580%:% -%:%1510=1581%:% -%:%1511=1582%:% -%:%1512=1583%:% -%:%1513=1584%:% -%:%1514=1585%:% -%:%1515=1586%:% -%:%1516=1587%:% -%:%1517=1588%:% -%:%1518=1589%:% -%:%1519=1590%:% -%:%1520=1591%:% -%:%1521=1592%:% -%:%1522=1593%:% -%:%1523=1594%:% -%:%1524=1595%:% -%:%1525=1596%:% -%:%1526=1597%:% -%:%1527=1598%:% -%:%1528=1599%:% -%:%1529=1600%:% -%:%1530=1601%:% -%:%1531=1602%:% -%:%1532=1603%:% -%:%1533=1604%:% -%:%1534=1605%:% -%:%1535=1606%:% -%:%1536=1607%:% -%:%1537=1608%:% -%:%1538=1609%:% -%:%1539=1610%:% -%:%1540=1611%:% -%:%1541=1612%:% -%:%1542=1613%:% -%:%1543=1614%:% -%:%1544=1615%:% -%:%1545=1616%:% -%:%1546=1617%:% -%:%1547=1618%:% -%:%1548=1619%:% -%:%1549=1620%:% -%:%1550=1621%:% -%:%1551=1622%:% -%:%1552=1623%:% -%:%1553=1624%:% -%:%1554=1625%:% -%:%1555=1626%:% -%:%1556=1627%:% -%:%1557=1628%:% -%:%1558=1629%:% -%:%1559=1630%:% -%:%1560=1631%:% -%:%1561=1632%:% -%:%1562=1633%:% -%:%1563=1634%:% -%:%1564=1635%:% -%:%1565=1636%:% -%:%1566=1637%:% -%:%1567=1638%:% -%:%1567=1754%:% -%:%1568=1755%:% -%:%1569=1756%:% -%:%1570=1757%:% -%:%1571=1758%:% -%:%1571=1919%:% -%:%1572=1920%:% -%:%1573=1921%:% -%:%1574=1922%:% -%:%1575=1923%:% -%:%1576=1924%:% -%:%1577=1925%:% -%:%1578=1926%:% -%:%1579=1927%:% -%:%1580=1928%:% -%:%1581=1929%:% -%:%1582=1930%:% -%:%1583=1931%:% -%:%1584=1932%:% -%:%1585=1933%:% -%:%1586=1934%:% -%:%1587=1935%:% -%:%1588=1936%:% -%:%1589=1937%:% -%:%1590=1938%:% -%:%1590=1939%:% -%:%1591=1940%:% -%:%1591=1941%:% -%:%1591=1942%:% -%:%1592=1943%:% -%:%1592=1944%:% -%:%1593=1945%:% -%:%1594=1946%:% -%:%1595=1947%:% -%:%1596=1948%:% -%:%1597=1949%:% -%:%1598=1950%:% -%:%1599=1951%:% -%:%1600=1952%:% -%:%1601=1953%:% -%:%1602=1954%:% -%:%1603=1955%:% -%:%1604=1956%:% -%:%1605=1957%:% -%:%1606=1958%:% -%:%1607=1959%:% -%:%1608=1960%:% -%:%1609=1961%:% -%:%1609=1962%:% -%:%1610=1963%:% -%:%1611=1964%:% -%:%1612=1965%:% -%:%1612=1966%:% -%:%1612=1967%:% -%:%1613=1968%:% -%:%1614=1969%:% -%:%1615=1970%:% -%:%1615=1971%:% -%:%1616=1972%:% -%:%1616=1973%:% -%:%1617=1974%:% -%:%1618=1975%:% -%:%1619=1976%:% -%:%1620=1977%:% -%:%1621=1978%:% -%:%1622=1979%:% -%:%1623=1980%:% -%:%1624=1981%:% -%:%1625=1982%:% -%:%1626=1983%:% -%:%1627=1984%:% -%:%1628=1985%:% -%:%1629=1986%:% -%:%1630=1987%:% -%:%1631=1988%:% -%:%1632=1989%:% -%:%1633=1990%:% -%:%1642=1995%:% -%:%1654=1999%:% -%:%1655=2000%:% -%:%1656=2001%:% -%:%1657=2002%:% -%:%1658=2003%:% -%:%1659=2004%:% -%:%1660=2005%:% -%:%1661=2006%:% -%:%1662=2007%:% -%:%1663=2008%:% -%:%1664=2009%:% -%:%1665=2010%:% -%:%1666=2011%:% -%:%1667=2012%:% -%:%1668=2013%:% -%:%1669=2014%:% -%:%1670=2015%:% -%:%1671=2016%:% -%:%1672=2017%:% -%:%1673=2018%:% -%:%1674=2019%:% -%:%1675=2020%:% -%:%1676=2021%:% -%:%1677=2022%:% -%:%1678=2023%:% -%:%1679=2024%:% -%:%1680=2025%:% -%:%1681=2026%:% -%:%1682=2027%:% -%:%1683=2028%:% -%:%1684=2029%:% -%:%1685=2030%:% -%:%1686=2031%:% -%:%1687=2032%:% -%:%1688=2033%:% -%:%1689=2034%:% -%:%1690=2035%:% -%:%1691=2036%:% -%:%1692=2037%:% -%:%1693=2038%:% -%:%1694=2039%:% -%:%1695=2040%:% -%:%1696=2041%:% -%:%1697=2042%:% -%:%1698=2043%:% -%:%1699=2044%:% -%:%1700=2045%:% -%:%1701=2046%:% -%:%1702=2047%:% -%:%1703=2048%:% -%:%1704=2049%:% -%:%1705=2050%:% -%:%1706=2051%:% -%:%1719=2057%:% \ No newline at end of file +%:%1467=1546%:% +%:%1476=1550%:% +%:%1488=1557%:% +%:%1489=1558%:% +%:%1490=1559%:% +%:%1491=1560%:% +%:%1492=1561%:% +%:%1493=1562%:% +%:%1494=1563%:% +%:%1503=1568%:% +%:%1515=1572%:% +%:%1516=1573%:% +%:%1517=1574%:% +%:%1518=1575%:% +%:%1519=1576%:% +%:%1520=1577%:% +%:%1521=1578%:% +%:%1522=1579%:% +%:%1523=1580%:% +%:%1524=1581%:% +%:%1525=1582%:% +%:%1526=1583%:% +%:%1527=1584%:% +%:%1528=1585%:% +%:%1529=1586%:% +%:%1530=1587%:% +%:%1531=1588%:% +%:%1532=1589%:% +%:%1533=1590%:% +%:%1534=1591%:% +%:%1535=1592%:% +%:%1536=1593%:% +%:%1537=1594%:% +%:%1538=1595%:% +%:%1539=1596%:% +%:%1540=1597%:% +%:%1541=1598%:% +%:%1542=1599%:% +%:%1543=1600%:% +%:%1544=1601%:% +%:%1545=1602%:% +%:%1546=1603%:% +%:%1547=1604%:% +%:%1548=1605%:% +%:%1549=1606%:% +%:%1550=1607%:% +%:%1551=1608%:% +%:%1552=1609%:% +%:%1553=1610%:% +%:%1554=1611%:% +%:%1555=1612%:% +%:%1556=1613%:% +%:%1557=1614%:% +%:%1558=1615%:% +%:%1559=1616%:% +%:%1560=1617%:% +%:%1561=1618%:% +%:%1562=1619%:% +%:%1563=1620%:% +%:%1564=1621%:% +%:%1565=1622%:% +%:%1566=1623%:% +%:%1567=1624%:% +%:%1568=1625%:% +%:%1569=1626%:% +%:%1570=1627%:% +%:%1571=1628%:% +%:%1572=1629%:% +%:%1573=1630%:% +%:%1574=1631%:% +%:%1575=1632%:% +%:%1576=1633%:% +%:%1577=1634%:% +%:%1578=1635%:% +%:%1579=1636%:% +%:%1580=1637%:% +%:%1581=1638%:% +%:%1582=1639%:% +%:%1583=1640%:% +%:%1584=1641%:% +%:%1585=1642%:% +%:%1586=1643%:% +%:%1587=1644%:% +%:%1588=1645%:% +%:%1589=1646%:% +%:%1590=1647%:% +%:%1591=1648%:% +%:%1592=1649%:% +%:%1593=1650%:% +%:%1594=1651%:% +%:%1595=1652%:% +%:%1596=1653%:% +%:%1597=1654%:% +%:%1598=1655%:% +%:%1599=1656%:% +%:%1600=1657%:% +%:%1601=1658%:% +%:%1602=1659%:% +%:%1603=1660%:% +%:%1604=1661%:% +%:%1604=1777%:% +%:%1605=1778%:% +%:%1606=1779%:% +%:%1607=1780%:% +%:%1608=1781%:% +%:%1608=1942%:% +%:%1609=1943%:% +%:%1610=1944%:% +%:%1611=1945%:% +%:%1612=1946%:% +%:%1613=1947%:% +%:%1614=1948%:% +%:%1615=1949%:% +%:%1616=1950%:% +%:%1617=1951%:% +%:%1618=1952%:% +%:%1619=1953%:% +%:%1620=1954%:% +%:%1621=1955%:% +%:%1622=1956%:% +%:%1623=1957%:% +%:%1624=1958%:% +%:%1625=1959%:% +%:%1626=1960%:% +%:%1627=1961%:% +%:%1627=1962%:% +%:%1628=1963%:% +%:%1628=1964%:% +%:%1628=1965%:% +%:%1629=1966%:% +%:%1629=1967%:% +%:%1630=1968%:% +%:%1631=1969%:% +%:%1632=1970%:% +%:%1633=1971%:% +%:%1634=1972%:% +%:%1635=1973%:% +%:%1636=1974%:% +%:%1637=1975%:% +%:%1638=1976%:% +%:%1639=1977%:% +%:%1640=1978%:% +%:%1641=1979%:% +%:%1642=1980%:% +%:%1643=1981%:% +%:%1644=1982%:% +%:%1645=1983%:% +%:%1646=1984%:% +%:%1646=1985%:% +%:%1647=1986%:% +%:%1648=1987%:% +%:%1649=1988%:% +%:%1649=1989%:% +%:%1649=1990%:% +%:%1650=1991%:% +%:%1651=1992%:% +%:%1652=1993%:% +%:%1652=1994%:% +%:%1653=1995%:% +%:%1653=1996%:% +%:%1654=1997%:% +%:%1655=1998%:% +%:%1656=1999%:% +%:%1657=2000%:% +%:%1658=2001%:% +%:%1659=2002%:% +%:%1660=2003%:% +%:%1661=2004%:% +%:%1662=2005%:% +%:%1663=2006%:% +%:%1664=2007%:% +%:%1665=2008%:% +%:%1666=2009%:% +%:%1667=2010%:% +%:%1668=2011%:% +%:%1669=2012%:% +%:%1670=2013%:% +%:%1679=2018%:% +%:%1691=2022%:% +%:%1692=2023%:% +%:%1693=2024%:% +%:%1694=2025%:% +%:%1695=2026%:% +%:%1696=2027%:% +%:%1697=2028%:% +%:%1698=2029%:% +%:%1699=2030%:% +%:%1700=2031%:% +%:%1701=2032%:% +%:%1702=2033%:% +%:%1703=2034%:% +%:%1704=2035%:% +%:%1705=2036%:% +%:%1706=2037%:% +%:%1707=2038%:% +%:%1708=2039%:% +%:%1709=2040%:% +%:%1710=2041%:% +%:%1711=2042%:% +%:%1712=2043%:% +%:%1713=2044%:% +%:%1714=2045%:% +%:%1715=2046%:% +%:%1716=2047%:% +%:%1717=2048%:% +%:%1718=2049%:% +%:%1719=2050%:% +%:%1720=2051%:% +%:%1721=2052%:% +%:%1722=2053%:% +%:%1723=2054%:% +%:%1724=2055%:% +%:%1725=2056%:% +%:%1726=2057%:% +%:%1727=2058%:% +%:%1728=2059%:% +%:%1729=2060%:% +%:%1730=2061%:% +%:%1731=2062%:% +%:%1732=2063%:% +%:%1733=2064%:% +%:%1734=2065%:% +%:%1735=2066%:% +%:%1736=2067%:% +%:%1737=2068%:% +%:%1738=2069%:% +%:%1739=2070%:% +%:%1740=2071%:% +%:%1741=2072%:% +%:%1742=2073%:% +%:%1743=2074%:% +%:%1756=2080%:% +%:%1759=2081%:% +%:%1760=2082%:% \ No newline at end of file diff -r a8b4d8593bdb -r 28458dec90f8 thys2/Journal/Paper.thy --- a/thys2/Journal/Paper.thy Thu Nov 04 15:11:11 2021 +0000 +++ b/thys2/Journal/Paper.thy Tue Dec 14 16:17:45 2021 +0000 @@ -265,10 +265,34 @@ @{thm blexersimp_correctness} \end{lemma} -The nice thing about the aove +The nice thing about the above \ +section \ Additional Simp Rules?\ + + +text \ +One question someone would ask is: +can we add more "atomic" simplification/rewriting rules, +so the simplification is even more aggressive, making +the intermediate results smaller, and therefore more space-efficient? +For example, one might want to do open up alternatives who is a child +of a sequence: + +\begin{center} + \begin{tabular}{lcl} + @{thm[mode=Rule] aggressive.intros(1)[of "bs" "bs1" "rs" "r"]}\\ + \end{tabular} +\end{center} + + +This rule allows us to simplify \mbox{@{term "ALT (SEQ (ALT a b) c) (SEQ a c)"}} + into \mbox{@{term "ALT (SEQ a c) (SEQ b c)"}}, +which is cannot be done under the \ rule because only alternatives which are +children of another alternative can be spilled out. +\ + section \Introduction\ @@ -2055,9 +2079,19 @@ end (*>*) + + (* \begin{center} + \begin{tabular} + @{thm[mode=Rule] aggressive.intros(1)[of "bs" "bs1" "rs" "r"]} + end{tabular} +\end{center} + + + +\begin{center} \begin{tabular}{lcl} @{thm (lhs) code.simps(1)} & $\dn$ & @{thm (rhs) code.simps(1)}\\ @{thm (lhs) code.simps(2)} & $\dn$ & @{thm (rhs) code.simps(2)}\\ diff -r a8b4d8593bdb -r 28458dec90f8 thys2/Journal/Paper.thy~ --- a/thys2/Journal/Paper.thy~ Thu Nov 04 15:11:11 2021 +0000 +++ b/thys2/Journal/Paper.thy~ Tue Dec 14 16:17:45 2021 +0000 @@ -131,19 +131,11 @@ (*>*) - - -section \Introduction\ - - +section\Core of the proof\ text \ -Trying out after lualatex. - - -uhuhuhu -This works builds on previous work by Ausaf and Urban using +This paper builds on previous work by Ausaf and Urban using regular expression'd bit-coded derivatives to do lexing that -is both fast and satisfied the POSIX specification. +is both fast and satisfies the POSIX specification. In their work, a bit-coded algorithm introduced by Sulzmann and Lu was formally verified in Isabelle, by a very clever use of flex function and retrieve to carefully mimic the way a value is @@ -151,10 +143,138 @@ In the previous work, Ausaf and Urban established the below equality: \begin{lemma} -@{thm [mode=IfThen] bder_retrieve} +@{thm [mode=IfThen] MAIN_decode} +\end{lemma} + +This lemma establishes a link with the lexer without bit-codes. + +With it we get the correctness of bit-coded algorithm. +\begin{lemma} +@{thm [mode=IfThen] blexer_correctness} +\end{lemma} + +However what is not certain is whether we can add simplification +to the bit-coded algorithm, without breaking the correct lexing output. + + +The reason that we do need to add a simplification phase +after each derivative step of $\textit{blexer}$ is +because it produces intermediate +regular expressions that can grow exponentially. +For example, the regular expression $(a+aa)^*$ after taking +derivative against just 10 $a$s will have size 8192. + +%TODO: add figure for this? + + +Therefore, we insert a simplification phase +after each derivation step, as defined below: +\begin{lemma} +@{thm blexer_simp_def} \end{lemma} -This lemma links the regular expression +The simplification function is given as follows: + +\begin{center} + \begin{tabular}{lcl} + @{thm (lhs) bsimp.simps(1)[of "bs" "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) bsimp.simps(1)[of "bs" "r\<^sub>1" "r\<^sub>2"]}\\ + @{thm (lhs) bsimp.simps(2)} & $\dn$ & @{thm (rhs) bsimp.simps(2)}\\ + @{thm (lhs) bsimp.simps(3)} & $\dn$ & @{thm (rhs) bsimp.simps(3)}\\ + +\end{tabular} +\end{center} + +And the two helper functions are: +\begin{center} + \begin{tabular}{lcl} + @{thm (lhs) bsimp_AALTs.simps(2)[of "bs\<^sub>1" "r" ]} & $\dn$ & @{thm (rhs) bsimp.simps(1)[of "bs\<^sub>1" "r" ]}\\ + @{thm (lhs) bsimp_AALTs.simps(2)} & $\dn$ & @{thm (rhs) bsimp.simps(2)}\\ + @{thm (lhs) bsimp_AALTs.simps(3)} & $\dn$ & @{thm (rhs) bsimp.simps(3)}\\ + +\end{tabular} +\end{center} + + +This might sound trivial in the case of producing a YES/NO answer, +but once we require a lexing output to be produced (which is required +in applications like compiler front-end, malicious attack domain extraction, +etc.), it is not straightforward if we still extract what is needed according +to the POSIX standard. + + + + + +By simplification, we mean specifically the following rules: + +\begin{center} + \begin{tabular}{lcl} + @{thm[mode=Axiom] rrewrite.intros(1)[of "bs" "r\<^sub>2"]}\\ + @{thm[mode=Axiom] rrewrite.intros(2)[of "bs" "r\<^sub>1"]}\\ + @{thm[mode=Axiom] rrewrite.intros(3)[of "bs" "bs\<^sub>1" "r\<^sub>1"]}\\ + @{thm[mode=Rule] rrewrite.intros(4)[of "r\<^sub>1" "r\<^sub>2" "bs" "r\<^sub>3"]}\\ + @{thm[mode=Rule] rrewrite.intros(5)[of "r\<^sub>3" "r\<^sub>4" "bs" "r\<^sub>1"]}\\ + @{thm[mode=Rule] rrewrite.intros(6)[of "r" "r'" "bs" "rs\<^sub>1" "rs\<^sub>2"]}\\ + @{thm[mode=Axiom] rrewrite.intros(7)[of "bs" "rs\<^sub>a" "rs\<^sub>b"]}\\ + @{thm[mode=Axiom] rrewrite.intros(8)[of "bs" "rs\<^sub>a" "bs\<^sub>1" "rs\<^sub>1" "rs\<^sub>b"]}\\ + @{thm[mode=Axiom] rrewrite.intros(9)[of "bs" "bs\<^sub>1" "rs"]}\\ + @{thm[mode=Axiom] rrewrite.intros(10)[of "bs" ]}\\ + @{thm[mode=Axiom] rrewrite.intros(11)[of "bs" "r\<^sub>1"]}\\ + @{thm[mode=Rule] rrewrite.intros(12)[of "a\<^sub>1" "a\<^sub>2" "bs" "rs\<^sub>a" "rs\<^sub>b" "rs\<^sub>c"]}\\ + + \end{tabular} +\end{center} + + +And these can be made compact by the following simplification function: + +where the function $\mathit{bsimp_AALTs}$ + +The core idea of the proof is that two regular expressions, +if "isomorphic" up to a finite number of rewrite steps, will +remain "isomorphic" when we take the same sequence of +derivatives on both of them. +This can be expressed by the following rewrite relation lemma: +\begin{lemma} +@{thm [mode=IfThen] central} +\end{lemma} + +This isomorphic relation implies a property that leads to the +correctness result: +if two (nullable) regular expressions are "rewritable" in many steps +from one another, +then a call to function $\textit{bmkeps}$ gives the same +bit-sequence : +\begin{lemma} +@{thm [mode=IfThen] rewrites_bmkeps} +\end{lemma} + +Given the same bit-sequence, the decode function +will give out the same value, which is the output +of both lexers: +\begin{lemma} +@{thm blexer_def} +\end{lemma} + +\begin{lemma} +@{thm blexer_simp_def} +\end{lemma} + +And that yields the correctness result: +\begin{lemma} +@{thm blexersimp_correctness} +\end{lemma} + +The nice thing about the aove +\ + + + +section \Introduction\ + + +text \ + Brzozowski \cite{Brzozowski1964} introduced the notion of the {\em derivative} @{term "der c r"} of a regular expression \r\ w.r.t.\ @@ -334,6 +454,9 @@ \ + + + section \Preliminaries\ text \\noindent Strings in Isabelle/HOL are lists of characters with @@ -1416,111 +1539,6 @@ @{thm lexer_flex} \end{center} -\begin{center} - \begin{tabular}{lcl} - @{thm (lhs) code.simps(1)} & $\dn$ & @{thm (rhs) code.simps(1)}\\ - @{thm (lhs) code.simps(2)} & $\dn$ & @{thm (rhs) code.simps(2)}\\ - @{thm (lhs) code.simps(3)} & $\dn$ & @{thm (rhs) code.simps(3)}\\ - @{thm (lhs) code.simps(4)} & $\dn$ & @{thm (rhs) code.simps(4)}\\ - @{thm (lhs) code.simps(5)[of "v\<^sub>1" "v\<^sub>2"]} & $\dn$ & @{thm (rhs) code.simps(5)[of "v\<^sub>1" "v\<^sub>2"]}\\ - @{thm (lhs) code.simps(6)} & $\dn$ & @{thm (rhs) code.simps(6)}\\ - @{thm (lhs) code.simps(7)} & $\dn$ & @{thm (rhs) code.simps(7)} -\end{tabular} -\end{center} - -\begin{center} -\begin{tabular}{lcl} - @{term areg} & $::=$ & @{term "AZERO"}\\ - & $\mid$ & @{term "AONE bs"}\\ - & $\mid$ & @{term "ACH bs c"}\\ - & $\mid$ & @{term "AALT bs r1 r2"}\\ - & $\mid$ & @{term "ASEQ bs r\<^sub>1 r\<^sub>2"}\\ - & $\mid$ & @{term "ASTAR bs r"} -\end{tabular} -\end{center} - - -\begin{center} - \begin{tabular}{lcl} - @{thm (lhs) intern.simps(1)} & $\dn$ & @{thm (rhs) intern.simps(1)}\\ - @{thm (lhs) intern.simps(2)} & $\dn$ & @{thm (rhs) intern.simps(2)}\\ - @{thm (lhs) intern.simps(3)} & $\dn$ & @{thm (rhs) intern.simps(3)}\\ - @{thm (lhs) intern.simps(4)[of "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) intern.simps(4)[of "r\<^sub>1" "r\<^sub>2"]}\\ - @{thm (lhs) intern.simps(5)[of "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) intern.simps(5)[of "r\<^sub>1" "r\<^sub>2"]}\\ - @{thm (lhs) intern.simps(6)} & $\dn$ & @{thm (rhs) intern.simps(6)}\\ -\end{tabular} -\end{center} - -\begin{center} - \begin{tabular}{lcl} - @{thm (lhs) erase.simps(1)} & $\dn$ & @{thm (rhs) erase.simps(1)}\\ - @{thm (lhs) erase.simps(2)[of bs]} & $\dn$ & @{thm (rhs) erase.simps(2)[of bs]}\\ - @{thm (lhs) erase.simps(3)[of bs]} & $\dn$ & @{thm (rhs) erase.simps(3)[of bs]}\\ - @{thm (lhs) erase.simps(4)[of bs "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) erase.simps(4)[of bs "r\<^sub>1" "r\<^sub>2"]}\\ - @{thm (lhs) erase.simps(5)[of bs "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) erase.simps(5)[of bs "r\<^sub>1" "r\<^sub>2"]}\\ - @{thm (lhs) erase.simps(6)[of bs]} & $\dn$ & @{thm (rhs) erase.simps(6)[of bs]}\\ -\end{tabular} -\end{center} - -Some simple facts about erase - -\begin{lemma}\mbox{}\\ -@{thm erase_bder}\\ -@{thm erase_intern} -\end{lemma} - -\begin{center} - \begin{tabular}{lcl} - @{thm (lhs) bnullable.simps(1)} & $\dn$ & @{thm (rhs) bnullable.simps(1)}\\ - @{thm (lhs) bnullable.simps(2)} & $\dn$ & @{thm (rhs) bnullable.simps(2)}\\ - @{thm (lhs) bnullable.simps(3)} & $\dn$ & @{thm (rhs) bnullable.simps(3)}\\ - @{thm (lhs) bnullable.simps(4)[of bs "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) bnullable.simps(4)[of bs "r\<^sub>1" "r\<^sub>2"]}\\ - @{thm (lhs) bnullable.simps(5)[of bs "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) bnullable.simps(5)[of bs "r\<^sub>1" "r\<^sub>2"]}\\ - @{thm (lhs) bnullable.simps(6)} & $\dn$ & @{thm (rhs) bnullable.simps(6)}\medskip\\ - -% \end{tabular} -% \end{center} - -% \begin{center} -% \begin{tabular}{lcl} - - @{thm (lhs) bder.simps(1)} & $\dn$ & @{thm (rhs) bder.simps(1)}\\ - @{thm (lhs) bder.simps(2)} & $\dn$ & @{thm (rhs) bder.simps(2)}\\ - @{thm (lhs) bder.simps(3)} & $\dn$ & @{thm (rhs) bder.simps(3)}\\ - @{thm (lhs) bder.simps(4)[of bs "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) bder.simps(4)[of bs "r\<^sub>1" "r\<^sub>2"]}\\ - @{thm (lhs) bder.simps(5)[of bs "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) bder.simps(5)[of bs "r\<^sub>1" "r\<^sub>2"]}\\ - @{thm (lhs) bder.simps(6)} & $\dn$ & @{thm (rhs) bder.simps(6)} - \end{tabular} - \end{center} - - -\begin{center} - \begin{tabular}{lcl} - @{thm (lhs) bmkeps.simps(1)} & $\dn$ & @{thm (rhs) bmkeps.simps(1)}\\ - @{thm (lhs) bmkeps.simps(2)[of bs "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) bmkeps.simps(2)[of bs "r\<^sub>1" "r\<^sub>2"]}\\ - @{thm (lhs) bmkeps.simps(3)[of bs "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) bmkeps.simps(3)[of bs "r\<^sub>1" "r\<^sub>2"]}\\ - @{thm (lhs) bmkeps.simps(4)} & $\dn$ & @{thm (rhs) bmkeps.simps(4)}\medskip\\ -\end{tabular} -\end{center} - - -@{thm [mode=IfThen] bder_retrieve} - -By induction on \r\ - -\begin{theorem}[Main Lemma]\mbox{}\\ -@{thm [mode=IfThen] MAIN_decode} -\end{theorem} - -\noindent -Definition of the bitcoded lexer - -@{thm blexer_def} - - -\begin{theorem} -@{thm blexer_correctness} -\end{theorem} \ @@ -1643,7 +1661,7 @@ \begin{tabular}{lcl} @{term areg} & $::=$ & @{term "AZERO"}\\ & $\mid$ & @{term "AONE bs"}\\ - & $\mid$ & @{term "ACH bs c"}\\ + & $\mid$ & @{term "ACHAR bs c"}\\ & $\mid$ & @{term "AALT bs r1 r2"}\\ & $\mid$ & @{term "ASEQ bs r\<^sub>1 r\<^sub>2"}\\ & $\mid$ & @{term "ASTAR bs r"} @@ -1977,19 +1995,6 @@ section \HERE\ text \ - \begin{center} - \begin{tabular}{llcl} - 1) & @{thm (lhs) erase.simps(1)} & $\dn$ & @{thm (rhs) erase.simps(1)}\\ - 2) & @{thm (lhs) erase.simps(2)[of bs]} & $\dn$ & @{thm (rhs) erase.simps(2)[of bs]}\\ - 3) & @{thm (lhs) erase.simps(3)[of bs]} & $\dn$ & @{thm (rhs) erase.simps(3)[of bs]}\\ - 4a) & @{term "erase (AALTs bs [])"} & $\dn$ & @{term ZERO}\\ - 4b) & @{term "erase (AALTs bs [r])"} & $\dn$ & @{term "erase r"}\\ - 4c) & @{term "erase (AALTs bs (r\<^sub>1#r\<^sub>2#rs))"} & $\dn$ & - @{term "ALT (erase r\<^sub>1) (erase (AALTs bs (r\<^sub>2#rs)))"}\\ - 5) & @{thm (lhs) erase.simps(5)[of bs "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) erase.simps(5)[of bs "r\<^sub>1" "r\<^sub>2"]}\\ - 6) & @{thm (lhs) erase.simps(6)[of bs]} & $\dn$ & @{thm (rhs) erase.simps(6)[of bs]}\\ - \end{tabular} - \end{center} \begin{lemma} @{thm [mode=IfThen] bder_retrieve} @@ -1999,7 +2004,7 @@ By induction on the definition of @{term "erase r"}. The cases for rule 1) and 2) are straightforward as @{term "der c ZERO"} and @{term "der c ONE"} are both equal to @{term ZERO}. This means @{term "\ v : ZERO"} cannot hold. Similarly in case of rule 3) - where @{term r} is of the form @{term "ACH d"} with @{term "c = d"}. Then by assumption + where @{term r} is of the form @{term "ACHAR d"} with @{term "c = d"}. Then by assumption we know @{term "\ v : ONE"}, which implies @{term "v = Void"}. The equation follows by simplification of left- and right-hand side. In case @{term "c \ d"} we have again @{term "\ v : ZERO"}, which cannot hold. @@ -2040,7 +2045,7 @@ and right-hand side are equal. This completes the proof. \end{proof} - + \bibliographystyle{plain} \bibliography{root} @@ -2048,4 +2053,225 @@ \ (*<*) end -(*>*) \ No newline at end of file +(*>*) + +(* + +\begin{center} + \begin{tabular}{lcl} + @{thm (lhs) code.simps(1)} & $\dn$ & @{thm (rhs) code.simps(1)}\\ + @{thm (lhs) code.simps(2)} & $\dn$ & @{thm (rhs) code.simps(2)}\\ + @{thm (lhs) code.simps(3)} & $\dn$ & @{thm (rhs) code.simps(3)}\\ + @{thm (lhs) code.simps(4)} & $\dn$ & @{thm (rhs) code.simps(4)}\\ + @{thm (lhs) code.simps(5)[of "v\<^sub>1" "v\<^sub>2"]} & $\dn$ & @{thm (rhs) code.simps(5)[of "v\<^sub>1" "v\<^sub>2"]}\\ + @{thm (lhs) code.simps(6)} & $\dn$ & @{thm (rhs) code.simps(6)}\\ + @{thm (lhs) code.simps(7)} & $\dn$ & @{thm (rhs) code.simps(7)} +\end{tabular} +\end{center} + +\begin{center} +\begin{tabular}{lcl} + @{term areg} & $::=$ & @{term "AZERO"}\\ + & $\mid$ & @{term "AONE bs"}\\ + & $\mid$ & @{term "ACHAR bs c"}\\ + & $\mid$ & @{term "AALT bs r1 r2"}\\ + & $\mid$ & @{term "ASEQ bs r\<^sub>1 r\<^sub>2"}\\ + & $\mid$ & @{term "ASTAR bs r"} +\end{tabular} +\end{center} + + +\begin{center} + \begin{tabular}{lcl} + @{thm (lhs) intern.simps(1)} & $\dn$ & @{thm (rhs) intern.simps(1)}\\ + @{thm (lhs) intern.simps(2)} & $\dn$ & @{thm (rhs) intern.simps(2)}\\ + @{thm (lhs) intern.simps(3)} & $\dn$ & @{thm (rhs) intern.simps(3)}\\ + @{thm (lhs) intern.simps(4)[of "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) intern.simps(4)[of "r\<^sub>1" "r\<^sub>2"]}\\ + @{thm (lhs) intern.simps(5)[of "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) intern.simps(5)[of "r\<^sub>1" "r\<^sub>2"]}\\ + @{thm (lhs) intern.simps(6)} & $\dn$ & @{thm (rhs) intern.simps(6)}\\ +\end{tabular} +\end{center} + +\begin{center} + \begin{tabular}{lcl} + @{thm (lhs) erase.simps(1)} & $\dn$ & @{thm (rhs) erase.simps(1)}\\ + @{thm (lhs) erase.simps(2)[of bs]} & $\dn$ & @{thm (rhs) erase.simps(2)[of bs]}\\ + @{thm (lhs) erase.simps(3)[of bs]} & $\dn$ & @{thm (rhs) erase.simps(3)[of bs]}\\ + @{thm (lhs) erase.simps(4)[of bs "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) erase.simps(4)[of bs "r\<^sub>1" "r\<^sub>2"]}\\ + @{thm (lhs) erase.simps(5)[of bs "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) erase.simps(5)[of bs "r\<^sub>1" "r\<^sub>2"]}\\ + @{thm (lhs) erase.simps(6)[of bs]} & $\dn$ & @{thm (rhs) erase.simps(6)[of bs]}\\ +\end{tabular} +\end{center} + +Some simple facts about erase + +\begin{lemma}\mbox{}\\ +@{thm erase_bder}\\ +@{thm erase_intern} +\end{lemma} + +\begin{center} + \begin{tabular}{lcl} + @{thm (lhs) bnullable.simps(1)} & $\dn$ & @{thm (rhs) bnullable.simps(1)}\\ + @{thm (lhs) bnullable.simps(2)} & $\dn$ & @{thm (rhs) bnullable.simps(2)}\\ + @{thm (lhs) bnullable.simps(3)} & $\dn$ & @{thm (rhs) bnullable.simps(3)}\\ + @{thm (lhs) bnullable.simps(4)[of bs "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) bnullable.simps(4)[of bs "r\<^sub>1" "r\<^sub>2"]}\\ + @{thm (lhs) bnullable.simps(5)[of bs "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) bnullable.simps(5)[of bs "r\<^sub>1" "r\<^sub>2"]}\\ + @{thm (lhs) bnullable.simps(6)} & $\dn$ & @{thm (rhs) bnullable.simps(6)}\medskip\\ + +% \end{tabular} +% \end{center} + +% \begin{center} +% \begin{tabular}{lcl} + + @{thm (lhs) bder.simps(1)} & $\dn$ & @{thm (rhs) bder.simps(1)}\\ + @{thm (lhs) bder.simps(2)} & $\dn$ & @{thm (rhs) bder.simps(2)}\\ + @{thm (lhs) bder.simps(3)} & $\dn$ & @{thm (rhs) bder.simps(3)}\\ + @{thm (lhs) bder.simps(4)[of bs "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) bder.simps(4)[of bs "r\<^sub>1" "r\<^sub>2"]}\\ + @{thm (lhs) bder.simps(5)[of bs "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) bder.simps(5)[of bs "r\<^sub>1" "r\<^sub>2"]}\\ + @{thm (lhs) bder.simps(6)} & $\dn$ & @{thm (rhs) bder.simps(6)} + \end{tabular} + \end{center} + + +\begin{center} + \begin{tabular}{lcl} + @{thm (lhs) bmkeps.simps(1)} & $\dn$ & @{thm (rhs) bmkeps.simps(1)}\\ + @{thm (lhs) bmkeps.simps(2)[of bs "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) bmkeps.simps(2)[of bs "r\<^sub>1" "r\<^sub>2"]}\\ + @{thm (lhs) bmkeps.simps(3)[of bs "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) bmkeps.simps(3)[of bs "r\<^sub>1" "r\<^sub>2"]}\\ + @{thm (lhs) bmkeps.simps(4)} & $\dn$ & @{thm (rhs) bmkeps.simps(4)}\medskip\\ +\end{tabular} +\end{center} + + +@{thm [mode=IfThen] bder_retrieve} + +By induction on \r\ + +\begin{theorem}[Main Lemma]\mbox{}\\ +@{thm [mode=IfThen] MAIN_decode} +\end{theorem} + +\noindent +Definition of the bitcoded lexer + +@{thm blexer_def} + + +\begin{theorem} +@{thm blexer_correctness} +\end{theorem} + + + + + +\begin{center} + \begin{tabular}{lcl} + @{thm (lhs) code.simps(1)} & $\dn$ & @{thm (rhs) code.simps(1)}\\ + @{thm (lhs) code.simps(2)} & $\dn$ & @{thm (rhs) code.simps(2)}\\ + @{thm (lhs) code.simps(3)} & $\dn$ & @{thm (rhs) code.simps(3)}\\ + @{thm (lhs) code.simps(4)} & $\dn$ & @{thm (rhs) code.simps(4)}\\ + @{thm (lhs) code.simps(5)[of "v\<^sub>1" "v\<^sub>2"]} & $\dn$ & @{thm (rhs) code.simps(5)[of "v\<^sub>1" "v\<^sub>2"]}\\ + @{thm (lhs) code.simps(6)} & $\dn$ & @{thm (rhs) code.simps(6)}\\ + @{thm (lhs) code.simps(7)} & $\dn$ & @{thm (rhs) code.simps(7)} +\end{tabular} +\end{center} + +\begin{center} +\begin{tabular}{lcl} + @{term areg} & $::=$ & @{term "AZERO"}\\ + & $\mid$ & @{term "AONE bs"}\\ + & $\mid$ & @{term "ACHAR bs c"}\\ + & $\mid$ & @{term "AALT bs r1 r2"}\\ + & $\mid$ & @{term "ASEQ bs r\<^sub>1 r\<^sub>2"}\\ + & $\mid$ & @{term "ASTAR bs r"} +\end{tabular} +\end{center} + + +\begin{center} + \begin{tabular}{lcl} + @{thm (lhs) intern.simps(1)} & $\dn$ & @{thm (rhs) intern.simps(1)}\\ + @{thm (lhs) intern.simps(2)} & $\dn$ & @{thm (rhs) intern.simps(2)}\\ + @{thm (lhs) intern.simps(3)} & $\dn$ & @{thm (rhs) intern.simps(3)}\\ + @{thm (lhs) intern.simps(4)[of "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) intern.simps(4)[of "r\<^sub>1" "r\<^sub>2"]}\\ + @{thm (lhs) intern.simps(5)[of "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) intern.simps(5)[of "r\<^sub>1" "r\<^sub>2"]}\\ + @{thm (lhs) intern.simps(6)} & $\dn$ & @{thm (rhs) intern.simps(6)}\\ +\end{tabular} +\end{center} + +\begin{center} + \begin{tabular}{lcl} + @{thm (lhs) erase.simps(1)} & $\dn$ & @{thm (rhs) erase.simps(1)}\\ + @{thm (lhs) erase.simps(2)[of bs]} & $\dn$ & @{thm (rhs) erase.simps(2)[of bs]}\\ + @{thm (lhs) erase.simps(3)[of bs]} & $\dn$ & @{thm (rhs) erase.simps(3)[of bs]}\\ + @{thm (lhs) erase.simps(4)[of bs "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) erase.simps(4)[of bs "r\<^sub>1" "r\<^sub>2"]}\\ + @{thm (lhs) erase.simps(5)[of bs "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) erase.simps(5)[of bs "r\<^sub>1" "r\<^sub>2"]}\\ + @{thm (lhs) erase.simps(6)[of bs]} & $\dn$ & @{thm (rhs) erase.simps(6)[of bs]}\\ +\end{tabular} +\end{center} + +Some simple facts about erase + +\begin{lemma}\mbox{}\\ +@{thm erase_bder}\\ +@{thm erase_intern} +\end{lemma} + +\begin{center} + \begin{tabular}{lcl} + @{thm (lhs) bnullable.simps(1)} & $\dn$ & @{thm (rhs) bnullable.simps(1)}\\ + @{thm (lhs) bnullable.simps(2)} & $\dn$ & @{thm (rhs) bnullable.simps(2)}\\ + @{thm (lhs) bnullable.simps(3)} & $\dn$ & @{thm (rhs) bnullable.simps(3)}\\ + @{thm (lhs) bnullable.simps(4)[of bs "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) bnullable.simps(4)[of bs "r\<^sub>1" "r\<^sub>2"]}\\ + @{thm (lhs) bnullable.simps(5)[of bs "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) bnullable.simps(5)[of bs "r\<^sub>1" "r\<^sub>2"]}\\ + @{thm (lhs) bnullable.simps(6)} & $\dn$ & @{thm (rhs) bnullable.simps(6)}\medskip\\ + +% \end{tabular} +% \end{center} + +% \begin{center} +% \begin{tabular}{lcl} + + @{thm (lhs) bder.simps(1)} & $\dn$ & @{thm (rhs) bder.simps(1)}\\ + @{thm (lhs) bder.simps(2)} & $\dn$ & @{thm (rhs) bder.simps(2)}\\ + @{thm (lhs) bder.simps(3)} & $\dn$ & @{thm (rhs) bder.simps(3)}\\ + @{thm (lhs) bder.simps(4)[of bs "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) bder.simps(4)[of bs "r\<^sub>1" "r\<^sub>2"]}\\ + @{thm (lhs) bder.simps(5)[of bs "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) bder.simps(5)[of bs "r\<^sub>1" "r\<^sub>2"]}\\ + @{thm (lhs) bder.simps(6)} & $\dn$ & @{thm (rhs) bder.simps(6)} + \end{tabular} + \end{center} + + +\begin{center} + \begin{tabular}{lcl} + @{thm (lhs) bmkeps.simps(1)} & $\dn$ & @{thm (rhs) bmkeps.simps(1)}\\ + @{thm (lhs) bmkeps.simps(2)[of bs "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) bmkeps.simps(2)[of bs "r\<^sub>1" "r\<^sub>2"]}\\ + @{thm (lhs) bmkeps.simps(3)[of bs "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) bmkeps.simps(3)[of bs "r\<^sub>1" "r\<^sub>2"]}\\ + @{thm (lhs) bmkeps.simps(4)} & $\dn$ & @{thm (rhs) bmkeps.simps(4)}\medskip\\ +\end{tabular} +\end{center} + + +@{thm [mode=IfThen] bder_retrieve} + +By induction on \r\ + +\begin{theorem}[Main Lemma]\mbox{}\\ +@{thm [mode=IfThen] MAIN_decode} +\end{theorem} + +\noindent +Definition of the bitcoded lexer + +@{thm blexer_def} + + +\begin{theorem} +@{thm blexer_correctness} +\end{theorem} + +\ +\*) \ No newline at end of file diff -r a8b4d8593bdb -r 28458dec90f8 thys2/Journal/session_graph.pdf Binary file thys2/Journal/session_graph.pdf has changed diff -r a8b4d8593bdb -r 28458dec90f8 thys2/PDerivs.thy --- a/thys2/PDerivs.thy Thu Nov 04 15:11:11 2021 +0000 +++ b/thys2/PDerivs.thy Tue Dec 14 16:17:45 2021 +0000 @@ -17,7 +17,7 @@ where "pder c ZERO = {}" | "pder c ONE = {}" -| "pder c (CHAR d) = (if c = d then {ONE} else {})" +| "pder c (CH d) = (if c = d then {ONE} else {})" | "pder c (ALT r1 r2) = (pder c r1) \ (pder c r2)" | "pder c (SEQ r1 r2) = (if nullable r1 then SEQs (pder c r1) r2 \ pder c r2 else SEQs (pder c r1) r2)" @@ -54,7 +54,7 @@ by (induct s) (simp_all) lemma pders_CHAR: - shows "pders s (CHAR c) \ {CHAR c, ONE}" + shows "pders s (CH c) \ {CH c, ONE}" by (induct s) (simp_all) subsection \Relating left-quotients and partial derivatives\ @@ -127,7 +127,7 @@ unfolding UNIV1_def pders_Set_def by (auto split: if_splits) lemma pders_Set_CHAR [simp]: - shows "pders_Set UNIV1 (CHAR c) = {ONE}" + shows "pders_Set UNIV1 (CH c) = {ONE}" unfolding UNIV1_def pders_Set_def apply(auto) apply(frule rev_subsetD) @@ -282,7 +282,7 @@ fun awidth :: "rexp \ nat" where "awidth ZERO = 0" | "awidth ONE = 0" | -"awidth (CHAR a) = 1" | +"awidth (CH a) = 1" | "awidth (ALT r1 r2) = awidth r1 + awidth r2" | "awidth (SEQ r1 r2) = awidth r1 + awidth r2" | "awidth (STAR r1) = awidth r1" @@ -364,7 +364,7 @@ fun subs :: "rexp \ rexp set" where "subs ZERO = {ZERO}" | "subs ONE = {ONE}" | -"subs (CHAR a) = {CHAR a, ONE}" | +"subs (CH a) = {CH a, ONE}" | "subs (ALT r1 r2) = (subs r1 \ subs r2 \ {ALT r1 r2})" | "subs (SEQ r1 r2) = (subs r1 \ subs r2 \ {SEQ r1 r2} \ SEQs (subs r1) r2)" | "subs (STAR r1) = (subs r1 \ {STAR r1} \ SEQs (subs r1) (STAR r1))" @@ -411,7 +411,7 @@ fun size2 :: "rexp \ nat" where "size2 ZERO = 1" | "size2 ONE = 1" | - "size2 (CHAR c) = 1" | + "size2 (CH c) = 1" | "size2 (ALT r1 r2) = Suc (size2 r1 + size2 r2)" | "size2 (SEQ r1 r2) = Suc (size2 r1 + size2 r2)" | "size2 (STAR r1) = Suc (size2 r1)" @@ -425,6 +425,7 @@ apply(simp_all) done +(* lemma subs_card: shows "card (subs r) \ Suc (size2 r + size2 r)" apply(induct r) @@ -433,6 +434,7 @@ apply(simp add: subs_finite) apply(simp add: subs_finite) oops +*) lemma subs_size2: shows "\r1 \ subs r. size2 r1 \ Suc (size2 r * size2 r)" @@ -532,7 +534,7 @@ fun height :: "rexp \ nat" where "height ZERO = 1" | "height ONE = 1" | - "height (CHAR c) = 1" | + "height (CH c) = 1" | "height (ALT r1 r2) = Suc (max (height r1) (height r2))" | "height (SEQ r1 r2) = Suc (max (height r1) (height r2))" | "height (STAR r1) = Suc (height r1)" @@ -555,7 +557,56 @@ apply(induct r) apply(auto)+ done - - + +fun lin_concat :: "(char \ rexp) \ rexp \ (char \ rexp)" (infixl "[.]" 91) + where +"(c, ZERO) [.] t = (c, ZERO)" +| "(c, ONE) [.] t = (c, t)" +| "(c, p) [.] t = (c, SEQ p t)" + + +fun circle_concat :: "(char \ rexp ) set \ rexp \ (char \ rexp) set" ( infixl "\" 90) + where +"l \ ZERO = {}" +| "l \ ONE = l" +| "l \ t = ( (\p. p [.] t) ` l ) " + + + +fun linear_form :: "rexp \( char \ rexp ) set" + where + "linear_form ZERO = {}" +| "linear_form ONE = {}" +| "linear_form (CH c) = {(c, ONE)}" +| "linear_form (ALT r1 r2) = (linear_form) r1 \ (linear_form r2)" +| "linear_form (SEQ r1 r2) = (if (nullable r1) then (linear_form r1) \ r2 \ linear_form r2 else (linear_form r1) \ r2) " +| "linear_form (STAR r ) = (linear_form r) \ (STAR r)" + + +value "linear_form (SEQ (STAR (CH x)) (STAR (ALT (SEQ (CH x) (CH x)) (CH y) )) )" + + +value "linear_form (STAR (ALT (SEQ (CH x) (CH x)) (CH y) )) " + +fun pdero :: "char \ rexp \ rexp set" + where +"pdero c t = \ ((\(d, p). if d = c then {p} else {}) ` (linear_form t) )" + +fun pderso :: "char list \ rexp \ rexp set" + where + "pderso [] r = {r}" +| "pderso (c # s) r = \ ( pderso s ` (pdero c r) )" + +lemma alternative_pder: + shows "pderso s r = pders s r" + sledgehammer + oops + + +export_code height pders subs pderso in Scala module_name Pders +export_code pdero pderso in Scala module_name Pderso +export_code pdero pderso in Scala module_name Pderso + + end \ No newline at end of file diff -r a8b4d8593bdb -r 28458dec90f8 thys2/SizeBound.thy --- a/thys2/SizeBound.thy Thu Nov 04 15:11:11 2021 +0000 +++ b/thys2/SizeBound.thy Tue Dec 14 16:17:45 2021 +0000 @@ -1556,7 +1556,17 @@ using blexer_correctness main_main by auto + +export_code blexer_simp blexer lexer bders bders_simp in Scala module_name VerifiedLexers + + unused_thms +inductive aggressive:: "arexp \ arexp \ bool" ("_ \? _" [99, 99] 99) + where + "ASEQ bs (AALTs bs1 rs) r \? AALTs (bs@bs1) (map (\r'. ASEQ [] r' r) rs) " + + + end diff -r a8b4d8593bdb -r 28458dec90f8 thys2/journal.pdf Binary file thys2/journal.pdf has changed