# HG changeset patch
# User Chengsong
# Date 1639499553 0
# Node ID c892847df987e93931835fe0bf2c8cfa1772f2ce
# Parent  28458dec90f8678d95247d53c357d884971a5f81
hi

diff -r 28458dec90f8 -r c892847df987 thys2/Journal/Paper.tex
--- a/thys2/Journal/Paper.tex	Tue Dec 14 16:17:45 2021 +0000
+++ b/thys2/Journal/Paper.tex	Tue Dec 14 16:32:33 2021 +0000
@@ -141,8 +141,8 @@
   \isa{\mbox{}\inferrule{\mbox{r\isactrlsub {\isadigit{1}}\ {\isasymleadsto}\ r\isactrlsub {\isadigit{2}}}}{\mbox{ASEQ\ bs\ r\isactrlsub {\isadigit{1}}\ r\isactrlsub {\isadigit{3}}\ {\isasymleadsto}\ ASEQ\ bs\ r\isactrlsub {\isadigit{2}}\ r\isactrlsub {\isadigit{3}}}}}\\
   \isa{\mbox{}\inferrule{\mbox{r\isactrlsub {\isadigit{3}}\ {\isasymleadsto}\ r\isactrlsub {\isadigit{4}}}}{\mbox{ASEQ\ bs\ r\isactrlsub {\isadigit{1}}\ r\isactrlsub {\isadigit{3}}\ {\isasymleadsto}\ ASEQ\ bs\ r\isactrlsub {\isadigit{1}}\ r\isactrlsub {\isadigit{4}}}}}\\
   \isa{\mbox{}\inferrule{\mbox{r\ {\isasymleadsto}\ r{\isacharprime}{\kern0pt}}}{\mbox{AALTs\ bs\ {\isacharparenleft}{\kern0pt}rs\isactrlsub {\isadigit{1}}\ {\isacharat}{\kern0pt}\ {\isacharbrackleft}{\kern0pt}r{\isacharbrackright}{\kern0pt}\ {\isacharat}{\kern0pt}\ rs\isactrlsub {\isadigit{2}}{\isacharparenright}{\kern0pt}\ {\isasymleadsto}\ AALTs\ bs\ {\isacharparenleft}{\kern0pt}rs\isactrlsub {\isadigit{1}}\ {\isacharat}{\kern0pt}\ {\isacharbrackleft}{\kern0pt}r{\isacharprime}{\kern0pt}{\isacharbrackright}{\kern0pt}\ {\isacharat}{\kern0pt}\ rs\isactrlsub {\isadigit{2}}{\isacharparenright}{\kern0pt}}}}\\
