MAJ terminée. Nous sommes passés en version 14.6.2 . Pour consulter les "releases notes" associées c'est ici :

https://about.gitlab.com/releases/2022/01/11/security-release-gitlab-14-6-2-released/
https://about.gitlab.com/releases/2022/01/04/gitlab-14-6-1-released/

Commit 00948a93 authored by Martin Clochard's avatar Martin Clochard
Browse files

2wp_gen: cont'd

parent 80cb510a
......@@ -268,10 +268,10 @@
<proof prover="3"><result status="valid" time="0.05" steps="47"/></proof>
</goal>
<goal name="dmn_witness_criterion.4.6.10.18" expl="18.">
<proof prover="3"><result status="valid" time="4.33" steps="5242"/></proof>
<proof prover="3"><result status="valid" time="4.28" steps="5242"/></proof>
</goal>
<goal name="dmn_witness_criterion.4.6.10.19" expl="19.">
<proof prover="3"><result status="valid" time="4.28" steps="5242"/></proof>
<proof prover="3"><result status="valid" time="4.33" steps="5242"/></proof>
</goal>
<goal name="dmn_witness_criterion.4.6.10.20" expl="20.">
<proof prover="3"><result status="valid" time="0.06" steps="57"/></proof>
......@@ -2108,7 +2108,7 @@
<proof prover="3"><result status="valid" time="0.31" steps="301"/></proof>
</goal>
<goal name="evolve_inflationary.26" expl="26.">
<proof prover="3"><result status="valid" time="9.07" steps="4251"/></proof>
<proof prover="1" steplimit="0"><result status="valid" time="1.57"/></proof>
</goal>
<goal name="evolve_inflationary.27" expl="27.">
<proof prover="1"><result status="valid" time="1.91"/></proof>
......
......@@ -178,6 +178,9 @@ module FmlaRules "W:non_conservative_extension:N" (* => FmlaRulesProof *)
holds c (enforce ((=) x) q) /\ holds c (ordering o) ->
holds c (enforce ((=) x) (inter q (o x)))
axiom enforce_step : forall g x,q:set 'a. game_wf g ->
g.transition x q -> enforce ((=) x) q g
axiom sequence : forall c,p q r:set 'a.
holds c (enforce p q) /\ holds c (enforce q r) -> holds c (enforce p r)
......@@ -1997,6 +2000,7 @@ module FmlaRulesProof
goal ordering_fmla,
goal enforce_monotonic,
goal enforce_does_progress,
goal enforce_step,
goal sequence,
goal external_pre,
goal kont_intro,
......
......@@ -93,7 +93,7 @@
</theory>
<theory name="FmlaRules" sum="d41d8cd98f00b204e9800998ecf8427e">
</theory>
<theory name="FmlaRulesProof" sum="d97da419a00424f9b2325ca183eaef18">
<theory name="FmlaRulesProof" sum="72e39c488b2d097239b55ca3761e824e" expanded="true">
<goal name="rel_map_equal">
<transf name="split_goal_wp">
<goal name="rel_map_equal.1" expl="1.">
......@@ -4400,6 +4400,9 @@
<goal name="FmlaRules.enforce_does_progress">
<proof prover="4"><result status="valid" time="0.16" steps="7"/></proof>
</goal>
<goal name="FmlaRules.enforce_step">
<proof prover="4" steplimit="0"><result status="valid" time="2.97" steps="2094"/></proof>
</goal>
<goal name="FmlaRules.sequence">
<proof prover="4"><result status="valid" time="0.13" steps="7"/></proof>
</goal>
......
......@@ -216,6 +216,16 @@ module Bridge "W:non_conservative_extension:N" (* => TransProof *)
(enforce (st_pre sys p) (st_post sys qn ql) (ugame sys) <->
forall lg. p (lg 0) -> correct sys qn ql lg)
(* TODO: correct those axioms, they can't work through st_pre/st_post *)
axiom egame_trans : false (*forall sys:system 'a 'o,n x y.
let p = st_pre sys ((=) x) in
let q = st_post sys ((=) y) in
system_wf sys -> enforce p q (egame sys)*)
axiom ugame_trans : false (*forall sys:system 'a 'o,n x.
let p = st_pre sys ((=) x) in
let q = st_post sys (* TODO: incorrect for post here. *)none none in
system_wf sys -> enforce p q (ugame sys)*)
end
module TransProof
......@@ -716,6 +726,14 @@ module TransProof
use import game_fmla.Subgame
use import game_fmla.FmlaRules
(* TODO: first add lemmas about mirroring ONE
transition inside e/u-games, can be reused for enforcements ?
Nope, they actually can't, as those will use local vision,
e.g without guarantee of log consistency => Delayed for later.
lemma egame_trans : forall sys:system 'a 'o,p x y.
let eg = egame sys in
system_wf sys /\ sys.transition x y -> enforce ? ? eg*)
lemma egame_enforce_2 : forall sys:system 'a 'o,p qn ql.
let pr = st_pre sys p in
let ps = st_post sys qn ql in
......@@ -738,9 +756,12 @@ module TransProof
so holds c (arrow (enforce ps none) (enforce ((=) sx) ps))
by let c' = conj c (enforce ps none) in
holds c' (enforce ((=) sx) ps)
by let i = \t s.
s = t /\ log_coh lg xtc s /\ valid sys s /\
forall n. 0 <= n /\ urange s.time (n+xtc+1) -> not qn (lg n) in
by let i = \t s. s = t /\ log_coh lg xtc s /\ valid sys s /\
match s.time with
| None -> false
| Some stc -> stc >= xtc /\
forall n. 0 <= n /\ n + xtc < stc -> not qn (lg n)
end in
subset none ps
so (subset ((=) sx) (i sx)
by forall n. 0 <= n /\ urange sx.time (n+xtc+1) -> false)
......@@ -748,6 +769,36 @@ module TransProof
by holds c' (universal (u_enforce i (const none)))
by holds c' (ordering og) /\ order og
so (holds c' (universal (u_enforce i (later og i)))
(* Reduce it to an atomic transition or exit. *)
by forall t. holds c' (enforce (i t) (later og i t))
by forall s. i t s -> holds c' (enforce ((=) s) (later og i t))
by match s.time with
| None -> false
| Some stc ->
let m = stc - xtc in
m >= 0
so (s.log stc = lg m by urange s.time (m+xtc))
so if qn (s.log stc)
then subset none (later og i t) so subset ((=) s) ps
so holds c' (enforce ps none)
else
let nlog = \n. if n <= stc then s.log n else lg (m+1) in
let ns = { time = Some (stc+1); log = nlog } in
sys.transition (s.log stc) (nlog (stc+1))
so (valid sys ns
by let cp = compose sys.projection ns.log in
monotone (<=) cp o
by forall a b. a <= b -> o (cp a) (cp b)
by forall a. a <= stc+1 -> o (cp a) (cp (stc+1))
by a = stc+1 || o (cp a) (cp stc)
) so (eg.G.transition s ((=) ns) by successor sys stc s.log ns)
so holds c' (enforce ((=) s) ((=) ns))
so subset ((=) ns) (later og i t)
by later og i t ns
by og t ns /\ (i ns ns
by log_coh lg xtc ns
/\ forall n. 0 <= n /\ n + xtc < stc+1 -> not qn (lg n))
end
)
so (step_limit c' og og i
by forall ch inh f. ch inh /\ monotone_on ch og f og /\
......@@ -770,8 +821,8 @@ module TransProof
so i x0 (f x0)
)
so (valid sys sp by og inh sp /\ sp <> inh)
so let cp = compose sys.projection sp.log in
let ch2 = image cp all in
so let cp2 = compose sys.projection sp.log in
let ch2 = image cp2 all in
let sp2 = sup o ch2 in
local_repr sys sp = Limit sp2
so ql sp2
......@@ -780,9 +831,30 @@ module TransProof
so exists x0. ch x0 /\ urange x0.time (n+xtc+1)
so i x0 (f x0))
so lim_reach sys ql lg
so let cp3 = compose sys.projection lg in
exists sp3. supremum sys.progress (image cp3 pos) sp3 /\ ql sp3
so sp3 = sp2
by supremum sys.progress ch2 sp3
by let c0 = \n. sys.projection (sp.log (n+xtc)) in
equalizer pos cp3 c0
so sext (image cp3 pos) (image c0 pos)
so monotone (<=) c0 o
so supremum sys.progress (image c0 all) sp3
so sext (image c0 all) ch2
by (forall u. image cp2 all u -> image c0 all u
by exists n. cp2 n = u so c0 (n-xtc) = u)
/\ (forall u. image c0 all u -> image cp2 all u
by exists n. c0 n = u so cp2 (n+xtc) = u)
)
end
lemma ugame_enforce_2 : forall sys:system 'a 'o,p qn ql.
let ug = ugame sys in
let pr = st_pre sys p in
let ps = st_post sys qn ql in
system_wf sys /\ (forall lg. p (lg 0) -> correct sys qn ql lg) ->
enforce pr ps ug
clone TransWf with
goal q_chain_complete_countable_complete,
goal gprogress_order,
......@@ -795,7 +867,9 @@ module TransProof
clone Bridge with
goal egame_enforce,
goal ugame_enforce
goal ugame_enforce,
goal egame_trans,
goal ugame_trans
end
......@@ -13,7 +13,7 @@
</theory>
<theory name="Bridge" sum="d41d8cd98f00b204e9800998ecf8427e">
</theory>
<theory name="TransProof" sum="e2802bd4ac8f7ddef82caa72e9fb9098" expanded="true">
<theory name="TransProof" sum="df360da3df65b3345b4a1a7b60dee0a3" expanded="true">
<goal name="q_chain_complete_countable_complete">
<transf name="split_goal_wp">
<goal name="q_chain_complete_countable_complete.1" expl="1.">
......@@ -1228,13 +1228,13 @@
</goal>
</transf>
</goal>
<goal name="egame_enforce_2" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="egame_enforce_2">
<transf name="split_goal_wp">
<goal name="egame_enforce_2.1" expl="1.">
<proof prover="0"><result status="valid" time="0.84" steps="625"/></proof>
<proof prover="0"><result status="valid" time="0.58" steps="625"/></proof>
</goal>
<goal name="egame_enforce_2.2" expl="2.">
<proof prover="4"><result status="valid" time="2.47"/></proof>
<proof prover="4"><result status="valid" time="3.09"/></proof>
</goal>
<goal name="egame_enforce_2.3" expl="3.">
<proof prover="0"><result status="valid" time="0.07" steps="14"/></proof>
......@@ -1249,7 +1249,7 @@
<proof prover="0"><result status="valid" time="0.13" steps="30"/></proof>
</goal>
<goal name="egame_enforce_2.7" expl="7.">
<proof prover="0"><result status="valid" time="0.19" steps="185"/></proof>
<proof prover="0"><result status="valid" time="0.19" steps="204"/></proof>
</goal>
<goal name="egame_enforce_2.8" expl="8.">
<proof prover="0"><result status="valid" time="0.10" steps="89"/></proof>
......@@ -1257,165 +1257,278 @@
<goal name="egame_enforce_2.9" expl="9.">
<proof prover="0"><result status="valid" time="0.11" steps="12"/></proof>
</goal>
<goal name="egame_enforce_2.10" expl="10." expanded="true">
<proof prover="0"><result status="timeout" time="4.98"/></proof>
<goal name="egame_enforce_2.10" expl="10.">
<proof prover="0"><result status="valid" time="0.12" steps="39"/></proof>
</goal>
<goal name="egame_enforce_2.11" expl="11.">
<proof prover="0"><result status="valid" time="0.15" steps="24"/></proof>
<proof prover="0"><result status="valid" time="0.12" steps="106"/></proof>
</goal>
<goal name="egame_enforce_2.12" expl="12.">
<proof prover="0"><result status="valid" time="0.12" steps="24"/></proof>
<proof prover="0"><result status="valid" time="0.11" steps="31"/></proof>
</goal>
<goal name="egame_enforce_2.13" expl="13.">
<proof prover="0"><result status="valid" time="0.08" steps="58"/></proof>
<proof prover="0"><result status="valid" time="0.12" steps="153"/></proof>
</goal>
<goal name="egame_enforce_2.14" expl="14.">
<proof prover="0"><result status="valid" time="0.35" steps="331"/></proof>
<proof prover="0"><result status="valid" time="0.07" steps="23"/></proof>
</goal>
<goal name="egame_enforce_2.15" expl="15.">
<proof prover="0"><result status="valid" time="0.12" steps="26"/></proof>
<proof prover="0"><result status="valid" time="0.41" steps="462"/></proof>
</goal>
<goal name="egame_enforce_2.16" expl="16.">
<proof prover="0"><result status="valid" time="0.13" steps="240"/></proof>
<proof prover="0"><result status="valid" time="1.02" steps="553"/></proof>
</goal>
<goal name="egame_enforce_2.17" expl="17.">
<proof prover="0"><result status="valid" time="0.07" steps="27"/></proof>
<proof prover="0"><result status="valid" time="0.06" steps="26"/></proof>
</goal>
<goal name="egame_enforce_2.18" expl="18.">
<proof prover="0"><result status="valid" time="0.10" steps="38"/></proof>
<proof prover="0"><result status="valid" time="2.91" steps="2929"/></proof>
</goal>
<goal name="egame_enforce_2.19" expl="19.">
<proof prover="0"><result status="valid" time="0.15" steps="208"/></proof>
<proof prover="0"><result status="valid" time="1.44" steps="1998"/></proof>
</goal>
<goal name="egame_enforce_2.20" expl="20.">
<proof prover="0"><result status="valid" time="1.00" steps="764"/></proof>
<proof prover="0"><result status="valid" time="5.65" steps="4102"/></proof>
</goal>
<goal name="egame_enforce_2.21" expl="21.">
<proof prover="0"><result status="valid" time="0.17" steps="33"/></proof>
<proof prover="0"><result status="valid" time="0.13" steps="29"/></proof>
</goal>
<goal name="egame_enforce_2.22" expl="22.">
<proof prover="0"><result status="valid" time="0.48" steps="513"/></proof>
<proof prover="0"><result status="valid" time="0.09" steps="56"/></proof>
</goal>
<goal name="egame_enforce_2.23" expl="23.">
<proof prover="0"><result status="valid" time="0.31" steps="192"/></proof>
<proof prover="0"><result status="valid" time="0.31" steps="206"/></proof>
</goal>
<goal name="egame_enforce_2.24" expl="24.">
<proof prover="0"><result status="valid" time="0.19" steps="174"/></proof>
<proof prover="0"><result status="valid" time="1.19" steps="1345"/></proof>
</goal>
<goal name="egame_enforce_2.25" expl="25.">
<proof prover="0"><result status="valid" time="0.12" steps="125"/></proof>
<proof prover="0"><result status="valid" time="0.50" steps="468"/></proof>
</goal>
<goal name="egame_enforce_2.26" expl="26.">
<proof prover="0"><result status="valid" time="0.09" steps="43"/></proof>
<proof prover="1"><result status="valid" time="3.93"/></proof>
</goal>
<goal name="egame_enforce_2.27" expl="27.">
<proof prover="0"><result status="valid" time="0.09" steps="30"/></proof>
<proof prover="0"><result status="valid" time="0.46" steps="398"/></proof>
</goal>
<goal name="egame_enforce_2.28" expl="28.">
<proof prover="0"><result status="valid" time="0.09" steps="41"/></proof>
<proof prover="0"><result status="valid" time="0.64" steps="805"/></proof>
</goal>
<goal name="egame_enforce_2.29" expl="29.">
<proof prover="0"><result status="valid" time="0.09" steps="35"/></proof>
<proof prover="1"><result status="valid" time="2.35"/></proof>
</goal>
<goal name="egame_enforce_2.30" expl="30.">
<proof prover="0"><result status="valid" time="0.19" steps="364"/></proof>
<proof prover="0"><result status="valid" time="0.14" steps="105"/></proof>
</goal>
<goal name="egame_enforce_2.31" expl="31.">
<proof prover="0"><result status="valid" time="0.07" steps="68"/></proof>
<proof prover="0"><result status="valid" time="0.09" steps="35"/></proof>
</goal>
<goal name="egame_enforce_2.32" expl="32." expanded="true">
<proof prover="0" obsolete="true"><result status="timeout" time="5.00"/></proof>
<proof prover="1" obsolete="true"><result status="timeout" time="6.01"/></proof>
<goal name="egame_enforce_2.32" expl="32.">
<proof prover="0"><result status="valid" time="0.19" steps="310"/></proof>
</goal>
<goal name="egame_enforce_2.33" expl="33.">
<proof prover="0"><result status="valid" time="0.28" steps="149"/></proof>
<proof prover="0"><result status="valid" time="0.19" steps="56"/></proof>
</goal>
<goal name="egame_enforce_2.34" expl="34.">
<proof prover="0"><result status="valid" time="0.09" steps="27"/></proof>
<proof prover="0"><result status="valid" time="2.12" steps="701"/></proof>
</goal>
<goal name="egame_enforce_2.35" expl="35.">
<proof prover="0"><result status="valid" time="0.10" steps="26"/></proof>
<proof prover="0"><result status="valid" time="0.15" steps="24"/></proof>
</goal>
<goal name="egame_enforce_2.36" expl="36.">
<proof prover="0"><result status="valid" time="0.17" steps="47"/></proof>
<proof prover="0"><result status="valid" time="0.12" steps="24"/></proof>
</goal>
<goal name="egame_enforce_2.37" expl="37.">
<proof prover="0"><result status="valid" time="0.19" steps="43"/></proof>
<proof prover="0"><result status="valid" time="0.20" steps="58"/></proof>
</goal>
<goal name="egame_enforce_2.38" expl="38.">
<proof prover="0"><result status="valid" time="0.23" steps="102"/></proof>
<proof prover="0"><result status="valid" time="0.35" steps="331"/></proof>
</goal>
<goal name="egame_enforce_2.39" expl="39.">
<proof prover="0"><result status="valid" time="0.17" steps="85"/></proof>
<proof prover="0"><result status="valid" time="0.12" steps="26"/></proof>
</goal>
<goal name="egame_enforce_2.40" expl="40.">
<proof prover="0"><result status="valid" time="0.25" steps="118"/></proof>
<proof prover="0"><result status="valid" time="0.29" steps="240"/></proof>
</goal>
<goal name="egame_enforce_2.41" expl="41.">
<proof prover="0"><result status="valid" time="1.60" steps="931"/></proof>
<proof prover="0"><result status="valid" time="0.07" steps="27"/></proof>
</goal>
<goal name="egame_enforce_2.42" expl="42.">
<proof prover="0"><result status="valid" time="0.16" steps="50"/></proof>
<proof prover="0"><result status="valid" time="0.10" steps="38"/></proof>
</goal>
<goal name="egame_enforce_2.43" expl="43.">
<proof prover="0"><result status="valid" time="0.18" steps="23"/></proof>
<proof prover="0"><result status="valid" time="0.31" steps="208"/></proof>
</goal>
<goal name="egame_enforce_2.44" expl="44.">
<proof prover="0"><result status="valid" time="0.06" steps="14"/></proof>
<proof prover="0"><result status="valid" time="1.54" steps="764"/></proof>
</goal>
<goal name="egame_enforce_2.45" expl="45.">
<proof prover="0"><result status="valid" time="0.14" steps="35"/></proof>
<proof prover="0"><result status="valid" time="0.17" steps="33"/></proof>
</goal>
<goal name="egame_enforce_2.46" expl="46.">
<proof prover="0"><result status="valid" time="0.08" steps="42"/></proof>
<proof prover="0"><result status="valid" time="0.48" steps="516"/></proof>
</goal>
<goal name="egame_enforce_2.47" expl="47.">
<proof prover="0"><result status="valid" time="0.31" steps="192"/></proof>
</goal>
<goal name="egame_enforce_2.48" expl="48.">
<proof prover="0"><result status="valid" time="0.31" steps="174"/></proof>
</goal>
<goal name="egame_enforce_2.49" expl="49.">
<proof prover="0"><result status="valid" time="0.12" steps="125"/></proof>
</goal>
<goal name="egame_enforce_2.50" expl="50.">
<proof prover="0"><result status="valid" time="0.09" steps="43"/></proof>
</goal>
<goal name="egame_enforce_2.51" expl="51.">
<proof prover="0"><result status="valid" time="0.09" steps="30"/></proof>
</goal>
<goal name="egame_enforce_2.52" expl="52.">
<proof prover="0"><result status="valid" time="0.09" steps="41"/></proof>
</goal>
<goal name="egame_enforce_2.53" expl="53.">
<proof prover="0"><result status="valid" time="0.09" steps="35"/></proof>
</goal>
<goal name="egame_enforce_2.54" expl="54.">
<proof prover="1"><result status="valid" time="7.62"/></proof>
</goal>
<goal name="egame_enforce_2.55" expl="55.">
<proof prover="0"><result status="valid" time="0.07" steps="68"/></proof>
</goal>
<goal name="egame_enforce_2.56" expl="56.">
<proof prover="0"><result status="valid" time="0.11" steps="38"/></proof>
</goal>
<goal name="egame_enforce_2.57" expl="57.">
<proof prover="0"><result status="valid" time="0.16" steps="87"/></proof>
</goal>
<goal name="egame_enforce_2.58" expl="58.">
<proof prover="0"><result status="valid" time="2.03" steps="1741"/></proof>
</goal>
<goal name="egame_enforce_2.59" expl="59.">
<proof prover="0"><result status="valid" time="2.20" steps="1151"/></proof>
</goal>
<goal name="egame_enforce_2.60" expl="60.">
<proof prover="0"><result status="valid" time="0.24" steps="335"/></proof>
</goal>
<goal name="egame_enforce_2.61" expl="61.">
<proof prover="0"><result status="valid" time="0.12" steps="53"/></proof>
</goal>
<goal name="egame_enforce_2.62" expl="62.">
<proof prover="0"><result status="valid" time="0.19" steps="53"/></proof>
</goal>
<goal name="egame_enforce_2.63" expl="63.">
<proof prover="0"><result status="valid" time="0.10" steps="57"/></proof>
</goal>
<goal name="egame_enforce_2.64" expl="64.">
<proof prover="0"><result status="valid" time="0.22" steps="186"/></proof>
</goal>
<goal name="egame_enforce_2.65" expl="65.">
<proof prover="0"><result status="valid" time="0.12" steps="56"/></proof>
</goal>
<goal name="egame_enforce_2.66" expl="66.">
<proof prover="0"><result status="valid" time="0.28" steps="187"/></proof>
</goal>
<goal name="egame_enforce_2.67" expl="67.">
<proof prover="0"><result status="valid" time="0.48" steps="560"/></proof>
</goal>
<goal name="egame_enforce_2.68" expl="68.">
<proof prover="0"><result status="valid" time="0.59" steps="565"/></proof>
</goal>
<goal name="egame_enforce_2.69" expl="69.">
<proof prover="0"><result status="valid" time="0.19" steps="128"/></proof>
</goal>
<goal name="egame_enforce_2.70" expl="70.">
<proof prover="0"><result status="valid" time="0.07" steps="26"/></proof>
</goal>
<goal name="egame_enforce_2.71" expl="71.">
<proof prover="0"><result status="valid" time="0.28" steps="149"/></proof>
</goal>
<goal name="egame_enforce_2.72" expl="72.">
<proof prover="0"><result status="valid" time="0.09" steps="27"/></proof>
</goal>
<goal name="egame_enforce_2.73" expl="73.">
<proof prover="0"><result status="valid" time="0.10" steps="26"/></proof>
</goal>
<goal name="egame_enforce_2.74" expl="74.">
<proof prover="0"><result status="valid" time="0.17" steps="48"/></proof>
</goal>
<goal name="egame_enforce_2.75" expl="75.">
<proof prover="0"><result status="valid" time="0.19" steps="44"/></proof>
</goal>
<goal name="egame_enforce_2.76" expl="76.">
<proof prover="0"><result status="valid" time="0.23" steps="102"/></proof>
</goal>
<goal name="egame_enforce_2.77" expl="77.">
<proof prover="0"><result status="valid" time="0.33" steps="85"/></proof>
</goal>
<goal name="egame_enforce_2.78" expl="78.">
<proof prover="0"><result status="valid" time="0.25" steps="118"/></proof>
</goal>
<goal name="egame_enforce_2.79" expl="79.">
<proof prover="0"><result status="valid" time="2.08" steps="943"/></proof>
</goal>
<goal name="egame_enforce_2.80" expl="80.">
<proof prover="0"><result status="valid" time="0.16" steps="51"/></proof>
</goal>
<goal name="egame_enforce_2.81" expl="81.">
<proof prover="0"><result status="valid" time="0.18" steps="23"/></proof>
</goal>
<goal name="egame_enforce_2.82" expl="82.">
<proof prover="0"><result status="valid" time="0.06" steps="14"/></proof>
</goal>
<goal name="egame_enforce_2.83" expl="83.">
<proof prover="0"><result status="valid" time="0.14" steps="35"/></proof>
</goal>
<goal name="egame_enforce_2.84" expl="84.">
<proof prover="0"><result status="valid" time="0.08" steps="42"/></proof>
</goal>
<goal name="egame_enforce_2.85" expl="85.">
<proof prover="0"><result status="valid" time="0.11" steps="17"/></proof>
</goal>
</transf>
</goal>
<goal name="TransWf.q_chain_complete_countable_complete">
<proof prover="0"><result status="valid" time="0.02" steps="3"/></proof>
<goal name="ugame_enforce_2" expanded="true">
</goal>
<goal name="TransWf.q_chain_complete_countable_complete" expanded="true">
<proof prover="0" obsolete="true"><result status="valid" time="0.02" steps="3"/></proof>
</goal>
<goal name="TransWf.gprogress_order">
<proof prover="0"><result status="valid" time="0.03" steps="4"/></proof>
<goal name="TransWf.gprogress_order" expanded="true">
<proof prover="0" obsolete="true"><result status="valid" time="0.03" steps="4"/></proof>
</goal>
<goal name="TransWf.lprogress_order">
<proof prover="0"><result status="valid" time="0.04" steps="4"/></proof>
<goal name="TransWf.lprogress_order" expanded="true">
<proof prover="0" obsolete="true"><result status="valid" time="0.04" steps="4"/></proof>
</goal>
<goal name="TransWf.local_repr_mono">
<proof prover="0"><result status="valid" time="0.03" steps="13"/></proof>
<goal name="TransWf.local_repr_mono" expanded="true">
<proof prover="0" obsolete="true"><result status="valid" time="0.03" steps="13"/></proof>
</goal>
<goal name="TransWf.gprogress_complete">
<proof prover="0"><result status="valid" time="0.03" steps="6"/></proof>
<goal name="TransWf.gprogress_complete" expanded="true">
<proof prover="0" obsolete="true"><result status="valid" time="0.03" steps="6"/></proof>
</goal>
<goal name="TransWf.local_repr_cont">
<proof prover="0"><result status="valid" time="0.06" steps="111"/></proof>
<goal name="TransWf.local_repr_cont" expanded="true">
<proof prover="0" obsolete="true"><result status="valid" time="0.06" steps="111"/></proof>
</goal>
<goal name="TransWf.egame_wf">
<proof prover="0"><result status="valid" time="0.03" steps="5"/></proof>
<goal name="TransWf.egame_wf" expanded="true">
<proof prover="0" obsolete="true"><result status="valid" time="0.03" steps="5"/></proof>
</goal>
<goal name="TransWf.ugame_wf">
<proof prover="0"><result status="valid" time="0.04" steps="5"/></proof>
<goal name="TransWf.ugame_wf" expanded="true">
<proof prover="0" obsolete="true"><result status="valid" time="0.04" steps="5"/></proof>
</goal>
<goal name="Bridge.egame_enforce" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="egame_enforce.1" expl="1.">
<proof prover="0"><result status="valid" time="0.05" steps="27"/></proof>
</goal>
<goal name="egame_enforce.2" expl="2." expanded="true">
</goal>
</transf>
<proof prover="0" obsolete="true"><result status="valid" time="0.10" steps="62"/></proof>
</goal>
<goal name="Bridge.ugame_enforce" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="ugame_enforce.1" expl="1.">
<proof prover="0"><result status="valid" time="0.07" steps="7"/></proof>
<goal name="ugame_enforce.1" expl="1." expanded="true">
<proof prover="0" obsolete="true"><result status="valid" time="0.07" steps="7"/></proof>
</goal>
<goal name="ugame_enforce.2" expl="2." expanded="true">
</goal>
</transf>
</goal>
<goal name="Bridge.egame_trans" expanded="true">
</goal>
<goal name="Bridge.ugame_trans" expanded="true">
</goal>
</theory>
</file>
</why3session>