From 4184d53bcedd1b09aebdc5f1525546366b39a565 Mon Sep 17 00:00:00 2001 From: Claude Marche Date: Wed, 22 Jul 2015 12:00:20 +0200 Subject: [PATCH] Prover example: some other proofs were missing.... --- .../in_progress/prover/Choice/why3session.xml | 21 +- .../in_progress/prover/Choice/why3shapes.gz | Bin 0 -> 20 bytes .../why3session.xml | 1272 +---- .../why3shapes.gz | Bin 0 -> 5417 bytes .../Firstorder_formula_spec/why3session.xml | 854 ++- .../Firstorder_formula_spec/why3shapes.gz | Bin 0 -> 27371 bytes .../prover/Firstorder_semantics.mlw | 723 ++- .../Firstorder_semantics/why3session.xml | 5063 ++--------------- .../prover/Firstorder_semantics/why3shapes.gz | Bin 0 -> 11628 bytes .../Firstorder_symbol_spec/why3session.xml | 124 +- .../Firstorder_symbol_spec/why3shapes.gz | Bin 0 -> 1832 bytes .../Firstorder_tableau_spec/why3session.xml | 1344 +---- .../Firstorder_tableau_spec/why3shapes.gz | Bin 0 -> 5257 bytes .../Firstorder_term_spec/why3session.xml | 3666 ++---------- .../prover/Firstorder_term_spec/why3shapes.gz | Bin 0 -> 11860 bytes .../prover/Functions/why3session.xml | 166 +- .../prover/Functions/why3shapes.gz | Bin 0 -> 347 bytes examples/in_progress/prover/Makefile | 2 +- .../prover/OptionFuncs/why3session.xml | 291 +- .../prover/OptionFuncs/why3shapes.gz | Bin 0 -> 557 bytes .../prover/Predicates/why3session.xml | 116 +- .../prover/Predicates/why3shapes.gz | Bin 0 -> 267 bytes .../in_progress/prover/Sum/why3session.xml | 21 +- examples/in_progress/prover/Sum/why3shapes.gz | Bin 0 -> 20 bytes 24 files changed, 2317 insertions(+), 11346 deletions(-) create mode 100644 examples/in_progress/prover/Choice/why3shapes.gz create mode 100644 examples/in_progress/prover/Firstorder_formula_list_spec/why3shapes.gz create mode 100644 examples/in_progress/prover/Firstorder_formula_spec/why3shapes.gz create mode 100644 examples/in_progress/prover/Firstorder_semantics/why3shapes.gz create mode 100644 examples/in_progress/prover/Firstorder_symbol_spec/why3shapes.gz create mode 100644 examples/in_progress/prover/Firstorder_tableau_spec/why3shapes.gz create mode 100644 examples/in_progress/prover/Firstorder_term_spec/why3shapes.gz create mode 100644 examples/in_progress/prover/Functions/why3shapes.gz create mode 100644 examples/in_progress/prover/OptionFuncs/why3shapes.gz create mode 100644 examples/in_progress/prover/Predicates/why3shapes.gz create mode 100644 examples/in_progress/prover/Sum/why3shapes.gz diff --git a/examples/in_progress/prover/Choice/why3session.xml b/examples/in_progress/prover/Choice/why3session.xml index 9980027b0..523181155 100644 --- a/examples/in_progress/prover/Choice/why3session.xml +++ b/examples/in_progress/prover/Choice/why3session.xml @@ -1,16 +1,9 @@ - - - - - - + + + + + + diff --git a/examples/in_progress/prover/Choice/why3shapes.gz b/examples/in_progress/prover/Choice/why3shapes.gz new file mode 100644 index 0000000000000000000000000000000000000000..0239669d57f6148035ad2dc4a6d54ae7db678e85 GIT binary patch literal 20 Scmb2|=3oGW|I82?NCE&DbOE&h literal 0 HcmV?d00001 diff --git a/examples/in_progress/prover/Firstorder_formula_list_spec/why3session.xml b/examples/in_progress/prover/Firstorder_formula_list_spec/why3session.xml index f2df608e3..898f09b12 100644 --- a/examples/in_progress/prover/Firstorder_formula_list_spec/why3session.xml +++ b/examples/in_progress/prover/Firstorder_formula_list_spec/why3session.xml @@ -1,1114 +1,162 @@ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/examples/in_progress/prover/Firstorder_formula_list_spec/why3shapes.gz b/examples/in_progress/prover/Firstorder_formula_list_spec/why3shapes.gz new file mode 100644 index 0000000000000000000000000000000000000000..81fdb05a5aa0e872ba7844123110838d5bc863ac GIT binary patch literal 5417 zcmZXVRa6{|l7w-Wpo0W=cY?e7puyb+cMSw5gS)#s1b0aY7HkF&PH=aJ{qMc|aL;Z( z)MKCOQ{Snkh(Uq*_q?AP8@jA^BnM45j6U}z4huInFG+GD!65{E{c@lewrw3B@-x3x zbTI$*R@v*%nsyAnGTU+!o;h6Xd@^|0!dTqouS!d(ETReN0-`hiychyoY1$miz1#hv zWl#6}gX?wh)>A`wRL)4w`PP%e!`-CGNcYY8+n){7)7!SnQwdQo>L)`Bf?K(?Su)X^ zJLuZ!59f9oJ&Kmo4l{^PHvCq&{K92r_#Ca~^5q5V!LzGF|Jv%C-|1N&+21cd!ffXo zCvSN;0ciz3R`NcLmck}q2G%J^un!fzyT0Cxn<1Ds?@j~Sm<*l9{c{-DSg`tQ880Lf z$_XlFaxOW9f#*NeRInEmVV&?*d`v#b>u8Fe)}AAvrt(l4SBxsax&(H7>G6A6v|h>h zb(J-6nLsvpsQ$Q?jzr5t(T^C%6%HW&LB`f76}3|o>Yj{u2!9`sYu}qZ725tGdd~>! z7mbnl8_%kV_{*B8$kZi96u>6O_OewlXsdPQHBdhWxk6%WN;~_b0HV?r|Kx;U1jqCX zd8YrvV*A;d!_j3kTHc!axp?HWi=s1)bUk^M@LePgW(DQ2 zm%C3{oUy2@=#(v9Is@dh9ymH5;A;ul3=)yAThieZ=qquQ*Lo?|$zi!pF$qVLpT^$^ z+wE1#WX-%-hw2Pj>2J~w|Nh={AHH6!5Q$afK_6jRlB=o2sl<4yz-v%#$K)mysFLUJ z>C+x`j<{azM&=M-gFUDyHxM0g4rt}%nG#l8m(fe#|QVsnC# zh-ME{rrz4#{QEm&-g$?2kMeugCKD-ac<@?Ol;>t4ypTg_zDp4AJgAoyXPi0iW%OqI$ zCu-!me=SJpVDB!VBluuqAgnshlS(XZZBkXld-LM`UBz7StozM1@Ub&4=Z_}kQ%`DW z$B>vZD2(IDY=y`g_?FcspH)9(BB_GLL9au|3zqT+(^wg8i)YQ}-%gl{+WTyTSi7$> zm{p-r$FJB4!_pIxQ7Qc(KwXVKu*yj81;@4gE~YdMp(slAd;yYB$1@}aF1Z^Pq8Jvc zx4*NY;+hlGMJjU$c1ZfH`c}2#47E>me4JOxpMeN=8(JC9D=W zC9jH_lIO+OHPbuwXMv>GtsXDJp>jXjfOqMTW)9*YeE3m$F4Y)6)tHRyDJS~!XO9b@ z6LS^dk%Z9yRx+C09IB`uVz*hP;U+>*!>&{Fo5d7!sWW+@m=}`BjT|Jr;wfiDV%oasx zFolL!h5o#3hA=5#&K|4X3#ZW1g@J(tMuG^zgQrKnFgD$X^X5M?T0;*-H!T8_X_-(#pOMhZ36e%Sn|jCi7Q zDP{573}j-1drI?1pwg9haPYYvCO|ff&All-%LK_N{mY1!qHQR`L>dAalUMHNJY4JH zET4RVF;BX8yYi1bCzupbDSD4P6b!F*)#q46J@PMm36ELu_q$2GHsrou&JiL!{KOVVpe6ylu-m{*Eo8DBVCsN8sP?CyDjDR)Cw;>gg-pqFN zyg1{HepSJBR%9>}^ROgw71{71Hl18d5fZ)cU%=Z`V|2ni-x|}T3k97DX8d5ZO|NuN zm+B|}hzn4rfKR7F1Y$SBENf(*EEeryN7sS7|8pJErB$M!V<6nUva`e2nFlMZjR0_GJLxbVVnX5!Jw_-4aPmQqccrwF8kM~Z( zbNv;G(!(?4*@H)Ahl;eNUeNobEHt+eJ^)nlSfH*w`D_Xv*>hA_uBX3oD#+N$auN|4 zO_e`<2%>=>O2tyANWRg69{X7>UkQ0eY8a$FEPrSNPmd#2ps!y3EbJ%cgIKb0k7aFp zjT+TT(aD>zckv7ZeVHgTT9WcQ>?q8y_Gw*hr9W^P)KF?{xa~^=N@r9^#YPGi2RM02 zW^U3`Zr{<^UokzFe~Gj6$@6yCRgeaWj?k}Qe){;FoHXR`oolvU=Mc;=u6=bzd>1=Y zs(8PCQJeAXlS^x|KIpM42>(Nf*h;?AT>}5!ME*=wdnV5%`U}+LqGc8*K4;{cHyCd> zjFMHRD0WstGs~i-!pQz5-E@1}7>WrbVLOYNU!y|B ziaf*&hA=9U71o)C6*TZ$4(vFEV&i%Jj)_;hf!mWVPC*XWhJa@_2kjeOX6Znf!)Wc$ zlu=dYNtNGIv!d=eZ~Nyt=XVYrURzJ>CVt=uOB(#3mAYJU*4Y^6s{Gt% zfnZ$|)sOtNSJ$;j{W;LmceBaLu^vP|#s+IF7Vha=_T@4A$z(-9^kZt!1a!W8Atq=a zAO|`WeDV7PLzK4Ua?mxNfWv&+hn$YcIB<@H*hW)kz78vHBGENa&0czuS&ZN&gD|E) z(gNtiYl6-)om<92kmU@3#XZp5(Y>EdTD3uVTbn8RWat zaOnA>&wd;Do|p-$%Q7eh6g@Um(M?Dka4DcHl z2Z@BBiX=}2B~l8LCD`$Z%sSD)N&$!@#o2Ql%r$Ph*1haPKwuyst#6|C_+W+|ujyKw zk(44WVcH5Thz8!hoPB&aAl|BzN!T?9?+nf1NqQ_D3f+NeX;A*&hr%xd&}=gvh07x5 zcf<*KhZ^H*Cp=`0j;};O2&U-qepzQ!->am$679!6-c|3c;z9!NE@pG_F{xxdvh|q@ z+l|XS%cVH(f4k<=J)UZ{fi9Pzz(sXq%huOfmf8JX>y~eSjg*SV?e)bx4kwr^Fek~+ zaqW5g;3LkJY3!$wswWAY@qG$wiU&L*7F-obOqL3MKEGb;`(ZxVA?(_vjytEHGT$1+N4*`6zX4+{{gTHy6+yw7q0Hp~40i)g@m{ks^>CFk zz%{A)lH9^>Cw0A-pGl%g>_5kBh2DhftS;~dMBfy%mOh>oIl_SX6OT^uE?^GfLTov8 zY0{*zVogbI^x3oXT)YKHk&U3dCe=Ythusle@tBg zOhCY8F9z5|;NIg_((aTNU_{@2DB(+{Bi>6_$%f-q#y310a?h6l`2=&qFRCuCZ)_q0VVyrq6URKV!MtM(WugPRf>;iHR9QEOt< z3O&7)uaiw>1rQS(pL7)14S?o@XWL}MF5y*^xYPlbEkE5gGR2wC_}t2f<8^a zeFZhZowIWoAdu^Pw(r^w5p^-Ux`mAWHT_Ki+JlDUgU_{lDz!tqaBR%0hH*LCglMgF#45#jrMmRMy2!>u9u~k zC6-+vV%fG$2w|)mx)U5%;{_&0kBcRDN;fsY0OwuPgfUqwbFo*DMqUCdFUk21Ll?)S zLcAPdW66^I-)zPUBlFZ8y({$5j8Hh{GYL8zh96;CoKVK7T}8v7ka3RGw!)G)AY286 z(;4xcwJBCmjp>`qT}np-%Yz8+E+qnJ*-?B}N3q&UP1z(-d#qD&{^Y+*XVB`<{L3_L zRdPmSlwvhlDtnrI9Lb8UN~jJtY@g38uA>B`IPZG9IIO77*V7=~PhN0qq_oS^iS(PT z7+XhepFsy2x2U&n_GcUlh}%cY(bh?7J8VPx$F<>Na<$ef@Kygkv$Xo7&r|6UzOSZc z#OKN7;9GO$>O{pfjCceKd*meaIwSei*>LW9Co4_C)t-S^OfeUOKEtz?UA6xs&`!K- zN}1S@nD`J#HuC~v8FfFASyWxzsGW2}n5m`Xl^RVgC$X)~B&Xf8ie$Oejv=98P++FB!@ztk*eOn5p&%0FpUOYy zTA9sS?Wa;f)&3|~{&qkk3%}3XQ4NAqwNYlyqP+b$kxo{|`7GN88T)j?=nO|inmfwg zgeDr;s<9r*{|Ua1JhX=#PDK=<^pREnM*JOyE z+V{9$&uo+jeJ!D^g~wDUjCU+A4*%*H;F*Ew&ny4vqHV021!>lXD57$53q#TH`lud$ zp~IL%^>m#n!SYy!JRcY}2YXU<7~7q?6vSDiF6YAI2DmP@Mb+!1#VuH4OMlWAAsc6$ zSInR<)(@?|nyXD*qcLmb_5<=XmE;1M^F5-FuaVLcZ|(}xK@eOsHG}FjIaUti2g(vT zz0OzA?}E>*Ug_d z9~sl-xOA5#(+URR4!1363kfwAi%rohV}F-vqh}C%#2hSc8;1n3jPjEd2&}*^>-OdK zyC3O&V_}78h!R_L)xqjzg7fDRBmW`j5H5mOn^F)`Kzsc`d(2*eVX|8cftHyV_tnGM7_CjNL%1Iq%QNV#{*tJdKm<_kaYrdP z5mhL7Xyy&Pytf>RzM$lIA=^B@wi$!jxAec#1aZ0;MlyB$f6{<#>WfLX70*qIU}ufd z4w0qztccJumIxxb`P+UihvvpLO`RS@mA+>h9nonT&6a-lBdi7|A$G3+4RiTq{%O$) zD&5?Nt`S^1x!ml$U%{Z4e~3z`V!S7h7qegT4an#H=rAE9F7df2KI}{J2=Wa`Xyc*$ zGT{N_y6pME)K%?Q&J9KB><3<)RUt*%TO|;Q3h!){;Qp6a$M2|W0S%pvAEFt=1h#tO zjKVx){SWA;uSeZdsJXd(%_7UP+KRHi=OwL9U2I6!bqM7>b45JaDBeXJd9OZ>c`7P^ zD*3dvKB)MF#8fgStk~Bngpc(mhDGav8TYAh$kdOPp^8=E4$1qUL=8Pa4pR8<|ylAcbi`&Fi587ENl=SSoT zWo99ND_v&Y#aUJY7B~K<6|GrcIf`&8Qgu;z5n^mMQtZFK!XCF}%1>l>%sVeB#e|c} zy!&%6X@!ApG1b_(WNwn*4mx42_0e#R14tgOhU}X2C;ituZ(qbmmW4erk6>W_2hA6S A^#A|> literal 0 HcmV?d00001 diff --git a/examples/in_progress/prover/Firstorder_formula_spec/why3session.xml b/examples/in_progress/prover/Firstorder_formula_spec/why3session.xml index 2a1ad9d2f..76f3ea25d 100644 --- a/examples/in_progress/prover/Firstorder_formula_spec/why3session.xml +++ b/examples/in_progress/prover/Firstorder_formula_spec/why3session.xml @@ -3,243 +3,211 @@ "http://why3.lri.fr/why3session.dtd"> - - + - - - - - + - + - + - - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - - - + + - + - - - - - - - - - - - - - + + + - + - - - - - - - - - - + + + - + - + - + - + - + - + - + - - - - - - - - - + + - + - + - + - - + - + - + - + - + - + - + - + - + - + - + - + - + @@ -294,1443 +262,1429 @@ - + - + - + - + - + - - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - - + - + - + - + - - + - + - + - + - + - + - + - - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - - + - + - + - + - + - + - + - - + - + - + - + - + - + - - + - + - + - + - + - + - + - - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + @@ -1738,23 +1692,21 @@ - + - + - + - - diff --git a/examples/in_progress/prover/Firstorder_formula_spec/why3shapes.gz b/examples/in_progress/prover/Firstorder_formula_spec/why3shapes.gz new file mode 100644 index 0000000000000000000000000000000000000000..5ca03bcd351ae511278fb725de918d015c6f1bbe GIT binary patch literal 27371 zcmV)GK)$~piwFP!00000|Lnb4k0UvfC;r}_qTcs~cF;%y|5 zo&>5YYcsPOv-|0nE=5Q#$q%}Y2t|ZX^>mlQ-FX;)X0(gOfFxuBi(ywhc!<`<`j2)# zvkmU2&8MHr*Ka?4|MGwHuYZ31{^iG)f8}3)%fJ8be=T3@f4=?x&)@tf|K*SJ<-dOV z?|%E<;lV~l_4DXMi0ZFT5C1>^hyU^GkFURe`Qyj-U(ep1d*RU3zeP3svj6<`oB!>% z&1D0}1p~($5BzWc_2v7I?-vf77Yv+lJMi&A(SkwIjj8$9KhowxTFQc9%S+KxFBp`* zF)jc8?NU;j1*0}M9`(O}{V_Re|M`D?`)8hhB3m6bQ{?D6;i z^LzOE+s4+W|L0%-{ByI}sLy|q=){Rei>72DjYdbw%Gn6YdCJd{`dj|P|NiBVfBYK1 z{=O5~U;h{t*#G9YulI+0{+Er~zy>!|CBncn|83V%t}oHy2X6T1MV;vSy{VnZ(6fU@p z7vMxMfaBea)2n{9kYEdk3{yjfi-rtKhkUd_KGJ&f6mj?>;_#ifLJs65387Nn+H|IceM$L` zA76g_pCu|-CG+!V`+u2~Hq|;l{{SX(w)4u!@-g$k2NN>r zmODy^>a)ISyzk{(!^~E{oLVyQ!Gyvtx1^RH=v&{=SeV&JmlMkjd|<{0Y;L@}4G(y3 zryBceX4h$_PR~pp_{2@_13giwjwHIRw$4GM$LNbeq{4y38q91d+pNfwAVzm2((|uB z{xkpa>-T?#?>`zX?A^PKTkh%0Z98s57oCD-JA?VWizD@_x9Qq@S=Uda+YRJtQ4Z4W zbw`%@8!s?)PxRP3_H(THz9ej>oh`UyP^$ldfp6;b zqt1?4l;93h!`u z&=Q95)4%+;FaD1oKcyVMWxrq0H=zdaDSU9-=+B@3Vwi)|#i7nNCMcn>6ek*7Fdmcn zsgm|b{Q5`Q+A|L(_%5?vUX9kSXfUX(x5atPK59>#B7q|#$)|UNuP2San{(2dy+Npa zBsxL0rwK4d?HH|yUh#EHT9>HN1ub2UmU5m0DI^{0KhEoNUwqwsCwOu_>Wy@)lXGUU zNx&;+LzQRPfk~B@Qplj&r?%Lg_)4ntPN%b*0ps)tdq<|Jx%)bhv#d=JfXGoI;~b2b5DfrmjObk+Ni~XoaXG3bw(&UXVNNS z-a7!WcoA=MRcCU>s5L2TO6igs2?XDqgz20aoqkq`Yz#IOO4)(UNwQZ^1**2ba4rvx z>>X4V>B89Q!uKSo6H3V%AB_vqB+aUVBm`#dtrf_xM$qRF>F2-b7<9F*MQNXscfqMr zlCU*a86@zpI>fD4>hoVJS5eM&+oNo&@U`fxY8PX6**di9^~Tuh#o9?-*X637yReSL zuIqO+>l?bte`WgVM#qt6J?OnMU7+viwYl;27jx^z+6mB7iYSxBCr2VGX)&P+9G0r1 zmB@B~dS~0}Hgf&c&!x%X=c_xp@B@?DVql2a+g7I12G7OO)@G*>Nj1>79qW7B%1wja zgHvDV5E#giT9TUnP;2F$V&F6u1t01j$NGP2=%(TEyRX=Ma{NQBSQj_%V&=o$0}uB< z%3`~Q?jKN}Te6`wT1FSz1=C09Lc^nyQM%|Ey4)zzehFP>v;Q9ou&8$7_u=kwxc~aa z*Z^pHVQv+hzdvBzE-pU;*kRd=qq29`(EWq<7XfzWc*A4iRqrDCBX}KFVd@uS1CSZK zzK|9(xGpnCEAG86vnMX@KY+P|7_R}%gRwPWPNCan3mgyOIAdVQXc-k8yQc0S1cwiS zoTL);^9|0E2YPne(44xHmZX~!4ths14haX$#&H(}&ejx%Ns|E=igp?;Y4`G;u3IX$ zBSCNh8;Z?7LgK=pB4lq9s8YOBW;BBI7@YA^Hs`CYjwxEu#^9g?a^31U?}#j+7~@lU zH;C+o&4Y4EMI_~P0%wg@LD)HOgp7{}D~(g zro2&=dlh4^fu(}VMeW6Q*wGP+5>7cKqbzz8^P7`m&$$FtID)OFPXUvyXcF=|ghHl@ zGAv_3@CRoS-DPYn0oSM>QSJw>{SuH?n6h@o3ppD~MU`~^0%HV=b&t0Mhdhr&)o8Xt zb?6E_E9**8x%2AiQbp`oZqF-^{V4&&Y6mWh%H%Uv&{K|{i!m;6ur`h5(L4tBC%u)@ zWrd8nDu;IoH#P$MvVO|roRMB$$yu7nw3o8m6#!cjOJI;Ydx<5Gs)m;=M)nD;(bl2o ziV-p;GjcpmEV-}_!ZHl?yUKkK9X}XB(R}B63!ss-x53WcKAZBib9?j3gm?4F47$6o zKe#eqi{Y_WziNzKz60&DRED0941u?G00#&0+}cE_^o2smuZo1(st^x`1bNCL7(2@@ z!$ask8biW!YZFL#MT7W7Qqs@qsJAr}+-PBr5vkjKWXCw}skK{H1$;z0&sD&9ERO0D z6L>>(diebCe0T`mM`IlI+}cFC!-wN2)Loz&-3Dz}{bAtw2%YOkV;uF|+GD1byjZo5 z$6_d|3tf$uYNk|`e?VWQv4yT5jj629txXgZd>;!vU2x?73q4ng5fo&^~G1 zGi=ywST?LTJZR!G3=gFH?35k$@OWzP5pg zP}NbB29=P4W?p&b9q>$Vy$gcND){7d_g^vEggNh0O)2Ajt9d=J=5Umhk`SFMB0geJ z(R<{m15lu7gmPYx@A={EYQ4)p7%84G%=cIe&dT5dyXU3%{R%<+LwJJV=7=p%_(E{mCgv zexqvTgV^XVznmrI?y#21SqebzY7#|Es!JX=Iw<{s%X!G?beVPCkW4gCcP5lvFl0~` zfn2hsxwzO15B@2olWnNx7@;>=TTdlB!@knpYSd~xm-aC@X(pxf`P!U*k;Q&i=kO@- zJX>qOyY5R6T6( zZoUC`zGd7zhAE7rczd)sai?|!M1ABFR@3C%peyL_LZ_qSA#cuThKc)Xo|Kj;DTZYSJCuom+D4D7)sQl zlCjl5A+k1WsB4^1=b%;V)g&)X)7}igeJMGghp#k>v7r)9 zlZm-hXpswSgR8$nz7LoV?y@TPov{+p)+I#2?q8GjECp4^ws-6P$>CLivX#=6gtDe6 zl)}Nd;-QGw99l0|xL!eB#7*N0>hXn#aJ=SQRdvTibzco2CM$7~s)Cvl5GrKg&zZ zjwfb!OE1N_*X1Q{S{9iNrGCymYEXm0AjIQGW8 z1c}{X6YhrB2b_3iE}hh=XXf&DPP{X>qw*nSGfT%)NaEYEQtZ9Wh|c0 z$sb%gJr_M zgFWAZU=rhS^;n*F=s}8_CZd>Oine|%mr_((D0;s6-G!pPu{>)9Uj|7Es);OJ?TaCz zwtwy}C9CTq!%M{QT?o1z#Sj6YjQ}u0zvj>FrS!AY^gGuS?n1xqD0ZsT2oSlA5Vaxaqu-hd+k}7?#6QwMmkD#Hwsu? z|05}Tj>UATt^tCuDjtI*H>QYB=-$^T-hUgSZresu_mPYFc7|=Ap8U6X?#Mpo---9G zTc((TCk~!9Wap7E`RJGcz-zI_EVP%Nnc~P``c$gK_#>Y!0993Cw*dRkhR1I!rT*jV z?|HK^=gX*{s_V_RVxBFinfGMaY?<;bEjFHh+094&vRB<_$My6@t4%dd^r}-dQN25R z@I-dNbGmnS!c#rF`KIvMD42T@Mila8w>!Qh^%(f=vhUl(z~DS) zyaNLl4c>{M!@3?FbiFw`3@UrezPFdtamGsk7r6;89>|zoMq3rOi5xUS&i3ySFD56> zSh;wSm3#3(25qxJ>Nf5sIIl!$+Y%W3UPG{Dr30-$l zfFjTi0+$esRwPkum%lP=+MKJ&0~FS63p8xp(B8P2`FwBPTuP6ZFmEnjtKuApwq&pv zPdWJl3Wz}&ovmdVTdP06ef`t_!~Yl#0?nFSJtK2;a4m*gi+MNGSI;_V>Tyw;!kj4k z{G5dGcIc%S(rZz|!5qEzX&rBeUZ%OPMQH;wl)8G@(md=%`7Lt`{FG7hc9z#Q_q8a2 z;@-<^n}@w9wPtR4cgZYoXLUifcQ)aH8MwJ%j#9e}nHQtfb1KaXcKDQY^9W!#Wa$j| z)(d3dOou&HyK@T;1r>mfx;Y9jz~PH+Aot|yUPb@>mly+!Q|x@mBF;(zSG-G*wF;yc zR9{-Gwj5G!_Zkd;{`?mV#dRsgzSwLex{{)}km>+~R;aHaY2F&s(wLPhoW_GMO1XgfN;F3?ApE6 z4sHej4^O_kt&>R%VoBCJ0Tn4CCN4lK!`X3$w}V&R+?RfUWzdSEA*kX@1|~Mw`(Z~){s*c1XFSB zf(Nh|v$n~SJ*$NOc0h6ALOl~kyG&e?AUFw(nmWEQJ|-&QgFQQs_mYG;sEoU_gH@hV zNl9Cul@G~QT|X+cTnC$shO@hOUuUdO2Mz0xOccr0){SBddjhHu%oT`PGd|?b+-~>H ziK4#Qrw6S*88!O2XY-k}XFXDHjlZW27@UgL$|9F2RGD9rw=w9t*CA`KM$d8d{r2T7 z%JQip(c=(7nO>LaX7&ry*qa_tJ8J1oZtAu_&yV?h@Z&!u`RvAxxTbAOZ|2vb+ z-1-kmzLDORbT?HaZ7%$GNziX@>}tW-Z|m9IyZGPIQqzL&Zh9`_24lwsW1lE}cfomt zXLtWwT4`R;-NdGHLH^pa%m2lwb#VH>V3&Kh|3iS{Tmz&L4G?6m%Olsn^j!5=j6{wB zL{;M>m#U{Bdj?~z1$|ey@7Z2E;+ZxD$tLG)KpjF-l8ejit5%sZJ9SoJ`azcO_G)4) z!31r_QiK(tB`uP z8*uustZ}ckNIF&3$=Kqxvy4fcPM(X>MHwVVFYNj+p%~GI>{|j=X8AI!@h$B6_`Hta>!1C4ZR?Q{p)=A#2y6DzilhD?B}#^$n7e(^tz_{-tmk6&`t+xKU7r=l<$)muhrI{Dn42<=VN4NbEO5|H-u!7njxKM(nTu&oFJY$hdulG5 z-OOk%9?a+c>GuOtXbdU1LDPa1(`O!1L(GGA`=BQzs0z|!-bXiBsiS^*TB-xxFGqvC zUQCc~0WRsIncAV5l58K$34r)qXJUf(EQivU6RgHoUvJ1YEI+vo z(n3jryy2$02n=20`+;95EV=`%RX9yJ>v3^d=CK4u9sivq#-UWpQWN?ef;3JWt z2SoO3MQ_x0!%L+C*G;|YNUo@^@%_LrRUxRG4Nv8T zypUA5o!)Sf7#QllhXt{t%r4wOdO6|*8RP`f+Xp>n7gzss#KIy&%wE4VCtFy3^OvJR zUcv09X`3?8pQ7QRDH_~9m}BGmj+v~=ILz#(4iyKP-M~4s3-y`Z$e5{6hpZb`*i<&c zg`^eO7}G>s(>1;y_@&H_-E3qc35OSFH@r5pfch+9Wr!s# zZy)ry-rD+?;|s|25Z8BKo@`O|%_H9dUBUIPX&Z8?KSf7_&Jox?nB(XAj+?9_I?VMB zYX^f|@6yTUIx~r1PEhMc~8`tEKand!uANYk_Z(KJUJCVL-E~t(6 zs$6f}9kzH-Jj(5$+NxR~F$1VUZU6R$BxlK69$ysJ(_hIcC`Z4Y=PDRx1n-fFT=hH#$o8mMc2Kl)1rf$e7GrjnQ!*D`o*L11sT{qHJ_9R&@>qXqyi_8-7;031aPfX3W`(8Wlw#UWVVs&6k19za)0o!W|}5^Os-OyNSQ09^_E zZeB1EN`U2wyss=7x)I+>Gz?cV?<0oCeSttN&cOQC5%2KuUP^ZNs4ptGyX@eE`)SZ8 zxcmI9<~JR=1?xzz5f$9z7_6@yPj}EE0<3qBW<^EkOP%(Cjfe`Cu9sm^!2=#bpd%L{ z@R*Mfx;P0>?GnADYOd=-OFe}^m4>>pykdQE+r?oTt%dLhE-|bP?dC`P5?nq%nwwbz zhlSN+{-Ew!3~b?OjYkmIdJy88c8~fTtxfm0Vw^7BSp#j1;rK~Cr*DELGBf(A3Sq#)tZ6JkvMAR7$Osz$Udhak%Wag z{q*Oz+TrLRgun4l4WH?1s!a%+Hq8d zV<}XkPA9p{w@kSGc`@q@CEO0PPIJQT9P5n6j5p8{GOnz50qeB+=FQ4Fugf|qW$f-T z69pkr)iSLmuYz+9a(7njr+@xY&4T!!KK$0z1pV^Ik8&7<-R5rg;kR4M6a0<&DP_~* zqjZ;`ugy6LEBam+eOW;@NYSBlrYj5?lcC5udM_F=hDJ+g#B0_?Am-GFHr)M z(FNAf$!fSg08E`!>r4rH_K9r$KS$`nFf|=w#Kv-!QzBDx_Rumw_V^du=Mf6%>_ypa5&=WcA#xjM8Z#AuvTsSqJIz zymR8Nx@-az63or_POYJnl>t`f5p>DMx`g1Payn>hlF@G~baEr1WUFqP zx~nO~rkqqn?`$Z^QSynkez?%dD+70KRh}!mU$rROrQ);&WxC5Id~qe(RFpDNllCg# zA~s?+vM#`AKrus>?owndNo*|IWu=1hzHZc}$XxK_X(K(kWxns&8rkKxJCAGI(aha; zG`V0$vls7ZD-b7usBD&?4S0?wJ5e?|a123QF2TWIcwb-P+8F3-2lq5Nl=n?qY;cT_Y*eyR+}xKBeC1e z9r{+>F;*SUJO}A!xI-@C4%@^XcIA#cb4P#@10@$smjwf=7|_Y67;=&BuBscji5J-0 zyR~+0ZeVjaH?Umb243-bAADknqU!&3!DbcEV#tXqNVTfa_3EMgyw@UqRk}Yg(yif? zumF${837PT1vNTLRUK#i5RTfFgH{f@n1iGkpOZ1bq6CUoHgq}bVzns_Rk`CWg0HyynUT8S1hI#Slh>%E%#5x8;%z!(4k&?;l95QrJ;KQ5-2 zLxq3}N#Y3r9^R{}@3%eaYqzJB5gwWm&_grQ%nlt9$`>wtAIU?tI_e8BJyiULn@q zF2$4!Dil&mAyfM?&&T#^U%(%&UhS1X-Zy_h60brm#%3(UQA&<=(^3!$xHCOxtGe^{(d=i%| z_zeF5o?soxn zo4B|XQqskjqI_3bpc>y%Vf~#ltS;r1fmQ~Zihg>jD!o*_g}SRVQHx}q0~8Y#P+arG z-i>K^Z|<5TzVgzAIt6BBox~6W8x%6$ zQ85bZA1FiAt2cSg5nq|}wbB<5jn~OLm&m#9egkF>q_PeHqi$9BAKRO~riicXaT$B0 z5?B(25FGi+C$UiF57FLt%o4-uOdN2tGcf`TQvyHTo9F_ z41qZ!JMGqcR8MlUUg2(x_m4vFs%C3dNr__4j;;2Fb2eH*pkxP)$n~1kH+N0y2LLh_ z>2@!Lr9>TkvBq(*nybnYeO_-tU2j4Cpqx=0>X^ve4Bl&2)$rjMMY|BCD`)J@JgX0Bh~D?*n`{@DR0+NR_DCoa8Tk>d6gzWLfbX_Z>z{w#q6&+3A(JvhxfG&k zB$%8)D`O%RHRDvYovc0{r0W};=9eLIoH`xs!ADQRM<(E7E{Bi36h7|W@Nw*;ts(*-<hQ;xOJkTD$nE0jhvmI=b??5oihK@5n`#USM3pG%kOGG)D3my% zH*m7)uyl9G)af9X@lJr=qB38h}+t!I=z zHve7fPr$)$A-OWxL)(u^K-Q#!HWD{Nxa9RHi5wycNwVCzBu)6M{tL%6gD! z<+`H43MFmDH&O{|CS8dv1 zidG6G0iE%u&8MI0CqF%Xe`x++`P=s@5%(SMTmG~_NH*nZS5E)i-$z}>%Y!d}TPSI$ zipZv<6Lmb$i8SWc9LhS@C&9%{0vDT4Zo+aRw4U6A{g^*DjAaa(`vYX>r^lY2{I>`* z=gubHyUqmVDvb~Wa{@)mMVErl6b(v9f_j8$sv7bA$G3mRA7B2JdmOZ<=z)d4luyO~ z``176%m#N+;@MwkG!C~@CgwKRT}<-x{A+NYeAWx({Nn%P>+gA^PLj~#*Wat=mHqen z@E}^ZuWroGbA8IbF}-QZcsI{ros&h&6O=Z39Lg6QoP4I%&@SY^{`RH(*iT|;Q<|US zQx7-F#A+GR=da)VZ@+CW0)6v=h92y3Fy9hv_W&nF{kHr17Pxubd*}vnnD_NOO8iJTN=gi^uf0|EkL8_sy3tWeNPTX;Vgh z1b;gOf0XTmd01CAG4tp@13#LclURN^n!_*0Mp4`3k=tjFZRj3YaGV7m<3{ei5irObG-I+3bIFdH5cKPq#_>wmR*=6rUT5cX7qQCNLVm_0nCc;zGHoBs!&Gm0+EN;ZDf3}vnSME% z!$mM*$AI&0i9Ou+Qox;VFo>CH~lbQOp;%Y-U7IVkwZL!k#vHFnzvvoNeL z=>`wQ8CrGELBZ|_t@bjsn)cbVT#8nfS+tr7UxYjwT4(3e-hX%CtLzS4m8YXm%fPFf zObvZxXz4*iOUw4bJb3L!Ut(zKo}s0W3@v?`p{03d_S?VhVkdf|r%kQHyTiekS#wLD zo*uY-FTG|Q?PJ)+X*N$D=jBYWKWpc6>Z+or7&&=ODw1;D1w6`9HgwlwZCCnR8fO0D zPRFC8kURh5(}B>7mqddUjd4$#SeW1lMRiZFDRv4`WCgI9SC?LV6+}-26TD~6?8CpkQEe)SjF5(0o zAjee2ZipEiG&`_XHE2cPWeD_EM{6@mFsP~OJ=u!4HhNWjvBj;H?+WHO17`7DwV;?; zBbzEsQDLXNx}c31ZOm%}*TM8=%P>dxF4c2?BJy%XilOLpSEbb%Usd9&6UV?h zQX~xyms+zI%>L}0@rPOfQ_YU7y{j9icG-dPiX4Slsu>b=S!Rcv<;V0AW{>h^FH4t| z+io>0R+d@}B?wRw(Z(wB5vg)5`=m{vQb;eY*gLD^sIK_I3c3#sIlD zw znXbH|c-tPgd#GLFVxp{IeQ2;IBJGR_m9F|zX3C7wvoe;@TQ(nC(_c~lK2h(uc$G62 zW;P}ylUWrn-c``6l=W(Atn9S1Q#(6Zp`=O3`b?;W(0NkPdn!QD+Y6%&>oP3O>C3@N zax4W*C3|2juB)iu-L<82StA=KWdHlO8&Dmz%M_AUNGT;1T}8gL2>^q)6zm$WzArSQTwD>WE6~Y7dg?uAH$k#vEPUyWHa2#^0A-w1WO!g5F?e$G&1b zTB|uES9LR&t%HIYtXi#%m77*>YPQ*3vaYz;U5RN>doKyIF(Sh$_+2^9tBVep#3egd?RlNFH$Et5*&4&aOTcDL{~8aA z{}x5_~k zhAJiRizKq5vMCuIhJtp$%yC0{nd$yKtCqQzqoOO`-Z9?Dbu~RxcR?h3%t<3S=QwIF zC2^q3EsWOd3V&XKyaM@pAlq0dWvRNo3NBR~JD&rnB%*wXHr`OVe^?rTP@N(wBeqgN zarPM4Bn7U!fsqGk&>O{mxIBx5(?J46cQvKIfjs2)NF)& zE^jEja3J`ccW8yp)vy7IXrtH=B$R|&17~Y0O9v9`1}pl$ci-fSzn84~nN0#-^Z(slP|L~nSf4=7a`L_Fg7oWO;J^yuhTyQ=v?3U%{ zPdyh0_)Y!ri5Yr}w-e{n9jFcd^;3Uu7;J2i?G9{JH(aPD_vRfH3I|l1C;ljjJ(nS^aq;Bu>Vr@Rylod#(_E6BxoR zafmm-AuhuqnC{Zs-mhb@K_7~E3Prdr7NN@NTc8og&# zS&0uj55U*KZonp5AuJ^#;u)OU`3_ho*JOCxi~(Ug&HuD8Grw z(Rf3Vqetkt1b=#L0~p4iuKI`W|2jsPhJMp>_VlLs>u$Psm*7vEkvX$#Tm_!MAKx5* z{UslfmW!5rLJu2QayA<|x+nQ~QMs@7$mt%$w^e(X&#oM9TXGrWJ8so;m?xI}JSps2 zk<(q?eG`czV_?5T;>Zo)C(Ga`dSg`o*D=6EdQF>C_=(&UenK1JOWANB_3hh1iVSlC$U|2lEL^vw@@ z=C`@P{5W`dVaWAsWMeNfLF||bVy8`zo-4X`zF-%(H!vLBGQ+{xjf4KLz z4rbJF=zVm8=1+&t%*OF?d%FMO80t)C4fNitJM~E`vtsP&W_SGjmq_GePJy)K?!MNd zIC3zSQCm&ns?)|-3fn`Z0iXSC`t#?%vLN=cl}f}t?xh%WeEQs%6ucad{; zA+EYRMS4HRowKK)dPwK&m`HAR&R)3Knw_DPnYw_l6#PrSx2F_h;uIc4E_R;jO6iVMvNj%!&%u>CW<>>xcE$x{Q8B`hSbPO|+CDr_ ztq?Z_&)Wts^yZ?_#V8(IBNvPCcvxKt5i*4C#Ed~zAmpkcItDb|#Q>bz;dt|aSOXRo z;b|g5GK?o`!xKLwo<@z|JL4&V4nBAts|9SUb*Z|;5*S_T5}|2Oi5gP^7On2Ga8m~; zee~-%sp4p_Jqsspfb^{OnRHDux3!-Xb!P9)3$6!Gm z6F7Hf!H}S{ULvqj=(93VnUBe3tGMbM;SQ?ps2YEfZhHfd^Qib67YEWR4$ktk9z-0B zIh*ez4sKxij-}d-ivwsA2d9?rV~B$>9=WqP=+cK>28?8)phvM(B(rlliifzM;QCz+ zj=z6<8gEs*Vl*h#>=06Q^uhURcVwMyEWzc~-gtZV#(r@zq6SFHB`gJU(5CK7RGf;* zfY54gtmeiNIAxa&DWfq(49X@aV7sI9x`0W6{Az8i*2ZdW+>--sHS48r*SUxUK$BB8 z$+N^@0%o~Kd~r249zYtb#>Q%FoJ)gJN>{BV2M$J35K#dPduxi5z*aqotnwFIc+EOk#oVob(#s z9e~+G$9Eqpp!*Cn6rHv1uIBVfoT41X7^SokS0C{`)Sn4uqY-Akd2CalJ8prZat580 ziB*M@D!fynk`&v@MUOv?ZSwTzzr-XQwXu+`crZ>OtLRlUIx%2!@7H%U&Iq6SOs$Vv z>u1ZJ+MP!l!;wOIoGiPDZMJE%J5_;nmmnLs6hSS{gOJYFBZH2iK>Dbr`%EtSOPlZg zRP>K$z>ll>eXc?p<*LzR@W)(*`bJ!ZotL}-h{JiD!>2soz1L0;nOw@@B49|UNKq9hnRE70DU(AiIU<;bqCn4! z{)~q`Gk&^4AWQ>nb6B_MgNe_hm^g*j+UBMCp#DF;{+_ob>DtFW^YRfqPfO8ltdC!R zuOc}6@3rSvVX=Wee)$F_)*O#YJ4xEFp}A>!q20<27r|>;`OjC^A6fx_4EU`caDw=5 zJEu!A4}4S5pYE#Xs0U~#Os6Mc%d&P(IW!#{TuCjvfyCL-V{7&bQXX3C^p& z(P<{l&_=v1v}F$3xPTToQ;qeoXfRPA39e1hm{{32gB2Li0y@3fE)j#b-TPs7^9Qp) z44P)F+_Rk9l(f6H#?ptDb?zL$R43pT;Fr`*@r%RvRrF<@T_Edh^P)|Z>A`Eu^t=aI zhcd7)nyygZf_>547ArK16})II9bY6>Gc=aYz!0kjGAAI;=aEcULcURQcRMoN~r zE?>xju>!@Tsxypen4Q(ec$HKCs-Cy&r&}G~joJau7vY zZWfHagFJ6;bA|XvhByQl5_YBUh(qYka0NnN6p#zLr1(~LfnI?Yf*{%3oa%&vIG~ig z3(S->7!&lm3#=@%1W#T`%%n3aQk*ec4TuFxRVgT>aJ!V8br)D6{yGrX%Imnjr`H;% z-S)a|Q#I$T6Ld{-6KlMhZqU_)r_jimhx8n`2{e^{h1 zFl(EGO=CBQH^YLfX^X&|gj_*GF;F4b)lvyDpjuGX_l{xE>!kAv$+rc`AQ)WxVP$o~th6*0t1UrtKaY@wT@m+T{?8SR1w}oqgRE;fzpb- zgygJ`V7dyo#%67t^V!?ml^6ZUo6HK>+W|JPCy}ZZC2>gt#q7wGfH5+8LRe5Xs`tN7 zsQT0Zyh(&lkl-SS&(U?42YJ)%)#fS8y}f^T;Osr91Jc}lxApxK4j4~s!MV0d!n$)1*f%d#S*mnq!61*hNY{2p|E-y38SJ)l)7qc2u-&f1m~GJ6xWI9tx+nvW#( zXVJAHe?|TX^0Ro!Ir~t$3mnOSq@q`_Cr}ujs#3OE z99lTXSi-}l&mWF;Tc<@r;p|DX|uN zE^mj+Ox~gn0!bI`5P|_6qtg|bNn7(aW!9>0t?Jgw|4sZ~jXw{p$){WxRaLVxX2ro6 z!*zoiDD$z}fU8hih0-dN?kJR80AqvlMHL5FsG5H!WjkI z>s%};y`c#`)z(5H(xq;cB(_@XiaE1%x34K(XXNBf?l!NZLT&$cb-kjSs8NSrZ&9$w ztDs5-)ZJl@j0TxhbSYY6UB$}dv+)Ytj|p7G#`-Q_$`k{+*zTrRhb8-jN(}z@DM~**cXN(k)t&Vm`ZI1}J@%R2xWV+yiiG_^^MC7WC91cH zPutadW~uvNqdy2MuTM)qs{sDv>l+nZ@iTmTf zd!j4$f_fFvRgX9Wv-hlPf2rJe3gVSIne4$t5za;K<-01OXL!Csw4?_Y;`86D z^5c6g^Hofe*=(kMTTK5M*MShT7SP^sHu4+8Qn&xKvpIj6(Z(K={SUCQlg{p>ss?Gb zmqxoVg%1{T6}h#ag~PSNTR3@j^;cBI+pXySqEM@aWyNzPR}zzF@v^CPzosv0Mgg%I zX4C2C1V_6XJjtH=TtQ{Pk{y~FlkX^$293kwDiYuBwGa*58c#jIQVc$P{%YKhmOhWZ zEVgW|@-e3gBQQ5Q^jr8kO4sVl%3(79N0bHVX2Rqh8q5A?A|ysaUtR#H?cFwA&psNa zM&o7a;c9H&h>4^AZ4su%-Ei-)({zl>bnL5&T}(q>dX0ur`T5tR%C_2J%;oUS;hvNY z%uTr8dotD(u$>Au@3v%-GWM=u$p#;t90`q6r4R=%iwfP10SaBWb#<3m$);<@I$LWh zcF7G@$jMc}%TlBTsu~|=9QT!GC8{ik0aVzJ^nhqK!u+A%BcLmPSUJaW(I$eb?p47^ z(4r=6OCDjr=+?QHJ0@@zIOTrcsllknb&0h(@p(!=ecH|hW1xzJ}9`qHbx@dmdAef4n{k=OU$f~BK|O4vEjPBmhrJ+MGk zy~03QvKVh8P_KhzpxH_3)0&=|GgP{6~Dc;zBmn6f}gA;$)9=*;_6wy1vA?0$2X_hv2?62Ky?;;jnm$ zhj=6*2zoNo_N)bxtouSpG;;_sH5_o_8)3N)_~n~@Xf^w$?D#BA2-2Eyk|6!_pMw6pTvxmA)e_}H@y96ZgY#?(Xm`6h_T`*(a@rzLIR zquU*Ux?%#bCql4XAv(=9B>SW%uFCRJ*yhE`%fHCAD!EVa8WYQOjHBXs_44U@-jJ(( zBkEx}JFuKf2)agyd`hsK7jqD0>5`Qdd~QRRD9??yu5Lu3A3y|VW)Q&2h!9rW2}4h4 ztt5VJZ{HCX;cTz{b(^3jDI+S9ZGcKRQ-*c`$e*-#}VRmA(gw)e+ z-W>R!WaOFBHXR0;(W=m;pZzI4xxxB&QDhJxQq>SrOEZi`Wd0R@6Rr-;{y$vE)ix+z zQ2pifO@`vrX{-^qGgQ}2r?`0)eY;~A{bQWyBbn33tp&@*$~7dIb_nn>)5Rocb`h`_ zeE~C2w6bYL9PSo*h#r=*+L@DzarXSJ-{rDamM*NV0W;6{=M}T9jt1NTLH?*oe>2&v z09~W*;jf2h6@Ti82sHeg>f|P zYd~8&cDq-1ZFPaw)Szou3LJ;}>K^DVU-K1O!)Zunp4|P0=z%tQj{& ziP_~?XO~T2l;?$yP&LiuTZ1Lk85R_>D3|OvAuL4m#Xe^)mAOSb6F>4*tNiim&s_4j zIZD&eRXA^2!f`Sbri2Hu$>Jf(i3!ugGnvRP4^rjVnbH+PjN&W8i)%fRssA2}h%#`B z+-~QU^)|C>97(aX+tBVx?eei1+)DMS^?jO!>)~NEB2e;Mcue0%Z2Iyp)+o|t+}(!4 zokj&maRXgTWAs~&XdDSUyG{&=5>W&GVqIh~*qBXXlBnK!eBIg-&v zBAHVzg*(N;_Z&1k_)sXHaP*x4J+v_Lk9-Qwd38KDi2vX=4CUtY7A6z zM~D*}O}1&}xoB$9-1*Jy`uKUbmJX)_+a_qYRx4)mt5!a+M(tC=ni;?FXmB07Taw*) zf5r#My5)Vsf!hDHb_oUyL^QQAjx)*ddgBH8ps8KI*TX9_zrRP&C_UmKsT?QWD*Dsm z_oTuPd;AdzT&AS9{!*`bI&qMt@ay@0PLURxn~M6VO$`U!pdgV64Bm9xZ6W&Mav}1G z)P@GL#Vfobp`e#KMwb(>7?G0EFqokQ3F{Xh>|(n6job*hT8mfky1zeh$E>88I$Kd9 zIm1j8IP2iH1%O}2*&V*B1AdYqMv+jjvF75~f>8sUOguR<1~@sA?s|j4N2BI*14l%bhq=b1o9qZaiDhfgDBTmfOKW!jYL&NclLn&Mc! z>Z9H=vjU$62pZ|P%v1m7nd#!lEexZl{O9J+A)uYt47~}jfPW# zPYHvAW3Y#&Vc#YHeq$JKI!b#9cEO_S|l--yWz(%59{awU0pWgMkwVp1|?;+ zkT}eA<^YRs30xcI0G?L0wvj|PpJ2NLwERb+`o^E)*x{04znF?-@HlYYKc3^;5!b@t z?nVcxDtWWwCsF9X@?ytgjOY={rl5J~)XC=eEouX9>NNumEyS(d$ymn9wU(`efmAoRG}h5v5Q4%wRaw?CxgD1gmPi z(6m)XL3JaWb?z~2%NSn;=6fTe$tooYm1=J+@pnaMtElmI(d(+zubC~51-bEDa!KiF zjL5?^;_X`L#NC#_-BPGfRPv2})s5hDXvWkTMb{0YQYcA7V5Ea3hv(BTCW(P$CJkHl zxd^)WzBJ(q3z3p7Yl~$dljG8gu$3FT(NYtF8#mwCNn9Fs(LZy)J27mrW!qgId9O>n ziDAeYPHLhhzHsu+1FZZYRt=ZSe?HaT<)G0Q}S=>n0U!mte8I z*=Cpushde9BHuY#;9MbIiot$`0m2!WGSDK(8c=GT%2&0#c^Ru(5+!}Y~+WD9b>zYBTJeq2pz9G;|8$C)kR zz;ALx>+tE3AW_BHgnA&v9u1c!jqIz`#$j(~M+>Fm#Zn zOdbm!{3quL`mnh@DSjSNdeOZ3ct1+aw#qjY$sGf+=d7I#x#aUji#f~? ztXnFcR|vYaJk^Qp$fylHcAXnN&Ckg_U<&6CfQL%|TvbVEw%I~y+KTqGk#}$_=)coh zey@G{K0k}}J@X{NH7ol#X3jNj#@-u|OSr5_DmY+@P@VKSpDl<}P4#_3Q} zNxW%-z@@uX(v$MVd|Y~Bz2hh(>-~1g@xA%0>9aTeeG-?g>Y}xRPJUON6w@d{G#zkW zYq7*YC*Rf%83>$TT0DlZk7m}S3$H#+uln;$b;u)jm6Ey@-Pm}m!jdx`-N@Az*TfCp zDhYJT;A^~PN4|Bz=Ja)semC-7sxy<0F?)Q&euwHL84G2D9=Ei_30lXwgF>*r%P(tV z%@#&jJ1HMV6ORh3pS8)uIrx)7O;wR z)&ar&`%0-y9@zE(Z<47Bv?2UKeMhc?l)82U*b5cd2fV_aoy$+%fP+pK8fDfyWsXe? zF1{pz7zMs|1EkvRDMkXB6RW9o2rjJKq=dI;Xt#%4tzsEh0o%xz?3g~a!@8$(nWwM|*Q)UG zyEkVt0^sVh=N5Z@tDF4A3OUkWyke&XBSOQadZNc|19%I)Skq|X7mTYN1l=*) z=T_n=A*4=C+n{49q#0p^fH84B{a9BgL}$ZPXG3o>XFcJ(XQ)Z3BpNm+)>5e|h-6EM zEXtLo={lM4Sh9`)%f)t!lWFv#CX^?hrWHgWbU#gSAnM~cIGSIj?Roq&>GDh55F>+d z7svYe=~Sj5{o~<50;ZYC8(qBC5Pmet#4&L`UzLPu(mIfX)!=c}Ct$|TeuZQQTIyDt zN_t$JHT|0M3lC}|{JaNd!^BGVtH=0A>{3pJ(9Vfc_P7U}-eo*$K)$dS`(ADWiLl@k zA7eJh@v&8ou@o`&Y6d&)N3aIS+rp#%S7s;&tsj?46FXvk&qQ4hY|4GgpIKBem$49= zbpbaR<6lWP{gB%edwcsj$g-|(9RF< ziJj}~5Q`=+i^*|klxx`mG7M+2Xo>RH6+7!$2ksY$1UzjH`~zs_naUJ#9McP!SgX_E zke06|Aa7GT-@3Bo9_0g!)R4i--(4Kvaqjsbs~0wl0)u#fX#$Lh9eiu}9xBitFYY;} zUPs^Zx=VxDHLTrz3NQREw14*InlCAAtg_F?e;kb;tWH=O?TG3Dsq;Jff{6bd z{0hM%=KNiXiL=Wc0>eF6XQhQ22{n3vP*33~SrPmdpfHo;GZA7RtkQ*#H7DFZiu=-vk9;mZ#uUR1&! z$&auS>B_=YwrG!PyBp{v^COlpT%H#j4zExDez>=SUKclFM!x)_5V?xliD=j`pZ_J` zx4wk}CG%>cv4v2pi#A5%=Dw=MxogOBZis^gSyfU}@G7m-i55;?x{mC}NS{)po-}n? zQUrok9t1$00TX*vf~$(QmNQsigJJqOo=INZoOGf{3z~#Dr4?mbenPszIM$F@i(Q6*c9#cL4r3Oi!jSG)L zVZM?{yvpmzW&u^E$hM-Y-DGOvvw~%$E{qsc6~PKe$BSL^)Ud4?3(s55to}>Dlw5L# z%=D7{nAkne(~gr`T9PnF`OkT&AJ1KStoGJm*=*%En^IZd*tXaF2{lAga5AR*>$Wjy zf?yAh)O$1(Em4PHyG--C-@x<{pi3PzN+DZDIU11u3^M8iEQ~f*>wZ+OO?~`5&?R}Q zDjaV(7Gk*{(Ru;>c!zh|^6??F%YWEIJb6Aq)puvfmWLDa{Vbm`yI~^d{(gsh=&3B3 zNJ%S zAXNVuaML?L^+`&jO#XWOKna7&DICgmGkS_FTYND~%fm)9h^-LIr{%@=D0gaP9CB}I zE895Keev2#xpRkYTe{?hbBV3-w)@+!@vT(_ECZl-l#Ey@hF+>^61D6cYeirFqtu)C zTYScB0}V!!!H*N;EP%6YV@J_57YJ72FE9!Xn`+5>p#(q%iXRaH96_ZU-f+!iah)mI(%u*JP71o&? zI$%n~7!%EjOUvgOd<7hp*5uh=a84*kF4d(Z_yn?l-PJG7w?3Hk)Ge7GKPz*#V(?sn z&e5e*uF0Q0d_M$R_BW$RtO)o6KdsZRX=Igc1wSw_=tX~*Rrw&3lTSs}++C&N;(IL=yZNsjr&UM?rFMIq*jPP6G~;3-;fLg7_>qlMUcI$}2z{ALbI4(kls#spl_} z**eC@ep}moUL~940k?cTM;G(^U--y=SCyz?JDi7bCk~1zlQ4^BT?tLhWT*~$U-I{) z3RO=3A3Sg5G@xtTjz-n0a2P3M_~Ito#jt2G0lK&ngrw%QU~e!ll{UR#O#Z$H$1sQE zpfi!{N;HI9qtE08N#p7emQsCBJLtjwz9=>GUQ|;e@4gj}W8gA*H~E+m6TA8J1M|1! zrO!#$C9y!>_pamGX#pdzqnEcU#N^x3!^QXLcWe-<;n<1#gW)n3@8;f}qRE=8o4^U3@vzFq%igBE`1)6E#5w@u;{!p~-=VByn{s z-ekHXaDL?IiavI>8lCa3sw9on!Adgf2YmaIjouWwOJl zaGCk5&E4BZP9TZ69{IY1YD>VH`TX&>+vvy3TeCd&`C8)3ahhT-WtuIWLn}T_UL~`f zA^@^VsTM6MNxvbP?l7lQwbzn`bF3=lOQZ6ff1{5rfd~My#HI&zk2s$*f{(^LrV0C+_Li(E&;1l>=L~@J527JU4#Ci$4}v zEh9-=SOsX5|BW+|KrL<DxGcv;77(Jn<afrHuOsy$`+WL&12D!&Mv<^)2c?CslLzFcECn@XW>nYzFj#^<#{L%lSae&L56wWa##I@j!= zt?c6bX?eoWq|bVn*`K%YKW6lQ?P|F>-!vv8vj71kQ=F8dV}qZlMGYDUVw1f8olJ+> zKJwyj^?UPn01oKWGJd9OBNqrjl=Y(4xOsJTPQ;N`A^GhPoENA57H{t~Y))A|v>gKn zg8H5eIwgH;cG|{`7fWwOxN}1-Eo|jm>*D;;)q8EPyWCHEW3rKN&0o5a6^o{ZVPm%} zho&G4*0s7^MZ)G6D5!dpq%}=gPy>#d6#LxdssJaMnL zfC6~`dVK$nVPaNo`$EpN+Rzytn%-y)-PTYt!KcsLZ|Q3qNtz0!nuc6d`+#a(VWO@ZXPoPdsd^!W&@s;?{qbe*VVt7I)JQG9rFA$@ znqe|uZ^pRFrki%e0DbF{rE%Lu;}e48>T;cMA4A7TCL3yhM(Dr1ikKD6vF@vsE>eSb zI8Uo#qQC@D1gcwF2&wm?q`=wB&tjeGY0ogxhth9U`5}pA#rICT2x)MqvhRkP)wih{ zXn}3%ED+A~)v5TJ8tWpQ?Sir61Y9th2Or6ieIVl-am@>X{m((k{+6Es8F*RcN#)}y zrmn-mT{_mTk(Sa%jQANmUt>dKHpPuuP0G*Jop#kS}1ypuv+;h_^?{pJKQc<3JNzromReT^@{Um=hB@bBx-Vx3c zBzyXO1S{fz1b1=}y0ls5o*bp-NGCVsoO|^Iu4!iFCq3;z+Y85Jo1DD#hPnuR9|!(Sf>Tb>CBPP0r{gsCM^H~ncx37NnbL8YSp=eaVyb>^~sq$FuETZ2`f z1e2+%rFjA)-V!oCb4ldzcZFH4r3WTzw30T`>Mj%1JF^43Ue7z8_tWZCa`tEV?fp@@ zL)qMwzO{Uf3#^e=LkmlisfhQshbj7Fm{DCo%H4DpdnJd^_nQqhArMb-*7;W1yGM*J z++9C5dN!2o+mw4tH=iV_LjtO1=JjI%+&>$sFty01ofDj0GK87F?r0bFb`9x;07U(x zEgsxIqautBs70i01>i#@RG$;U-Z9d_?VIez#sz8@BTw%vu@*gaGWwB2@5C07{y&P8 z75$GQv7r7{WC7`aDe_7LVOR3M#4$>cxyew2`dpmQ9OQl|{WSjPxkIZ!-d75G^F2_G z5+)ksT!!VJiK^%;BF#CC#x!6kXN~k;mjvDGK)z&hr52KcTIvf(iF@|eV51CvtD*@+ zgIsp?%UZDhx<&~UxuBfqm(~rF&UKvKl$IkV2IUYz9gxz(&O~%b3;oj&uyQDb{GnQY4hlXlG&WCf;L4*P~Fxw`JQ+yC%fZFL(~Bs!+4 zv$Ge=!&5Dk*iTM|GX5+TOd-kL=sDmU=fCFm?kl5o;~GSmjIU!HtN?zV1vO^MZbMdX z20!J#iXk#K&7;gps@B|R%x7xy6ep1wPm&}qSpoYz!$Lh#y3(_%H2LsPr=OFHuqWCA zVPoFTKOMP)Jl7hiB{SlB$gGi3PP=}*8(GiI!Nef6U2F)cF8%m(LLEI%%e}9oSqnYz z^mr02m0oNc#7;%KsVYLCDq3P7 zFIDzGmmI7Cz1{~xRkT&zEO&4eBo&<~fypGe*tE*I83J?vk2omSenhDFxd1Md`<4C49VO z4`VoY+v9B8<77@hW-7Pu2%%U@I%S3M=82(|a&&q}KjUk?skgkmN{PbY?(tz}X)tZp zPM~+3TwNTWqJOus*xr=~8~WSKqV&QJ(DvDjV7#~$H1+apzgPDGv8k&&2wp=Uo|>{e zgGGH@YskR#g@u4*Q|YUB_ll$Y**kY9f+FSZ)3>~bgs1;!Euy^T`FAa1C%MvkIW&oX z>X+qrAhtz~>fA3HLj%>rhXX3~ursB+(efSRQB4~K-ic9d zJ=vqY#?JJ0JZb8m5G|tvd`(2v&@aymHct8KXy>8FPK0&W>OfiYY|IRQVu5AV3PtjP z3NzEium_$@X&gw@JaS@z%!p$D44C=XV{*RSLuuHV>~s>9+kA@sfOL}1_Cx6=8mvRz zTZ*kmA(!v>LeC~65ol~SOTP73s99iCGDaD8oqTirmd9eeu~2GwhL z)o&;SJMhnE7Yvcoz%2g!6I+~i(vEs<3t;4?VUwu4`Id-!wxg}%b zZI>T749iwAIBgKsM6B%xy#Tf_YbvAKDM7uo{2`OTNTwv3SmZw6 z9wU3ofY@isHi_+$M(f8+T2a{0z6d1sC|C677i7Bts*`}H$;|}aZ5F<5BTBOXROi6h z?~%tGienU;or!8Ric!9U0{i@Vj{vo5p;f26Bl2BNTy(UhR(YWT_W>1Va?&b_Q2kFA zC;Si6{#4Vu1mC=qEpPJ5BCd5+&>NH3VEvQA(rB3jK)!Z|bT1{~>r&iX)vwb*GqvzP z!(XZ>wm6sA7Sn&FVNQn9rm@jWpj#-W!KaCDbZ>v8^4*WS7hMpN3e?e1*oMR%b8H0= zt_v3nRs63Q^+BeW+1NW=b*38RnfaFBIN!Zfd`w2zIy4v!zw%T&rc`H4ab||s7qiMf z5b9RTl5=xM0FF@wO~a4bvlfb1kp?Es^O&a}?R$zu(^r4Lf>43qHiu9x#~MRlJvI*R zIlEzXo&YzZnhuvXH*M?}@jkye9S@Y!p1WLHY7jNGrsf0cyeZ0St|8qJcxM{xY$x8A zoGI%lfHb{!yvMGCwAj_rKQjZVs;!oc$t9IPg=|hNn=O?#$03;~svyH5 zCG3W)mn;BE!4%Kdye|LScbDU>tNlzZX!W6!^3*yKQxoC;vw#{od*5NGbjj8VoE6t~ici$WQ1N}j4XV^@O zF$}dc_}l~vEv6;QX`uVSi4r$gyM&(x6osxxW7MhDF`8!=Ve=l2>Q^9o4L3-E6{{>L z_Ww0zhbZVn@ft@(YtmcX(`#{}mPXoSHMTI?M}@oG(@F3WYfQXivcu1NZzTtcW1wi*L;IQ62X-l(+hPc{U%uz! z-HAsIUz091a-s{fH=lV{-ZygkXX`+re2YBUQ}U&JUq|V=zb=+sfxCmMN3A8Wlvo&lDuZkye*Z3v znwJ}ZLI*|2S6zpYU~oOC@jKG+w^}|4cI>yw=LNPOTYsOLuJ;W3pACXoIyu+5I<~lm z>kjQm$h&SAObtrKMotaxsgLav6lCFxE%e0s!#3pm81xCqdgQmoUi>^-1=l~UJMBnO z!UC-?rw+$bW7$KCjJyeq9uT#M@{ERtZD%gMzoe|=r7kk#6P8uYmK$5h%&>u?Y3;mp z4hqdOCQ8EC`~RpqiyJnSQimN$UO}9B%nY-)>_Wa$NPmM-SSA(-iv1pX{2itV53h#f z8J5JVim0uU>cn literal 0 HcmV?d00001 diff --git a/examples/in_progress/prover/Firstorder_semantics.mlw b/examples/in_progress/prover/Firstorder_semantics.mlw index 85d356d96..dac2121b5 100644 --- a/examples/in_progress/prover/Firstorder_semantics.mlw +++ b/examples/in_progress/prover/Firstorder_semantics.mlw @@ -1,6 +1,6 @@ module Sem - + use import Choice.Choice use import Functions.Func use export HighOrd @@ -13,26 +13,26 @@ module Sem use import list.List use import option.Option use import OptionFuncs.Funcs - - type model 'ls 'st = { - interp_fun : func 'ls (func (list 'st) 'st) ; - interp_pred : func 'ls (pred (list 'st)) ; + + type model 'fsymb 'st = { + interp_fun : func 'fsymb (func (list 'st) 'st) ; + interp_pred : func 'fsymb (pred (list 'st)) ; } - - function term_semantic (t:fo_term 'ls 'b) (m:model 'ls 'st) + + function term_semantic (t:fo_term 'fsymb 'b) (m:model 'fsymb 'st) (rho:func 'b 'st) : 'st = match t with | Var_fo_term x -> rho x | App (Var_symbol f) l -> let ifun = m.interp_fun in ifun f (term_list_semantic l m rho) end - - with term_list_semantic (t:fo_term_list 'ls 'b) (m:model 'ls 'st) + + with term_list_semantic (t:fo_term_list 'fsymb 'b) (m:model 'fsymb 'st) (rho:func 'b 'st) : list 'st = match t with | FONil -> Nil | FOCons x q -> Cons (term_semantic x m rho) (term_list_semantic q m rho) end - - predicate formula_semantic (t:fo_formula 'ls 'b) (m:model 'ls 'st) + + predicate formula_semantic (t:fo_formula 'fsymb 'b) (m:model 'fsymb 'st) (rho:func 'b 'st) = match t with | Forall t -> forall x:'st. formula_semantic t m (ocase rho x) @@ -46,29 +46,29 @@ module Sem | PApp (Var_symbol p) l -> let ipred = m.interp_pred in ipred p (term_list_semantic l m rho) end - - predicate formula_list_conj_semantic (t:fo_formula_list 'ls 'b) - (m:model 'ls 'st) (rho:func 'b 'st) = match t with + + predicate formula_list_conj_semantic (t:fo_formula_list 'fsymb 'b) + (m:model 'fsymb 'st) (rho:func 'b 'st) = match t with | FOFNil -> true | FOFCons x q -> formula_semantic x m rho /\ formula_list_conj_semantic q m rho end - - predicate formula_list_disj_semantic (t:fo_formula_list 'ls 'b) - (m:model 'ls 'st) (rho:func 'b 'st) = match t with + + predicate formula_list_disj_semantic (t:fo_formula_list 'fsymb 'b) + (m:model 'fsymb 'st) (rho:func 'b 'st) = match t with | FOFNil -> false | FOFCons x q -> formula_semantic x m rho \/ formula_list_disj_semantic q m rho end - - predicate tableau_node (b:bool) (phib:fo_formula_list 'ls 'b) - (phi0:fo_formula 'ls 'b) (m:model 'ls 'st) (rho:func 'b 'st) = + + predicate tableau_node (b:bool) (phib:fo_formula_list 'fsymb 'b) + (phi0:fo_formula 'fsymb 'b) (m:model 'fsymb 'st) (rho:func 'b 'st) = ( b = True /\ formula_semantic phi0 m rho) \/ formula_list_disj_semantic phib m rho - + (* This one work by accumulation, as it is related to a context. *) - predicate tableau_semantic_with (t:tableau 'ls 'b) - (b:bool) (m:model 'ls 'st) (rho:func 'b 'st) = + predicate tableau_semantic_with (t:tableau 'fsymb 'b) + (b:bool) (m:model 'fsymb 'st) (rho:func 'b 'st) = match t with | Root -> b = True | Node tnext phi0 phib -> @@ -77,17 +77,17 @@ module Sem else False in tableau_semantic_with tnext b' m rho end - + (* Abstraction-definition axiom : - function semantic_subst (s:func 'b (fo_term 'ls 'c)) - (m:model 'ls 'st) (rho:func 'c 'st) : func 'b 'st = + function semantic_subst (s:func 'b (fo_term 'fsymb 'c)) + (m:model 'fsymb 'st) (rho:func 'c 'st) : func 'b 'st = (\ x:'b. term_semantic (s x) m rho) *) - function semantic_subst (s:func 'b (fo_term 'ls 'c)) - (m:model 'ls 'st) (rho:func 'c 'st) : func 'b 'st - axiom semantic_subst_def : forall s:func 'b (fo_term 'ls 'c), - m:model 'ls 'st, rho:func 'c 'st, x:'b. + function semantic_subst (s:func 'b (fo_term 'fsymb 'c)) + (m:model 'fsymb 'st) (rho:func 'c 'st) : func 'b 'st + axiom semantic_subst_def : forall s:func 'b (fo_term 'fsymb 'c), + m:model 'fsymb 'st, rho:func 'c 'st, x:'b. semantic_subst s m rho x = term_semantic (s x) m rho - + (*(* Abstraction-definition axiom : constant symbol_name : func (symbol 'b) 'b = (\ x:symbol 'b. match x with Var_symbol x -> x end) *) @@ -104,26 +104,26 @@ module Sem (rcompose symbol_name subst_id_symbol) } ; assert { extensionalEqual (identity:func 'b 'b) (rcompose subst_id_symbol symbol_name) }*) - + function model_rename (r:func 'b 'c) (m:model 'c 'st) : model 'b 'st = { interp_fun = rcompose r m.interp_fun ; interp_pred = rcompose r m.interp_pred ; } - + lemma model_rename_id : forall m:model 'b 'st. model_rename identity m = m - + (* semantic commutation with substitution. Required for example for universal quantification elimination deduction rule: forall x. phi -> phi[x <- t] come from this lemma (*and generally speaking, quantifier handling*) *) - - let rec lemma term_semantic_subst_commutation (t:fo_term 'ls 'b) - (m:model 'ls2 'st) (rho : func 'c 'st) - (thetal:func 'ls 'ls2) - (theta:func 'b (fo_term 'ls2 'c)) : unit + + let rec lemma term_semantic_subst_commutation (t:fo_term 'fsymb 'b) + (m:model 'fsymb2 'st) (rho : func 'c 'st) + (thetal:func 'fsymb 'fsymb2) + (theta:func 'b (fo_term 'fsymb2 'c)) : unit ensures { term_semantic ( subst_fo_term t (rcompose thetal subst_id_symbol) theta) m rho = term_semantic t (model_rename thetal m) (semantic_subst theta m rho) } @@ -141,11 +141,11 @@ module Sem assert { eval m.interp_fun (thetal f) l2 = eval m2.interp_fun f l2 } end - - with lemma term_list_semantic_subst_commutation (t:fo_term_list 'ls 'b) - (m:model 'ls2 'st) (rho : func 'c 'st) - (thetal:func 'ls 'ls2) - (theta:func 'b (fo_term 'ls2 'c)) : unit + + with lemma term_list_semantic_subst_commutation (t:fo_term_list 'fsymb 'b) + (m:model 'fsymb2 'st) (rho : func 'c 'st) + (thetal:func 'fsymb 'fsymb2) + (theta:func 'b (fo_term 'fsymb2 'c)) : unit ensures { term_list_semantic ( subst_fo_term_list t (rcompose thetal subst_id_symbol) theta) m rho = term_list_semantic t (model_rename thetal m) @@ -157,10 +157,10 @@ module Sem | FOCons x q -> term_semantic_subst_commutation x m rho thetal theta ; term_list_semantic_subst_commutation q m rho thetal theta end - - let lemma term_list_semantic_rename_commutation (t:fo_term_list 'ls 'b) - (m:model 'ls2 'st) (rho:func 'c 'st) - (thetal:func 'ls 'ls2) (theta:func 'b 'c) : unit + + let lemma term_list_semantic_rename_commutation (t:fo_term_list 'fsymb 'b) + (m:model 'fsymb2 'st) (rho:func 'c 'st) + (thetal:func 'fsymb 'fsymb2) (theta:func 'b 'c) : unit ensures { term_list_semantic ( rename_fo_term_list t thetal theta) m rho = term_list_semantic t (model_rename thetal m) @@ -169,19 +169,19 @@ module Sem let p1 = rcompose theta rho in let p2 = semantic_subst (rcompose theta subst_id_fo_term) m rho in assert { extensionalEqual p1 p2 && p1 = p2 } - - let lemma term_semantic_rename_commutation (t:fo_term 'ls 'b) - (m:model 'ls2 'st) (rho:func 'c 'st) - (thetal:func 'ls 'ls2) (theta:func 'b 'c) : unit + + let lemma term_semantic_rename_commutation (t:fo_term 'fsymb 'b) + (m:model 'fsymb2 'st) (rho:func 'c 'st) + (thetal:func 'fsymb 'fsymb2) (theta:func 'b 'c) : unit ensures { term_semantic (rename_fo_term t thetal theta) m rho = term_semantic t (model_rename thetal m) (rcompose theta rho) } = assert { extensionalEqual (rcompose theta rho) (semantic_subst (subst_of_rename_fo_term theta) m rho) } - - - let lemma semantic_lifting_commutation (theta:func 'b (fo_term 'ls 'c)) - (rho : func 'c 'st) (m:model 'ls 'st) (x:'st) : unit + + + let lemma semantic_lifting_commutation (theta:func 'b (fo_term 'fsymb 'c)) + (rho : func 'c 'st) (m:model 'fsymb 'st) (x:'st) : unit ensures { semantic_subst (olifts_fo_term theta) m (ocase rho x) = ocase (semantic_subst theta m rho) x } = @@ -195,21 +195,21 @@ module Sem | Some z -> p1 (Some z) = p2 (Some z) end && p1 x = p2 x } ; assert { extensionalEqual p1 p2 } - - let lemma formula_semantic_subst_commutation (t0:fo_formula 'ls 'b) - (m0:model 'ls2 'st) - (thetal0:func 'ls 'ls2) - (theta0:func 'b (fo_term 'ls2 'c)) + + let lemma formula_semantic_subst_commutation (t0:fo_formula 'fsymb 'b) + (m0:model 'fsymb2 'st) + (thetal0:func 'fsymb 'fsymb2) + (theta0:func 'b (fo_term 'fsymb2 'c)) (rho:func 'c 'st) : unit ensures { formula_semantic ( subst_fo_formula t0 (rcompose thetal0 subst_id_symbol) theta0) m0 rho <-> formula_semantic t0 (model_rename thetal0 m0) (semantic_subst theta0 m0 rho) } = - let rec ghost aux (t:fo_formula 'ls3 'b2) - (m:model 'ls4 'st) - (thetal:func 'ls3 'ls4) - (theta:func 'b2 (fo_term 'ls4 'c2)) : unit + let rec ghost aux (t:fo_formula 'fsymb3 'b2) + (m:model 'fsymb4 'st) + (thetal:func 'fsymb3 'fsymb4) + (theta:func 'b2 (fo_term 'fsymb4 'c2)) : unit ensures { forall rho:func 'c2 'st. formula_semantic ( subst_fo_formula t (rcompose thetal subst_id_symbol) theta) m rho @@ -257,10 +257,10 @@ module Sem formula_semantic t2 m rho) } end in aux t0 m0 thetal0 theta0 - + let lemma formula_semantic_rename_commutation - (t:fo_formula 'ls 'b) (m:model 'ls2 'st) - (thetal:func 'ls 'ls2) + (t:fo_formula 'fsymb 'b) (m:model 'fsymb2 'st) + (thetal:func 'fsymb 'fsymb2) (theta:func 'b 'c) (rho:func 'c 'st) : unit ensures { formula_semantic (rename_fo_formula t thetal theta) m rho <-> formula_semantic t (model_rename thetal m) (rcompose theta rho) } @@ -270,10 +270,10 @@ module Sem subst_fo_formula t (rcompose thetal subst_id_symbol) thetas } ; let p1 = rcompose theta rho in let p2 = semantic_subst thetas m rho in assert { extensionalEqual p1 p2 && p1 = p2 } - + let lemma formula_semantic_term_subst_commutation - (t:fo_formula 'ls 'b) (m:model 'ls 'st) - (theta:func 'b (fo_term 'ls 'c)) (rho:func 'c 'st) : unit + (t:fo_formula 'fsymb 'b) (m:model 'fsymb 'st) + (theta:func 'b (fo_term 'fsymb 'c)) (rho:func 'c 'st) : unit ensures { formula_semantic (subst_fo_formula t subst_id_symbol theta) m rho <-> formula_semantic t m (semantic_subst theta m rho) } @@ -282,19 +282,19 @@ module Sem let rho2 = semantic_subst theta m rho in assert { formula_semantic t2 m rho <-> formula_semantic t (model_rename identity m) rho2 } - + let lemma formula_semantic_term_rename_commutation - (t:fo_formula 'ls 'b) (m:model 'ls 'st) + (t:fo_formula 'fsymb 'b) (m:model 'fsymb 'st) (theta:func 'b 'c) (rho:func 'c 'st) : unit ensures { formula_semantic (rename_fo_formula t identity theta) m rho <-> formula_semantic t m (rcompose theta rho) } = () - + let rec lemma formula_list_conj_semantic_subst_commutation - (t:fo_formula_list 'ls 'b) (m:model 'ls2 'st) - (thetal:func 'ls 'ls2) - (theta:func 'b (fo_term 'ls2 'c)) (rho:func 'c 'st) : unit + (t:fo_formula_list 'fsymb 'b) (m:model 'fsymb2 'st) + (thetal:func 'fsymb 'fsymb2) + (theta:func 'b (fo_term 'fsymb2 'c)) (rho:func 'c 'st) : unit ensures { formula_list_conj_semantic ( subst_fo_formula_list t (rcompose thetal subst_id_symbol) theta) m rho <-> formula_list_conj_semantic t @@ -303,11 +303,11 @@ module Sem = match t with | FOFNil -> () | FOFCons _ q -> formula_list_conj_semantic_subst_commutation q m thetal theta rho end - + let rec lemma formula_list_disj_semantic_subst_commutation - (t:fo_formula_list 'ls 'b) (m:model 'ls2 'st) - (thetal:func 'ls 'ls2) - (theta:func 'b (fo_term 'ls2 'c)) (rho:func 'c 'st) : unit + (t:fo_formula_list 'fsymb 'b) (m:model 'fsymb2 'st) + (thetal:func 'fsymb 'fsymb2) + (theta:func 'b (fo_term 'fsymb2 'c)) (rho:func 'c 'st) : unit ensures { formula_list_disj_semantic ( subst_fo_formula_list t (rcompose thetal subst_id_symbol) theta) m rho <-> formula_list_disj_semantic t @@ -317,30 +317,30 @@ module Sem match t with | FOFNil -> () | FOFCons _ q -> formula_list_disj_semantic_subst_commutation q m thetal theta rho end - + let lemma formula_list_conj_semantic_term_subst_commutation - (t:fo_formula_list 'ls 'b) (m:model 'ls 'st) - (theta:func 'b (fo_term 'ls 'c)) (rho:func 'c 'st) : unit + (t:fo_formula_list 'fsymb 'b) (m:model 'fsymb 'st) + (theta:func 'b (fo_term 'fsymb 'c)) (rho:func 'c 'st) : unit ensures { formula_list_conj_semantic (subst_fo_formula_list t subst_id_symbol theta) m rho <-> formula_list_conj_semantic t m (semantic_subst theta m rho) } = formula_list_conj_semantic_subst_commutation t m identity theta rho - + let lemma formula_list_disj_semantic_term_subst_commutation - (t:fo_formula_list 'ls 'b) (m:model 'ls 'st) - (theta:func 'b (fo_term 'ls 'c)) (rho:func 'c 'st) : unit + (t:fo_formula_list 'fsymb 'b) (m:model 'fsymb 'st) + (theta:func 'b (fo_term 'fsymb 'c)) (rho:func 'c 'st) : unit ensures { formula_list_disj_semantic (subst_fo_formula_list t subst_id_symbol theta) m rho <-> formula_list_disj_semantic t m (semantic_subst theta m rho) } = formula_list_disj_semantic_subst_commutation t m identity theta rho - + let rec lemma tableau_semantic_subst_commutation - (t:tableau 'ls 'b) (m:model 'ls2 'st) + (t:tableau 'fsymb 'b) (m:model 'fsymb2 'st) (b:bool) - (thetal:func 'ls 'ls2) - (theta:func 'b (fo_term 'ls2 'c)) (rho:func 'c 'st) : unit + (thetal:func 'fsymb 'fsymb2) + (theta:func 'b (fo_term 'fsymb2 'c)) (rho:func 'c 'st) : unit ensures { tableau_semantic_with ( subst_tableau t (rcompose thetal subst_id_symbol) theta) b m rho <-> tableau_semantic_with t b @@ -358,20 +358,20 @@ module Sem else False in tableau_semantic_subst_commutation tnext m b' thetal theta rho end - + let lemma tableau_semantic_term_subst_commutation - (t:tableau 'ls 'b) (b:bool) (m:model 'ls 'st) - (theta:func 'b (fo_term 'ls 'c)) (rho:func 'c 'st) : unit + (t:tableau 'fsymb 'b) (b:bool) (m:model 'fsymb 'st) + (theta:func 'b (fo_term 'fsymb 'c)) (rho:func 'c 'st) : unit ensures { tableau_semantic_with ( subst_tableau t subst_id_symbol theta) b m rho <-> tableau_semantic_with t b m (semantic_subst theta m rho) } = tableau_semantic_subst_commutation t m b identity theta rho - + let rec lemma term_semantic_depend_only_free_var - (t:fo_term 'ls 'b) (m1 m2:model 'ls 'st) + (t:fo_term 'fsymb 'b) (m1 m2:model 'fsymb 'st) (rho1 rho2:func 'b 'st) : unit - requires { forall f:'ls. is_symbol_free_var_in_fo_term f t -> + requires { forall f:'fsymb. is_symbol_free_var_in_fo_term f t -> eval m1.interp_fun f = eval m2.interp_fun f /\ eval m1.interp_pred f = eval m2.interp_pred f } requires { forall x:'b. is_fo_term_free_var_in_fo_term x t -> @@ -382,11 +382,11 @@ module Sem match t with Var_fo_term x -> () | App (Var_symbol f) l -> term_list_semantic_depend_only_free_var l m1 m2 rho1 rho2 ; assert { is_symbol_free_var_in_fo_term f t } end - + with lemma term_list_semantic_depend_only_free_var - (t:fo_term_list 'ls 'b) (m1 m2:model 'ls 'st) + (t:fo_term_list 'fsymb 'b) (m1 m2:model 'fsymb 'st) (rho1 rho2:func 'b 'st) : unit - requires { forall f:'ls. is_symbol_free_var_in_fo_term_list f t -> + requires { forall f:'fsymb. is_symbol_free_var_in_fo_term_list f t -> eval m1.interp_fun f = eval m2.interp_fun f /\ eval m1.interp_pred f = eval m2.interp_pred f } requires { forall x:'b. is_fo_term_free_var_in_fo_term_list x t -> @@ -397,19 +397,19 @@ module Sem match t with FONil -> () | FOCons x q -> term_semantic_depend_only_free_var x m1 m2 rho1 rho2 ; term_list_semantic_depend_only_free_var q m1 m2 rho1 rho2 end - + let lemma formula_semantic_depend_only_free_var - (t:fo_formula 'ls0 'b0) (m1 m2:model 'ls0 'st0) + (t:fo_formula 'fsymb0 'b0) (m1 m2:model 'fsymb0 'st0) (rho1 rho2:func 'b0 'st0) : unit - requires { forall f:'ls0. is_symbol_free_var_in_fo_formula f t -> + requires { forall f:'fsymb0. is_symbol_free_var_in_fo_formula f t -> eval m1.interp_fun f = eval m2.interp_fun f /\ eval m1.interp_pred f = eval m2.interp_pred f } requires { forall x:'b0. is_fo_term_free_var_in_fo_formula x t -> rho1 x = rho2 x } ensures { formula_semantic t m1 rho1 <-> formula_semantic t m2 rho2 } = - let rec aux (t:fo_formula 'ls 'b) (m1 m2:model 'ls 'st) : unit - requires { forall f:'ls. is_symbol_free_var_in_fo_formula f t -> + let rec aux (t:fo_formula 'fsymb 'b) (m1 m2:model 'fsymb 'st) : unit + requires { forall f:'fsymb. is_symbol_free_var_in_fo_formula f t -> eval m1.interp_fun f = eval m2.interp_fun f /\ eval m1.interp_pred f = eval m2.interp_pred f } ensures { forall rho1 rho2:func 'b 'st. @@ -456,11 +456,11 @@ module Sem eval m2.interp_pred p (term_list_semantic l m2 rho2)) } end in aux t m1 m2 - + let rec lemma formula_list_conj_semantic_depend_only_free_var - (t:fo_formula_list 'ls 'b) (m1 m2:model 'ls 'st) + (t:fo_formula_list 'fsymb 'b) (m1 m2:model 'fsymb 'st) (rho1 rho2:func 'b 'st) : unit - requires { forall f:'ls. is_symbol_free_var_in_fo_formula_list f t -> + requires { forall f:'fsymb. is_symbol_free_var_in_fo_formula_list f t -> eval m1.interp_fun f = eval m2.interp_fun f /\ eval m1.interp_pred f = eval m2.interp_pred f } requires { forall x:'b. is_fo_term_free_var_in_fo_formula_list x t -> @@ -472,11 +472,11 @@ module Sem match t with FOFNil -> () | FOFCons x q -> formula_semantic_depend_only_free_var x m1 m2 rho1 rho2 ; formula_list_conj_semantic_depend_only_free_var q m1 m2 rho1 rho2 end - + let rec lemma formula_list_disj_semantic_depend_only_free_var - (t:fo_formula_list 'ls 'b) (m1 m2:model 'ls 'st) + (t:fo_formula_list 'fsymb 'b) (m1 m2:model 'fsymb 'st) (rho1 rho2:func 'b 'st) : unit - requires { forall f:'ls. is_symbol_free_var_in_fo_formula_list f t -> + requires { forall f:'fsymb. is_symbol_free_var_in_fo_formula_list f t -> eval m1.interp_fun f = eval m2.interp_fun f /\ eval m1.interp_pred f = eval m2.interp_pred f } requires { forall x:'b. is_fo_term_free_var_in_fo_formula_list x t -> @@ -488,79 +488,79 @@ module Sem match t with FOFNil -> () | FOFCons x q -> formula_semantic_depend_only_free_var x m1 m2 rho1 rho2 ; formula_list_disj_semantic_depend_only_free_var q m1 m2 rho1 rho2 end - - predicate formula_list_mem (phi:fo_formula 'ls 'b) - (l:fo_formula_list 'ls 'b) = match l with + + predicate formula_list_mem (phi:fo_formula 'fsymb 'b) + (l:fo_formula_list 'fsymb 'b) = match l with | FOFNil -> false | FOFCons x q -> x = phi \/ formula_list_mem phi q end - + let rec lemma formula_list_conj_semantic_other_def - (l:fo_formula_list 'ls 'b) (m:model 'ls 'st) + (l:fo_formula_list 'fsymb 'b) (m:model 'fsymb 'st) (rho:func 'b 'st) : unit ensures { formula_list_conj_semantic l m rho <-> - (forall phi:fo_formula 'ls 'b. + (forall phi:fo_formula 'fsymb 'b. formula_list_mem phi l -> formula_semantic phi m rho) } variant { size_fo_formula_list l } = match l with FOFNil -> () | FOFCons _ q -> formula_list_conj_semantic_other_def q m rho end - + let rec lemma formula_list_disj_semantic_other_def - (l:fo_formula_list 'ls 'b) (m:model 'ls 'st) + (l:fo_formula_list 'fsymb 'b) (m:model 'fsymb 'st) (rho:func 'b 'st) : unit ensures { formula_list_disj_semantic l m rho <-> - (exists phi:fo_formula 'ls 'b. + (exists phi:fo_formula 'fsymb 'b. formula_list_mem phi l /\ formula_semantic phi m rho) } variant { size_fo_formula_list l } = match l with FOFNil -> () | FOFCons x q -> formula_list_disj_semantic_other_def q m rho end - + (* Problem : validity/unsatifiability are not even axiomatizable in why3, since we would have to introduce it from a type quantification. However, we can define a demonstrability predicate and show for it the same elimination principle as unsatisfiability. *) - + (* Demonstration object (not directly a predicate, so we can actually construct the proof object ourselves). *) - + (* G |- A can be read as : for every model+interpretation, if /\G is true then A too. Which in particular mean : if G |- false, G have no model, so we can use G |- false instead of unsat predicate as long as it can represent all our demonstration steps. *) - - (*type demonstration 'ls 'b = + + (*type demonstration 'fsymb 'b = | Axiom - | ModusPonens (demonstration 'ls 'b) (demonstration 'ls 'b) - (fo_formula 'ls 'b) - | Abstraction (demonstration 'ls 'b) (fo_formula 'ls 'b) - (fo_formula 'ls 'b) - | ConjunctionIntro (demonstration 'ls 'b) (fo_formula 'ls 'b) - (demonstration 'ls 'b) (fo_formula 'ls 'b) - | ConjunctionLeft (demonstration 'ls 'b) (fo_formula 'ls 'b) - | ConjunctionRight (demonstration 'ls 'b) (fo_formula 'ls 'b) - | DisjunctionLeft (demonstration 'ls 'b) (fo_formula 'ls 'b) - (fo_formula 'ls 'b) - | DisjunctionRight (demonstration 'ls 'b) (fo_formula 'ls 'b) - (fo_formula 'ls 'b) - | DisjunctionElim (demonstration 'ls 'b) (demonstration 'ls 'b) - (demonstration 'ls 'b) (fo_formula 'ls 'b) (fo_formula 'ls 'b) - | UniversalInstantiation (demonstration 'ls 'b) - (fo_formula 'ls (option 'b)) (fo_term 'ls 'b) - | Instantiation (demonstration 'ls 'b) - (fo_formula_list 'ls 'b) - (fo_formula 'ls 'b) 'b (fo_term 'ls 'b) - | ExistentialIntroduction (demonstration 'ls 'b) - (fo_formula 'ls (option 'b)) (fo_term 'ls 'b) - | ExistentialElimination (demonstration 'ls 'b) - (demonstration 'ls 'b) - (fo_formula 'ls (option 'b)) (fo_formula 'ls (option 'b)) - | PointlessExistential (demonstration 'ls 'b) - | ExFalso (demonstration 'ls 'b) + | ModusPonens (demonstration 'fsymb 'b) (demonstration 'fsymb 'b) + (fo_formula 'fsymb 'b) + | Abstraction (demonstration 'fsymb 'b) (fo_formula 'fsymb 'b) + (fo_formula 'fsymb 'b) + | ConjunctionIntro (demonstration 'fsymb 'b) (fo_formula 'fsymb 'b) + (demonstration 'fsymb 'b) (fo_formula 'fsymb 'b) + | ConjunctionLeft (demonstration 'fsymb 'b) (fo_formula 'fsymb 'b) + | ConjunctionRight (demonstration 'fsymb 'b) (fo_formula 'fsymb 'b) + | DisjunctionLeft (demonstration 'fsymb 'b) (fo_formula 'fsymb 'b) + (fo_formula 'fsymb 'b) + | DisjunctionRight (demonstration 'fsymb 'b) (fo_formula 'fsymb 'b) + (fo_formula 'fsymb 'b) + | DisjunctionElim (demonstration 'fsymb 'b) (demonstration 'fsymb 'b) + (demonstration 'fsymb 'b) (fo_formula 'fsymb 'b) (fo_formula 'fsymb 'b) + | UniversalInstantiation (demonstration 'fsymb 'b) + (fo_formula 'fsymb (option 'b)) (fo_term 'fsymb 'b) + | Instantiation (demonstration 'fsymb 'b) + (fo_formula_list 'fsymb 'b) + (fo_formula 'fsymb 'b) 'b (fo_term 'fsymb 'b) + | ExistentialIntroduction (demonstration 'fsymb 'b) + (fo_formula 'fsymb (option 'b)) (fo_term 'fsymb 'b) + | ExistentialElimination (demonstration 'fsymb 'b) + (demonstration 'fsymb 'b) + (fo_formula 'fsymb (option 'b)) (fo_formula 'fsymb (option 'b)) + | PointlessExistential (demonstration 'fsymb 'b) + | ExFalso (demonstration 'fsymb 'b) | Trivial - | Weakening (demonstration 'ls 'b) (fo_formula_list 'ls 'b) - | Skolemization (demonstration 'ls 'b) (fo_formula 'ls 'b) 'ls*) - - (*predicate is_skolem_axiom (phi:fo_formula 'ls 'b) (f:'ls) - (env:fo_term_list 'ls 'b) = + | Weakening (demonstration 'fsymb 'b) (fo_formula_list 'fsymb 'b) + | Skolemization (demonstration 'fsymb 'b) (fo_formula 'fsymb 'b) 'fsymb*) + + (*predicate is_skolem_axiom (phi:fo_formula 'fsymb 'b) (f:'fsymb) + (env:fo_term_list 'fsymb 'b) = match phi with | Forall phi2 -> is_skolem_axiom phi2 f (FOCons (Var_fo_term None) (rename_fo_term_list env identity some)) @@ -570,7 +570,7 @@ module Sem not(is_symbol_free_var_in_fo_formula f phi2) | _ -> false end*) - + (*(* Hack to force possibility of instantiation of extend_env definition axiom ! *) function extend_env_selection (g:func (list 'st) (func 'b 'st)) @@ -590,63 +590,63 @@ module Sem | Cons y q -> extend_env_selection g x y q | Nil -> default end - + lemma extend_env_none : forall g:func (list 'st) (func 'b 'st), y:'st,l:list 'st. extend_env g (Cons y l) None = y lemma extend_env_some : forall g:func (list 'st) (func 'b 'st), x:'b,y:'st,l:list 'st. extend_env g (Cons y l) (Some x) = g l x*) - + (* Abstraction-definition axiom : - function skolem_predicate (phi:fo_formula 'ls (option 'b)) - (m:model 'ls 'st) (rho:func 'b 'st) : pred 'st = + function skolem_predicate (phi:fo_formula 'fsymb (option 'b)) + (m:model 'fsymb 'st) (rho:func 'b 'st) : pred 'st = (\ x:'st. formula_semantic phi m (ocase rho x) ) *) - function skolem_predicate (phi:fo_formula 'ls (option 'b)) - (m:model 'ls 'st) (rho:func 'b 'st) : pred 'st - axiom skolem_predicate_def : forall phi:fo_formula 'ls (option 'b), - m:model 'ls 'st,rho:func 'b 'st,x:'st. + function skolem_predicate (phi:fo_formula 'fsymb (option 'b)) + (m:model 'fsymb 'st) (rho:func 'b 'st) : pred 'st + axiom skolem_predicate_def : forall phi:fo_formula 'fsymb (option 'b), + m:model 'fsymb 'st,rho:func 'b 'st,x:'st. skolem_predicate phi m rho x <-> formula_semantic phi m (ocase rho x) - + (* Abstraction-definition axiom : - function skolem_function (phi:fo_formula 'ls (option 'b)) - (m:model 'ls 'st) (g:func (list 'st) (func 'b 'st)) : func (list 'st) 'st + function skolem_function (phi:fo_formula 'fsymb (option 'b)) + (m:model 'fsymb 'st) (g:func (list 'st) (func 'b 'st)) : func (list 'st) 'st = (\ l:list 'st. choice (skolem_predicate phi m rho (g l)) ) *) - function skolem_function (phi:fo_formula 'ls (option 'b)) - (m:model 'ls 'st) (g:func (list 'st) (func 'b 'st)) : func (list 'st) 'st - axiom skolem_function_def : forall phi:fo_formula 'ls (option 'b), - m:model 'ls 'st,g:func (list 'st) (func 'b 'st),l:list 'st. + function skolem_function (phi:fo_formula 'fsymb (option 'b)) + (m:model 'fsymb 'st) (g:func (list 'st) (func 'b 'st)) : func (list 'st) 'st + axiom skolem_function_def : forall phi:fo_formula 'fsymb (option 'b), + m:model 'fsymb 'st,g:func (list 'st) (func 'b 'st),l:list 'st. skolem_function phi m g l = choice (skolem_predicate phi m (g l)) - + (* Abstraction-definition axiom : - function skolem_transformer (phi:fo_formula 'ls (option 'b)) (f:'ls) - (g:func (list 'st) (func 'b 'st)) : func (model 'ls 'st) (model 'ls 'st) = - (\ m:model 'ls 'st. + function skolem_transformer (phi:fo_formula 'fsymb (option 'b)) (f:'fsymb) + (g:func (list 'st) (func 'b 'st)) : func (model 'fsymb 'st) (model 'fsymb 'st) = + (\ m:model 'fsymb 'st. { interp_fun = m.interp_fun[f <- skolem_function phi m g] ; interp_pred = m.interp_pred ; }) *) - - function skolem_transformer (phi:fo_formula 'ls (option 'b)) (f:'ls) - (g:func (list 'st) (func 'b 'st)) : func (model 'ls 'st) (model 'ls 'st) - axiom skolem_transformer_def : forall phi:fo_formula 'ls (option 'b),f:'ls, - g:func (list 'st) (func 'b 'st), m:model 'ls 'st. + + function skolem_transformer (phi:fo_formula 'fsymb (option 'b)) (f:'fsymb) + (g:func (list 'st) (func 'b 'st)) : func (model 'fsymb 'st) (model 'fsymb 'st) + axiom skolem_transformer_def : forall phi:fo_formula 'fsymb (option 'b),f:'fsymb, + g:func (list 'st) (func 'b 'st), m:model 'fsymb 'st. skolem_transformer phi f g m = { interp_fun = m.interp_fun[f <- skolem_function phi m g] ; interp_pred = m.interp_pred ; } - - let ghost skolem_model_transformer (phi:fo_formula 'ls (option 'b)) (f:'ls) - (vars:fo_term_list 'ls 'b) - (g:func (list 'st) (func 'b 'st)) : func (model 'ls 'st) (model 'ls 'st) + + let ghost skolem_model_transformer (phi:fo_formula 'fsymb (option 'b)) (f:'fsymb) + (vars:fo_term_list 'fsymb 'b) + (g:func (list 'st) (func 'b 'st)) : func (model 'fsymb 'st) (model 'fsymb 'st) requires { not(is_symbol_free_var_in_fo_formula f phi) } - requires { forall m:model 'ls 'st, rho:func 'b 'st,x:'b. + requires { forall m:model 'fsymb 'st, rho:func 'b 'st,x:'b. is_fo_term_free_var_in_fo_formula (Some x) phi -> g (term_list_semantic vars m rho) x = rho x } requires { not(is_symbol_free_var_in_fo_term_list f vars) } - ensures { forall m:model 'ls 'st. + ensures { forall m:model 'fsymb 'st. m.interp_pred = (result m).interp_pred } - ensures { forall m:model 'ls 'st,f0:'ls. + ensures { forall m:model 'fsymb 'st,f0:'fsymb. f0 <> f -> eval m.interp_fun f0 = eval (result m).interp_fun f0 } - ensures { forall m:model 'ls 'st,rho:func 'b 'st. + ensures { forall m:model 'fsymb 'st,rho:func 'b 'st. formula_semantic (Exists phi) m rho -> formula_semantic (subst_fo_formula phi subst_id_symbol (ocase subst_id_fo_term (App (Var_symbol f) vars))) (result m) rho } @@ -655,7 +655,7 @@ module Sem let skt = App (Var_symbol f) vars in let sks = ocase subst_id_fo_term skt in let phi' = subst_fo_formula phi subst_id_symbol sks in - assert { forall m:model 'ls 'st,rho:func 'b 'st. + assert { forall m:model 'fsymb 'st,rho:func 'b 'st. let semf = skolem_function phi m g in let skm = skf m in let em = term_list_semantic vars m rho in @@ -675,7 +675,7 @@ module Sem s1 None = s2 None && (forall y:'b. s1 (Some y) = s2 (Some y)) && extensionalEqual s1 s2 && - (forall f':'ls. is_symbol_free_var_in_fo_formula f' phi -> + (forall f':'fsymb. is_symbol_free_var_in_fo_formula f' phi -> eval m.interp_fun f' = eval skm.interp_fun f' /\ eval m.interp_pred f' = eval skm.interp_pred f') && (forall x:'st. @@ -691,22 +691,22 @@ module Sem formula_semantic phi' skm rho) } ; skf - + (* - let ghost skolemized_model (phi0:fo_formula 'ls0 'b0) (f0:'ls0) - (m0:model 'ls0 'st) : model 'ls0 'st + let ghost skolemized_model (phi0:fo_formula 'fsymb0 'b0) (f0:'fsymb0) + (m0:model 'fsymb0 'st) : model 'fsymb0 'st requires { is_skolem_axiom phi0 f0 FONil } requires { forall x:'b0. not(is_fo_term_free_var_in_fo_formula x phi0) } ensures { forall rho:func 'b0 'st. formula_semantic phi0 result rho } ensures { m0.interp_pred = result.interp_pred } - ensures { forall f':'ls0. f0 <> f' -> + ensures { forall f':'fsymb0. f0 <> f' -> eval m0.interp_fun f' = eval result.interp_fun f' } = - let rec aux (phi:fo_formula 'ls 'b) (f:'ls) - (env:fo_term_list 'ls 'b) + let rec aux (phi:fo_formula 'fsymb 'b) (f:'fsymb) + (env:fo_term_list 'fsymb 'b) (g:func (list 'st) (func 'b 'st)) - (m:model 'ls 'st) : model 'ls 'st + (m:model 'fsymb 'st) : model 'fsymb 'st requires { is_skolem_axiom phi f env } requires { forall rho:func 'b 'st,x:'b. is_fo_term_free_var_in_fo_formula x phi -> @@ -715,7 +715,7 @@ module Sem ensures { forall rho:func 'b 'st. formula_semantic phi result rho } ensures { m.interp_pred = result.interp_pred } - ensures { forall f':'ls. f <> f' -> + ensures { forall f':'fsymb. f <> f' -> eval m.interp_fun f' = eval result.interp_fun f' } variant { size_fo_formula phi } = @@ -762,7 +762,7 @@ module Sem s1 None = s2 None && (forall y:'b. s1 (Some y) = s2 (Some y)) && extensionalEqual s1 s2 && - (forall f':'ls. is_symbol_free_var_in_fo_formula f' phi2 -> + (forall f':'fsymb. is_symbol_free_var_in_fo_formula f' phi2 -> eval m.interp_fun f' = eval skm.interp_fun f' /\ eval m.interp_pred f' = eval skm.interp_pred f') && (forall x:'st. @@ -780,9 +780,9 @@ module Sem | _ -> absurd end in aux phi0 f0 FONil default m0*) - - (*predicate deducible_from (gamma:fo_formula_list 'ls 'b) - (phi:fo_formula 'ls 'b) (d:demonstration 'ls 'b) = + + (*predicate deducible_from (gamma:fo_formula_list 'fsymb 'b) + (phi:fo_formula 'fsymb 'b) (d:demonstration 'fsymb 'b) = match d with | Axiom -> formula_list_mem phi gamma | ModusPonens d1 d2 phi2 -> deducible_from gamma phi2 d1 /\ @@ -827,7 +827,7 @@ module Sem | Trivial -> phi = FTrue | Weakening d gamma2 -> deducible_from gamma2 phi d /\ - (forall phi0:fo_formula 'ls 'b. + (forall phi0:fo_formula 'fsymb 'b. formula_list_mem phi0 gamma2 -> formula_list_mem phi0 gamma) | Skolemization d phis f -> @@ -837,17 +837,17 @@ module Sem is_skolem_axiom phis f FONil /\ (forall x:'b. not(is_fo_term_free_var_in_fo_formula x phis)) end - - let lemma deducible_correct (gamma0:fo_formula_list 'ls 'b0) - (phi0:fo_formula 'ls 'b0) (d0:demonstration 'ls 'b0) - (m0:model 'ls 'st0) (rho0:func 'b0 'st0) : unit + + let lemma deducible_correct (gamma0:fo_formula_list 'fsymb 'b0) + (phi0:fo_formula 'fsymb 'b0) (d0:demonstration 'fsymb 'b0) + (m0:model 'fsymb 'st0) (rho0:func 'b0 'st0) : unit requires { deducible_from gamma0 phi0 d0 } requires { formula_list_conj_semantic gamma0 m0 rho0 } ensures { formula_semantic phi0 m0 rho0 } = - let rec ghost aux (gamma:fo_formula_list 'ls 'b) - (phi:fo_formula 'ls 'b) (d:demonstration 'ls 'b) - (m:model 'ls 'st) : unit + let rec ghost aux (gamma:fo_formula_list 'fsymb 'b) + (phi:fo_formula 'fsymb 'b) (d:demonstration 'fsymb 'b) + (m:model 'fsymb 'st) : unit requires { deducible_from gamma phi d } ensures { forall rho:func 'b 'st. formula_list_conj_semantic gamma m rho -> @@ -915,56 +915,56 @@ module Sem | _ -> absurd end in aux gamma0 phi0 d0 m0 - - predicate entail (gamma:fo_formula_list 'ls 'b) - (phi:fo_formula 'ls 'b) = - exists d:demonstration 'ls 'b. + + predicate entail (gamma:fo_formula_list 'fsymb 'b) + (phi:fo_formula 'fsymb 'b) = + exists d:demonstration 'fsymb 'b. deducible_from gamma phi d - - predicate unsat (gamma:fo_formula_list 'ls 'b) = + + predicate unsat (gamma:fo_formula_list 'fsymb 'b) = entail gamma FFalse - - predicate valid (phi:fo_formula 'ls 'b) = + + predicate valid (phi:fo_formula 'fsymb 'b) = entail FOFNil phi - - lemma entail_correct : forall gamma:fo_formula_list 'ls 'b, - phi:fo_formula 'ls 'b,m:model 'ls 'st,rho:func 'b 'st. + + lemma entail_correct : forall gamma:fo_formula_list 'fsymb 'b, + phi:fo_formula 'fsymb 'b,m:model 'fsymb 'st,rho:func 'b 'st. entail gamma phi -> formula_list_conj_semantic gamma m rho -> formula_semantic phi m rho - - lemma unsat_correct : forall gamma:fo_formula_list 'ls 'b, - m:model 'ls 'st,rho:func 'b 'st. + + lemma unsat_correct : forall gamma:fo_formula_list 'fsymb 'b, + m:model 'fsymb 'st,rho:func 'b 'st. unsat gamma -> not(formula_list_conj_semantic gamma m rho) - - lemma valid_correct : forall phi:fo_formula 'ls 'b, - m:model 'ls 'st,rho:func 'b 'st. + + lemma valid_correct : forall phi:fo_formula 'fsymb 'b, + m:model 'fsymb 'st,rho:func 'b 'st. valid phi -> formula_semantic phi m rho - - function imply (phi1 phi2:fo_formula 'ls 'b) : fo_formula 'ls 'b = + + function imply (phi1 phi2:fo_formula 'fsymb 'b) : fo_formula 'fsymb 'b = Or (Not phi1) phi2 - - function equiv (phi1 phi2:fo_formula 'ls 'b) : fo_formula 'ls 'b = + + function equiv (phi1 phi2:fo_formula 'fsymb 'b) : fo_formula 'fsymb 'b = And (imply phi1 phi2) (imply phi2 phi1) - - type sequent 'ls 'b = { - demo : demonstration 'ls 'b ; - context : fo_formula_list 'ls 'b ; - conclusion : fo_formula 'ls 'b ; + + type sequent 'fsymb 'b = { + demo : demonstration 'fsymb 'b ; + context : fo_formula_list 'fsymb 'b ; + conclusion : fo_formula 'fsymb 'b ; } - - predicate sequent_correct (s:sequent 'ls 'b) = + + predicate sequent_correct (s:sequent 'fsymb 'b) = deducible_from s.context s.conclusion s.demo - - let ghost make_axiom (gamma:fo_formula_list 'ls 'b) - (phi:fo_formula 'ls 'b) : sequent 'ls 'b + + let ghost make_axiom (gamma:fo_formula_list 'fsymb 'b) + (phi:fo_formula 'fsymb 'b) : sequent 'fsymb 'b requires { formula_list_mem phi gamma } ensures { sequent_correct result } ensures { result.context = gamma } ensures { result.conclusion = phi } = { demo = Axiom ; context = gamma ; conclusion = phi } - - let ghost make_abstraction (s:sequent 'ls 'b) : - sequent 'ls 'b + + let ghost make_abstraction (s:sequent 'fsymb 'b) : + sequent 'fsymb 'b requires { sequent_correct s } requires { match s.context with FOFNil -> false | _ -> true end } ensures { sequent_correct result } @@ -974,8 +974,8 @@ module Sem | FOFCons x q -> { demo = Abstraction s.demo x s.conclusion ; context = q ; conclusion = imply x s.conclusion } end - - let ghost modus_ponens (s1 s2:sequent 'ls 'b) : sequent 'ls 'b + + let ghost modus_ponens (s1 s2:sequent 'fsymb 'b) : sequent 'fsymb 'b requires { sequent_correct s1 /\ sequent_correct s2 } requires { match s1.conclusion with | Or (Not phi1) phi2 -> s2.conclusion = phi1 @@ -991,15 +991,15 @@ module Sem context = s1.context ; conclusion = phi2 } | _ -> absurd end - - let ghost make_classical (gamma:fo_formula_list 'ls 'b) - (phi:fo_formula 'ls 'b) : sequent 'ls 'b + + let ghost make_classical (gamma:fo_formula_list 'fsymb 'b) + (phi:fo_formula 'fsymb 'b) : sequent 'fsymb 'b ensures { sequent_correct result } ensures { result.context = gamma } ensures { result.conclusion = Or (Not phi) phi } = make_abstraction (make_axiom (FOFCons phi gamma) phi) - - let ghost disjunction_elimination (s1 s2 s3:sequent 'ls 'b) : sequent 'ls 'b + + let ghost disjunction_elimination (s1 s2 s3:sequent 'fsymb 'b) : sequent 'fsymb 'b requires { sequent_correct s1 /\ sequent_correct s2 /\ sequent_correct s3 } requires { match s1.conclusion , s2.conclusion , s3.conclusion with | Or phi1 phi2 , Or (Not phi1') phi3 , Or (Not phi2') phi3' -> @@ -1019,9 +1019,9 @@ module Sem conclusion = phi3 ; } | _ -> absurd end - - let ghost disjunction_left (s:sequent 'ls 'b) (phi2:fo_formula 'ls 'b) : - sequent 'ls 'b + + let ghost disjunction_left (s:sequent 'fsymb 'b) (phi2:fo_formula 'fsymb 'b) : + sequent 'fsymb 'b requires { sequent_correct s } ensures { sequent_correct result } ensures { result.conclusion = Or s.conclusion phi2 } @@ -1030,9 +1030,9 @@ module Sem { demo = DisjunctionLeft s.demo s.conclusion phi2 ; context = s.context ; conclusion = Or s.conclusion phi2 } - - let ghost disjunction_right (phi1:fo_formula 'ls 'b) (s:sequent 'ls 'b) : - sequent 'ls 'b + + let ghost disjunction_right (phi1:fo_formula 'fsymb 'b) (s:sequent 'fsymb 'b) : + sequent 'fsymb 'b requires { sequent_correct s } ensures { sequent_correct result } ensures { result.conclusion = Or phi1 s.conclusion } @@ -1041,8 +1041,8 @@ module Sem { demo = DisjunctionRight s.demo phi1 s.conclusion ; context = s.context ; conclusion = Or phi1 s.conclusion } - - let ghost conjunction (s1 s2:sequent 'ls 'b) : sequent 'ls 'b + + let ghost conjunction (s1 s2:sequent 'fsymb 'b) : sequent 'fsymb 'b requires { sequent_correct s1 /\ sequent_correct s2 } requires { s1.context = s2.context } ensures { sequent_correct result } @@ -1052,8 +1052,8 @@ module Sem { demo = ConjunctionIntro s1.demo s1.conclusion s2.demo s2.conclusion ; context = s1.context ; conclusion = And s1.conclusion s2.conclusion } - - let ghost conjunction_left (s:sequent 'ls 'b) : sequent 'ls 'b + + let ghost conjunction_left (s:sequent 'fsymb 'b) : sequent 'fsymb 'b requires { sequent_correct s } requires { match s.conclusion with And _ _ -> true | _ -> false end } ensures { sequent_correct result } @@ -1066,8 +1066,8 @@ module Sem conclusion = phi1 } | _ -> absurd end - - let ghost conjunction_right (s:sequent 'ls 'b) : sequent 'ls 'b + + let ghost conjunction_right (s:sequent 'fsymb 'b) : sequent 'fsymb 'b requires { sequent_correct s } requires { match s.conclusion with And _ _ -> true | _ -> false end } ensures { sequent_correct result } @@ -1080,25 +1080,25 @@ module Sem conclusion = phi1 } | _ -> absurd end - - let ghost exfalso (s:sequent 'ls 'b) (phi:fo_formula 'ls 'b) : sequent 'ls 'b + + let ghost exfalso (s:sequent 'fsymb 'b) (phi:fo_formula 'fsymb 'b) : sequent 'fsymb 'b requires { sequent_correct s } requires { match s.conclusion with FFalse -> true | _ -> false end } ensures { sequent_correct result } ensures { result.context = s.context } ensures { result.conclusion = phi } = { demo = ExFalso s.demo ; context = s.context ; conclusion = phi } - - let ghost make_trivial (gamma:fo_formula_list 'ls 'b) : sequent 'ls 'b + + let ghost make_trivial (gamma:fo_formula_list 'fsymb 'b) : sequent 'fsymb 'b ensures { sequent_correct result } ensures { result.context = gamma } ensures { result.conclusion = FTrue } = { demo = Trivial ; context = gamma ; conclusion = FTrue } - - let ghost weaken (gamma:fo_formula_list 'ls 'b) - (s:sequent 'ls 'b) : sequent 'ls 'b + + let ghost weaken (gamma:fo_formula_list 'fsymb 'b) + (s:sequent 'fsymb 'b) : sequent 'fsymb 'b requires { sequent_correct s } - requires { forall phi:fo_formula 'ls 'b. + requires { forall phi:fo_formula 'fsymb 'b. formula_list_mem phi s.context -> formula_list_mem phi gamma } ensures { sequent_correct result } ensures { result.context = gamma } @@ -1106,8 +1106,8 @@ module Sem = { demo = Weakening s.demo s.context ; context = gamma ; conclusion = s.conclusion } - - let ghost skolem_elim (f:'ls) (s:sequent 'ls 'b) : sequent 'ls 'b + + let ghost skolem_elim (f:'fsymb) (s:sequent 'fsymb 'b) : sequent 'fsymb 'b requires { sequent_correct s } requires { match s.context with FOFCons phis gamma -> is_skolem_axiom phis f FONil /\ @@ -1124,8 +1124,8 @@ module Sem context = gamma ; conclusion = s.conclusion } | _ -> absurd end - - let ghost conjunction_commutative (s:sequent 'ls 'b) : sequent 'ls 'b + + let ghost conjunction_commutative (s:sequent 'fsymb 'b) : sequent 'fsymb 'b requires { sequent_correct s } requires { match s.conclusion with And _ _ -> true | _ -> false end } ensures { sequent_correct result } @@ -1133,21 +1133,21 @@ module Sem ensures { match s.conclusion with And phi1 phi2 -> result.conclusion = And phi2 phi1 | _ -> false end } = conjunction (conjunction_right s) (conjunction_left s) - - let ghost equiv_reflexive (gamma:fo_formula_list 'ls 'b) - (phi:fo_formula 'ls 'b) : sequent 'ls 'b + + let ghost equiv_reflexive (gamma:fo_formula_list 'fsymb 'b) + (phi:fo_formula 'fsymb 'b) : sequent 'fsymb 'b ensures { sequent_correct result } ensures { result.context = gamma } ensures { result.conclusion = equiv phi phi } = let u = make_classical gamma phi in conjunction u u - + (* - - let ghost imply_or_morphism (gamma:fo_formula_list 'ls 'b) - (phi1 phi2 phi3 phi4:fo_formula 'ls 'b) - (d1 d2:demonstration 'ls 'b) : demonstration 'ls 'b + + let ghost imply_or_morphism (gamma:fo_formula_list 'fsymb 'b) + (phi1 phi2 phi3 phi4:fo_formula 'fsymb 'b) + (d1 d2:demonstration 'fsymb 'b) : demonstration 'fsymb 'b requires { deducible_from gamma (imply phi1 phi3) d1 } requires { deducible_from gamma (imply phi2 phi4) d2 } ensures { deducible_from gamma @@ -1170,10 +1170,10 @@ module Sem (disjunction_left gamma121 phi3 phi4 d1)) (make_abstraction gamma12 phi2 o34 (disjunction_right gamma122 phi3 phi4 d2)) - - let ghost equiv_or_morphism (gamma:fo_formula_list 'ls 'b) - (phi1 phi2 phi3 phi4:fo_formula 'ls 'b) - (d1 d2:demonstration 'ls 'b) : demonstration 'ls 'b + + let ghost equiv_or_morphism (gamma:fo_formula_list 'fsymb 'b) + (phi1 phi2 phi3 phi4:fo_formula 'fsymb 'b) + (d1 d2:demonstration 'fsymb 'b) : demonstration 'fsymb 'b requires { deducible_from gamma (equiv phi1 phi3) d1 } requires { deducible_from gamma (equiv phi2 phi4) d2 } ensures { deducible_from gamma @@ -1188,12 +1188,12 @@ module Sem (conjunction_right gamma (imply phi2 phi4) (imply phi4 phi2) d2) in conjunction (imply o12 o34) (imply o34 o12) way1 way2 *) - - + + (* - let ghost disjunction_commutation (gamma:fo_formula_list 'ls 'b) - (phi1 phi2:fo_formula 'ls 'b) (d:demonstration 'ls 'b) : - demonstration 'ls 'b + let ghost disjunction_commutation (gamma:fo_formula_list 'fsymb 'b) + (phi1 phi2:fo_formula 'fsymb 'b) (d:demonstration 'fsymb 'b) : + demonstration 'fsymb 'b requires { deducible_from gamma (Or phi1 phi2) d } ensures { deducible_from gamma (Or phi2 phi1) result } = @@ -1204,10 +1204,10 @@ module Sem let d1 = make_abstraction gamma phi1 o d1 in let d2 = make_abstraction gamma phi2 o d2 in disjunction_elimination gamma phi1 phi2 o d d1 d2 - - let ghost disjunction_associative_r (gamma:fo_formula_list 'ls 'b) - (phi1 phi2 phi3:fo_formula 'ls 'b) (d:demonstration 'ls 'b) : - demonstration 'ls 'b + + let ghost disjunction_associative_r (gamma:fo_formula_list 'fsymb 'b) + (phi1 phi2 phi3:fo_formula 'fsymb 'b) (d:demonstration 'fsymb 'b) : + demonstration 'fsymb 'b requires { deducible_from gamma (Or (Or phi1 phi2) phi3) d } ensures { deducible_from gamma (Or phi1 (Or phi2 phi3)) result } = @@ -1232,10 +1232,10 @@ module Sem let d12 = make_abstraction gamma o12 oa d12 in let d3 = make_abstraction gamma phi3 oa d3 in disjunction_elimination gamma o12 phi3 oa d d12 d3 - - let ghost disjunction_associative_l (gamma:fo_formula_list 'ls 'b) - (phi1 phi2 phi3:fo_formula 'ls 'b) (d:demonstration 'ls 'b) : - demonstration 'ls 'b + + let ghost disjunction_associative_l (gamma:fo_formula_list 'fsymb 'b) + (phi1 phi2 phi3:fo_formula 'fsymb 'b) (d:demonstration 'fsymb 'b) : + demonstration 'fsymb 'b requires { deducible_from gamma (Or phi1 (Or phi2 phi3)) d } ensures { deducible_from gamma (Or (Or phi1 phi2) phi3) result } = @@ -1261,11 +1261,11 @@ module Sem let d1 = make_abstraction gamma phi1 oa d1 in disjunction_elimination gamma phi1 o23 oa d d1 d23 *) - + (* - let ghost double_negation_elimination (gamma:fo_formula_list 'ls 'b) - (phi:fo_formula 'ls 'b) (d:demonstration 'ls 'b) : - demonstration 'ls 'b + let ghost double_negation_elimination (gamma:fo_formula_list 'fsymb 'b) + (phi:fo_formula 'fsymb 'b) (d:demonstration 'fsymb 'b) : + demonstration 'fsymb 'b requires { deducible_from gamma (Not (Not phi)) d } ensures { deducible_from gamma phi result } = @@ -1275,147 +1275,147 @@ module Sem let d2 = disjunction_left gamma nnphi phi d in disjunction_elimination gamma nphi phi phi d0 d2 d0 *) - - (*let ghost false_neutral_left_disjunction (gamma:fo_formula_list 'ls 'b) - (phi:fo_formula 'ls 'b) (d:demonstration 'ls 'b) : - demonstration 'ls 'b + + (*let ghost false_neutral_left_disjunction (gamma:fo_formula_list 'fsymb 'b) + (phi:fo_formula 'fsymb 'b) (d:demonstration 'fsymb 'b) : + demonstration 'fsymb 'b requires { deducible_from gamma (Or FFalse phi) d } ensures { deducible_from gamma phi result } = let d1 = Abstraction (ExFalso Axiom) FFalse phi in let d2 = Abstraction Axiom phi phi in DisjunctionElim d d1 d2 FFalse phi - - let ghost false_neutral_right_disjunction (gamma:fo_formula_list 'ls 'b) - (phi:fo_formula 'ls 'b) (d:demonstration 'ls 'b) : - demonstration 'ls 'b + + let ghost false_neutral_right_disjunction (gamma:fo_formula_list 'fsymb 'b) + (phi:fo_formula 'fsymb 'b) (d:demonstration 'fsymb 'b) : + demonstration 'fsymb 'b requires { deducible_from gamma (Or phi FFalse) d } ensures { deducible_from gamma phi result } = false_neutral_left_disjunction gamma phi (disjunction_commutation gamma phi FFalse d)*) - + (*(* Now we do not need the demonstration object anymore. *) - - let lemma entail_axiom (gamma:fo_formula_list 'ls 'b) - (phi:fo_formula 'ls 'b) : unit + + let lemma entail_axiom (gamma:fo_formula_list 'fsymb 'b) + (phi:fo_formula 'fsymb 'b) : unit requires { formula_list_mem phi gamma } ensures { entail gamma phi } = () - - let lemma entail_modus_ponens (gamma:fo_formula_list 'ls 'b) - (phi1 phi2:fo_formula 'ls 'b) : unit + + let lemma entail_modus_ponens (gamma:fo_formula_list 'fsymb 'b) + (phi1 phi2:fo_formula 'fsymb 'b) : unit requires { entail gamma phi1 /\ entail gamma (Or (Not phi1) phi2) } ensures { entail gamma phi2 } = - assert { forall d1 d2:demonstration 'ls 'b. + assert { forall d1 d2:demonstration 'fsymb 'b. deducible_from gamma phi1 d1 /\ deducible_from gamma (Or (Not phi1) phi2) d2 -> deducible_from gamma phi2 (ModusPonens d1 d2 phi1) } - - let lemma entail_abstraction (gamma:fo_formula_list 'ls 'b) - (phi1 phi2:fo_formula 'ls 'b) : unit + + let lemma entail_abstraction (gamma:fo_formula_list 'fsymb 'b) + (phi1 phi2:fo_formula 'fsymb 'b) : unit requires { entail (FOFCons phi1 gamma) phi2 } ensures { entail gamma (Or (Not phi1) phi2) } = - assert { forall d:demonstration 'ls 'b. + assert { forall d:demonstration 'fsymb 'b. deducible_from (FOFCons phi1 gamma) phi2 d -> deducible_from gamma (Or (Not phi1) phi2) (Abstraction d phi1 phi2) } - - let lemma entail_conjunction (gamma:fo_formula_list 'ls 'b) - (phi1 phi2:fo_formula 'ls 'b) : unit + + let lemma entail_conjunction (gamma:fo_formula_list 'fsymb 'b) + (phi1 phi2:fo_formula 'fsymb 'b) : unit ensures { entail gamma (And phi1 phi2) <-> entail gamma phi1 /\ entail gamma phi2 } = - assert { forall d:demonstration 'ls 'b. + assert { forall d:demonstration 'fsymb 'b. deducible_from gamma (And phi1 phi2) d -> deducible_from gamma phi1 (ConjunctionLeft d phi2) /\ deducible_from gamma phi2 (ConjunctionRight d phi1) } ; - assert { forall d1 d2:demonstration 'ls 'b. + assert { forall d1 d2:demonstration 'fsymb 'b. deducible_from gamma phi1 d1 /\ deducible_from gamma phi2 d2 -> deducible_from gamma (And phi1 phi2) (ConjunctionIntro d1 phi1 d2 phi2) } - - let lemma entail_disjunction_left (gamma:fo_formula_list 'ls 'b) - (phi1 phi2:fo_formula 'ls 'b) + + let lemma entail_disjunction_left (gamma:fo_formula_list 'fsymb 'b) + (phi1 phi2:fo_formula 'fsymb 'b) requires { entail gamma phi1 } ensures { entail gamma (Or phi1 phi2) } = - assert { forall d:demonstration 'ls 'b. + assert { forall d:demonstration 'fsymb 'b. deducible_from gamma phi1 d -> deducible_from gamma (Or phi1 phi2) (DisjunctionLeft d phi1 phi2) } - - let lemma entail_disjunction_right (gamma:fo_formula_list 'ls 'b) - (phi1 phi2:fo_formula 'ls 'b) + + let lemma entail_disjunction_right (gamma:fo_formula_list 'fsymb 'b) + (phi1 phi2:fo_formula 'fsymb 'b) requires { entail gamma phi2 } ensures { entail gamma (Or phi1 phi2) } = - assert { forall d:demonstration 'ls 'b. + assert { forall d:demonstration 'fsymb 'b. deducible_from gamma phi2 d -> deducible_from gamma (Or phi1 phi2) (DisjunctionRight d phi1 phi2) } - - let lemma entail_disjunction_elim (gamma:fo_formula_list 'ls 'b) - (phi1 phi2 phi3:fo_formula 'ls 'b) + + let lemma entail_disjunction_elim (gamma:fo_formula_list 'fsymb 'b) + (phi1 phi2 phi3:fo_formula 'fsymb 'b) requires { entail gamma (Or phi1 phi2) } requires { entail gamma (Or (Not phi1) phi3) } requires { entail gamma (Or (Not phi2) phi3) } ensures { entail gamma phi3 } = - assert { forall d1 d2 d3:demonstration 'ls 'b. + assert { forall d1 d2 d3:demonstration 'fsymb 'b. deducible_from gamma (Or phi1 phi2) d1 /\ deducible_from gamma (Or (Not phi1) phi3) d2 /\ deducible_from gamma (Or (Not phi2) phi3) d3 -> deducible_from gamma phi3 (DisjunctionElim d1 d2 d3 phi1 phi2) } - - let lemma entail_universal_instantiation (gamma:fo_formula_list 'ls 'b) - (phi:fo_formula 'ls (option 'b)) (t:fo_term 'ls 'b) + + let lemma entail_universal_instantiation (gamma:fo_formula_list 'fsymb 'b) + (phi:fo_formula 'fsymb (option 'b)) (t:fo_term 'fsymb 'b) requires { entail gamma (Forall phi) } ensures { entail gamma (subst_fo_formula phi (ocase subst_id_fo_term t)) } = - assert { forall d:demonstration 'ls 'b. + assert { forall d:demonstration 'fsymb 'b. deducible_from gamma (Forall phi) d -> deducible_from gamma (subst_fo_formula phi (ocase subst_id_fo_term t)) (UniversalInstantiation d phi t) } - - let lemma entail_instantiation (gamma:fo_formula_list 'ls 'b) - (phi:fo_formula 'ls 'b) (x:'b) (t:fo_term 'ls 'b) + + let lemma entail_instantiation (gamma:fo_formula_list 'fsymb 'b) + (phi:fo_formula 'fsymb 'b) (x:'b) (t:fo_term 'fsymb 'b) requires { entail gamma phi } ensures { let s = subst_id_fo_term[x<-t] in entail (subst_fo_formula_list gamma s) (subst_fo_formula phi s) } = let s = subst_id_fo_term[x<-t] in - assert { forall d:demonstration 'ls 'b. + assert { forall d:demonstration 'fsymb 'b. deducible_from gamma phi d -> deducible_from (subst_fo_formula_list gamma s) (subst_fo_formula phi s) (Instantiation d gamma phi x t) } - - let lemma entail_existential_introduction (gamma:fo_formula_list 'ls 'b) - (phi:fo_formula 'ls (option 'b)) (t:fo_term 'ls 'b) + + let lemma entail_existential_introduction (gamma:fo_formula_list 'fsymb 'b) + (phi:fo_formula 'fsymb (option 'b)) (t:fo_term 'fsymb 'b) requires { entail gamma (subst_fo_formula phi (ocase subst_id_fo_term t)) } ensures { entail gamma (Exists phi) } = - assert { forall d:demonstration 'ls 'b. + assert { forall d:demonstration 'fsymb 'b. deducible_from gamma (subst_fo_formula phi (ocase subst_id_fo_term t)) d -> deducible_from gamma (Exists phi) (ExistentialIntroduction d phi t) } - - let lemma entail_existential_elimination (gamma:fo_formula_list 'ls 'b) - (phi1 phi2:fo_formula 'ls (option 'b)) + + let lemma entail_existential_elimination (gamma:fo_formula_list 'fsymb 'b) + (phi1 phi2:fo_formula 'fsymb (option 'b)) requires { entail gamma (Forall (Or (Not phi1) phi2)) } requires { entail gamma (Exists phi1) } ensures { entail gamma (Exists phi2) } = - assert { forall d1 d2:demonstration 'ls 'b. + assert { forall d1 d2:demonstration 'fsymb 'b. deducible_from gamma (Forall (Or (Not phi1) phi2)) d1 /\ deducible_from gamma (Exists phi1) d2 -> deducible_from gamma (Exists phi2) (ExistentialElimination d1 d2 phi1 phi2) } - - let lemma disjunction_commutative (gamma:fo_formula_list 'ls 'b) - (phi1 phi2:fo_formula 'ls 'b) + + let lemma disjunction_commutative (gamma:fo_formula_list 'fsymb 'b) + (phi1 phi2:fo_formula 'fsymb 'b) requires { entail gamma (Or phi1 phi2) } ensures { entail gamma (Or phi2 phi1) } = @@ -1426,4 +1426,3 @@ module Sem entail_disjunction_elim gamma phi1 phi2 (Or phi2 phi1)*) *) end - diff --git a/examples/in_progress/prover/Firstorder_semantics/why3session.xml b/examples/in_progress/prover/Firstorder_semantics/why3session.xml index 010b35b17..caf5c0af2 100644 --- a/examples/in_progress/prover/Firstorder_semantics/why3session.xml +++ b/examples/in_progress/prover/Firstorder_semantics/why3session.xml @@ -1,4488 +1,627 @@ - - - - - - - - - - - - - - - - - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - - + + + + + + + + + + + + + + + + + + - - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - - + + + + + + + + + + + + + + - - - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/examples/in_progress/prover/Firstorder_semantics/why3shapes.gz b/examples/in_progress/prover/Firstorder_semantics/why3shapes.gz new file mode 100644 index 0000000000000000000000000000000000000000..87b9670a88d5507091674f0960797572a4d5b3b2 GIT binary patch literal 11628 zcmV-yEtAq8iwFP!00000|LuM2jvTpi=Ku2)dVvMv!Yg0{9t=(c0)!c3y{JEng~01t zwxpgTY3y_M>6gr^&dRD}X0f`frIwVo$Lh)pGZ>eT5kWHOiBblar6;8%7#~R3D5U|5 zl2E*I?>^>te}DDQ?!$dd@85n(AKi!K-o^Cs%eycC*uf6&{=&%KMHMY*1umozNE;wb zm{J6WSG!+d<@-;szNAkd-hNIWTzNOV{rso@{N-)9|M20@FYe2``;Whl-#U5F?H|nd zZ|mh9xKHJsKkh%LojBZj7vFyV#|MA^ekXTo$EUBC7pA1|#7?!_V@f*&&_WEkDY){&<`J{J29L?!Vc8{r$T_*GPgbcbgx5Go$TD z##y&_2s`P1`Qwj)W&8e4X*+#>AfSG?y!2*;W3NwnenNJ$#ZK;@_5V5%{FD3q?*FCp z4^OY{V0`wU1DxGDW72N7gTm+kd^OOp!yVoIg)Di6w)}(aRIouoM(aR@Bpq3NReJa( z+<%Pks)>A4y&NS}UYHt-zB})f7m~>eVG<}KR16X$3-l=~Mv(c{f4NWZO8c*33ZGK> z*b2K%Kf8|v>M7Ul-IVeolAYd}8O>5lv=-nMgQ|6S9*2wlq zLqU4yyoQi;f)KgS<$N5+Pl+3t-}EpkMkCl6n`|`TS$WV5NrRwlynVb^{9WjHCzqlJ z^d3ZvQt4a-XtXbWcwocX=HR~r9eoJ^`CZ7`L~ns@jM|telcp?yGUS+&&C!dM(R)w8 zbogH5{^99UT`1IFBl3|`a+0E{-TK9)zkf*|KUW&w|MhQw7XPtaeRIZ`$@@o6KgeNl z3a1~Kr3nIsXrnHe%@n*NsY`^)F*p~4O==!HeJ#oqGD3 z#`6m4_16~?xB^xjf&)NlMT#oQkRTS|w_w_N&`X-Uz@Ky0^sDYUBTjCgGi1+&`~3Fo z>kom7zyZ@Mu5AA#@f6TN8Ck8iL21o_WVyOZ`vT9W z^zX0SJ!cmXAdr>LrR3NLkdO#PK|lc+f^9elOFH=a`_;i%1jfdNluR9PtjRvvB1I?A z7Qu#(AW_lZag4xXJd?qO^$|9$xLy<5piy7NcQT@Ic{V8sjB$-m9sJcfRUJJV>GXVKr# z%In8|U*F{W`mQL!jDoWW7;%T^uG9{xT-;$78Iw4?ChX7XcxdUaF&{p*utQO23GVJc zx%cnq_fZZHs0KSx_Vh*#G?<>=lm=J3b7<;ro^qVDaDK@&Q%mFBH|N$d@?!TC@e$ri ze1tvX`|ICJc=@@(Qd=J&Xo=5u^oC%dfx5(JSG)7j)SCG0EyTCy#nZ&s1wviolXnf? zljtW!^^j5;?4U)h@V>NgCGT7P;{JYh0bFUYqhEThUwm!9+%F&F?n&yya4Yp;XsS<- z=^h&B0wP*B-G`>u*nG9=w)%Aii@P9+x_G<>No1~8pWi<{QG3MAv`6%e9lzawncrmI z-)%^V`;DBtaFlzDoaKs?_xf!f832L{F(zjWX>jZSz4BfeA>%g$ibE*+#18tH zqcAF3Z(^V%qE}K#$zIw(MulsDVlh$h{Q<>om>ZRVh~$9;C7*RLPWo(9of!*g&oj*5 z5l}p{sJ|vq+(y)jg^AH>DCU&dNKR6)gp?zt;#-L41d3^IYJQ;#K|alWh(V_0g@{&# zB%CMd7)hcI5h%zjdNa?OUhK^yRp$yrxTHEWOSl4Gi=G0&hNSpG~W8YAui*H73(*N9~SqVUEY1@rrn9UgqHw9aB7YDNSjLmYO;zsXSUf+?>Th zz5i?@L*a-vvK@s90w(Y zk}O5`wzwZ)9q7olsE9J8RyG7&u$IOcuOC>x3G0zAw_saqR@FjPu?#PPi(QB;v=1H~ z`ZZuZFuz?vVp)uvupXUbNm6-E#5yG(q63nOL?ESn23GD;{g{OTt>rtLHF0dR>M$&c zEPbc|XpBe(EF*#WVFsl{v2(@Pv#;EAo9@MuVEm$PY@^SRsB;8tRR&#RWZH2-I78yl4{VB$Y?Yhu8FY zA-dS>F)isa{v>*AgswYmjY~SlTDnH(5OTB$gN-H9zNE)L*KWR9UJL3PEI@vL8Hn+xjHiiU0-~2^3kIO zFMR7tw(543zk^}SmSnIg0WS)hLkt9pYsuzBt_D`wnAQ@wZ$Tyjk#{)>#TK1&2?S>u zb8=4QVpxrw)suws`kVIFU^2D4+JjRdlxD9uK~!jz7mlv6f$x(8rJGtammW(C7_yWg zK|^wWSeq%Y;lM;88r#ml3wAhf&{}C^M#}-}@|a9$bW)L=Ru?C{Zi;)ae*_bgtgVQc zGkFAwD1)_@8Od_Fm0(f9_QigN*4KxcS}y983A~fLuDP_iw>iAp*sXIa*kcX;r+oW? zi(_kTYG#378J=SSW++3pa59sKvZ$&}HYt~VS_}MMP&cxKkiEx3xY9X-6d_5Jp8b#r zxwu;38RUM^NBgD>GciOR3P8J%wMY>IA*EU(Jpi+^>z35zwe2RWnz-4W280}$(j+_j zEK~6(6DrBduw|oyi6R#Nr+A>|oa`aiDRTdhx2GIFtrooe^!0B2yp5UEW)&+P{bI#iEJZ!fLi`Gix^5Iq5_zX;I)zws zNJgV3BNcr&l35|_aoF8M*zK@eIBR@DD*xky0iPUdnWWGvNgr{R+iLjT7eesXXnQd* zx?*^}5Tjil?A0x)8Repu!nKDuXddaB=(Ll>In=HD*_ANPc8kk~p)S zzP|SvOOGU0O}A4LSDNnaCD9K}8++&Mjl?E9sZ!KF3Q95wfl4RLPDmw>2Ld_&KDj?v zoy6HQ|NZXEzt?=_dDU-y-g8-#pnq#OaOlzD-lZccxVGf}=l%VcmqX6$1yamAw=a1# z)M0vf=3^ml97xVZT_<~SEVe&M>Db}=(D@toZvDuOXCc4-cjlfRsX6)CaDc{JYo~d+ z-ztf%^L~=%44I5|C1mxEwHMASvdXZB5_X?q%?nbnqkmCVf1Wg9g(4X?N+c^KCXIDT zX!*&-^-~ud(i`)CO6?#D)2_uNfQ1F+N;sQTJs{WF0MQ2w1(-0OJEbp38k@OaW$w37 z7O%4RUX_u{G1lcIzHWYwC7iKRgSLy~*n*q3q)oUOH}t8`JU+mEgs}L*QvvHIet+b& zULvLGD-312FY>t0Ab(~SsuJ9(NM3jmY^X~=%SZ!>tS>H?vZ8(DO-z5JkMZsO$M^qu zn?I%Ww&3-`>EEThrdZthwc6*)2X-&NT%i8*p_3y8Z{K|!+bfoSeq7qw0ysQ2J-ag* z@{bkiYn7hyhuW`(8%y=Hh&W&ll@=!zNQbq9wNBywFEOo5cqq;|-sJMv>-C-_(DQ zwvr8M0HJLOG@Q4rx%}%`^c*d;tdmRUYfnx>opKMR+=I*9gC_TIm!BKPnj z_f!eWVq~ki_-n#ys^^uE(IN|}>(00<&OgL+o$ERl+@355#n}n7!${m@_H~w9jkd+? z8`*3%*GtTX;^f=pqOR+yH7kf@gz_p86Nr>w{qZTyHT8i|8VRL2p)?Xoec(bTY<+?h zcq#?HECp^#L5!Uf^UjH}bK;^D#6>B12R3^R(PA(tATa0*oPEY5vo&og++f7`N%>to zxFqVj>u7Wcfs*#@>IrlvhU(c(myTY9v-R;G7RUcnFu#p7zry%`8AkJ=^q5)JaqwtrGRLR9DL>mr)e5Mye%kys@}))@?_) zbapW6lFsY{r%Ol6UwHpX`r3?(a4Jmf)K_fl>od46t8r2Dr0qwZ#9j1#jw5!FZPyRa z_IZbAyTGcQeGHQ(2iZ3vKu)_aJGDkOaX^hcP;(xrkq4LH{O}ERdC<{yKZ}ZjgC&N# z@2UJRQ1-<&&$<7Q^IlUOxLK^e#Yj8hqwQm(ZE_JtF2bCPFme(4xCoaa6$^YiElkuT zr4A+9iIGyS_5W>xj^e$KSI$$;4tlygSUnQoz6QKq;xQ$gxp+lIF(m>fFTof=N|84u zz=ZWU@`l+3dv_JfAL#;p4G-v|T60h`Yw}oh8nm^}Yne>s;x-7j;$qNvox1&8%rznc zMwUXjh}K3y7;@dm!Z8SAI_iaf^|Aj3kg}KYv!O{9?v*NZo$oRc@3T2Dhi_a?GL!*F zJ7s(V4B*ii86p5nCy=Za3rU?DL*mp4zKup*pW4G*Nk*tk5ZXqZc=;w(@PQovOn+q{emA zF11q2*R;y;!oFI;IrHt*LWY$`YutZWi8O?b&to9tCk9WxaWMOEuz2&F>)}?j8eF+n z%N32kYFVwGeo`F>?plXh9;j#(Iv7sRw(dR@x4t~EKgxND)YhSxC+~~>k;%=6%;Y1D z^AlzbnTGMz>&MhgZD}<*Gcv{wjAqpD4 zEp=JG;3Wkg2-}I4^t z2A~?Mr+B9(esbwym+C3GWB`f=DjH??hFgV-MzEm@JI(P|;l1giqI`&&QnW`Y+J+SE zQHr)line}dS&E8oVgL#&>vRjj>a7x}H4sb}-~5PR8q2R9)@dqjwpgc+PL6IkIr`}2 z=pH9WbN$W=>+lf<@cXA_{nyJLj&683y7c(y;pozdKK(1RJjvfYbZ5mXV zojI>7X#%311}nush04svpokm8L1z*V~TFX?tdRnR zkVq?k&8e+wcFC^d-7!bDv*W4v(?h)Xoi3yNLyT3ldKQAg@pe5OvnSuB&k8@oP=osT zd$9Fp_H^Qpl^Q ze$9u(@f*#O{O1i}Lw5E0amXJs+Fgm)I;q(_A)wOLPACuL>@(iy+2113vy2dE!hzQg`1Ue!D^&kR08jxuU$kYYM)C6Q20h#82 zOd}vu43 z7G3#oQcbhaqgl-Ce7wosR({DWSgQziCvHT_Yq(VtcD@&Y#4qj}D>8IHH9Tc5AM28QwDJe%W!<89h6QNOq-93G1eJl&JTUBMAI_v!Pv z--74+EqL5-!9Dve`0_4&p)Hsoqb#Gg@+CAS@Tir`C=(gme?rF-XXOtIi?><%=a`iT z;p@)zn%kC|fa(s>oPDGc)05Wj8_&wG%6^-bf7-0PGuqdBF&eY70YwPGsFbu5E`yJ^ znw4*D_qf6%Z|*kPJo0bok*^u$=8-?qBliJ>Q95vzXi~^QQs6S$N}F@Y4BM>yOPzjP zHH&Tf@oCeKUL}b-S%ILe6EZ2A(Aca(P{m$&o0Z?p;wLnVV1pnVUBb*<%z~n})=<*X zP=<>$9lf*if8FK}U)cQNs#R_ChfkY7)X7CJv+#yOamS>Il#(}DSOlv=|5U}2?QFC1 zn^paER#l=H(lK+gL9r^9lxwaDbFC}|F^e0`%CFd4SGr-F0Nm0IKTo%3qov*k#P%FGdl`R=xbUQ|=3?-|+I-2Pf z-)zz6+~d``qT6YjwYrPFY1Rcrzqzhmqv(A6_^iSl9B+?vju$@8k5=?)>HO}TaZAz1 z!uj)j@pzNFv&9#;I0!2kl<>~`lt2raG)C4YdZV0>eQ{e0YVGZjb|FI1%X8BD8Rn$* zSDKSvGx=sAxqUd+C?rQG8F;!P1;1eOM|_*7;o*3jx)br&nEcIS!N-PUQ*VvCbeNmo z8js!@&%HGsy*2Lf6Zo>X#+jTpI{E~Hvo^t^_rm+)y#!cM)ZAeLxbn+Hd&LV)^VzI9mi>>MT7K%MB6f<795MxH8 zl#0PPBa|Q{UBWY)1#F?%7K(lSP;AZOw@B=Xkyx>J$I=^RFhn%WE*jR>A*&$at8G`U z<@2|_s?V`kRd~>n*%3c$=y&LgZe|CEIX!mNK zmI;g}kIom^jW@Y_dELcjAKH3CF8F6%Cf1rm5Gp(EV~Qe~J`-pyJldN;W8G2JOLJln zy+eh)JJE{a7?&+Mb@Sv@Oe7Ko>9Td&8Ai{nyr+adI-xtKo4%1w4Cm==N^x_gNLK1Az(3d& z*!WBoIS7y8RH&z&o_LTY z0z0#l4gaY=k1cepFEp^x);^Cw2@n0g#M;{Na~mwY9rqgJe6KN%dyTOtnnzmFglVvj zUBNmwgLNE(b({z5I0oz36RhLqVBLd_U_ALO6*<&0n-Z~?p|EI!Pu{=U{rajj_v%4% z13nkc_>WPBZ)5r+eT;AKKfeFRNXV~l`Gs@sX+BZ($ld*Z_uISoH)!eg+7o!W5gb~X z4USdp(+%-mS~|2pjHoT)-%eEz-=XPuW~+7%56u?m?5~d*?AH37!z0aLsSOTxk%^D8 z9sBIIWACa8{(ArM^KQ3mWHe>1g)yPLXJY)o@#gF}jb{soq#}A*mJVkDK z*dPre*9lRtmE$Z0vW=>Ei*D&Glc(6?gXaVX18*^Qy5^>54avU0&1E+@F1x|`vKt(i z-C)PEn+J2boM#Urc>zjDB{6!4&XJIybSyDOGHKOmxv?)WDayNN`Jm9Y;zCoUrx6_X zL~tY0w3t7JaX1g-a17(HBaAzI=5j2Tp*S?D3~Ev*sJo3cJ7r{`5R}z=VYU8KF#V@w zvk9TZ#{tO4=%PrdgtJg<6$&7CMNO5jKL|Ai@<^#a=NMk4eXU+yJ(f-c{+t8q;WL*# z(h{3ki;)o}ra;<9kJi`v{)m8TJ>a_`c1|6&n<&`T7QYw&a~k{JkGf95rh8kkC+RYg z{JbyY1{a)faKUkd3wGp2CZ5&0f+3S74Wia7F2ldZppA1i047QzE}Y(TE1!Q;r5{L@ zpv2B#WzssaBJu%p(J0pFvFMb44)6IEk?d{8zi$!A-o$!dY`A%y^?diSX9TNUajm74nz^U=?(=oIr;`_&c6R>6Qts(dExlfQqG_?SN4DJ4mV5dU?O$f2 zd^Xx58u0bNOjkxv%0Y`%?0;#y@l$N^C&)dOaNLx@NdQZ-DQWM7(#l7rLIz)bk}dc2 zY)KIjGNCCE1tF4gStu|*%BtB>2?ty5=_YJ;Dyl##8G#YV1EiG8|7Xj>6Wg@qp0?c6 zV{%W@OBFQS z0>#Dz=OXGL9A%A?UB|ko`!D~VKD~`8|2kIySqu1_8O(?DVORTqAf%}%X1sOpOsayzq%K>c3zg9`rlZU?7=ECFuH)__1$ESZ#cA%L|u`4m(H zg%_(jJWV$99Ktz$D2yd9rMJ1Rs?#Mp$yojq)^mulzoycYx!AI4StNT-aZ0QpYQrGw zsR_xHsMTbj6sr_iU95@l!ql?2+t$aBOj61_OYDsI?CR0j$r}zPiH`j9MGW|*sb_z^ zFxswRfLUnPbT!)?#M%v(!EL=k-GKqK0ix&9UHJ7NB!LTN;8abkgE- zaigcn<}wC=M#X_;ju4}g0zfBlHslc4IEzoAZ`BX$q%Ws}m&WEOty7d^VstW7fdTa7 zO}NH+Y-`ne4=&P|vy=5aVF2Y^z=&nQwo-T$zBo7eUNK!f1_?| zT?^H787NZec~)G+tP+4hr>w)J!v?SDM;~Lpa<`L0j=@WlbMiKDLO{sHt6?J6X7rjr z|L6Vt^x^IB=G!ly+{e$Ag7j%dxBL93FC zV`4%SE;SBMeK=#UhN|W)3@JZKtAD)Be|{Xop7V>7w(ITJzl|KL+fycu9bWn4Q;Pez zcKkVM0_z(y8SaZTH_^`k0npcN+9u9Nmp(@SN%Z)qmP;zFy*|BH158+mx9v`jo z-06F(#GkxZw_>-&w`coUYUuQ`oNbPsN`3y;a8+JWkLVYd{{AI>{9H}`{a^p~XANM@ zNy(nE!^ZvF{fBgNh^~FObk}_TxBHK2`f&aIrY!>f#*H58U^hd^z9{0l_prG)Yp5(Z zC#IgXdz2l?Yqk@s_Uu}^N5j2|Ia6Wy9`Z`dp+f$idtCZ^8R2&FO+UzuUz)&b{a69<-_=^4 zzRP!%M!Unq@u{_%@+fojP*8bY<_C=)=Ehg38xv9GxxW-Y&--A577B!oDG>lm?MWyE zYs}ideKjN*FCc##0h{mD7Y>?fhScuDn{B&-Avd?y=EzVx%o!~|I<*%(d25a6leY@} zYoMtgGHs_;1+$#o)P`m+4Tc3>sk(iZt_7KVlG7Z4jrZDwdV+Nims*g?XOJmQAoGOx z)B?;Ux$5>t|6z}73+f-e&%cS5bu0dxqfVMBSYitW4{|&eb{i{U2`hEoFujC^g-;8& zbiFfi%33I?e;AOYeHntIs5^@i96(ZB1Crh*c5I?mL!L27&xSc9TLOBYvT9bs*#vzP zK@a#eodOwtbqjhw2huBO$wFwQQAL?BBbR@(w8}>vSv%D(d9-ZzuQzr0uGK-i6paem zVNirIM$`!`>7MEyp(38^5Q-M zKmL*rF5IQb>4lgMhX`r(QYIy7HhuiI`l$CQiAiRm@05mvK3)~dMW-AZAOl&4f?5Vd z(Mrt-q86NmwNP$wrx$Cl4PQGq;r(XTTrN(;6 z=d`2N`CNMgYuM4FkLOylBQ>!jwb{`Nv7^Ck9&-rV!vy429+C)>HL^s7Hl$jITPkp% zR1!KmIkBU5roU+~n|*Eewb@s-FNjIhdI&CSkRYu|C_R|qAUkK-H^!;PES+r5()Cmv z9x_m`ueV(_w_Wv>ZMSt0_1>sk3oIUc4)v1l>WS^@&30dk?c#o-?r6K6r+pu6m#?v1 z8wDqAB2e_~m1bpvLYK=g>1}NJn5}tv*`Al*tar2C&3d2DdW{jvr_3@clOsFO#bisI z=uu{YbSZm%(}g>)R{`Q%EZlhns5BSud{t0+Q44oAPpACP0YW&G5gMi4wKoHsz)mrJrtI?9AP%^IL&#eEDM~I1?ZjjDeQc1mLDmLY8)QA#E)0sI zmLy0hS+Gvh2g46Wv`1K-z{vkmMvu-m}y2LL;RK$fBr+EDSyoN{$i z3#`_Z3JmHe@5^0;x@}+Xwl8-B$qgjG1CXSw8Myd>q)l{A>Ux+wfb(Rm$#h; zK6$M!T3CVBIcUVzrq!of2fovePB50_fdD$bx)o2V4Q#DT!`~d$(oSn0&`J5| - - + + - + - + - + - - - + + + - - - + + + - + - + - + - + - + - + - + - + - - - + + + - - - + + + - - - + + + - - - + + + - + - - - + + + - - - + + + - - - + + + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - - + + - + - + - + - + - + diff --git a/examples/in_progress/prover/Firstorder_symbol_spec/why3shapes.gz b/examples/in_progress/prover/Firstorder_symbol_spec/why3shapes.gz new file mode 100644 index 0000000000000000000000000000000000000000..2ea2418391254b0c3c4fda57ffaec46459354b07 GIT binary patch literal 1832 zcmV+@2iN!?iwFP!00000|Fv03kK;BIz57@6Jr{1p1xP-8!5{_(2yzMFYokaOCkDFh ziS21*^6OLHWXYy1soQh$A{SXtubyh5L(%~aA}I~lAW_gtWtpR*7`4Zz#iysT-aKuW z|I+i<^>(>izR~jwy}sh}_WNsGzuL={9Y;AUAL5s%oHWiN~gPRJl# zEQ*3R6pS#C65qZGrIFq8%U`?hUB~YO8m!0aqR7$Vy)2o}tn)HPASekiB}-Q34B2X7 zgoNzRfY&d}vfEak(i$sg#HU3Su9`1L8wS;}UC7GKd}OyzH&1f^ZkG%*xG$Ujv0l;5 z<~35TmNrqiO<@AJ>sMOn2{3-Wg)kuK8y^pWe2Zfe&qHAU+`sX2HlO+AEQ?ekNKZLC zDE3}%Sd2k$JbG(GL8-J3$*Cl@ z4V}J*o_BxI>a_iX8!WCAh)$vR(G{e`^`0L)t{gUCCZC!<^5Fb{# zfmkoxhj!5BqJjgbG70Mp_q@fEDk4YBX#9w-^z?V_aP87 z_x?I2V}Y|}(8gpHP07s2h*tFu0aa{QePkWxgkJUWPPmL{9fLt2>$KI81Zz4dFO+w| zC&YWS3^%KNh$l3d^(`hc^bmjZnaM($!ed;BCOS<*pyG*&oD^PhMjBajN3@E4DC+U8 z7KaI~mJ7YImJ^PQ$)>Ec;_1RL z2tyeHG2tC@+mH2q_jjJ27M3cDW0&%PWUR-;PnRP|P?F){gjBRrA>V)z-4nPr_`w6X zyV;@zV``#lEuGI&h=J!hD=8(#dM1Y;z(^2^MR1u^nuF`F8`{$5jdyJw$2X9xNA#Vv z-*<{XpB0y7@KU?tRe>Cm(U}K5FRVy}QD4oPWkdA*#yh0-YP;KfONW0Bma8|~?5Q|y z+&gvd!F;Y?W>!>5!h-kN8zmxm5m});XDUrz=HuU>+>aK$3O|BSkQy@-lt+q<|)c&eg!Fa2`&XqjHS>MGrGjp?uj+KA>7gr1%5{k*T7>2mN5wHf{#fA z<)jpd-~vKnuuq(GS+V)hagXxQ!U5xPNFKH=6wQrxP{=7z7H2Y#0g8w42=K(!WLE+5 zLq+&`lnCFa7%Wj+C5z0KG$+ zFb^f75H0sfXk;#c93q_{NCN9p@lCpIpwi#pmT&k%t3>;DuX+|z8Ol1Dwq>AO2A2}C zA7OcjWNh3b1_vlJ3NGf_Ysx`-XNuLNhrreU92t$yv<%wJwG5zT0B!g%|Glp#mc75I z8bh`P(zab#W+-uQTPR=w3(S>u+3Uhxu8}-V=v;0X%Cy;6sA*BW6QmmA4z2T9kP=+6 z65W1qjF4e}^lwGBm<=U265~)Xq2=`|6t|JPqIJ;V<~DnSds){TWsY1;Y_6px*S-N) Wxq&NfK1ys?q5BWLqs@kFBLD!Us*b4u literal 0 HcmV?d00001 diff --git a/examples/in_progress/prover/Firstorder_tableau_spec/why3session.xml b/examples/in_progress/prover/Firstorder_tableau_spec/why3session.xml index 56817b0b5..3bc555482 100644 --- a/examples/in_progress/prover/Firstorder_tableau_spec/why3session.xml +++ b/examples/in_progress/prover/Firstorder_tableau_spec/why3session.xml @@ -1,1179 +1,169 @@ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/examples/in_progress/prover/Firstorder_tableau_spec/why3shapes.gz b/examples/in_progress/prover/Firstorder_tableau_spec/why3shapes.gz new file mode 100644 index 0000000000000000000000000000000000000000..7b5b1e265e423a48b7874c73fde97e82c7c531bd GIT binary patch literal 5257 zcmV;46n5($iwFP!00000|Lt8{Z{;|Sey?9q@B1R^E?|4HgGL7kP}l|L!LNa?Jprnc zo+RCv*})KB{D;qCe1@#$^&bJ}qA z?nva9IF8kp`hT9C@8W;x?vwCw77=N2`C0u%4{eYA%`Q9CL5Dli(Zvn@vLo(e3o>5d*ff#LHR#{ZY0qR^__-7Fz7`Em z>T~%^$ICr+d_yONNn@o+V`bW-)=t!m=@q>!D`H?yXvc7bHS-`PID)YTW@cO5DeQU7|yM|ThPMWn_hD%ewpHbdq7Jzhs z^AAq#0!%su{N+G*_w4JxznSN+iDJ#}N7`@xL*u~sT&Ql4+EE;q^v+N?!Z1r+@-I7%s2oKjB$0bq(+IL0%(f%ahAceC9S z&-A{Ghs-z!XynGXBeCY7uh(tWZx_(F!)C%n2A?@*NQs*rvAl*rO+zvsU@bUUVsi)D z>~MPE=6EX3>yFM9N0QeH)}uM26)ek$DsexMxE9n;8GZ_NXOy=ghSvzZ#Z+m^2}fAR zWebbz7dnOdW@p+8vy{9~aW=iNg75FwZ_NQ0@vSJ@oi|9aUAwcPPVP;q#s1#;qPwXSiOv(Q2Y-lc~$WKQfU=(I!AoHHA&~-u=8zguY zIQLR8Wu(*;d7+4446FeDInK(PeSUI-5&MzWW53di(U!5CAssES6)ZrIN^umd@Wg4R zB>w!DetFbSZ=apFFJ8a;pHhhFybSVW(I$wyyHAv1XEiktqfg*OdV~Yl!E!*BSa05s zL~s7!<_|uWKX})3F*gKUf@Ut7Ne0qu&wP-9N)6r-6d~lNp=vD^mq-4i+p|7iA6P{z z@n+NW6+3Y>GAlGlnMQ}}kK=-#^;x;vvlmY2DeMUd8@!SPyb+puqKUAASVE}vi`42L zFaFiP{N*QggG8Lkuh}HqoR_IEH$HtoeX=nH$3{wvTSbbQq!`W7nfRfV;gIEUNI|sZ zG|@^-919pl`4Z%b=Rj0kReB*cCLWtvt~R`Q{}4l*Xri88-(LQ-Lvif!=`a8C+OIQr z3VD=x7$o=j_!y4E-TnLD(Ho0_$=Aa(N79c^M^>YAyx;cZ(sT2>*0!jm3%rjVE<|K8 z7+IeNnV*K0ClghZ9c!3@9N!TGE#qE$biuQ#k5=VJ+w>$Y4t0?wJp4d=P79!-GxJ#n z6`a)V5sCeXw>>`u#Sy>Oa%oL)R0XU&<%miL3bbO32;)llEkQOj@vJ`a(OCYLlNqf) z8tvnDnZb(8VE^-fSXh%@snMx|zp~(w4?`V|ocHi}A>YsmPks^+$8|w9;;;cz+eUz4m`#p^6 z_I_tpbrXR-nia#yTEv;B1c>ws2j&d%K16e?4Xc~g8Gtjh&l+YwZ&=CEu&zCOw5;1F z;EJa86lq`snoAbf8_;hqvW#)+Tr{%U#w8`jC29Qe^8APXUB6`_({(GKxUf7=RWA|e zYPV>)b~mLa^JPw^tE^3Jq!+v9^``5+?o3*pO6-eOW@2q7Y1>Ses(xF{)zR?WeKMLV zr?reLs}PhTI$*8AaM|xRq^3z{=RrUPKZ$)wAcN={A-{CZ3Z^(kMZ zyGUc7j!Ym8)l~$bab&;rsbjSCnteVt-uPS6<&c3+`s@JTjrS){@+o&iZaU@g%a|Pf z;=@~4wrcwX7OsRY;fi^RSE5RyjV#NCTq22UoG|R;mU`b^WmXua=aTB$rS+%8XxRJn;s`$$UY?S9< z8J}cm220AnOgKCPmJI5vX-LP%Xl{HA4>xLni)|R$4oepK#93G}Si+K$6qbw^L`x&f zteT>Ya@#nk6gpN9O_=C+_Z=8+$mLF}nY3r0mI{^|qSvc~xj2GL!FWqGU{(^|k&OfQ)_q9lAw_NKtAFb9Y3d_9lrL|6_ z{z-mGH~q8@TC5CuzDkkX%1fs$br!3#iXXTpFPC6siS_c5H?<*&n(=Hhfett7de-m# zJ4MgN#YyaIl1?BeX&T_Qp(jyy9DQp6Z*#=H+_89;dR=wVut}-vrVA#v3ukQ?sNqIc zTVf-8it)mU@q&rw8wPh@Mb`=(vB^10XnH~XF?GI^}=tJgWj5+!9rT&P9B4A9FPCYfm^Ng~7wh z#<*q4v9NuAobg0vm|j3;D@vS`8R;-juVzw7m9x*@&+eWqvy8a<^*ugGQYFyz3;C8r zaj9gJ7t#fQMK%Hpbp+C@nHb=HQY@L@-6*7zt>XQM5w=T*lyKCru@?>brJU#D(@R{A zg{oi0I0hp4?h`VYTdSqx&RWF@#g;~2g(-N=DEIUC*nXh98DGJ{`*#!>@*W|rgZ5aV zJ_{0*Bu-JQ1joUi_KxB?Q=9TQc}*xX1>A9qwN+M86$FR=O;Fpv+pYxrtY2UKOFzen zM}zZ$2Y3_kRKHIkxtIcLLYOY@UI=!qlc&HAO4`-%-T~^^>5?^|3GvpTC{N)K#Mn+) zk3tY02Y{?(FW~oz<1Ls}+`rM8UQMM(Qql{*M=t93`0!nv6GU9}d(i0j3U8p2Y;WH` zpj2r*xeC8!IQfI&SBxI73_s4CvkEco4Z#c?;+h6yg>eK~A!QbR;sWqnS-9lj7tyLF zS5xWn6{Q(ooW9CZA|jbY-h85W!%S6qG9h%1|MJNfI=oj8o|vY6yqQ z#U+Xem0daGGN$DXzO#x6m*%9l*AepgSka!LMBL6~rSa4s&9@uybjLxp+liB+7j;rK z>j4`i2Wz6Md#DxBd>mopjIf8#P;C%4Ia%0Q?^YG@+Dn^r5m)w0lwI4;AYGLaF6z`4 z*`kfIExN^;RAu`Nw0xuh4Ow^6YvZq z^_p|5qSp${c!~g-zCf;m1OE{Le_N29y&(HA_`g~An{~fg_wu$F>WvD-Nh)=~oN5}p zWkNeJG2q9SC^B7PZS^sf^X6x6e&*(9ehTT{{LHy&1B*2^MtZCb3&D%Pjps60>YPw| zOIhsjZ(0{y8$j7B6;%1m%Gf*LrT&`islaMxv(~!eB@-i6{#;$Fn{4q)=laREiMeux z?4yW0>noEf#VsOVb(R$`b%wWW6!g{VWFJJvS&un(t6C(y>N2;O*+!q)HVf~(TBbz6 zl1S^lmevNtybj!XYB-?+bXczF-hsnf*2@BQLK|l(Xs4JU)N)3(Qi6e(#K60(mr>6I zQgP-D0vZHI#9Bk0a)LR<5u4^pZ%F4gA7uX3azCN!60F{6_haP$cI#n zn;So4)%!tYd;|aa;J2OzrxOkN7+@v7Of<7h|kG9)J-{^-xQX+7?&f9+V@Z9Fl3 zfB%$E#$TYOaEv$bI)tag#Jh=Gt!QJiT6muygCp+B8q&YII~^CtMGsmI#UtK)>%~oQw z0~wW_KsiKs`wP*3QlPdQDr!=+oI4iBnK;0pcn2@<996%3i{^9((&%<2!auSM1>FIh z=nfS3wI1oAEb>i%!~C#7kb*N7&d^#wjOSvW2~(oNJS` zoxOG-uq+TD{qQsHj{sw2sY zR>rGl5R$w%!Y~}ydALIHs+CDHg>^n_GaS4Es(cp>N2I*VrOt9OG1{xRm}oi6yFU(9 zW`h7CQd(kr5YQ9Y6a;MVgtT^YS)L2iby=Rz2m+S8tdH=FAb=E%%Q|}vK|p?zwzJoS z0g=T(v^-;uCa$U1US~-T_$`o9DJgZTYo;ZKdMWxPhf35|N+oxhFn1RHlE2H)uQ}OD z=N+Z(W2rgWQBZZR8eKnS#i?lLsztd~RPKz|XB|zx6i?$-3+iaz^ML3NO+H@nc-6of zokDn#gqOp2Wm)zHAC77H7#^OE7AekiJ!?#5wtf@|sg#h~?%t`&8R!-FzP%ID+R0^k zE=<>Dc|OCvFL_xX;Ti6o77WNbdkyYAKS|r!s{=sg3#c6%)4e!e)Ut1^P>Agqq;%j^ z$ID9Y@>29m?vlY)N+oBQFn1RHk~hoHues1l=N;qiW2w1NR@lIj z$7s&8C6BqkYIAAL)*RK97EoSmA=TQGcZbN-7m3#0AwQee3P8$BBoVVp5gDYkCJ4iW z3Y?k%^EYX#Mr(BnRhJVfN%e?kRc+B^Q%Fp*_9j!a`Cafpr9KtO&%5MZthINI+Eq?Ti>w8sG4SPaSounGuHSs>g{a6`d6 PL&5(8JDUpYC&d5&Dy%_! literal 0 HcmV?d00001 diff --git a/examples/in_progress/prover/Firstorder_term_spec/why3session.xml b/examples/in_progress/prover/Firstorder_term_spec/why3session.xml index 97f63719e..ca8523856 100644 --- a/examples/in_progress/prover/Firstorder_term_spec/why3session.xml +++ b/examples/in_progress/prover/Firstorder_term_spec/why3session.xml @@ -1,3210 +1,460 @@ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/examples/in_progress/prover/Firstorder_term_spec/why3shapes.gz b/examples/in_progress/prover/Firstorder_term_spec/why3shapes.gz new file mode 100644 index 0000000000000000000000000000000000000000..d0e067f2844f9266a0ac4ce892420b1a609b6473 GIT binary patch literal 11860 zcmY+nV~{3I7q#1*wr%5X+t##g+qP}nwr$(yw5@5|-QPTKoD=6e`D0g9Mny(u?RBjc zNe~4I^uO_Q^pXADs7s6B7NF39_>)&W zy!4XC@574=f3%--OXYc+YAFE=TEas4w>ok-E8plcee50;-|R-eSKC)@H#3XB)BO94 zhPvy`nb}J3=L6y6?L{zsy3X(0!!WynhwwpHe9j$mz;a)G5qys3H2iwHoqj**?eK1i zpTBd?FZ=c7Z7CZ6a|V|m6QTOC4V1GV7~!#hQf?+qDU7H`td5_dC+}hz=JCbALCvt0 zTH)p|6?NMnk>sioDKhh4?h>E-hkj~Qf>%YuB@F5_-1Fw*WysoWMpn9zld zS*&UqU6UQIWcQirg+U5u+mkcdzb;p?G0Nac*4jS&B6Dacx#}n>$&nB!fkS77B2|MK zD<>CgbJq*S@fP|IYkr$`yL@~x&*wj4)p?FbkAiUkS|53fW9v;{*8RTT5IMc18TP)P zFa94JU%v!ff*m5XXe^Lm!qY){viAKQtkJ|N;>DBM?qjARlbv_<;7+#RYr z^S)K3+ZvubaiK(#IDP+f%*3iuRP{x|z~1u9L;jy9n`w}bU9>M7CC8dQ5b%rZx2}+*|!>W z>GlaNO=U8Xxb|JWNdV*|{K< zEx$TYG>?-VL8_~>kf?t#Y3=+HBpPs{TZvnks4tGxxKg|~+=d^u6k=D)4H{kY9U80g zLJ|7!+sH`>+LvIpXPg_%@_qCmR}s6wo*=sJK6THO0A3)a<}#qWa?rik7IdGrW;VxpMMcsLe~jrf0qKJ^la$j zd~J~$gAi3!gD+@vC#&8xD}98GAMb7YRUXbN4@bM1%}YDBb1jb?g9Ce}GUr1hCN*W% z0nmB;Ixz6M;u!W&3NlC`Dp0y#!H~h&Qq3yCu6rS6KWzJhJk68wZ$_rd-mQoXTRY!F z+(I<+c0S3ooTEHQ31C6z2uR5w3&6Z{4n@)j+RExg-hk&%COrObr_r_UdtZp=XFPLDA^WBz*S9l|@+=`2CoE&UJIkjH(9IO$x>NiQ zTD~@M!BdFzxHG6+FO@Buz$Ba_NA_49U>RbUMzvwDgPOr3qGXq?GE5P3CPL<2lbz(my&JJHnqei`K#fQOrFl+~;t`&9>0dYp%aZd?%Ujg5p?L&GIi)LO z(PhC6sq0ekm4n+x)OE})zT~88RhS_zlnGd5iseQXa8!Q@JFp{feI-8MPWb%pe}CLY zI^Sx0KHbXN*KbL|K&PLI-3efV3S)tY<2};*Wzff+EVb!*+v^3sVf)^`;WeFctb7uN zy3pmM6U+7Ua>*-bmS9Oh1qa8McE>5W;WP!sc&ucnPsWfZatR&FUktIV3B+Sc8j3&z zBK&&T4$xlD)p!@&66zwl)h0cvkR*&1Mdo;q6&VVfe~Xyd~)@^te`N+-ma2>sStZ65SQi1Ni19kuM#>n6{rwKP1cl+_A zWv7fu6D(p9_t(OhcdsXcL>XAb54&e#;sKzZ3Oio)kVtbG4R|3bpx|Ss1y#iFhdLuTZf*j z#4LKX9uv(?Bl)|ZgT1WFP@7Y-1uY0rlmNITV9sXbRX=FE(o17$2L}`QJR$T@GdRgO z)1_3WWU zJ0VF!vl)_&s!u26MOH{Ftu z>eNh+w5CZ0W&Fx@(tG513}$1TYm?$ycPmLh5ekwcPbooN_5=hX5QoI9K1+L2eGVX-Ogs%MtDJDHNW5KeFChdd5A2}ZNyf`LUqBKDw>3?+@7z;!WW493cc zEcDa7eeUO^=m#!&-_Auw8eqkPs+$HSNi^GcN3j!#dZFBS>+@3(Ml}U@jNZ`qt7H3~b!RMYCOUDN~1c#|@af5>p|I3*~Sp6Xmx=Ss1y| zm^4;Uta;4&lD%}8Dq=IP zVCcoWz*6>qy9M>Z=`Jl#QN;8(s5bzVqsd}L5FtkdV)Yp_I;K?pVF)g&d%cZY8ojPj8<{E=1%g_?4lZUvt&)qu<@6D+XBbAi;yno;ZtWVI&qeSxCRBdtFPn zV!rXK?_g$wKE*pG(md{X0#2mj7>z&^Bm{)O#SnFK;>*`T7GDxi?gOPCHG@1%1g$^v zi&$CH9;eSRK|4-zAG4U)_|Z>rUVQSAy=ytbm>;9xK3@8@BX@JU;x*aX=5a}YlO#Co z7mE!7+7kR(7Yv~VkSdkbCeY_}9!sMh4ZY~}=o)pRdi^9Zv+R1EN83a4L4F(4|BmD| zT6&V#EOsNINhaZ8zdnDTBLO2Qpw~QPEQx{yujH_yZYH)i_DqJJu>-XPt0!M zv4$epm2=W@LcL}++RG&51-1OXzvEt6a#Wy;s#XhSM&)iLbiR_JvJ$qplTEu7PUn~L zmk6YAH1~|4{V_>S5kWc)yqk*-2;M;yRKk>W-lZMC@6#VK4xRy|0t@++Dn%j&uDfhVw zrsSu56JjWgUEm&Y2s+J(?TYc~9DUvo%MZ)0<%IzrA1!kV^Mbe@pPR0Y`<<=Vj@5HJ z5V&UJbSJ_km#_~-v<|OIxt?+fVr3o(_SGs0H|8iuGQ0*r18Ic@b0+(b|?G3`YI;V-J z`&bD=G{fI)-dMWN~4Dp?=KUlXobf${0pOE7 zPqZfk>g-7J371JszP4ilMb>zm3PVrdB*A}T(Jx2u_yPF- z(l9HKyB#f@a6BNBDBI zaDPcWW1L?PjK;99{K8jP`}usvDADp6`X2p!gm6jhdgGhLQh&y@hL>M6u64U>SPz_{6CsgNiR-^Gg=a@iwZryH~s>l^{fW${tm35>6xKRBRGa zCK@H`r3G)8Mhy!k*#%K5m4+|^xz(B07kK02y6DP#k`s4hP3Tv2bx|}KSWY+K!)T7z zBbzWu}K9drF4=^ziwe3x|YJlTcvP zOP<|Tjk31(y+iu)TEdSt^N6b~H=FCOSn7|f_j0QDD(;xKakjpysM#y1l^@AX9Pz_I z3rOIwg&xJB5^@#AN>8h7>DVj^hS&d!xs8aRem--i3hXkQJqF0TO#h$LWbP22E=k5jamN}`}bq$cD@}^`iicVrJ5QSth z=swNTz$``;i7k4C967pg7A4JnI<0;(D=%*MS*07KYWU9bvJh5bhsq)X{L);-exUWV zx7&%g9h}TN#5Py-{g8VwLBY|$q5147+ zgS|ILUF;^IATsNxCn2u*0;k1!>W-wh7-2nktjf)}yZTMZia)jsuyO0L5b0Wn>% z4`v&O2~>eU#fOpW2YQdc0q2ul=)&@hz;2S3pu(RD#P8sBZw+ZL{7^_ZS#(bh7IPo$ zHHl;|&P-5wRgksBbSS?O!{S|s)&qC1TY>xLA=G?rz*k+L6D`G5>kcEu3WkcJY=H-y zbb{L>Uy*C7!(i2;M*3cD(%}#aV@XEsqcg{wUiLb`vsDc}EXbOpZrT$KjUw5}Ide20 zjVh0);jrk-ZEZcig%dr=QhhaZUmE0T5-YT!xhY#>$k^>twX)&2KQ0}Yi7eEBsIlgr zJum}(NvmH#krRj}+@TdS$)6g#D6{og&{kr*i zG$AD^I&z^QvyjpgDTsoEix9CIH0&>HAz>Eqq4J2t-^XwcqmLo_n8a@pgDY6-q zux-jXnIOyIThON@?gj0F8<5?(e@osgb8C&Olx+F_T)-z$V^l-X(f?@Fjx1JxmJIEuC(%(>gsVZGJUOXprb@>Q>O zDaqW5Ty%#Dv6|Af{PUW149I z3uqZAmS<0ccco8mfjPnevvZs2wmO+B%}`JT^dRz#iw7+VD#RGJ`|Aca?^ttq-Ix67 zOs$$5Qyv3}nBI%e4Bh8rkOfgmC_1KbtVFkc|Krj(=BveuW194hO6%FX@3Mcn4(Qy9LtJm84w>=3Vw`+UKuDR`#4$%4a(W%(18YBEQR_ zQ?D_5L;#@Iww$O6*|Y-;14XfES@Ab?Eem71R2TV$k$i3d#`IQ-YSOqcktNZRlrkAa z(6~?&i3dP)j3M%yAZi>RrnqL0)^xl#sFaY;=dG7je#der&VO|+P9us)0iriVCO)XZ zo3e|=i@nR*3Ilb}*_Ypx6y=G^nza3g6KLyocZ0xqX?xOnC**mbtu%5}jvOKW@@(oQ zU4y>~-8}waysYI$Y825+VJNb(DH~k;y|unhu+H-e7Imsa2=~Zm$lX*JdOSJr%*c~{ zZzy&faW;~<a~Z?t>nmP8f(}jraJxowr}9ulM25gid0l^D zN!vJG&uU-uwRq7deb6McDm6C3&x)Thg4~ofzwC_>arH%XhiSLyU5Rlw{NZcu#C11q zg+i|{G7Ee6I6=?8Zjp^JD}9}TjOk3t*k`%(jaawG-65FF9haM(?fT4tlMg?Lb z3-sIf)vOE#$~G3%VBn`-?t7ZjFVFRL>G%2!B=<{`CRh~+Pykj05%mKG2+NW;*)8g> z9jD zl+g&&RKVvC8D0PB>o0wlhKHP-TOBm!Y`;c}w6=!w4PcIcQ-C#$yOOb0LGC$q1w?uE z4r2vmuMta*>Gy+P5@$%p$jid>;$5^Efz0E+Crvcpo_kx$G=CM;_3H_A_RbP%*3^BO zVHay3g2g;SQwic5x8S?%-PVGN~}@;I^6DrXsht6<)#PGpbA@b=qL za3C=5`)T&ug-yu>NSvU%T0qI>iuKxK0!6`4YjG1#X&fJyb zr+p_iju2u8p!eB)Y_Nfk^IUnF(0S%WOKer^MjOPk$|TNt)|pyy)rR8K*YYt1%qL^z z%kAKR9w z8dBL|;sqj=EEt|YP1ka#_IVk%b!c-xb2Q8fN$8xoo2L(_*8C#LRr*a^f=?0I{Vm}9 zcUpGYZ~_mk=)CMX>d5(iroCVV@Bz3wfTI*udXN}F!2zDE>-z|Kv|zO{&g?6I2kUFH zs0;?XG&=Y&hDBp%JNk$YqJMmGcs{{zpvli7lQ5Tc4T*Jm<;BMG+JWAO;&dcJ<$*Kx zvgM1Z#TBUv7cC>(m1ZYy=JRa5hVX35AHhvG`Xxeo))g5+i=xJZ5g4DGTN06ilxHN~ zr5Cjwa6&cf^l&9Em7Zhw}wA$oHXR5Ml|H4X!E2cat|bIdg36I>{C0jL2t(b+C`ES zD!!vHEYra6{e=`1u0s*-9XRC6G1=^5Wt^4q^(5 z^ldOpkL*$>jvQ(D-s3ElCQf3^Iy79j)aopxaU)psU3i3+Taf!(kPXZuKqICzv$=73 zHLC?(Jc5;CwtNwYMCLASLFba^MK%HnC~s@srw`k<()AA0efv&=kN;uP7saVSuYYiT zL-6f6EdmTFDZAc$tDZcwe!Lcg`3({0I)e}pZi}u43qC9pQ#gbpFl;>dik?b|*I@_+ zmIZc7uYG_r8N4YeJU40V3BmjXo!R>$@|c|~t6UxU-&BqaDeW=O&T5J5NwQkFrmCbO zLauR2SWH3xQu_d|D!_Yr;?2CVaKL#M%wX4+pc$g9S94|0s*^;irRIoPv!t{6KWO8V zwjY=JPuE){c&7B}5}V z4Q9A>**Mb-=;vvsS*vt}JeI=?O&7GAG?9G+-|=@c;=Pk`uc7UC+?CJsgeVQeof05U zuroy+XBP1|`*oVGGoPHy(V2*vQL;mT2qQ`ZHHH3NgDc`2S8@c3Cq0ku4(jhoI0`Ae zEFC@enL#@Xa+b{`AK2hPZ`feF#~8wOhX^Y}1!pmTtr%dEM@2m(95vyDGFqo3qpc09 z!laEpYoc+}hcn)kG?I%=Dlj0IECx^(b)+H79Mym~I2=zYK+`p&$xL=ykOuq`D@tW=JRC~fuipkg)>&(~w=T~C zSL|leOn_^xW3v>lqry|zm0>-nctCpF6kJo^|9zZFYcRsPECD7a&=XKOk)OU2Y8Ps z04#xz7$|ZLW=%6tma%b!bJEmy%nU9}qS=Fb;VqjnnJpdjo;4c20=`RV@2E;lzG-aq zlmRy5k20+be?R>j{b*vQDYDAhRD7D;1yoE#`Bi)lV#=sBN|(~Cr&fRk7x!clf=v*T z7u7vo1OcL@K6iY0RgNC)`|_PS9>a2JthoGkc5hyrBh~D>(I<@LHe>0ikt*R81-O<) z?L40O>Wx3l3q$v^=5`bxi`oWjy)1U&__h`q1pA?90jkzZJRW!p!Wj}%6IRqfsZ;g{ zEMegmD8!}BtFp0_3azVUOPLfqRbQDDrPdZwto&I>Z53acMKsO3_p>px2+A*UCC52+ zC@ZCv%%=Ls7m@iZYvGlp#!cP*ZyQjY^;Jy^=f9QK)YsR6@c*oA0u}4gX8uvP8cP*O zU6qVA@fzC%h6xb7bM$A&LP2edr`chBxuui08PK%Da+mQ=hNf&App3$mU;SHBhn%iv z@p7e)d7FoO!wybz0(3vpHd2x-Z_ojgXcTCCw2FC<){w8I{fSbZX4 zI9%KEBIT9{a?9TOGz;~P(T(10!}_2>X$N8gDvnKEmK81*`P!pc;!&aov)e6icWzL0 zlrYdx)`_^EL8eD_5A5zNJE_^8+0m4N5W+IwqYGESWA_jhR}Tk45Uyyw>I+*8REiO` zTr^aE*gUmOFA5gss*N~H>@*4d`mLdv80T!%+|$gVaa0$zlT8J0inYW?c-PCy-sb$q z_E|Ae002G{s6XvM-$5kHRfY>ZWt`6FRfP^Nl_crZH7xdb5yrP)vES5#qPZ=}$D+30 zN-vWgh^?)8I?f(cUx``y;m8Gu&4iqmqOJzWL}Eym@GIwc(dxL|9v*ImZEQ={nN^oUeS5w zvr+e<)6!gWZ_!F}z}6C{BAEsu^^mi65%2jiIfT3-r(##H95R0LfvvF8FwuofqvI39 zlgG@ALzCh&gGi&3Gh?sp$gGb1qHh6je6k9DgSiqpN*FVOiTWaFc@PZM09tv&`*o+% z^oWnXJyhtW?u-z1ZLq*g(-|hp@1qW;$wfq*plOdnQ(z7uF5zBUygWNw*K@kU^#u`& z-WG8x2zKJ?$FA)8@0XT0|Cy1*h<(yt@ZFZ&ZQX5VddQjkb2r=TNUaosBB}he(OZd= zeq$xF5-Ib#mTT`k15d*l*5UZ+)q3px$9cgA*=b1slj9ujly!Wy_NiI$mC9`6%x7(VjxRNpVd&<$#2q!X8iGyzUSTQeO50Q5;VHb? z8>+g5lUc^zoUt?S<;k43BLX8Ne^F96Dvr9P6*Kw^DljOKL(ixUmLO-w?war%kMs*5 zu=vJePNc}y>v7)Nz^&~mwN?6jV}C9+STds3PseMJI{+UqSOzipH^xDOm|NhNPx!CM zJV>T-1dqYzgu4{!u#*f(9Psh&^EORrESl@!XV*sh88p``sR#7&z0iMFYa0MdRcf5u zjX$10UVMDif|j3+DCkQHn=2QbAyrM~6?AV@I(XYzW~ z&AZdjr`&a9ZzByXO+II3l^8*kX;ng1bx0~Q6QS6@5_Vrj|EVX{XU1PpJ10h#KNIzw z`xm2IbRiNk*Hj>3q{P0;Q7Y10us|_S`w3LAl@!J`;jnkDCj`;ICth%S5TX=uGB>2d z|M%{OcmOZ7B^ds{$sG_#K{SK}lrk)JnXpBOig4&1$mrm#O(`R8x^J58w~Qc|D;di| z$0Ac*wVka3Hti`7)VBu$Nskw%d82-ADmNcGKHOr*88iGOK_xjlK+$yvi!(TM6AOdZ z4%F3^v0f(ic_c*XT)W_;AFH?2x{I8dvCT!3@>2GAWk8mKF14jsGXRqp&V{At#A5j;h24o(Ex2)Oir8F1i6exoM;Mx;cnOYDoA& z8HBN8hEA^KFW?3CO_K{w2<8HifSb{l2{|t-N;)XEp^d1QYkV!)SEg!@0R?mz$t9ce zTZ~pcP8HiQvTRP*1kf>`KzesU!l|vn>Dj6>c^`lP!VXG04TshI5<4ZnXKHsZtT zhZS`sA({B;;r=80CTsh|_i=61V5)G{&-=9vZrL4ebG>Tf3~k+%2(+y9w9E?J8&xfv z$x6vCr4N;w!w=j&PGVc7kK-kge;hAS&baX@)i14ML`!?KtMufHw(OYo{)48YU?_s5 z5|7P$1)4LvIisbY{8nv6`5sFNpj%S0Oc|Iui9OFFE(N9*>tQPooy<2+#*VwC8|>?m z9N5(5(ycZ2ztU!m7sQMjPi4q@N>~(~y=VU;_3l>yp22_Sy?|FBXC<4Gly!p5oFyhY=WO`etb< zCw=YIi6CSxywG3ja_$yA9S|MtV13&00mJyF?k~-FCG)-xp)E*9sxXy*Mx{-34e#h_ z*5G=J-u#ZOkWzQOCv&SnM>QRUn`s4ZlH@Y3882)Wi2KeJluaptx=cmF`XIX)o?la< znI8^viF+dZKp2)2ltfjTHQ+t8(2rT-)O^Jo75M)b+#f3_;+qd`XV&&JAn ztN%*{7fV4h%+B3-=RP6}zRkYf_+&D8HHcz%z4+iFm_+?Gm_*qU zyI0-xl>i@B-2VvTpnK`SG8Oq3TvZGAHXk#HKD`g`vh_Q?_lP}>8h!r&I*_kX%>6IJ zIW7q(;&a$LjA_HOlJgTe#xsTmdnShkVelaxCOM}vPKV3Ijj_WRR29rNj}4{}7l~}j zaaoyUanOVHM#??CVJ9O=gXv|2(A|W*xYyH8pu3(+Jfx5vg{M9t+enGfC=GMFb4iQ; zcO-&cB?+NX2Oq!W)rKsaQ&M0ztG>?J_GOASHKZs$KaYd=ww)uZA} zBHf}-@vcdeGzEa=k#@C^9#x_ZX$tQQUTp}IK`Agxg!`sQgon$*#3)EybtErmoVgzf zfg$i%Zu33auS1XW!gQDsz0e%xhHN#(d!akd30-T9|G$%Fb3(8Tzl)r)$w~s5vKEnr zTS!;Iuwk9?z1ZN#V#OK|FLYm=8--6b#5!H4)qN)+9`Q_)d1Q{O8OI^1uZVg*j>Y_Q z+r5S&7s^)BLdmCwrsJRk4lHn!)HafHL}@=7pJ(Uw1vNx+z3$0YoXEbbcz{!2s2V3e zCpbu3XeJSk^8HwQmGkzllBQ_Z2pXt=pf&G{vyLgsf}j8i$pFM<3Az|VF&y9>FK{GM zsBN5WUqs(=O5x%y2_w`3L9iPgh@_$iB3=k@iSUNeh=y~pS$PgG^Y`4D) z=(yBg!qyphL$+hp-a1GX{|4&C0jXEJ=g)dcbG~gU*Hd_y zl{^)AN34d|w6_d!5UatI1hFO!Uv)crwR62h>QM#G0Wt_e9G1E=&sQ!Wmlb(7I(_ge zxo^_=%u0cqbdMG?nzS!h0E89^1%_*L2&Ieq%>C(;8|_tVQzf^Pzz+t((2YA6W_rFQ2kC})&@RZg`_W*kMxq`nyuH( YCERM+s|Bx - - - - - - - - - - - - - - - - - - - - - - - - - + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/examples/in_progress/prover/Functions/why3shapes.gz b/examples/in_progress/prover/Functions/why3shapes.gz new file mode 100644 index 0000000000000000000000000000000000000000..fe26b2ce42ca5eefae4dd5c532e6bbb32442aded GIT binary patch literal 347 zcmV-h0i^yPiwFP!00000|CLh9PQx$|yyq+O34T8gNK}YOTsY=ht?gZiRFcxTsQf*K zHhmYw!Cu=lyE7V@D`Sv&us%s=gd?3oj9f-pHUX}NuBUEO-|gx>td|Kgwyfo?_+CvV zBP4C2H#~7+fpf!^W!jSg!9c?wGvxGK?(*q*A{R_HRiu!>SwWF}N>QN>7%dP1*UWiW zw+}T9t2z#E%VEShjN=eH$lV9-Rd?7_x3Y)Z{#0IPfSZi{*bO}_9^con_)m9JDQ1iW zgur;|P!>=G2^K+cM^fv_ZkMpnUH+W+xX!Dha_)5^6gf6KM~mtK|Hbm@kXy8qX-(ys zi_9@)6$BMyi65D_#(9q<4X{Jv{g~%d?hB-RCGbKi!LaFc)x-~S+0#_qGa&;ft0D<9 tK0&fJxFmT9gic;}vg%%5FRUCaZ0pgNyJ_l}b2+D}z5t%svcx+B0075xq4)p* literal 0 HcmV?d00001 diff --git a/examples/in_progress/prover/Makefile b/examples/in_progress/prover/Makefile index 486a63ba4..20b99e1d3 100644 --- a/examples/in_progress/prover/Makefile +++ b/examples/in_progress/prover/Makefile @@ -73,7 +73,7 @@ replay: @printf "Starting time (UTC): " @date --utc +%H:%M @printf "===================================\n" - @for i in $(MLWUTIL) $(MLWIMPL); do \ + @for i in *.mlw; do \ printf "Replaying $$i..." ; \ why3 $(WHY3FLAGS) replay -q $$i ; \ done diff --git a/examples/in_progress/prover/OptionFuncs/why3session.xml b/examples/in_progress/prover/OptionFuncs/why3session.xml index e4e0d5afb..f205a71e4 100644 --- a/examples/in_progress/prover/OptionFuncs/why3session.xml +++ b/examples/in_progress/prover/OptionFuncs/why3session.xml @@ -1,249 +1,46 @@ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/examples/in_progress/prover/OptionFuncs/why3shapes.gz b/examples/in_progress/prover/OptionFuncs/why3shapes.gz new file mode 100644 index 0000000000000000000000000000000000000000..f7852aa07d281727261079d7a170acae87befd34 GIT binary patch literal 557 zcmV+|0@D2-iwFP!00000|CLnRirX*{efL-72MU^zMi*$ICDf07Dfp$7Fp@@KNaAdg zE$QD^cAV^PNR}=bOCCvQ&dfP-0UsH>(vjmnx0QT(BiY*K7x1~QVzRcrS9ugm< zQyuWnVIv)07HSCFCKW?yA|`L8AZ1jpkd+XkNrqE=5AVmYl@8h_CI?`fO^p_7iHKl(y-YL2U$%Bt3zdT1>etWJVmc5I`xg^bd>F(AGW;y{`Ac2$9vl* zSn`4%h@`RzV*J<`7N5~73Vf%UbzhECHN%E?;Ruk8S0u5zA*#2P^;x#Z{`mKrU<&g~ zc%IyG - - - - - - - - - - - - - - - - - - - - - + + + + + + + + + + + + + + + + + + + diff --git a/examples/in_progress/prover/Predicates/why3shapes.gz b/examples/in_progress/prover/Predicates/why3shapes.gz new file mode 100644 index 0000000000000000000000000000000000000000..e2397076d6d10c28a0b5595811eafd3428735950 GIT binary patch literal 267 zcmV+m0rdVKiwFP!00000|CLe8PQ)+_y!R{e3C%k_Ac4?U;=&2#x^f&xinO%dHbu+d z6S1^{y#ObB?D5P<4hn=dM%!dDQoNg!(a6trge%? z$hV$*;rS=4Z$eOpBY@&n#OOA;4r41#h)T#r9lO=3_wr8;SJu<>9*le0H&Qx{T2r)! zD~?@@(Iyk6)T%>)ocTwV#+gkxzE0ypM_85-GnD*ByWzIno2%tF2wPXj4=~LX50^s2 zlE(o~hw}=je~R=?Cpb|Il8}Qxx60-TFYFGZc|s`jpN&2 R!u{a(%?JM=Q%(i~003mjescf- litera