-  \isa{\mbox{}\inferrule{\mbox{}}{\mbox{AALTs\ bs\ {\isacharparenleft}{\kern0pt}rs\isactrlsub a\ {\isacharat}{\kern0pt}\ AZERO\mbox{$\,$}{\isacharcolon}{\kern0pt}{\isacharcolon}{\kern0pt}\mbox{$\,$}rs\isactrlsub b{\isacharparenright}{\kern0pt}\ {\isasymleadsto}\ AALTs\ bs\ {\isacharparenleft}{\kern0pt}rs\isactrlsub a\ {\isacharat}{\kern0pt}\ rs\isactrlsub b{\isacharparenright}{\kern0pt}}}}\\
-  \isa{\mbox{}\inferrule{\mbox{}}{\mbox{AALTs\ bs\ {\isacharparenleft}{\kern0pt}rs\isactrlsub a\ {\isacharat}{\kern0pt}\ AALTs\ bs\isactrlsub {\isadigit{1}}\ rs\isactrlsub {\isadigit{1}}\mbox{$\,$}{\isacharcolon}{\kern0pt}{\isacharcolon}{\kern0pt}\mbox{$\,$}rs\isactrlsub b{\isacharparenright}{\kern0pt}\ {\isasymleadsto}\ AALTs\ bs\ {\isacharparenleft}{\kern0pt}rs\isactrlsub a\ {\isacharat}{\kern0pt}\ map\ {\isacharparenleft}{\kern0pt}fuse\ bs\isactrlsub {\isadigit{1}}{\isacharparenright}{\kern0pt}\ rs\isactrlsub {\isadigit{1}}\ {\isacharat}{\kern0pt}\ rs\isactrlsub b{\isacharparenright}{\kern0pt}}}}\\
+  \isa{\mbox{}\inferrule{\mbox{}}{\mbox{AALTs\ bs\ {\isacharparenleft}{\kern0pt}rs\isactrlsub a\ {\isacharat}{\kern0pt}\ {\isacharbrackleft}{\kern0pt}AZERO{\isacharbrackright}{\kern0pt}\ {\isacharat}{\kern0pt}\ rs\isactrlsub b{\isacharparenright}{\kern0pt}\ {\isasymleadsto}\ AALTs\ bs\ {\isacharparenleft}{\kern0pt}rs\isactrlsub a\ {\isacharat}{\kern0pt}\ rs\isactrlsub b{\isacharparenright}{\kern0pt}}}}\\
+  \isa{\mbox{}\inferrule{\mbox{}}{\mbox{AALTs\ bs\ {\isacharparenleft}{\kern0pt}rs\isactrlsub a\ {\isacharat}{\kern0pt}\ {\isacharbrackleft}{\kern0pt}AALTs\ bs\isactrlsub {\isadigit{1}}\ rs\isactrlsub {\isadigit{1}}{\isacharbrackright}{\kern0pt}\ {\isacharat}{\kern0pt}\ rs\isactrlsub b{\isacharparenright}{\kern0pt}\ {\isasymleadsto}\ AALTs\ bs\ {\isacharparenleft}{\kern0pt}rs\isactrlsub a\ {\isacharat}{\kern0pt}\ map\ {\isacharparenleft}{\kern0pt}fuse\ bs\isactrlsub {\isadigit{1}}{\isacharparenright}{\kern0pt}\ rs\isactrlsub {\isadigit{1}}\ {\isacharat}{\kern0pt}\ rs\isactrlsub b{\isacharparenright}{\kern0pt}}}}\\
   \isa{\mbox{}\inferrule{\mbox{}}{\mbox{AALTs\ {\isacharparenleft}{\kern0pt}bs\ {\isacharat}{\kern0pt}\ bs\isactrlsub {\isadigit{1}}{\isacharparenright}{\kern0pt}\ rs\ {\isasymleadsto}\ AALTs\ bs\ {\isacharparenleft}{\kern0pt}map\ {\isacharparenleft}{\kern0pt}fuse\ bs\isactrlsub {\isadigit{1}}{\isacharparenright}{\kern0pt}\ rs{\isacharparenright}{\kern0pt}}}}\\
   \isa{\mbox{}\inferrule{\mbox{}}{\mbox{AALTs\ bs\ {\isacharbrackleft}{\kern0pt}{\isacharbrackright}{\kern0pt}\ {\isasymleadsto}\ AZERO}}}\\
   \isa{\mbox{}\inferrule{\mbox{}}{\mbox{AALTs\ bs\ {\isacharbrackleft}{\kern0pt}r\isactrlsub {\isadigit{1}}{\isacharbrackright}{\kern0pt}\ {\isasymleadsto}\ fuse\ bs\ r\isactrlsub {\isadigit{1}}}}}\\
@@ -225,10 +225,7 @@
   \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  \<leadsto> rule%
+This rule allows us to simplify \mbox{\isa{a\ {\isacharplus}{\kern0pt}\ b\ {\isasymcdot}\ c\ {\isacharplus}{\kern0pt}\ a\ {\isasymcdot}\ c}}%
 \end{isamarkuptext}\isamarkuptrue%
 %
 \isadelimdocument
@@ -1911,1465 +1908,1462 @@
 %:%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%:%
-%:%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
+%:%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%:%
\ No newline at end of file
diff -r 28458dec90f8 -r c892847df987 thys2/Journal/Paper.thy
--- a/thys2/Journal/Paper.thy	Tue Dec 14 16:17:45 2021 +0000
+++ b/thys2/Journal/Paper.thy	Tue Dec 14 16:32:33 2021 +0000
@@ -286,14 +286,14 @@
   \end{tabular}
 \end{center}
 
+This rule allows us to simplify \mbox{@{term "ALT (SEQ (ALT a b) c) (SEQ a c)"}}
 
-This rule allows us to simplify \mbox{@{term "ALT (SEQ (ALT a b) c) (SEQ a c)"}}
+\<close>
+
+(*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  \<leadsto> rule because only alternatives which are 
-children of another alternative can be spilled out.
-\<close>
-
-
+children of another alternative can be spilled out.*)
 section \<open>Introduction\<close>
 
 
diff -r 28458dec90f8 -r c892847df987 thys2/Journal/session_graph.pdf
Binary file thys2/Journal/session_graph.pdf has changed
diff -r 28458dec90f8 -r c892847df987 thys2/journal.pdf
Binary file thys2/journal.pdf has changed