--- a/thys2/Journal/Paper.tex Thu Nov 04 13:31:17 2021 +0000
+++ b/thys2/Journal/Paper.tex Thu Nov 04 13:52:17 2021 +0000
@@ -89,13 +89,34 @@
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}
+\isa{blexer{\isacharunderscore}{\kern0pt}simp\ r\ s\ {\isasymequiv}\ \textrm{if}\ nullable\mbox{$_b$}\ {\isacharparenleft}{\kern0pt}bders{\isacharunderscore}{\kern0pt}simp\ {\isacharparenleft}{\kern0pt}r\mbox{$^\uparrow$}{\isacharparenright}{\kern0pt}\ s{\isacharparenright}{\kern0pt}\ \textrm{then}\ decode\ {\isacharparenleft}{\kern0pt}mkeps\mbox{$_b$}\ {\isacharparenleft}{\kern0pt}bders{\isacharunderscore}{\kern0pt}simp\ {\isacharparenleft}{\kern0pt}r\mbox{$^\uparrow$}{\isacharparenright}{\kern0pt}\ s{\isacharparenright}{\kern0pt}{\isacharparenright}{\kern0pt}\ r\ \textrm{else}\ None}
+\end{lemma}
+
+The simplification function is given as follows:
+
\begin{center}
\begin{tabular}{lcl}
\isa{bsimp\ {\isacharparenleft}{\kern0pt}ASEQ\ bs\ r\isactrlsub {\isadigit{1}}\ r\isactrlsub {\isadigit{2}}{\isacharparenright}{\kern0pt}} & $\dn$ & \isa{bsimp{\isacharunderscore}{\kern0pt}ASEQ\ bs\ {\isacharparenleft}{\kern0pt}bsimp\ r\isactrlsub {\isadigit{1}}{\isacharparenright}{\kern0pt}\ {\isacharparenleft}{\kern0pt}bsimp\ r\isactrlsub {\isadigit{2}}{\isacharparenright}{\kern0pt}}\\
\isa{bsimp\ {\isacharparenleft}{\kern0pt}AALTs\ bs{\isadigit{1}}{\isachardot}{\kern0pt}{\isadigit{0}}\ rs{\isacharparenright}{\kern0pt}} & $\dn$ & \isa{bsimp{\isacharunderscore}{\kern0pt}AALTs\ bs{\isadigit{1}}{\isachardot}{\kern0pt}{\isadigit{0}}\ {\isacharparenleft}{\kern0pt}distinctBy\ {\isacharparenleft}{\kern0pt}flts\ {\isacharparenleft}{\kern0pt}map\ bsimp\ rs{\isacharparenright}{\kern0pt}{\isacharparenright}{\kern0pt}\ erase\ {\isasymemptyset}{\isacharparenright}{\kern0pt}}\\
\isa{bsimp\ AZERO} & $\dn$ & \isa{AZERO}\\
- \isa{{\isacharparenleft}{\kern0pt}r\isactrlsub {\isadigit{1}}\ {\isacharplus}{\kern0pt}\ r\isactrlsub {\isadigit{2}}{\isacharparenright}{\kern0pt}\mbox{$^\uparrow$}} & $\dn$ & \isa{AALT\ {\isacharbrackleft}{\kern0pt}{\isacharbrackright}{\kern0pt}\ {\isacharparenleft}{\kern0pt}fuse\ {\isacharbrackleft}{\kern0pt}Z{\isacharbrackright}{\kern0pt}\ {\isacharparenleft}{\kern0pt}r\isactrlsub {\isadigit{1}}\mbox{$^\uparrow$}{\isacharparenright}{\kern0pt}{\isacharparenright}{\kern0pt}\ {\isacharparenleft}{\kern0pt}fuse\ {\isacharbrackleft}{\kern0pt}S{\isacharbrackright}{\kern0pt}\ {\isacharparenleft}{\kern0pt}r\isactrlsub {\isadigit{2}}\mbox{$^\uparrow$}{\isacharparenright}{\kern0pt}{\isacharparenright}{\kern0pt}}\\
+
+\end{tabular}
+\end{center}
+
+And the two helper functions are:
+\begin{center}
+ \begin{tabular}{lcl}
+ \isa{bsimp{\isacharunderscore}{\kern0pt}AALTs\ bs\isactrlsub {\isadigit{1}}\ {\isacharbrackleft}{\kern0pt}r{\isacharbrackright}{\kern0pt}} & $\dn$ & \isa{bsimp{\isacharunderscore}{\kern0pt}ASEQ\ bs\isactrlsub {\isadigit{1}}\ {\isacharparenleft}{\kern0pt}bsimp\ r{\isacharparenright}{\kern0pt}\ {\isacharparenleft}{\kern0pt}bsimp\ r{\isadigit{2}}{\isachardot}{\kern0pt}{\isadigit{0}}{\isacharparenright}{\kern0pt}}\\
+ \isa{bsimp{\isacharunderscore}{\kern0pt}AALTs\ bs{\isadigit{1}}{\isachardot}{\kern0pt}{\isadigit{0}}\ {\isacharbrackleft}{\kern0pt}r{\isacharbrackright}{\kern0pt}} & $\dn$ & \isa{bsimp{\isacharunderscore}{\kern0pt}AALTs\ bs{\isadigit{1}}{\isachardot}{\kern0pt}{\isadigit{0}}\ {\isacharparenleft}{\kern0pt}distinctBy\ {\isacharparenleft}{\kern0pt}flts\ {\isacharparenleft}{\kern0pt}map\ bsimp\ rs{\isacharparenright}{\kern0pt}{\isacharparenright}{\kern0pt}\ erase\ {\isasymemptyset}{\isacharparenright}{\kern0pt}}\\
+ \isa{bsimp{\isacharunderscore}{\kern0pt}AALTs\ bs{\isadigit{1}}{\isachardot}{\kern0pt}{\isadigit{0}}\ {\isacharparenleft}{\kern0pt}v\mbox{$\,$}{\isacharcolon}{\kern0pt}{\isacharcolon}{\kern0pt}\mbox{$\,$}vb\mbox{$\,$}{\isacharcolon}{\kern0pt}{\isacharcolon}{\kern0pt}\mbox{$\,$}vc{\isacharparenright}{\kern0pt}} & $\dn$ & \isa{AZERO}\\
+
\end{tabular}
\end{center}
@@ -122,8 +143,7 @@
\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}map\ {\isacharparenleft}{\kern0pt}fuse\ r\isactrlsub {\isadigit{2}}{\isacharparenright}{\kern0pt}\ rs{\isacharparenright}{\kern0pt}\ {\isasymleadsto}\ AALTs\ {\isacharparenleft}{\kern0pt}bs\ {\isacharat}{\kern0pt}\ r\isactrlsub {\isadigit{2}}{\isacharparenright}{\kern0pt}\ rs}}}\\
- \isa{\mbox{}\inferrule{\mbox{}}{\mbox{AALTs\ {\isacharparenleft}{\kern0pt}bs\ {\isacharat}{\kern0pt}\ r\isactrlsub {\isadigit{1}}{\isacharparenright}{\kern0pt}\ rs\ {\isasymleadsto}\ AALTs\ bs\ {\isacharparenleft}{\kern0pt}map\ {\isacharparenleft}{\kern0pt}fuse\ r\isactrlsub {\isadigit{1}}{\isacharparenright}{\kern0pt}\ rs{\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}}}}}\\
\isa{\mbox{}\inferrule{\mbox{a\isactrlsub {\isadigit{1}}\mbox{$^\downarrow$}\ {\isacharequal}{\kern0pt}\ a\isactrlsub {\isadigit{2}}\mbox{$^\downarrow$}}}{\mbox{AALTs\ bs\ {\isacharparenleft}{\kern0pt}rs\isactrlsub a\ {\isacharat}{\kern0pt}\ {\isacharbrackleft}{\kern0pt}a\isactrlsub {\isadigit{1}}{\isacharbrackright}{\kern0pt}\ {\isacharat}{\kern0pt}\ rs\isactrlsub b\ {\isacharat}{\kern0pt}\ {\isacharbrackleft}{\kern0pt}a\isactrlsub {\isadigit{2}}{\isacharbrackright}{\kern0pt}\ {\isacharat}{\kern0pt}\ rs\isactrlsub c{\isacharparenright}{\kern0pt}\ {\isasymleadsto}\ AALTs\ bs\ {\isacharparenleft}{\kern0pt}rs\isactrlsub a\ {\isacharat}{\kern0pt}\ {\isacharbrackleft}{\kern0pt}a\isactrlsub {\isadigit{1}}{\isacharbrackright}{\kern0pt}\ {\isacharat}{\kern0pt}\ rs\isactrlsub b\ {\isacharat}{\kern0pt}\ rs\isactrlsub c{\isacharparenright}{\kern0pt}}}}\\
@@ -168,8 +188,10 @@
And that yields the correctness result:
\begin{lemma}
-\isa{blexer{\isacharunderscore}{\kern0pt}simp\ r\ s\ {\isacharequal}{\kern0pt}\ lexer\ r\ s}
-\end{lemma}%
+\isa{lexer\ r\ s\ {\isacharequal}{\kern0pt}\ blexer{\isacharunderscore}{\kern0pt}simp\ r\ s}
+\end{lemma}
+
+The nice thing about the aove%
\end{isamarkuptext}\isamarkuptrue%
%
\isadelimdocument
@@ -1813,33 +1835,33 @@
%:%170=244%:%
%:%171=245%:%
%:%172=246%:%
-%:%181=251%:%
-%:%193=257%:%
-%:%194=258%:%
-%:%195=259%:%
-%:%196=260%:%
-%:%196=261%:%
-%:%197=262%:%
-%:%198=263%:%
-%:%199=264%:%
-%:%200=265%:%
-%:%201=266%:%
-%:%202=267%:%
-%:%203=268%:%
-%:%204=269%:%
-%:%205=270%:%
-%:%206=271%:%
-%:%207=272%:%
-%:%208=273%:%
-%:%209=274%:%
-%:%210=275%:%
-%:%211=276%:%
-%:%212=277%:%
-%:%213=278%:%
-%:%214=279%:%
-%:%215=280%:%
-%:%216=281%:%
-%:%217=282%:%
+%:%173=247%:%
+%:%174=248%:%
+%:%175=249%:%
+%:%176=250%:%
+%:%177=251%:%
+%:%178=252%:%
+%:%179=253%:%
+%:%180=254%:%
+%:%181=255%:%
+%:%182=256%:%
+%:%183=257%:%
+%:%184=258%:%
+%:%185=259%:%
+%:%186=260%:%
+%:%187=261%:%
+%:%188=262%:%
+%:%189=263%:%
+%:%190=264%:%
+%:%191=265%:%
+%:%192=266%:%
+%:%193=267%:%
+%:%194=268%:%
+%:%203=273%:%
+%:%215=279%:%
+%:%216=280%:%
+%:%217=281%:%
+%:%218=282%:%
%:%218=283%:%
%:%219=284%:%
%:%220=285%:%
@@ -1883,28 +1905,28 @@
%:%258=323%:%
%:%259=324%:%
%:%260=325%:%
-%:%260=326%:%
-%:%261=327%:%
-%:%262=328%:%
-%:%263=329%:%
-%:%264=330%:%
-%:%265=331%:%
-%:%266=332%:%
-%:%267=333%:%
-%:%268=334%:%
-%:%269=335%:%
-%:%270=336%:%
-%:%271=337%:%
-%:%272=338%:%
-%:%273=339%:%
-%:%274=340%:%
-%:%275=341%:%
-%:%276=342%:%
-%:%277=343%:%
-%:%278=344%:%
-%:%279=345%:%
-%:%280=346%:%
-%:%281=347%:%
+%:%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%:%
@@ -1989,31 +2011,31 @@
%:%363=429%:%
%:%364=430%:%
%:%365=431%:%
-%:%374=438%:%
-%:%386=440%:%
-%:%387=441%:%
-%:%387=442%:%
-%:%388=443%:%
-%:%389=444%:%
-%:%390=445%:%
-%:%391=446%:%
-%:%392=447%:%
-%:%393=448%:%
-%:%394=449%:%
-%:%395=450%:%
-%:%396=451%:%
-%:%397=452%:%
-%:%398=453%:%
-%:%399=454%:%
-%:%400=455%:%
-%:%401=456%:%
-%:%402=457%:%
-%:%403=458%:%
-%:%404=459%:%
-%:%405=460%:%
-%:%406=461%:%
-%:%407=462%:%
-%:%408=463%:%
+%:%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%:%
@@ -2032,34 +2054,34 @@
%:%424=479%:%
%:%425=480%:%
%:%426=481%:%
-%:%426=482%:%
-%:%427=483%:%
-%:%428=484%:%
-%:%429=485%:%
-%:%430=486%:%
-%:%431=487%:%
-%:%431=488%:%
-%:%432=489%:%
-%:%433=490%:%
-%:%434=491%:%
-%:%435=492%:%
-%:%436=493%:%
-%:%437=494%:%
-%:%438=495%:%
-%:%439=496%:%
-%:%440=497%:%
-%:%441=498%:%
-%:%442=499%:%
-%:%443=500%:%
-%:%444=501%:%
-%:%445=502%:%
-%:%446=503%:%
-%:%447=504%:%
-%:%448=505%:%
-%:%449=506%:%
-%:%450=507%:%
-%:%451=508%:%
-%:%452=509%:%
+%:%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%:%
@@ -2128,29 +2150,29 @@
%:%518=575%:%
%:%519=576%:%
%:%520=577%:%
-%:%529=581%:%
-%:%541=585%:%
-%:%542=586%:%
-%:%543=587%:%
-%:%544=588%:%
-%:%545=589%:%
-%:%546=590%:%
-%:%547=591%:%
-%:%548=592%:%
-%:%549=593%:%
-%:%550=594%:%
-%:%551=595%:%
-%:%552=596%:%
-%:%553=597%:%
-%:%554=598%:%
-%:%555=599%:%
-%:%556=600%:%
-%:%557=601%:%
-%:%558=602%:%
-%:%559=603%:%
-%:%560=604%:%
-%:%561=605%:%
-%:%562=606%:%
+%:%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%:%
@@ -2244,33 +2266,33 @@
%:%653=697%:%
%:%654=698%:%
%:%655=699%:%
-%:%655=700%:%
-%:%656=701%:%
-%:%656=702%:%
-%:%657=703%:%
-%:%658=704%:%
-%:%658=705%:%
-%:%659=706%:%
-%:%660=707%:%
-%:%661=708%:%
-%:%662=709%:%
-%:%663=710%:%
-%:%664=711%:%
-%:%665=712%:%
-%:%666=713%:%
-%:%667=714%:%
-%:%668=715%:%
-%:%669=716%:%
-%:%670=717%:%
-%:%671=718%:%
-%:%672=719%:%
-%:%673=720%:%
-%:%674=721%:%
-%:%675=722%:%
-%:%676=723%:%
-%:%677=724%:%
-%:%678=725%:%
-%:%679=726%:%
+%:%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%:%
@@ -2306,39 +2328,39 @@
%:%712=759%:%
%:%713=760%:%
%:%714=761%:%
-%:%714=762%:%
-%:%714=763%:%
-%:%715=764%:%
-%:%716=765%:%
-%:%717=766%:%
-%:%718=767%:%
-%:%719=768%:%
-%:%720=769%:%
-%:%721=770%:%
-%:%722=771%:%
-%:%723=772%:%
-%:%723=773%:%
-%:%724=774%:%
-%:%725=775%:%
-%:%726=776%:%
-%:%727=777%:%
-%:%728=778%:%
-%:%729=779%:%
-%:%730=780%:%
-%:%731=781%:%
-%:%732=782%:%
-%:%733=783%:%
-%:%734=784%:%
-%:%735=785%:%
-%:%736=786%:%
-%:%737=787%:%
-%:%738=788%:%
-%:%739=789%:%
-%:%740=790%:%
-%:%741=791%:%
-%:%742=792%:%
-%:%743=793%:%
-%:%744=794%:%
+%:%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%:%
@@ -2353,57 +2375,57 @@
%:%756=806%:%
%:%757=807%:%
%:%758=808%:%
-%:%758=809%:%
-%:%759=810%:%
-%:%760=811%:%
-%:%761=812%:%
-%:%762=813%:%
-%:%763=814%:%
-%:%764=815%:%
-%:%765=816%:%
-%:%765=817%:%
-%:%766=818%:%
-%:%767=819%:%
-%:%768=820%:%
-%:%768=821%:%
-%:%769=822%:%
-%:%770=823%:%
-%:%771=824%:%
-%:%772=825%:%
-%:%773=826%:%
-%:%774=827%:%
-%:%775=828%:%
-%:%776=829%:%
-%:%777=830%:%
-%:%778=831%:%
-%:%779=832%:%
-%:%779=833%:%
-%:%780=834%:%
-%:%781=835%:%
-%:%782=836%:%
-%:%783=837%:%
-%:%783=838%:%
-%:%784=839%:%
-%:%785=840%:%
-%:%786=841%:%
-%:%787=842%:%
-%:%788=843%:%
-%:%789=844%:%
-%:%790=845%:%
-%:%791=846%:%
-%:%792=847%:%
-%:%793=848%:%
-%:%794=849%:%
-%:%795=850%:%
-%:%796=851%:%
-%:%797=852%:%
-%:%798=853%:%
-%:%799=854%:%
-%:%800=855%:%
-%:%801=856%:%
-%:%802=857%:%
-%:%803=858%:%
-%:%804=859%:%
+%:%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%:%
@@ -2441,28 +2463,28 @@
%:%839=894%:%
%:%840=895%:%
%:%841=896%:%
-%:%841=897%:%
-%:%842=898%:%
-%:%843=899%:%
-%:%844=900%:%
-%:%845=901%:%
-%:%846=902%:%
-%:%847=903%:%
-%:%848=904%:%
-%:%849=905%:%
-%:%850=906%:%
-%:%851=907%:%
-%:%852=908%:%
-%:%853=909%:%
-%:%854=910%:%
-%:%855=911%:%
-%:%856=912%:%
-%:%857=913%:%
-%:%858=914%:%
-%:%859=915%:%
-%:%860=916%:%
-%:%861=917%:%
-%:%862=918%:%
+%:%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%:%
@@ -2475,28 +2497,28 @@
%:%872=928%:%
%:%873=929%:%
%:%874=930%:%
-%:%874=931%:%
-%:%875=932%:%
-%:%876=933%:%
-%:%877=934%:%
-%:%878=935%:%
-%:%879=936%:%
-%:%880=937%:%
-%:%881=938%:%
-%:%882=939%:%
-%:%883=940%:%
-%:%884=941%:%
-%:%885=942%:%
-%:%886=943%:%
-%:%887=944%:%
-%:%888=945%:%
-%:%889=946%:%
-%:%890=947%:%
-%:%891=948%:%
-%:%892=949%:%
-%:%893=950%:%
-%:%894=951%:%
-%:%895=952%:%
+%:%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%:%
@@ -2506,37 +2528,37 @@
%:%902=959%:%
%:%903=960%:%
%:%904=961%:%
-%:%904=962%:%
-%:%905=963%:%
-%:%906=964%:%
-%:%907=965%:%
-%:%908=966%:%
-%:%909=967%:%
-%:%910=968%:%
-%:%911=969%:%
-%:%912=970%:%
-%:%912=971%:%
-%:%913=972%:%
-%:%914=973%:%
-%:%915=974%:%
-%:%916=975%:%
-%:%917=976%:%
-%:%918=977%:%
-%:%919=978%:%
-%:%920=979%:%
-%:%921=980%:%
-%:%922=981%:%
-%:%923=982%:%
-%:%924=983%:%
-%:%925=984%:%
-%:%926=985%:%
-%:%927=986%:%
-%:%928=987%:%
-%:%929=988%:%
-%:%930=989%:%
-%:%931=990%:%
-%:%932=991%:%
-%:%933=992%:%
+%:%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%:%
@@ -2553,35 +2575,35 @@
%:%947=1006%:%
%:%948=1007%:%
%:%949=1008%:%
-%:%949=1009%:%
-%:%949=1010%:%
-%:%950=1011%:%
-%:%950=1012%:%
-%:%950=1013%:%
-%:%951=1014%:%
-%:%952=1015%:%
-%:%952=1016%:%
-%:%953=1017%:%
-%:%954=1018%:%
-%:%955=1019%:%
-%:%956=1020%:%
-%:%957=1021%:%
-%:%958=1022%:%
-%:%959=1023%:%
-%:%960=1024%:%
-%:%961=1025%:%
-%:%962=1026%:%
-%:%963=1027%:%
-%:%964=1028%:%
-%:%965=1029%:%
-%:%966=1030%:%
-%:%967=1031%:%
-%:%968=1032%:%
-%:%969=1033%:%
-%:%970=1034%:%
-%:%971=1035%:%
-%:%972=1036%:%
-%:%973=1037%:%
+%:%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%:%
@@ -2595,34 +2617,34 @@
%:%984=1048%:%
%:%985=1049%:%
%:%986=1050%:%
-%:%986=1051%:%
-%:%987=1052%:%
-%:%988=1053%:%
-%:%989=1054%:%
-%:%989=1055%:%
-%:%989=1056%:%
-%:%989=1057%:%
-%:%990=1058%:%
-%:%991=1059%:%
-%:%992=1060%:%
-%:%993=1061%:%
-%:%994=1062%:%
-%:%995=1063%:%
-%:%996=1064%:%
-%:%997=1065%:%
-%:%998=1066%:%
-%:%999=1067%:%
-%:%1000=1068%:%
-%:%1001=1069%:%
-%:%1002=1070%:%
-%:%1003=1071%:%
-%:%1004=1072%:%
-%:%1005=1073%:%
-%:%1006=1074%:%
-%:%1007=1075%:%
-%:%1008=1076%:%
-%:%1009=1077%:%
-%:%1010=1078%:%
+%:%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%:%
@@ -2639,29 +2661,29 @@
%:%1024=1092%:%
%:%1025=1093%:%
%:%1026=1094%:%
-%:%1035=1098%:%
-%:%1047=1102%:%
-%:%1048=1103%:%
-%:%1049=1104%:%
-%:%1050=1105%:%
-%:%1051=1106%:%
-%:%1052=1107%:%
-%:%1053=1108%:%
-%:%1054=1109%:%
-%:%1055=1110%:%
-%:%1056=1111%:%
-%:%1057=1112%:%
-%:%1058=1113%:%
-%:%1059=1114%:%
-%:%1060=1115%:%
-%:%1061=1116%:%
-%:%1062=1117%:%
-%:%1063=1118%:%
-%:%1064=1119%:%
-%:%1065=1120%:%
-%:%1066=1121%:%
-%:%1067=1122%:%
-%:%1068=1123%:%
+%:%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%:%
@@ -2756,40 +2778,40 @@
%:%1160=1215%:%
%:%1161=1216%:%
%:%1162=1217%:%
-%:%1162=1218%:%
-%:%1163=1219%:%
-%:%1164=1220%:%
-%:%1165=1221%:%
-%:%1166=1222%:%
-%:%1167=1223%:%
-%:%1168=1224%:%
-%:%1169=1225%:%
-%:%1170=1226%:%
-%:%1171=1227%:%
-%:%1172=1228%:%
-%:%1173=1229%:%
-%:%1173=1230%:%
-%:%1174=1231%:%
-%:%1175=1232%:%
-%:%1176=1233%:%
-%:%1177=1234%:%
-%:%1178=1235%:%
-%:%1179=1236%:%
-%:%1180=1237%:%
-%:%1181=1238%:%
-%:%1182=1239%:%
-%:%1183=1240%:%
-%:%1184=1241%:%
-%:%1185=1242%:%
-%:%1186=1243%:%
-%:%1187=1244%:%
-%:%1188=1245%:%
-%:%1189=1246%:%
-%:%1190=1247%:%
-%:%1191=1248%:%
-%:%1192=1249%:%
-%:%1193=1250%:%
-%:%1194=1251%:%
+%:%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%:%
@@ -2823,40 +2845,40 @@
%:%1225=1282%:%
%:%1226=1283%:%
%:%1227=1284%:%
-%:%1227=1285%:%
-%:%1227=1286%:%
-%:%1228=1287%:%
-%:%1229=1288%:%
-%:%1229=1289%:%
-%:%1229=1290%:%
-%:%1229=1291%:%
-%:%1230=1292%:%
-%:%1231=1293%:%
-%:%1232=1294%:%
-%:%1233=1295%:%
-%:%1234=1296%:%
-%:%1234=1297%:%
-%:%1235=1298%:%
-%:%1236=1299%:%
-%:%1237=1300%:%
-%:%1238=1301%:%
-%:%1239=1302%:%
-%:%1240=1303%:%
-%:%1241=1304%:%
-%:%1242=1305%:%
-%:%1243=1306%:%
-%:%1244=1307%:%
-%:%1245=1308%:%
-%:%1246=1309%:%
-%:%1247=1310%:%
-%:%1248=1311%:%
-%:%1249=1312%:%
-%:%1250=1313%:%
-%:%1251=1314%:%
-%:%1252=1315%:%
-%:%1253=1316%:%
-%:%1254=1317%:%
-%:%1255=1318%:%
+%:%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%:%
@@ -2884,44 +2906,44 @@
%:%1280=1343%:%
%:%1281=1344%:%
%:%1282=1345%:%
-%:%1282=1346%:%
-%:%1283=1347%:%
-%:%1283=1348%:%
-%:%1284=1349%:%
-%:%1284=1350%:%
-%:%1285=1351%:%
-%:%1286=1352%:%
-%:%1287=1353%:%
-%:%1288=1354%:%
-%:%1289=1355%:%
-%:%1290=1356%:%
-%:%1291=1357%:%
-%:%1291=1358%:%
-%:%1292=1359%:%
-%:%1292=1360%:%
-%:%1293=1361%:%
-%:%1293=1362%:%
-%:%1294=1363%:%
-%:%1295=1364%:%
-%:%1296=1365%:%
-%:%1297=1366%:%
-%:%1298=1367%:%
-%:%1299=1368%:%
-%:%1300=1369%:%
-%:%1301=1370%:%
-%:%1302=1371%:%
-%:%1303=1372%:%
-%:%1304=1373%:%
-%:%1305=1374%:%
-%:%1306=1375%:%
-%:%1307=1376%:%
-%:%1308=1377%:%
-%:%1309=1378%:%
-%:%1310=1379%:%
-%:%1311=1380%:%
-%:%1312=1381%:%
-%:%1313=1382%:%
-%:%1314=1383%:%
+%:%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%:%
@@ -2932,83 +2954,83 @@
%:%1322=1391%:%
%:%1323=1392%:%
%:%1324=1393%:%
-%:%1324=1394%:%
-%:%1325=1395%:%
-%:%1326=1396%:%
-%:%1327=1397%:%
-%:%1328=1398%:%
-%:%1329=1399%:%
-%:%1330=1400%:%
-%:%1331=1401%:%
-%:%1331=1402%:%
-%:%1332=1403%:%
-%:%1333=1404%:%
-%:%1334=1405%:%
-%:%1334=1406%:%
-%:%1335=1407%:%
-%:%1336=1408%:%
-%:%1337=1409%:%
-%:%1337=1410%:%
-%:%1338=1411%:%
-%:%1338=1412%:%
-%:%1339=1413%:%
-%:%1339=1414%:%
-%:%1340=1415%:%
-%:%1341=1416%:%
-%:%1342=1417%:%
-%:%1342=1418%:%
-%:%1343=1419%:%
-%:%1343=1420%:%
-%:%1344=1421%:%
-%:%1344=1422%:%
-%:%1344=1423%:%
-%:%1344=1424%:%
-%:%1345=1425%:%
-%:%1345=1426%:%
-%:%1346=1427%:%
-%:%1347=1428%:%
-%:%1347=1430%:%
-%:%1347=1431%:%
-%:%1347=1432%:%
-%:%1347=1433%:%
-%:%1347=1434%:%
-%:%1348=1435%:%
-%:%1348=1436%:%
-%:%1349=1437%:%
-%:%1349=1438%:%
-%:%1350=1439%:%
-%:%1350=1440%:%
-%:%1351=1441%:%
-%:%1352=1442%:%
-%:%1353=1443%:%
-%:%1354=1444%:%
-%:%1354=1445%:%
-%:%1355=1446%:%
-%:%1355=1447%:%
-%:%1356=1448%:%
-%:%1357=1449%:%
-%:%1357=1450%:%
-%:%1358=1451%:%
-%:%1359=1452%:%
-%:%1360=1453%:%
-%:%1361=1454%:%
-%:%1362=1455%:%
-%:%1363=1456%:%
-%:%1364=1457%:%
-%:%1365=1458%:%
-%:%1366=1459%:%
-%:%1367=1460%:%
-%:%1368=1461%:%
-%:%1369=1462%:%
-%:%1370=1463%:%
-%:%1371=1464%:%
-%:%1372=1465%:%
-%:%1373=1466%:%
-%:%1374=1467%:%
-%:%1375=1468%:%
-%:%1376=1469%:%
-%:%1377=1470%:%
-%:%1378=1471%:%
+%:%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%:%
@@ -3039,37 +3061,37 @@
%:%1406=1499%:%
%:%1407=1500%:%
%:%1408=1501%:%
-%:%1417=1505%:%
-%:%1429=1512%:%
-%:%1430=1513%:%
-%:%1431=1514%:%
-%:%1432=1515%:%
-%:%1433=1516%:%
-%:%1434=1517%:%
-%:%1435=1518%:%
-%:%1444=1523%:%
-%:%1456=1527%:%
-%:%1457=1528%:%
-%:%1458=1529%:%
-%:%1459=1530%:%
-%:%1460=1531%:%
-%:%1461=1532%:%
-%:%1462=1533%:%
-%:%1463=1534%:%
-%:%1464=1535%:%
-%:%1465=1536%:%
-%:%1466=1537%:%
-%:%1467=1538%:%
-%:%1468=1539%:%
-%:%1469=1540%:%
-%:%1470=1541%:%
-%:%1471=1542%:%
-%:%1472=1543%:%
-%:%1473=1544%:%
-%:%1474=1545%:%
-%:%1475=1546%:%
-%:%1476=1547%:%
-%:%1477=1548%:%
+%:%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%:%
+%:%1466=1545%:%
%:%1478=1549%:%
%:%1479=1550%:%
%:%1480=1551%:%
@@ -3138,106 +3160,106 @@
%:%1543=1614%:%
%:%1544=1615%:%
%:%1545=1616%:%
-%:%1545=1732%:%
-%:%1546=1733%:%
-%:%1547=1734%:%
-%:%1548=1735%:%
-%:%1549=1736%:%
-%:%1549=1897%:%
-%:%1550=1898%:%
-%:%1551=1899%:%
-%:%1552=1900%:%
-%:%1553=1901%:%
-%:%1554=1902%:%
-%:%1555=1903%:%
-%:%1556=1904%:%
-%:%1557=1905%:%
-%:%1558=1906%:%
-%:%1559=1907%:%
-%:%1560=1908%:%
-%:%1561=1909%:%
-%:%1562=1910%:%
-%:%1563=1911%:%
-%:%1564=1912%:%
-%:%1565=1913%:%
-%:%1566=1914%:%
-%:%1567=1915%:%
-%:%1568=1916%:%
-%:%1568=1917%:%
-%:%1569=1918%:%
-%:%1569=1919%:%
-%:%1569=1920%:%
-%:%1570=1921%:%
-%:%1570=1922%:%
-%:%1571=1923%:%
-%:%1572=1924%:%
-%:%1573=1925%:%
-%:%1574=1926%:%
-%:%1575=1927%:%
-%:%1576=1928%:%
-%:%1577=1929%:%
-%:%1578=1930%:%
-%:%1579=1931%:%
-%:%1580=1932%:%
-%:%1581=1933%:%
-%:%1582=1934%:%
-%:%1583=1935%:%
-%:%1584=1936%:%
-%:%1585=1937%:%
-%:%1586=1938%:%
-%:%1587=1939%:%
-%:%1587=1940%:%
-%:%1588=1941%:%
-%:%1589=1942%:%
-%:%1590=1943%:%
-%:%1590=1944%:%
-%:%1590=1945%:%
-%:%1591=1946%:%
-%:%1592=1947%:%
-%:%1593=1948%:%
-%:%1593=1949%:%
-%:%1594=1950%:%
-%:%1594=1951%:%
-%:%1595=1952%:%
-%:%1596=1953%:%
-%:%1597=1954%:%
-%:%1598=1955%:%
-%:%1599=1956%:%
-%:%1600=1957%:%
-%:%1601=1958%:%
-%:%1602=1959%:%
-%:%1603=1960%:%
-%:%1604=1961%:%
-%:%1605=1962%:%
-%:%1606=1963%:%
-%:%1607=1964%:%
-%:%1608=1965%:%
-%:%1609=1966%:%
-%:%1610=1967%:%
-%:%1611=1968%:%
-%:%1620=1973%:%
-%:%1632=1977%:%
-%:%1633=1978%:%
-%:%1634=1979%:%
-%:%1635=1980%:%
-%:%1636=1981%:%
-%:%1637=1982%:%
-%:%1638=1983%:%
-%:%1639=1984%:%
-%:%1640=1985%:%
-%:%1641=1986%:%
-%:%1642=1987%:%
-%:%1643=1988%:%
-%:%1644=1989%:%
-%:%1645=1990%:%
-%:%1646=1991%:%
-%:%1647=1992%:%
-%:%1648=1993%:%
-%:%1649=1994%:%
-%:%1650=1995%:%
-%:%1651=1996%:%
-%:%1652=1997%:%
-%:%1653=1998%:%
+%:%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%:%
@@ -3269,4 +3291,26 @@
%:%1682=2027%:%
%:%1683=2028%:%
%:%1684=2029%:%
-%:%1697=2035%:%
\ No newline at end of file
+%:%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
--- a/thys2/Journal/Paper.thy Thu Nov 04 13:31:17 2021 +0000
+++ b/thys2/Journal/Paper.thy Thu Nov 04 13:52:17 2021 +0000
@@ -166,17 +166,31 @@
%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}
+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)}\\
- @{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"]}\\
+
+\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}
@@ -203,11 +217,10 @@
@{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" "r\<^sub>2"]}\\
- @{thm[mode=Axiom] rrewrite.intros(10)[of "bs" "r\<^sub>1"]}\\
- @{thm[mode=Axiom] rrewrite.intros(11)[of "bs" ]}\\
- @{thm[mode=Axiom] rrewrite.intros(12)[of "bs" "r\<^sub>1"]}\\
- @{thm[mode=Rule] rrewrite.intros(13)[of "a\<^sub>1" "a\<^sub>2" "bs" "rs\<^sub>a" "rs\<^sub>b" "rs\<^sub>c"]}\\
+ @{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}
@@ -252,8 +265,10 @@
@{thm blexersimp_correctness}
\end{lemma}
+The nice thing about the aove
+\<close>
-\<close>
+
section \<open>Introduction\<close>
Binary file thys2/Journal/session_graph.pdf has changed
Binary file thys2/journal.pdf has changed