src/HOL/Import/HOL/HOL4Prob.thy
changeset 14516 a183dec876ab
child 15013 34264f5e4691
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Import/HOL/HOL4Prob.thy	Fri Apr 02 17:37:45 2004 +0200
     1.3 @@ -0,0 +1,3981 @@
     1.4 +theory HOL4Prob = HOL4Real:
     1.5 +
     1.6 +;setup_theory prob_extra
     1.7 +
     1.8 +lemma BOOL_BOOL_CASES_THM: "ALL f. f = (%b. False) | f = (%b. True) | f = (%b. b) | f = Not"
     1.9 +  by (import prob_extra BOOL_BOOL_CASES_THM)
    1.10 +
    1.11 +lemma EVEN_ODD_BASIC: "EVEN 0 & ~ EVEN 1 & EVEN 2 & ~ ODD 0 & ODD 1 & ~ ODD 2"
    1.12 +  by (import prob_extra EVEN_ODD_BASIC)
    1.13 +
    1.14 +lemma EVEN_ODD_EXISTS_EQ: "ALL n. EVEN n = (EX m. n = 2 * m) & ODD n = (EX m. n = Suc (2 * m))"
    1.15 +  by (import prob_extra EVEN_ODD_EXISTS_EQ)
    1.16 +
    1.17 +lemma DIV_THEN_MULT: "ALL p q. Suc q * (p div Suc q) <= p"
    1.18 +  by (import prob_extra DIV_THEN_MULT)
    1.19 +
    1.20 +lemma DIV_TWO_UNIQUE: "(All::(nat => bool) => bool)
    1.21 + (%n::nat.
    1.22 +     (All::(nat => bool) => bool)
    1.23 +      (%q::nat.
    1.24 +          (All::(nat => bool) => bool)
    1.25 +           (%r::nat.
    1.26 +               (op -->::bool => bool => bool)
    1.27 +                ((op &::bool => bool => bool)
    1.28 +                  ((op =::nat => nat => bool) n
    1.29 +                    ((op +::nat => nat => nat)
    1.30 +                      ((op *::nat => nat => nat)
    1.31 +                        ((number_of::bin => nat)
    1.32 +                          ((op BIT::bin => bool => bin)
    1.33 +                            ((op BIT::bin => bool => bin) (bin.Pls::bin)
    1.34 +                              (True::bool))
    1.35 +                            (False::bool)))
    1.36 +                        q)
    1.37 +                      r))
    1.38 +                  ((op |::bool => bool => bool)
    1.39 +                    ((op =::nat => nat => bool) r (0::nat))
    1.40 +                    ((op =::nat => nat => bool) r (1::nat))))
    1.41 +                ((op &::bool => bool => bool)
    1.42 +                  ((op =::nat => nat => bool) q
    1.43 +                    ((op div::nat => nat => nat) n
    1.44 +                      ((number_of::bin => nat)
    1.45 +                        ((op BIT::bin => bool => bin)
    1.46 +                          ((op BIT::bin => bool => bin) (bin.Pls::bin)
    1.47 +                            (True::bool))
    1.48 +                          (False::bool)))))
    1.49 +                  ((op =::nat => nat => bool) r
    1.50 +                    ((op mod::nat => nat => nat) n
    1.51 +                      ((number_of::bin => nat)
    1.52 +                        ((op BIT::bin => bool => bin)
    1.53 +                          ((op BIT::bin => bool => bin) (bin.Pls::bin)
    1.54 +                            (True::bool))
    1.55 +                          (False::bool)))))))))"
    1.56 +  by (import prob_extra DIV_TWO_UNIQUE)
    1.57 +
    1.58 +lemma DIVISION_TWO: "ALL n::nat.
    1.59 +   n = (2::nat) * (n div (2::nat)) + n mod (2::nat) &
    1.60 +   (n mod (2::nat) = (0::nat) | n mod (2::nat) = (1::nat))"
    1.61 +  by (import prob_extra DIVISION_TWO)
    1.62 +
    1.63 +lemma DIV_TWO: "ALL n::nat. n = (2::nat) * (n div (2::nat)) + n mod (2::nat)"
    1.64 +  by (import prob_extra DIV_TWO)
    1.65 +
    1.66 +lemma MOD_TWO: "ALL n. n mod 2 = (if EVEN n then 0 else 1)"
    1.67 +  by (import prob_extra MOD_TWO)
    1.68 +
    1.69 +lemma DIV_TWO_BASIC: "(0::nat) div (2::nat) = (0::nat) &
    1.70 +(1::nat) div (2::nat) = (0::nat) & (2::nat) div (2::nat) = (1::nat)"
    1.71 +  by (import prob_extra DIV_TWO_BASIC)
    1.72 +
    1.73 +lemma DIV_TWO_MONO: "(All::(nat => bool) => bool)
    1.74 + (%m::nat.
    1.75 +     (All::(nat => bool) => bool)
    1.76 +      (%n::nat.
    1.77 +          (op -->::bool => bool => bool)
    1.78 +           ((op <::nat => nat => bool)
    1.79 +             ((op div::nat => nat => nat) m
    1.80 +               ((number_of::bin => nat)
    1.81 +                 ((op BIT::bin => bool => bin)
    1.82 +                   ((op BIT::bin => bool => bin) (bin.Pls::bin)
    1.83 +                     (True::bool))
    1.84 +                   (False::bool))))
    1.85 +             ((op div::nat => nat => nat) n
    1.86 +               ((number_of::bin => nat)
    1.87 +                 ((op BIT::bin => bool => bin)
    1.88 +                   ((op BIT::bin => bool => bin) (bin.Pls::bin)
    1.89 +                     (True::bool))
    1.90 +                   (False::bool)))))
    1.91 +           ((op <::nat => nat => bool) m n)))"
    1.92 +  by (import prob_extra DIV_TWO_MONO)
    1.93 +
    1.94 +lemma DIV_TWO_MONO_EVEN: "(All::(nat => bool) => bool)
    1.95 + (%m::nat.
    1.96 +     (All::(nat => bool) => bool)
    1.97 +      (%n::nat.
    1.98 +          (op -->::bool => bool => bool) ((EVEN::nat => bool) n)
    1.99 +           ((op =::bool => bool => bool)
   1.100 +             ((op <::nat => nat => bool)
   1.101 +               ((op div::nat => nat => nat) m
   1.102 +                 ((number_of::bin => nat)
   1.103 +                   ((op BIT::bin => bool => bin)
   1.104 +                     ((op BIT::bin => bool => bin) (bin.Pls::bin)
   1.105 +                       (True::bool))
   1.106 +                     (False::bool))))
   1.107 +               ((op div::nat => nat => nat) n
   1.108 +                 ((number_of::bin => nat)
   1.109 +                   ((op BIT::bin => bool => bin)
   1.110 +                     ((op BIT::bin => bool => bin) (bin.Pls::bin)
   1.111 +                       (True::bool))
   1.112 +                     (False::bool)))))
   1.113 +             ((op <::nat => nat => bool) m n))))"
   1.114 +  by (import prob_extra DIV_TWO_MONO_EVEN)
   1.115 +
   1.116 +lemma DIV_TWO_CANCEL: "ALL n. 2 * n div 2 = n & Suc (2 * n) div 2 = n"
   1.117 +  by (import prob_extra DIV_TWO_CANCEL)
   1.118 +
   1.119 +lemma EXP_DIV_TWO: "ALL n::nat. (2::nat) ^ Suc n div (2::nat) = (2::nat) ^ n"
   1.120 +  by (import prob_extra EXP_DIV_TWO)
   1.121 +
   1.122 +lemma EVEN_EXP_TWO: "ALL n. EVEN (2 ^ n) = (n ~= 0)"
   1.123 +  by (import prob_extra EVEN_EXP_TWO)
   1.124 +
   1.125 +lemma DIV_TWO_EXP: "ALL (n::nat) k::nat.
   1.126 +   (k div (2::nat) < (2::nat) ^ n) = (k < (2::nat) ^ Suc n)"
   1.127 +  by (import prob_extra DIV_TWO_EXP)
   1.128 +
   1.129 +consts
   1.130 +  inf :: "(real => bool) => real" 
   1.131 +
   1.132 +defs
   1.133 +  inf_primdef: "inf == %P. - sup (IMAGE uminus P)"
   1.134 +
   1.135 +lemma inf_def: "ALL P. inf P = - sup (IMAGE uminus P)"
   1.136 +  by (import prob_extra inf_def)
   1.137 +
   1.138 +lemma INF_DEF_ALT: "ALL P. inf P = - sup (%r. P (- r))"
   1.139 +  by (import prob_extra INF_DEF_ALT)
   1.140 +
   1.141 +lemma REAL_SUP_EXISTS_UNIQUE: "(All::((real => bool) => bool) => bool)
   1.142 + (%P::real => bool.
   1.143 +     (op -->::bool => bool => bool)
   1.144 +      ((op &::bool => bool => bool) ((Ex::(real => bool) => bool) P)
   1.145 +        ((Ex::(real => bool) => bool)
   1.146 +          (%z::real.
   1.147 +              (All::(real => bool) => bool)
   1.148 +               (%x::real.
   1.149 +                   (op -->::bool => bool => bool) (P x)
   1.150 +                    ((op <=::real => real => bool) x z)))))
   1.151 +      ((Ex1::(real => bool) => bool)
   1.152 +        (%s::real.
   1.153 +            (All::(real => bool) => bool)
   1.154 +             (%y::real.
   1.155 +                 (op =::bool => bool => bool)
   1.156 +                  ((Ex::(real => bool) => bool)
   1.157 +                    (%x::real.
   1.158 +                        (op &::bool => bool => bool) (P x)
   1.159 +                         ((op <::real => real => bool) y x)))
   1.160 +                  ((op <::real => real => bool) y s)))))"
   1.161 +  by (import prob_extra REAL_SUP_EXISTS_UNIQUE)
   1.162 +
   1.163 +lemma REAL_SUP_MAX: "(All::((real => bool) => bool) => bool)
   1.164 + (%P::real => bool.
   1.165 +     (All::(real => bool) => bool)
   1.166 +      (%z::real.
   1.167 +          (op -->::bool => bool => bool)
   1.168 +           ((op &::bool => bool => bool) (P z)
   1.169 +             ((All::(real => bool) => bool)
   1.170 +               (%x::real.
   1.171 +                   (op -->::bool => bool => bool) (P x)
   1.172 +                    ((op <=::real => real => bool) x z))))
   1.173 +           ((op =::real => real => bool) ((sup::(real => bool) => real) P)
   1.174 +             z)))"
   1.175 +  by (import prob_extra REAL_SUP_MAX)
   1.176 +
   1.177 +lemma REAL_INF_MIN: "(All::((real => bool) => bool) => bool)
   1.178 + (%P::real => bool.
   1.179 +     (All::(real => bool) => bool)
   1.180 +      (%z::real.
   1.181 +          (op -->::bool => bool => bool)
   1.182 +           ((op &::bool => bool => bool) (P z)
   1.183 +             ((All::(real => bool) => bool)
   1.184 +               (%x::real.
   1.185 +                   (op -->::bool => bool => bool) (P x)
   1.186 +                    ((op <=::real => real => bool) z x))))
   1.187 +           ((op =::real => real => bool) ((inf::(real => bool) => real) P)
   1.188 +             z)))"
   1.189 +  by (import prob_extra REAL_INF_MIN)
   1.190 +
   1.191 +lemma HALF_POS: "(0::real) < (1::real) / (2::real)"
   1.192 +  by (import prob_extra HALF_POS)
   1.193 +
   1.194 +lemma HALF_CANCEL: "(2::real) * ((1::real) / (2::real)) = (1::real)"
   1.195 +  by (import prob_extra HALF_CANCEL)
   1.196 +
   1.197 +lemma POW_HALF_POS: "ALL n::nat. (0::real) < ((1::real) / (2::real)) ^ n"
   1.198 +  by (import prob_extra POW_HALF_POS)
   1.199 +
   1.200 +lemma POW_HALF_MONO: "(All::(nat => bool) => bool)
   1.201 + (%m::nat.
   1.202 +     (All::(nat => bool) => bool)
   1.203 +      (%n::nat.
   1.204 +          (op -->::bool => bool => bool) ((op <=::nat => nat => bool) m n)
   1.205 +           ((op <=::real => real => bool)
   1.206 +             ((op ^::real => nat => real)
   1.207 +               ((op /::real => real => real) (1::real)
   1.208 +                 ((number_of::bin => real)
   1.209 +                   ((op BIT::bin => bool => bin)
   1.210 +                     ((op BIT::bin => bool => bin) (bin.Pls::bin)
   1.211 +                       (True::bool))
   1.212 +                     (False::bool))))
   1.213 +               n)
   1.214 +             ((op ^::real => nat => real)
   1.215 +               ((op /::real => real => real) (1::real)
   1.216 +                 ((number_of::bin => real)
   1.217 +                   ((op BIT::bin => bool => bin)
   1.218 +                     ((op BIT::bin => bool => bin) (bin.Pls::bin)
   1.219 +                       (True::bool))
   1.220 +                     (False::bool))))
   1.221 +               m))))"
   1.222 +  by (import prob_extra POW_HALF_MONO)
   1.223 +
   1.224 +lemma POW_HALF_TWICE: "ALL n::nat.
   1.225 +   ((1::real) / (2::real)) ^ n = (2::real) * ((1::real) / (2::real)) ^ Suc n"
   1.226 +  by (import prob_extra POW_HALF_TWICE)
   1.227 +
   1.228 +lemma X_HALF_HALF: "ALL x::real. (1::real) / (2::real) * x + (1::real) / (2::real) * x = x"
   1.229 +  by (import prob_extra X_HALF_HALF)
   1.230 +
   1.231 +lemma REAL_SUP_LE_X: "(All::((real => bool) => bool) => bool)
   1.232 + (%P::real => bool.
   1.233 +     (All::(real => bool) => bool)
   1.234 +      (%x::real.
   1.235 +          (op -->::bool => bool => bool)
   1.236 +           ((op &::bool => bool => bool) ((Ex::(real => bool) => bool) P)
   1.237 +             ((All::(real => bool) => bool)
   1.238 +               (%r::real.
   1.239 +                   (op -->::bool => bool => bool) (P r)
   1.240 +                    ((op <=::real => real => bool) r x))))
   1.241 +           ((op <=::real => real => bool) ((sup::(real => bool) => real) P)
   1.242 +             x)))"
   1.243 +  by (import prob_extra REAL_SUP_LE_X)
   1.244 +
   1.245 +lemma REAL_X_LE_SUP: "(All::((real => bool) => bool) => bool)
   1.246 + (%P::real => bool.
   1.247 +     (All::(real => bool) => bool)
   1.248 +      (%x::real.
   1.249 +          (op -->::bool => bool => bool)
   1.250 +           ((op &::bool => bool => bool) ((Ex::(real => bool) => bool) P)
   1.251 +             ((op &::bool => bool => bool)
   1.252 +               ((Ex::(real => bool) => bool)
   1.253 +                 (%z::real.
   1.254 +                     (All::(real => bool) => bool)
   1.255 +                      (%r::real.
   1.256 +                          (op -->::bool => bool => bool) (P r)
   1.257 +                           ((op <=::real => real => bool) r z))))
   1.258 +               ((Ex::(real => bool) => bool)
   1.259 +                 (%r::real.
   1.260 +                     (op &::bool => bool => bool) (P r)
   1.261 +                      ((op <=::real => real => bool) x r)))))
   1.262 +           ((op <=::real => real => bool) x
   1.263 +             ((sup::(real => bool) => real) P))))"
   1.264 +  by (import prob_extra REAL_X_LE_SUP)
   1.265 +
   1.266 +lemma ABS_BETWEEN_LE: "ALL (x::real) (y::real) d::real.
   1.267 +   ((0::real) <= d & x - d <= y & y <= x + d) = (abs (y - x) <= d)"
   1.268 +  by (import prob_extra ABS_BETWEEN_LE)
   1.269 +
   1.270 +lemma ONE_MINUS_HALF: "(1::real) - (1::real) / (2::real) = (1::real) / (2::real)"
   1.271 +  by (import prob_extra ONE_MINUS_HALF)
   1.272 +
   1.273 +lemma HALF_LT_1: "(1::real) / (2::real) < (1::real)"
   1.274 +  by (import prob_extra HALF_LT_1)
   1.275 +
   1.276 +lemma POW_HALF_EXP: "ALL n::nat. ((1::real) / (2::real)) ^ n = inverse (real ((2::nat) ^ n))"
   1.277 +  by (import prob_extra POW_HALF_EXP)
   1.278 +
   1.279 +lemma INV_SUC_POS: "ALL n. 0 < 1 / real (Suc n)"
   1.280 +  by (import prob_extra INV_SUC_POS)
   1.281 +
   1.282 +lemma INV_SUC_MAX: "ALL x. 1 / real (Suc x) <= 1"
   1.283 +  by (import prob_extra INV_SUC_MAX)
   1.284 +
   1.285 +lemma INV_SUC: "ALL n. 0 < 1 / real (Suc n) & 1 / real (Suc n) <= 1"
   1.286 +  by (import prob_extra INV_SUC)
   1.287 +
   1.288 +lemma ABS_UNIT_INTERVAL: "(All::(real => bool) => bool)
   1.289 + (%x::real.
   1.290 +     (All::(real => bool) => bool)
   1.291 +      (%y::real.
   1.292 +          (op -->::bool => bool => bool)
   1.293 +           ((op &::bool => bool => bool)
   1.294 +             ((op <=::real => real => bool) (0::real) x)
   1.295 +             ((op &::bool => bool => bool)
   1.296 +               ((op <=::real => real => bool) x (1::real))
   1.297 +               ((op &::bool => bool => bool)
   1.298 +                 ((op <=::real => real => bool) (0::real) y)
   1.299 +                 ((op <=::real => real => bool) y (1::real)))))
   1.300 +           ((op <=::real => real => bool)
   1.301 +             ((abs::real => real) ((op -::real => real => real) x y))
   1.302 +             (1::real))))"
   1.303 +  by (import prob_extra ABS_UNIT_INTERVAL)
   1.304 +
   1.305 +lemma MEM_NIL: "ALL l. (ALL x. ~ x mem l) = (l = [])"
   1.306 +  by (import prob_extra MEM_NIL)
   1.307 +
   1.308 +lemma MAP_MEM: "ALL f l x. x mem map f l = (EX y. y mem l & x = f y)"
   1.309 +  by (import prob_extra MAP_MEM)
   1.310 +
   1.311 +lemma MEM_NIL_MAP_CONS: "ALL x l. ~ [] mem map (op # x) l"
   1.312 +  by (import prob_extra MEM_NIL_MAP_CONS)
   1.313 +
   1.314 +lemma FILTER_TRUE: "ALL l. [x:l. True] = l"
   1.315 +  by (import prob_extra FILTER_TRUE)
   1.316 +
   1.317 +lemma FILTER_FALSE: "ALL l. [x:l. False] = []"
   1.318 +  by (import prob_extra FILTER_FALSE)
   1.319 +
   1.320 +lemma FILTER_MEM: "(All::(('a => bool) => bool) => bool)
   1.321 + (%P::'a => bool.
   1.322 +     (All::('a => bool) => bool)
   1.323 +      (%x::'a.
   1.324 +          (All::('a list => bool) => bool)
   1.325 +           (%l::'a list.
   1.326 +               (op -->::bool => bool => bool)
   1.327 +                ((op mem::'a => 'a list => bool) x
   1.328 +                  ((filter::('a => bool) => 'a list => 'a list) P l))
   1.329 +                (P x))))"
   1.330 +  by (import prob_extra FILTER_MEM)
   1.331 +
   1.332 +lemma MEM_FILTER: "(All::(('a => bool) => bool) => bool)
   1.333 + (%P::'a => bool.
   1.334 +     (All::('a list => bool) => bool)
   1.335 +      (%l::'a list.
   1.336 +          (All::('a => bool) => bool)
   1.337 +           (%x::'a.
   1.338 +               (op -->::bool => bool => bool)
   1.339 +                ((op mem::'a => 'a list => bool) x
   1.340 +                  ((filter::('a => bool) => 'a list => 'a list) P l))
   1.341 +                ((op mem::'a => 'a list => bool) x l))))"
   1.342 +  by (import prob_extra MEM_FILTER)
   1.343 +
   1.344 +lemma FILTER_OUT_ELT: "ALL x l. x mem l | [y:l. y ~= x] = l"
   1.345 +  by (import prob_extra FILTER_OUT_ELT)
   1.346 +
   1.347 +lemma IS_PREFIX_NIL: "ALL x. IS_PREFIX x [] & IS_PREFIX [] x = (x = [])"
   1.348 +  by (import prob_extra IS_PREFIX_NIL)
   1.349 +
   1.350 +lemma IS_PREFIX_REFL: "ALL x. IS_PREFIX x x"
   1.351 +  by (import prob_extra IS_PREFIX_REFL)
   1.352 +
   1.353 +lemma IS_PREFIX_ANTISYM: "(All::('a list => bool) => bool)
   1.354 + (%x::'a list.
   1.355 +     (All::('a list => bool) => bool)
   1.356 +      (%y::'a list.
   1.357 +          (op -->::bool => bool => bool)
   1.358 +           ((op &::bool => bool => bool)
   1.359 +             ((IS_PREFIX::'a list => 'a list => bool) y x)
   1.360 +             ((IS_PREFIX::'a list => 'a list => bool) x y))
   1.361 +           ((op =::'a list => 'a list => bool) x y)))"
   1.362 +  by (import prob_extra IS_PREFIX_ANTISYM)
   1.363 +
   1.364 +lemma IS_PREFIX_TRANS: "(All::('a list => bool) => bool)
   1.365 + (%x::'a list.
   1.366 +     (All::('a list => bool) => bool)
   1.367 +      (%y::'a list.
   1.368 +          (All::('a list => bool) => bool)
   1.369 +           (%z::'a list.
   1.370 +               (op -->::bool => bool => bool)
   1.371 +                ((op &::bool => bool => bool)
   1.372 +                  ((IS_PREFIX::'a list => 'a list => bool) x y)
   1.373 +                  ((IS_PREFIX::'a list => 'a list => bool) y z))
   1.374 +                ((IS_PREFIX::'a list => 'a list => bool) x z))))"
   1.375 +  by (import prob_extra IS_PREFIX_TRANS)
   1.376 +
   1.377 +lemma IS_PREFIX_BUTLAST: "ALL x y. IS_PREFIX (x # y) (butlast (x # y))"
   1.378 +  by (import prob_extra IS_PREFIX_BUTLAST)
   1.379 +
   1.380 +lemma IS_PREFIX_LENGTH: "(All::('a list => bool) => bool)
   1.381 + (%x::'a list.
   1.382 +     (All::('a list => bool) => bool)
   1.383 +      (%y::'a list.
   1.384 +          (op -->::bool => bool => bool)
   1.385 +           ((IS_PREFIX::'a list => 'a list => bool) y x)
   1.386 +           ((op <=::nat => nat => bool) ((size::'a list => nat) x)
   1.387 +             ((size::'a list => nat) y))))"
   1.388 +  by (import prob_extra IS_PREFIX_LENGTH)
   1.389 +
   1.390 +lemma IS_PREFIX_LENGTH_ANTI: "(All::('a list => bool) => bool)
   1.391 + (%x::'a list.
   1.392 +     (All::('a list => bool) => bool)
   1.393 +      (%y::'a list.
   1.394 +          (op -->::bool => bool => bool)
   1.395 +           ((op &::bool => bool => bool)
   1.396 +             ((IS_PREFIX::'a list => 'a list => bool) y x)
   1.397 +             ((op =::nat => nat => bool) ((size::'a list => nat) x)
   1.398 +               ((size::'a list => nat) y)))
   1.399 +           ((op =::'a list => 'a list => bool) x y)))"
   1.400 +  by (import prob_extra IS_PREFIX_LENGTH_ANTI)
   1.401 +
   1.402 +lemma IS_PREFIX_SNOC: "ALL x y z. IS_PREFIX (SNOC x y) z = (IS_PREFIX y z | z = SNOC x y)"
   1.403 +  by (import prob_extra IS_PREFIX_SNOC)
   1.404 +
   1.405 +lemma FOLDR_MAP: "ALL (f::'b => 'c => 'c) (e::'c) (g::'a => 'b) l::'a list.
   1.406 +   foldr f (map g l) e = foldr (%x::'a. f (g x)) l e"
   1.407 +  by (import prob_extra FOLDR_MAP)
   1.408 +
   1.409 +lemma LAST_MEM: "ALL h t. last (h # t) mem h # t"
   1.410 +  by (import prob_extra LAST_MEM)
   1.411 +
   1.412 +lemma LAST_MAP_CONS: "ALL (b::bool) (h::bool list) t::bool list list.
   1.413 +   EX x::bool list. last (map (op # b) (h # t)) = b # x"
   1.414 +  by (import prob_extra LAST_MAP_CONS)
   1.415 +
   1.416 +lemma EXISTS_LONGEST: "(All::('a list => bool) => bool)
   1.417 + (%x::'a list.
   1.418 +     (All::('a list list => bool) => bool)
   1.419 +      (%y::'a list list.
   1.420 +          (Ex::('a list => bool) => bool)
   1.421 +           (%z::'a list.
   1.422 +               (op &::bool => bool => bool)
   1.423 +                ((op mem::'a list => 'a list list => bool) z
   1.424 +                  ((op #::'a list => 'a list list => 'a list list) x y))
   1.425 +                ((All::('a list => bool) => bool)
   1.426 +                  (%w::'a list.
   1.427 +                      (op -->::bool => bool => bool)
   1.428 +                       ((op mem::'a list => 'a list list => bool) w
   1.429 +                         ((op #::'a list => 'a list list => 'a list list) x
   1.430 +                           y))
   1.431 +                       ((op <=::nat => nat => bool)
   1.432 +                         ((size::'a list => nat) w)
   1.433 +                         ((size::'a list => nat) z)))))))"
   1.434 +  by (import prob_extra EXISTS_LONGEST)
   1.435 +
   1.436 +lemma UNION_DEF_ALT: "ALL s t. pred_set.UNION s t = (%x. s x | t x)"
   1.437 +  by (import prob_extra UNION_DEF_ALT)
   1.438 +
   1.439 +lemma INTER_UNION_RDISTRIB: "ALL p q r.
   1.440 +   pred_set.INTER (pred_set.UNION p q) r =
   1.441 +   pred_set.UNION (pred_set.INTER p r) (pred_set.INTER q r)"
   1.442 +  by (import prob_extra INTER_UNION_RDISTRIB)
   1.443 +
   1.444 +lemma SUBSET_EQ: "ALL x xa. (x = xa) = (SUBSET x xa & SUBSET xa x)"
   1.445 +  by (import prob_extra SUBSET_EQ)
   1.446 +
   1.447 +lemma INTER_IS_EMPTY: "ALL s t. (pred_set.INTER s t = EMPTY) = (ALL x. ~ s x | ~ t x)"
   1.448 +  by (import prob_extra INTER_IS_EMPTY)
   1.449 +
   1.450 +lemma UNION_DISJOINT_SPLIT: "(All::(('a => bool) => bool) => bool)
   1.451 + (%s::'a => bool.
   1.452 +     (All::(('a => bool) => bool) => bool)
   1.453 +      (%t::'a => bool.
   1.454 +          (All::(('a => bool) => bool) => bool)
   1.455 +           (%u::'a => bool.
   1.456 +               (op -->::bool => bool => bool)
   1.457 +                ((op &::bool => bool => bool)
   1.458 +                  ((op =::('a => bool) => ('a => bool) => bool)
   1.459 +                    ((pred_set.UNION::('a => bool)
   1.460 +=> ('a => bool) => 'a => bool)
   1.461 +                      s t)
   1.462 +                    ((pred_set.UNION::('a => bool)
   1.463 +=> ('a => bool) => 'a => bool)
   1.464 +                      s u))
   1.465 +                  ((op &::bool => bool => bool)
   1.466 +                    ((op =::('a => bool) => ('a => bool) => bool)
   1.467 +                      ((pred_set.INTER::('a => bool)
   1.468 +  => ('a => bool) => 'a => bool)
   1.469 +                        s t)
   1.470 +                      (EMPTY::'a => bool))
   1.471 +                    ((op =::('a => bool) => ('a => bool) => bool)
   1.472 +                      ((pred_set.INTER::('a => bool)
   1.473 +  => ('a => bool) => 'a => bool)
   1.474 +                        s u)
   1.475 +                      (EMPTY::'a => bool))))
   1.476 +                ((op =::('a => bool) => ('a => bool) => bool) t u))))"
   1.477 +  by (import prob_extra UNION_DISJOINT_SPLIT)
   1.478 +
   1.479 +lemma GSPEC_DEF_ALT: "ALL f. GSPEC f = (%v. EX x. (v, True) = f x)"
   1.480 +  by (import prob_extra GSPEC_DEF_ALT)
   1.481 +
   1.482 +;end_setup
   1.483 +
   1.484 +;setup_theory prob_canon
   1.485 +
   1.486 +consts
   1.487 +  alg_twin :: "bool list => bool list => bool" 
   1.488 +
   1.489 +defs
   1.490 +  alg_twin_primdef: "alg_twin == %x y. EX l. x = SNOC True l & y = SNOC False l"
   1.491 +
   1.492 +lemma alg_twin_def: "ALL x y. alg_twin x y = (EX l. x = SNOC True l & y = SNOC False l)"
   1.493 +  by (import prob_canon alg_twin_def)
   1.494 +
   1.495 +constdefs
   1.496 +  alg_order_tupled :: "bool list * bool list => bool" 
   1.497 +  "(op ==::(bool list * bool list => bool)
   1.498 +        => (bool list * bool list => bool) => prop)
   1.499 + (alg_order_tupled::bool list * bool list => bool)
   1.500 + ((WFREC::(bool list * bool list => bool list * bool list => bool)
   1.501 +          => ((bool list * bool list => bool)
   1.502 +              => bool list * bool list => bool)
   1.503 +             => bool list * bool list => bool)
   1.504 +   ((Eps::((bool list * bool list => bool list * bool list => bool) => bool)
   1.505 +          => bool list * bool list => bool list * bool list => bool)
   1.506 +     (%R::bool list * bool list => bool list * bool list => bool.
   1.507 +         (op &::bool => bool => bool)
   1.508 +          ((WF::(bool list * bool list => bool list * bool list => bool)
   1.509 +                => bool)
   1.510 +            R)
   1.511 +          ((All::(bool => bool) => bool)
   1.512 +            (%h'::bool.
   1.513 +                (All::(bool => bool) => bool)
   1.514 +                 (%h::bool.
   1.515 +                     (All::(bool list => bool) => bool)
   1.516 +                      (%t'::bool list.
   1.517 +                          (All::(bool list => bool) => bool)
   1.518 +                           (%t::bool list.
   1.519 +                               R ((Pair::bool list
   1.520 +   => bool list => bool list * bool list)
   1.521 +                                   t t')
   1.522 +                                ((Pair::bool list
   1.523 +  => bool list => bool list * bool list)
   1.524 +                                  ((op #::bool => bool list => bool list) h
   1.525 +                                    t)
   1.526 +                                  ((op #::bool => bool list => bool list) h'
   1.527 +                                    t')))))))))
   1.528 +   (%alg_order_tupled::bool list * bool list => bool.
   1.529 +       (split::(bool list => bool list => bool)
   1.530 +               => bool list * bool list => bool)
   1.531 +        (%(v::bool list) v1::bool list.
   1.532 +            (list_case::bool
   1.533 +                        => (bool => bool list => bool) => bool list => bool)
   1.534 +             ((list_case::bool
   1.535 +                          => (bool => bool list => bool)
   1.536 +                             => bool list => bool)
   1.537 +               (True::bool) (%(v8::bool) v9::bool list. True::bool) v1)
   1.538 +             (%(v4::bool) v5::bool list.
   1.539 +                 (list_case::bool
   1.540 +                             => (bool => bool list => bool)
   1.541 +                                => bool list => bool)
   1.542 +                  (False::bool)
   1.543 +                  (%(v10::bool) v11::bool list.
   1.544 +                      (op |::bool => bool => bool)
   1.545 +                       ((op &::bool => bool => bool)
   1.546 +                         ((op =::bool => bool => bool) v4 (True::bool))
   1.547 +                         ((op =::bool => bool => bool) v10 (False::bool)))
   1.548 +                       ((op &::bool => bool => bool)
   1.549 +                         ((op =::bool => bool => bool) v4 v10)
   1.550 +                         (alg_order_tupled
   1.551 +                           ((Pair::bool list
   1.552 +                                   => bool list => bool list * bool list)
   1.553 +                             v5 v11))))
   1.554 +                  v1)
   1.555 +             v)))"
   1.556 +
   1.557 +lemma alg_order_tupled_primitive_def: "(op =::(bool list * bool list => bool)
   1.558 +       => (bool list * bool list => bool) => bool)
   1.559 + (alg_order_tupled::bool list * bool list => bool)
   1.560 + ((WFREC::(bool list * bool list => bool list * bool list => bool)
   1.561 +          => ((bool list * bool list => bool)
   1.562 +              => bool list * bool list => bool)
   1.563 +             => bool list * bool list => bool)
   1.564 +   ((Eps::((bool list * bool list => bool list * bool list => bool) => bool)
   1.565 +          => bool list * bool list => bool list * bool list => bool)
   1.566 +     (%R::bool list * bool list => bool list * bool list => bool.
   1.567 +         (op &::bool => bool => bool)
   1.568 +          ((WF::(bool list * bool list => bool list * bool list => bool)
   1.569 +                => bool)
   1.570 +            R)
   1.571 +          ((All::(bool => bool) => bool)
   1.572 +            (%h'::bool.
   1.573 +                (All::(bool => bool) => bool)
   1.574 +                 (%h::bool.
   1.575 +                     (All::(bool list => bool) => bool)
   1.576 +                      (%t'::bool list.
   1.577 +                          (All::(bool list => bool) => bool)
   1.578 +                           (%t::bool list.
   1.579 +                               R ((Pair::bool list
   1.580 +   => bool list => bool list * bool list)
   1.581 +                                   t t')
   1.582 +                                ((Pair::bool list
   1.583 +  => bool list => bool list * bool list)
   1.584 +                                  ((op #::bool => bool list => bool list) h
   1.585 +                                    t)
   1.586 +                                  ((op #::bool => bool list => bool list) h'
   1.587 +                                    t')))))))))
   1.588 +   (%alg_order_tupled::bool list * bool list => bool.
   1.589 +       (split::(bool list => bool list => bool)
   1.590 +               => bool list * bool list => bool)
   1.591 +        (%(v::bool list) v1::bool list.
   1.592 +            (list_case::bool
   1.593 +                        => (bool => bool list => bool) => bool list => bool)
   1.594 +             ((list_case::bool
   1.595 +                          => (bool => bool list => bool)
   1.596 +                             => bool list => bool)
   1.597 +               (True::bool) (%(v8::bool) v9::bool list. True::bool) v1)
   1.598 +             (%(v4::bool) v5::bool list.
   1.599 +                 (list_case::bool
   1.600 +                             => (bool => bool list => bool)
   1.601 +                                => bool list => bool)
   1.602 +                  (False::bool)
   1.603 +                  (%(v10::bool) v11::bool list.
   1.604 +                      (op |::bool => bool => bool)
   1.605 +                       ((op &::bool => bool => bool)
   1.606 +                         ((op =::bool => bool => bool) v4 (True::bool))
   1.607 +                         ((op =::bool => bool => bool) v10 (False::bool)))
   1.608 +                       ((op &::bool => bool => bool)
   1.609 +                         ((op =::bool => bool => bool) v4 v10)
   1.610 +                         (alg_order_tupled
   1.611 +                           ((Pair::bool list
   1.612 +                                   => bool list => bool list * bool list)
   1.613 +                             v5 v11))))
   1.614 +                  v1)
   1.615 +             v)))"
   1.616 +  by (import prob_canon alg_order_tupled_primitive_def)
   1.617 +
   1.618 +consts
   1.619 +  alg_order :: "bool list => bool list => bool" 
   1.620 +
   1.621 +defs
   1.622 +  alg_order_primdef: "alg_order == %x x1. alg_order_tupled (x, x1)"
   1.623 +
   1.624 +lemma alg_order_curried_def: "ALL x x1. alg_order x x1 = alg_order_tupled (x, x1)"
   1.625 +  by (import prob_canon alg_order_curried_def)
   1.626 +
   1.627 +lemma alg_order_ind: "(All::((bool list => bool list => bool) => bool) => bool)
   1.628 + (%P::bool list => bool list => bool.
   1.629 +     (op -->::bool => bool => bool)
   1.630 +      ((op &::bool => bool => bool)
   1.631 +        ((All::(bool => bool) => bool)
   1.632 +          (%x::bool.
   1.633 +              (All::(bool list => bool) => bool)
   1.634 +               (%xa::bool list.
   1.635 +                   P ([]::bool list)
   1.636 +                    ((op #::bool => bool list => bool list) x xa))))
   1.637 +        ((op &::bool => bool => bool) (P ([]::bool list) ([]::bool list))
   1.638 +          ((op &::bool => bool => bool)
   1.639 +            ((All::(bool => bool) => bool)
   1.640 +              (%x::bool.
   1.641 +                  (All::(bool list => bool) => bool)
   1.642 +                   (%xa::bool list.
   1.643 +                       P ((op #::bool => bool list => bool list) x xa)
   1.644 +                        ([]::bool list))))
   1.645 +            ((All::(bool => bool) => bool)
   1.646 +              (%x::bool.
   1.647 +                  (All::(bool list => bool) => bool)
   1.648 +                   (%xa::bool list.
   1.649 +                       (All::(bool => bool) => bool)
   1.650 +                        (%xb::bool.
   1.651 +                            (All::(bool list => bool) => bool)
   1.652 +                             (%xc::bool list.
   1.653 +                                 (op -->::bool => bool => bool) (P xa xc)
   1.654 +                                  (P ((op #::bool => bool list => bool list)
   1.655 + x xa)
   1.656 +                                    ((op #::bool => bool list => bool list)
   1.657 +xb xc))))))))))
   1.658 +      ((All::(bool list => bool) => bool)
   1.659 +        (%x::bool list. (All::(bool list => bool) => bool) (P x))))"
   1.660 +  by (import prob_canon alg_order_ind)
   1.661 +
   1.662 +lemma alg_order_def: "alg_order [] (v6 # v7) = True &
   1.663 +alg_order [] [] = True &
   1.664 +alg_order (v2 # v3) [] = False &
   1.665 +alg_order (h # t) (h' # t') =
   1.666 +(h = True & h' = False | h = h' & alg_order t t')"
   1.667 +  by (import prob_canon alg_order_def)
   1.668 +
   1.669 +consts
   1.670 +  alg_sorted :: "bool list list => bool" 
   1.671 +
   1.672 +defs
   1.673 +  alg_sorted_primdef: "alg_sorted ==
   1.674 +WFREC (SOME R. WF R & (ALL x z y. R (y # z) (x # y # z)))
   1.675 + (%alg_sorted.
   1.676 +     list_case True
   1.677 +      (%v2. list_case True
   1.678 +             (%v6 v7. alg_order v2 v6 & alg_sorted (v6 # v7))))"
   1.679 +
   1.680 +lemma alg_sorted_primitive_def: "alg_sorted =
   1.681 +WFREC (SOME R. WF R & (ALL x z y. R (y # z) (x # y # z)))
   1.682 + (%alg_sorted.
   1.683 +     list_case True
   1.684 +      (%v2. list_case True
   1.685 +             (%v6 v7. alg_order v2 v6 & alg_sorted (v6 # v7))))"
   1.686 +  by (import prob_canon alg_sorted_primitive_def)
   1.687 +
   1.688 +lemma alg_sorted_ind: "(All::((bool list list => bool) => bool) => bool)
   1.689 + (%P::bool list list => bool.
   1.690 +     (op -->::bool => bool => bool)
   1.691 +      ((op &::bool => bool => bool)
   1.692 +        ((All::(bool list => bool) => bool)
   1.693 +          (%x::bool list.
   1.694 +              (All::(bool list => bool) => bool)
   1.695 +               (%y::bool list.
   1.696 +                   (All::(bool list list => bool) => bool)
   1.697 +                    (%z::bool list list.
   1.698 +                        (op -->::bool => bool => bool)
   1.699 +                         (P ((op #::bool list
   1.700 +                                    => bool list list => bool list list)
   1.701 +                              y z))
   1.702 +                         (P ((op #::bool list
   1.703 +                                    => bool list list => bool list list)
   1.704 +                              x ((op #::bool list
   1.705 +  => bool list list => bool list list)
   1.706 +                                  y z)))))))
   1.707 +        ((op &::bool => bool => bool)
   1.708 +          ((All::(bool list => bool) => bool)
   1.709 +            (%v::bool list.
   1.710 +                P ((op #::bool list => bool list list => bool list list) v
   1.711 +                    ([]::bool list list))))
   1.712 +          (P ([]::bool list list))))
   1.713 +      ((All::(bool list list => bool) => bool) P))"
   1.714 +  by (import prob_canon alg_sorted_ind)
   1.715 +
   1.716 +lemma alg_sorted_def: "alg_sorted (x # y # z) = (alg_order x y & alg_sorted (y # z)) &
   1.717 +alg_sorted [v] = True & alg_sorted [] = True"
   1.718 +  by (import prob_canon alg_sorted_def)
   1.719 +
   1.720 +consts
   1.721 +  alg_prefixfree :: "bool list list => bool" 
   1.722 +
   1.723 +defs
   1.724 +  alg_prefixfree_primdef: "alg_prefixfree ==
   1.725 +WFREC (SOME R. WF R & (ALL x z y. R (y # z) (x # y # z)))
   1.726 + (%alg_prefixfree.
   1.727 +     list_case True
   1.728 +      (%v2. list_case True
   1.729 +             (%v6 v7. ~ IS_PREFIX v6 v2 & alg_prefixfree (v6 # v7))))"
   1.730 +
   1.731 +lemma alg_prefixfree_primitive_def: "alg_prefixfree =
   1.732 +WFREC (SOME R. WF R & (ALL x z y. R (y # z) (x # y # z)))
   1.733 + (%alg_prefixfree.
   1.734 +     list_case True
   1.735 +      (%v2. list_case True
   1.736 +             (%v6 v7. ~ IS_PREFIX v6 v2 & alg_prefixfree (v6 # v7))))"
   1.737 +  by (import prob_canon alg_prefixfree_primitive_def)
   1.738 +
   1.739 +lemma alg_prefixfree_ind: "(All::((bool list list => bool) => bool) => bool)
   1.740 + (%P::bool list list => bool.
   1.741 +     (op -->::bool => bool => bool)
   1.742 +      ((op &::bool => bool => bool)
   1.743 +        ((All::(bool list => bool) => bool)
   1.744 +          (%x::bool list.
   1.745 +              (All::(bool list => bool) => bool)
   1.746 +               (%y::bool list.
   1.747 +                   (All::(bool list list => bool) => bool)
   1.748 +                    (%z::bool list list.
   1.749 +                        (op -->::bool => bool => bool)
   1.750 +                         (P ((op #::bool list
   1.751 +                                    => bool list list => bool list list)
   1.752 +                              y z))
   1.753 +                         (P ((op #::bool list
   1.754 +                                    => bool list list => bool list list)
   1.755 +                              x ((op #::bool list
   1.756 +  => bool list list => bool list list)
   1.757 +                                  y z)))))))
   1.758 +        ((op &::bool => bool => bool)
   1.759 +          ((All::(bool list => bool) => bool)
   1.760 +            (%v::bool list.
   1.761 +                P ((op #::bool list => bool list list => bool list list) v
   1.762 +                    ([]::bool list list))))
   1.763 +          (P ([]::bool list list))))
   1.764 +      ((All::(bool list list => bool) => bool) P))"
   1.765 +  by (import prob_canon alg_prefixfree_ind)
   1.766 +
   1.767 +lemma alg_prefixfree_def: "alg_prefixfree (x # y # z) = (~ IS_PREFIX y x & alg_prefixfree (y # z)) &
   1.768 +alg_prefixfree [v] = True & alg_prefixfree [] = True"
   1.769 +  by (import prob_canon alg_prefixfree_def)
   1.770 +
   1.771 +consts
   1.772 +  alg_twinfree :: "bool list list => bool" 
   1.773 +
   1.774 +defs
   1.775 +  alg_twinfree_primdef: "alg_twinfree ==
   1.776 +WFREC (SOME R. WF R & (ALL x z y. R (y # z) (x # y # z)))
   1.777 + (%alg_twinfree.
   1.778 +     list_case True
   1.779 +      (%v2. list_case True
   1.780 +             (%v6 v7. ~ alg_twin v2 v6 & alg_twinfree (v6 # v7))))"
   1.781 +
   1.782 +lemma alg_twinfree_primitive_def: "alg_twinfree =
   1.783 +WFREC (SOME R. WF R & (ALL x z y. R (y # z) (x # y # z)))
   1.784 + (%alg_twinfree.
   1.785 +     list_case True
   1.786 +      (%v2. list_case True
   1.787 +             (%v6 v7. ~ alg_twin v2 v6 & alg_twinfree (v6 # v7))))"
   1.788 +  by (import prob_canon alg_twinfree_primitive_def)
   1.789 +
   1.790 +lemma alg_twinfree_ind: "(All::((bool list list => bool) => bool) => bool)
   1.791 + (%P::bool list list => bool.
   1.792 +     (op -->::bool => bool => bool)
   1.793 +      ((op &::bool => bool => bool)
   1.794 +        ((All::(bool list => bool) => bool)
   1.795 +          (%x::bool list.
   1.796 +              (All::(bool list => bool) => bool)
   1.797 +               (%y::bool list.
   1.798 +                   (All::(bool list list => bool) => bool)
   1.799 +                    (%z::bool list list.
   1.800 +                        (op -->::bool => bool => bool)
   1.801 +                         (P ((op #::bool list
   1.802 +                                    => bool list list => bool list list)
   1.803 +                              y z))
   1.804 +                         (P ((op #::bool list
   1.805 +                                    => bool list list => bool list list)
   1.806 +                              x ((op #::bool list
   1.807 +  => bool list list => bool list list)
   1.808 +                                  y z)))))))
   1.809 +        ((op &::bool => bool => bool)
   1.810 +          ((All::(bool list => bool) => bool)
   1.811 +            (%v::bool list.
   1.812 +                P ((op #::bool list => bool list list => bool list list) v
   1.813 +                    ([]::bool list list))))
   1.814 +          (P ([]::bool list list))))
   1.815 +      ((All::(bool list list => bool) => bool) P))"
   1.816 +  by (import prob_canon alg_twinfree_ind)
   1.817 +
   1.818 +lemma alg_twinfree_def: "alg_twinfree (x # y # z) = (~ alg_twin x y & alg_twinfree (y # z)) &
   1.819 +alg_twinfree [v] = True & alg_twinfree [] = True"
   1.820 +  by (import prob_canon alg_twinfree_def)
   1.821 +
   1.822 +consts
   1.823 +  alg_longest :: "bool list list => nat" 
   1.824 +
   1.825 +defs
   1.826 +  alg_longest_primdef: "alg_longest == FOLDR (%h t. if t <= length h then length h else t) 0"
   1.827 +
   1.828 +lemma alg_longest_def: "alg_longest = FOLDR (%h t. if t <= length h then length h else t) 0"
   1.829 +  by (import prob_canon alg_longest_def)
   1.830 +
   1.831 +consts
   1.832 +  alg_canon_prefs :: "bool list => bool list list => bool list list" 
   1.833 +
   1.834 +specification (alg_canon_prefs_primdef: alg_canon_prefs) alg_canon_prefs_def: "(ALL l. alg_canon_prefs l [] = [l]) &
   1.835 +(ALL l h t.
   1.836 +    alg_canon_prefs l (h # t) =
   1.837 +    (if IS_PREFIX h l then alg_canon_prefs l t else l # h # t))"
   1.838 +  by (import prob_canon alg_canon_prefs_def)
   1.839 +
   1.840 +consts
   1.841 +  alg_canon_find :: "bool list => bool list list => bool list list" 
   1.842 +
   1.843 +specification (alg_canon_find_primdef: alg_canon_find) alg_canon_find_def: "(ALL l. alg_canon_find l [] = [l]) &
   1.844 +(ALL l h t.
   1.845 +    alg_canon_find l (h # t) =
   1.846 +    (if alg_order h l
   1.847 +     then if IS_PREFIX l h then h # t else h # alg_canon_find l t
   1.848 +     else alg_canon_prefs l (h # t)))"
   1.849 +  by (import prob_canon alg_canon_find_def)
   1.850 +
   1.851 +consts
   1.852 +  alg_canon1 :: "bool list list => bool list list" 
   1.853 +
   1.854 +defs
   1.855 +  alg_canon1_primdef: "alg_canon1 == FOLDR alg_canon_find []"
   1.856 +
   1.857 +lemma alg_canon1_def: "alg_canon1 = FOLDR alg_canon_find []"
   1.858 +  by (import prob_canon alg_canon1_def)
   1.859 +
   1.860 +consts
   1.861 +  alg_canon_merge :: "bool list => bool list list => bool list list" 
   1.862 +
   1.863 +specification (alg_canon_merge_primdef: alg_canon_merge) alg_canon_merge_def: "(ALL l. alg_canon_merge l [] = [l]) &
   1.864 +(ALL l h t.
   1.865 +    alg_canon_merge l (h # t) =
   1.866 +    (if alg_twin l h then alg_canon_merge (butlast h) t else l # h # t))"
   1.867 +  by (import prob_canon alg_canon_merge_def)
   1.868 +
   1.869 +consts
   1.870 +  alg_canon2 :: "bool list list => bool list list" 
   1.871 +
   1.872 +defs
   1.873 +  alg_canon2_primdef: "alg_canon2 == FOLDR alg_canon_merge []"
   1.874 +
   1.875 +lemma alg_canon2_def: "alg_canon2 = FOLDR alg_canon_merge []"
   1.876 +  by (import prob_canon alg_canon2_def)
   1.877 +
   1.878 +consts
   1.879 +  alg_canon :: "bool list list => bool list list" 
   1.880 +
   1.881 +defs
   1.882 +  alg_canon_primdef: "alg_canon == %l. alg_canon2 (alg_canon1 l)"
   1.883 +
   1.884 +lemma alg_canon_def: "ALL l. alg_canon l = alg_canon2 (alg_canon1 l)"
   1.885 +  by (import prob_canon alg_canon_def)
   1.886 +
   1.887 +consts
   1.888 +  algebra_canon :: "bool list list => bool" 
   1.889 +
   1.890 +defs
   1.891 +  algebra_canon_primdef: "algebra_canon == %l. alg_canon l = l"
   1.892 +
   1.893 +lemma algebra_canon_def: "ALL l. algebra_canon l = (alg_canon l = l)"
   1.894 +  by (import prob_canon algebra_canon_def)
   1.895 +
   1.896 +lemma ALG_TWIN_NIL: "ALL l. ~ alg_twin l [] & ~ alg_twin [] l"
   1.897 +  by (import prob_canon ALG_TWIN_NIL)
   1.898 +
   1.899 +lemma ALG_TWIN_SING: "ALL x l.
   1.900 +   alg_twin [x] l = (x = True & l = [False]) &
   1.901 +   alg_twin l [x] = (l = [True] & x = False)"
   1.902 +  by (import prob_canon ALG_TWIN_SING)
   1.903 +
   1.904 +lemma ALG_TWIN_CONS: "ALL x y z h t.
   1.905 +   alg_twin (x # y # z) (h # t) = (x = h & alg_twin (y # z) t) &
   1.906 +   alg_twin (h # t) (x # y # z) = (x = h & alg_twin t (y # z))"
   1.907 +  by (import prob_canon ALG_TWIN_CONS)
   1.908 +
   1.909 +lemma ALG_TWIN_REDUCE: "ALL h t t'. alg_twin (h # t) (h # t') = alg_twin t t'"
   1.910 +  by (import prob_canon ALG_TWIN_REDUCE)
   1.911 +
   1.912 +lemma ALG_TWINS_PREFIX: "(All::(bool list => bool) => bool)
   1.913 + (%x::bool list.
   1.914 +     (All::(bool list => bool) => bool)
   1.915 +      (%l::bool list.
   1.916 +          (op -->::bool => bool => bool)
   1.917 +           ((IS_PREFIX::bool list => bool list => bool) x l)
   1.918 +           ((op |::bool => bool => bool)
   1.919 +             ((op =::bool list => bool list => bool) x l)
   1.920 +             ((op |::bool => bool => bool)
   1.921 +               ((IS_PREFIX::bool list => bool list => bool) x
   1.922 +                 ((SNOC::bool => bool list => bool list) (True::bool) l))
   1.923 +               ((IS_PREFIX::bool list => bool list => bool) x
   1.924 +                 ((SNOC::bool => bool list => bool list) (False::bool)
   1.925 +                   l))))))"
   1.926 +  by (import prob_canon ALG_TWINS_PREFIX)
   1.927 +
   1.928 +lemma ALG_ORDER_NIL: "ALL x. alg_order [] x & alg_order x [] = (x = [])"
   1.929 +  by (import prob_canon ALG_ORDER_NIL)
   1.930 +
   1.931 +lemma ALG_ORDER_REFL: "ALL x. alg_order x x"
   1.932 +  by (import prob_canon ALG_ORDER_REFL)
   1.933 +
   1.934 +lemma ALG_ORDER_ANTISYM: "(All::(bool list => bool) => bool)
   1.935 + (%x::bool list.
   1.936 +     (All::(bool list => bool) => bool)
   1.937 +      (%y::bool list.
   1.938 +          (op -->::bool => bool => bool)
   1.939 +           ((op &::bool => bool => bool)
   1.940 +             ((alg_order::bool list => bool list => bool) x y)
   1.941 +             ((alg_order::bool list => bool list => bool) y x))
   1.942 +           ((op =::bool list => bool list => bool) x y)))"
   1.943 +  by (import prob_canon ALG_ORDER_ANTISYM)
   1.944 +
   1.945 +lemma ALG_ORDER_TRANS: "(All::(bool list => bool) => bool)
   1.946 + (%x::bool list.
   1.947 +     (All::(bool list => bool) => bool)
   1.948 +      (%y::bool list.
   1.949 +          (All::(bool list => bool) => bool)
   1.950 +           (%z::bool list.
   1.951 +               (op -->::bool => bool => bool)
   1.952 +                ((op &::bool => bool => bool)
   1.953 +                  ((alg_order::bool list => bool list => bool) x y)
   1.954 +                  ((alg_order::bool list => bool list => bool) y z))
   1.955 +                ((alg_order::bool list => bool list => bool) x z))))"
   1.956 +  by (import prob_canon ALG_ORDER_TRANS)
   1.957 +
   1.958 +lemma ALG_ORDER_TOTAL: "ALL x y. alg_order x y | alg_order y x"
   1.959 +  by (import prob_canon ALG_ORDER_TOTAL)
   1.960 +
   1.961 +lemma ALG_ORDER_PREFIX: "(All::(bool list => bool) => bool)
   1.962 + (%x::bool list.
   1.963 +     (All::(bool list => bool) => bool)
   1.964 +      (%y::bool list.
   1.965 +          (op -->::bool => bool => bool)
   1.966 +           ((IS_PREFIX::bool list => bool list => bool) y x)
   1.967 +           ((alg_order::bool list => bool list => bool) x y)))"
   1.968 +  by (import prob_canon ALG_ORDER_PREFIX)
   1.969 +
   1.970 +lemma ALG_ORDER_PREFIX_ANTI: "(All::(bool list => bool) => bool)
   1.971 + (%x::bool list.
   1.972 +     (All::(bool list => bool) => bool)
   1.973 +      (%y::bool list.
   1.974 +          (op -->::bool => bool => bool)
   1.975 +           ((op &::bool => bool => bool)
   1.976 +             ((alg_order::bool list => bool list => bool) x y)
   1.977 +             ((IS_PREFIX::bool list => bool list => bool) x y))
   1.978 +           ((op =::bool list => bool list => bool) x y)))"
   1.979 +  by (import prob_canon ALG_ORDER_PREFIX_ANTI)
   1.980 +
   1.981 +lemma ALG_ORDER_PREFIX_MONO: "(All::(bool list => bool) => bool)
   1.982 + (%x::bool list.
   1.983 +     (All::(bool list => bool) => bool)
   1.984 +      (%y::bool list.
   1.985 +          (All::(bool list => bool) => bool)
   1.986 +           (%z::bool list.
   1.987 +               (op -->::bool => bool => bool)
   1.988 +                ((op &::bool => bool => bool)
   1.989 +                  ((alg_order::bool list => bool list => bool) x y)
   1.990 +                  ((op &::bool => bool => bool)
   1.991 +                    ((alg_order::bool list => bool list => bool) y z)
   1.992 +                    ((IS_PREFIX::bool list => bool list => bool) z x)))
   1.993 +                ((IS_PREFIX::bool list => bool list => bool) y x))))"
   1.994 +  by (import prob_canon ALG_ORDER_PREFIX_MONO)
   1.995 +
   1.996 +lemma ALG_ORDER_PREFIX_TRANS: "(All::(bool list => bool) => bool)
   1.997 + (%x::bool list.
   1.998 +     (All::(bool list => bool) => bool)
   1.999 +      (%y::bool list.
  1.1000 +          (All::(bool list => bool) => bool)
  1.1001 +           (%z::bool list.
  1.1002 +               (op -->::bool => bool => bool)
  1.1003 +                ((op &::bool => bool => bool)
  1.1004 +                  ((alg_order::bool list => bool list => bool) x y)
  1.1005 +                  ((IS_PREFIX::bool list => bool list => bool) y z))
  1.1006 +                ((op |::bool => bool => bool)
  1.1007 +                  ((alg_order::bool list => bool list => bool) x z)
  1.1008 +                  ((IS_PREFIX::bool list => bool list => bool) x z)))))"
  1.1009 +  by (import prob_canon ALG_ORDER_PREFIX_TRANS)
  1.1010 +
  1.1011 +lemma ALG_ORDER_SNOC: "ALL x l. ~ alg_order (SNOC x l) l"
  1.1012 +  by (import prob_canon ALG_ORDER_SNOC)
  1.1013 +
  1.1014 +lemma ALG_SORTED_MIN: "(All::(bool list => bool) => bool)
  1.1015 + (%h::bool list.
  1.1016 +     (All::(bool list list => bool) => bool)
  1.1017 +      (%t::bool list list.
  1.1018 +          (op -->::bool => bool => bool)
  1.1019 +           ((alg_sorted::bool list list => bool)
  1.1020 +             ((op #::bool list => bool list list => bool list list) h t))
  1.1021 +           ((All::(bool list => bool) => bool)
  1.1022 +             (%x::bool list.
  1.1023 +                 (op -->::bool => bool => bool)
  1.1024 +                  ((op mem::bool list => bool list list => bool) x t)
  1.1025 +                  ((alg_order::bool list => bool list => bool) h x)))))"
  1.1026 +  by (import prob_canon ALG_SORTED_MIN)
  1.1027 +
  1.1028 +lemma ALG_SORTED_DEF_ALT: "(All::(bool list => bool) => bool)
  1.1029 + (%h::bool list.
  1.1030 +     (All::(bool list list => bool) => bool)
  1.1031 +      (%t::bool list list.
  1.1032 +          (op =::bool => bool => bool)
  1.1033 +           ((alg_sorted::bool list list => bool)
  1.1034 +             ((op #::bool list => bool list list => bool list list) h t))
  1.1035 +           ((op &::bool => bool => bool)
  1.1036 +             ((All::(bool list => bool) => bool)
  1.1037 +               (%x::bool list.
  1.1038 +                   (op -->::bool => bool => bool)
  1.1039 +                    ((op mem::bool list => bool list list => bool) x t)
  1.1040 +                    ((alg_order::bool list => bool list => bool) h x)))
  1.1041 +             ((alg_sorted::bool list list => bool) t))))"
  1.1042 +  by (import prob_canon ALG_SORTED_DEF_ALT)
  1.1043 +
  1.1044 +lemma ALG_SORTED_TL: "(All::(bool list => bool) => bool)
  1.1045 + (%h::bool list.
  1.1046 +     (All::(bool list list => bool) => bool)
  1.1047 +      (%t::bool list list.
  1.1048 +          (op -->::bool => bool => bool)
  1.1049 +           ((alg_sorted::bool list list => bool)
  1.1050 +             ((op #::bool list => bool list list => bool list list) h t))
  1.1051 +           ((alg_sorted::bool list list => bool) t)))"
  1.1052 +  by (import prob_canon ALG_SORTED_TL)
  1.1053 +
  1.1054 +lemma ALG_SORTED_MONO: "(All::(bool list => bool) => bool)
  1.1055 + (%x::bool list.
  1.1056 +     (All::(bool list => bool) => bool)
  1.1057 +      (%y::bool list.
  1.1058 +          (All::(bool list list => bool) => bool)
  1.1059 +           (%z::bool list list.
  1.1060 +               (op -->::bool => bool => bool)
  1.1061 +                ((alg_sorted::bool list list => bool)
  1.1062 +                  ((op #::bool list => bool list list => bool list list) x
  1.1063 +                    ((op #::bool list => bool list list => bool list list) y
  1.1064 +                      z)))
  1.1065 +                ((alg_sorted::bool list list => bool)
  1.1066 +                  ((op #::bool list => bool list list => bool list list) x
  1.1067 +                    z)))))"
  1.1068 +  by (import prob_canon ALG_SORTED_MONO)
  1.1069 +
  1.1070 +lemma ALG_SORTED_TLS: "ALL l b. alg_sorted (map (op # b) l) = alg_sorted l"
  1.1071 +  by (import prob_canon ALG_SORTED_TLS)
  1.1072 +
  1.1073 +lemma ALG_SORTED_STEP: "ALL l1 l2.
  1.1074 +   alg_sorted (map (op # True) l1 @ map (op # False) l2) =
  1.1075 +   (alg_sorted l1 & alg_sorted l2)"
  1.1076 +  by (import prob_canon ALG_SORTED_STEP)
  1.1077 +
  1.1078 +lemma ALG_SORTED_APPEND: "ALL h h' t t'.
  1.1079 +   alg_sorted ((h # t) @ h' # t') =
  1.1080 +   (alg_sorted (h # t) & alg_sorted (h' # t') & alg_order (last (h # t)) h')"
  1.1081 +  by (import prob_canon ALG_SORTED_APPEND)
  1.1082 +
  1.1083 +lemma ALG_SORTED_FILTER: "(All::((bool list => bool) => bool) => bool)
  1.1084 + (%P::bool list => bool.
  1.1085 +     (All::(bool list list => bool) => bool)
  1.1086 +      (%b::bool list list.
  1.1087 +          (op -->::bool => bool => bool)
  1.1088 +           ((alg_sorted::bool list list => bool) b)
  1.1089 +           ((alg_sorted::bool list list => bool)
  1.1090 +             ((filter::(bool list => bool)
  1.1091 +                       => bool list list => bool list list)
  1.1092 +               P b))))"
  1.1093 +  by (import prob_canon ALG_SORTED_FILTER)
  1.1094 +
  1.1095 +lemma ALG_PREFIXFREE_TL: "(All::(bool list => bool) => bool)
  1.1096 + (%h::bool list.
  1.1097 +     (All::(bool list list => bool) => bool)
  1.1098 +      (%t::bool list list.
  1.1099 +          (op -->::bool => bool => bool)
  1.1100 +           ((alg_prefixfree::bool list list => bool)
  1.1101 +             ((op #::bool list => bool list list => bool list list) h t))
  1.1102 +           ((alg_prefixfree::bool list list => bool) t)))"
  1.1103 +  by (import prob_canon ALG_PREFIXFREE_TL)
  1.1104 +
  1.1105 +lemma ALG_PREFIXFREE_MONO: "(All::(bool list => bool) => bool)
  1.1106 + (%x::bool list.
  1.1107 +     (All::(bool list => bool) => bool)
  1.1108 +      (%y::bool list.
  1.1109 +          (All::(bool list list => bool) => bool)
  1.1110 +           (%z::bool list list.
  1.1111 +               (op -->::bool => bool => bool)
  1.1112 +                ((op &::bool => bool => bool)
  1.1113 +                  ((alg_sorted::bool list list => bool)
  1.1114 +                    ((op #::bool list => bool list list => bool list list) x
  1.1115 +                      ((op #::bool list => bool list list => bool list list)
  1.1116 +                        y z)))
  1.1117 +                  ((alg_prefixfree::bool list list => bool)
  1.1118 +                    ((op #::bool list => bool list list => bool list list) x
  1.1119 +                      ((op #::bool list => bool list list => bool list list)
  1.1120 +                        y z))))
  1.1121 +                ((alg_prefixfree::bool list list => bool)
  1.1122 +                  ((op #::bool list => bool list list => bool list list) x
  1.1123 +                    z)))))"
  1.1124 +  by (import prob_canon ALG_PREFIXFREE_MONO)
  1.1125 +
  1.1126 +lemma ALG_PREFIXFREE_ELT: "(All::(bool list => bool) => bool)
  1.1127 + (%h::bool list.
  1.1128 +     (All::(bool list list => bool) => bool)
  1.1129 +      (%t::bool list list.
  1.1130 +          (op -->::bool => bool => bool)
  1.1131 +           ((op &::bool => bool => bool)
  1.1132 +             ((alg_sorted::bool list list => bool)
  1.1133 +               ((op #::bool list => bool list list => bool list list) h t))
  1.1134 +             ((alg_prefixfree::bool list list => bool)
  1.1135 +               ((op #::bool list => bool list list => bool list list) h t)))
  1.1136 +           ((All::(bool list => bool) => bool)
  1.1137 +             (%x::bool list.
  1.1138 +                 (op -->::bool => bool => bool)
  1.1139 +                  ((op mem::bool list => bool list list => bool) x t)
  1.1140 +                  ((op &::bool => bool => bool)
  1.1141 +                    ((Not::bool => bool)
  1.1142 +                      ((IS_PREFIX::bool list => bool list => bool) x h))
  1.1143 +                    ((Not::bool => bool)
  1.1144 +                      ((IS_PREFIX::bool list => bool list => bool) h
  1.1145 +                        x)))))))"
  1.1146 +  by (import prob_canon ALG_PREFIXFREE_ELT)
  1.1147 +
  1.1148 +lemma ALG_PREFIXFREE_TLS: "ALL l b. alg_prefixfree (map (op # b) l) = alg_prefixfree l"
  1.1149 +  by (import prob_canon ALG_PREFIXFREE_TLS)
  1.1150 +
  1.1151 +lemma ALG_PREFIXFREE_STEP: "ALL l1 l2.
  1.1152 +   alg_prefixfree (map (op # True) l1 @ map (op # False) l2) =
  1.1153 +   (alg_prefixfree l1 & alg_prefixfree l2)"
  1.1154 +  by (import prob_canon ALG_PREFIXFREE_STEP)
  1.1155 +
  1.1156 +lemma ALG_PREFIXFREE_APPEND: "ALL h h' t t'.
  1.1157 +   alg_prefixfree ((h # t) @ h' # t') =
  1.1158 +   (alg_prefixfree (h # t) &
  1.1159 +    alg_prefixfree (h' # t') & ~ IS_PREFIX h' (last (h # t)))"
  1.1160 +  by (import prob_canon ALG_PREFIXFREE_APPEND)
  1.1161 +
  1.1162 +lemma ALG_PREFIXFREE_FILTER: "(All::((bool list => bool) => bool) => bool)
  1.1163 + (%P::bool list => bool.
  1.1164 +     (All::(bool list list => bool) => bool)
  1.1165 +      (%b::bool list list.
  1.1166 +          (op -->::bool => bool => bool)
  1.1167 +           ((op &::bool => bool => bool)
  1.1168 +             ((alg_sorted::bool list list => bool) b)
  1.1169 +             ((alg_prefixfree::bool list list => bool) b))
  1.1170 +           ((alg_prefixfree::bool list list => bool)
  1.1171 +             ((filter::(bool list => bool)
  1.1172 +                       => bool list list => bool list list)
  1.1173 +               P b))))"
  1.1174 +  by (import prob_canon ALG_PREFIXFREE_FILTER)
  1.1175 +
  1.1176 +lemma ALG_TWINFREE_TL: "(All::(bool list => bool) => bool)
  1.1177 + (%h::bool list.
  1.1178 +     (All::(bool list list => bool) => bool)
  1.1179 +      (%t::bool list list.
  1.1180 +          (op -->::bool => bool => bool)
  1.1181 +           ((alg_twinfree::bool list list => bool)
  1.1182 +             ((op #::bool list => bool list list => bool list list) h t))
  1.1183 +           ((alg_twinfree::bool list list => bool) t)))"
  1.1184 +  by (import prob_canon ALG_TWINFREE_TL)
  1.1185 +
  1.1186 +lemma ALG_TWINFREE_TLS: "ALL l b. alg_twinfree (map (op # b) l) = alg_twinfree l"
  1.1187 +  by (import prob_canon ALG_TWINFREE_TLS)
  1.1188 +
  1.1189 +lemma ALG_TWINFREE_STEP1: "(All::(bool list list => bool) => bool)
  1.1190 + (%l1::bool list list.
  1.1191 +     (All::(bool list list => bool) => bool)
  1.1192 +      (%l2::bool list list.
  1.1193 +          (op -->::bool => bool => bool)
  1.1194 +           ((alg_twinfree::bool list list => bool)
  1.1195 +             ((op @::bool list list => bool list list => bool list list)
  1.1196 +               ((map::(bool list => bool list)
  1.1197 +                      => bool list list => bool list list)
  1.1198 +                 ((op #::bool => bool list => bool list) (True::bool)) l1)
  1.1199 +               ((map::(bool list => bool list)
  1.1200 +                      => bool list list => bool list list)
  1.1201 +                 ((op #::bool => bool list => bool list) (False::bool))
  1.1202 +                 l2)))
  1.1203 +           ((op &::bool => bool => bool)
  1.1204 +             ((alg_twinfree::bool list list => bool) l1)
  1.1205 +             ((alg_twinfree::bool list list => bool) l2))))"
  1.1206 +  by (import prob_canon ALG_TWINFREE_STEP1)
  1.1207 +
  1.1208 +lemma ALG_TWINFREE_STEP2: "(All::(bool list list => bool) => bool)
  1.1209 + (%l1::bool list list.
  1.1210 +     (All::(bool list list => bool) => bool)
  1.1211 +      (%l2::bool list list.
  1.1212 +          (op -->::bool => bool => bool)
  1.1213 +           ((op &::bool => bool => bool)
  1.1214 +             ((op |::bool => bool => bool)
  1.1215 +               ((Not::bool => bool)
  1.1216 +                 ((op mem::bool list => bool list list => bool)
  1.1217 +                   ([]::bool list) l1))
  1.1218 +               ((Not::bool => bool)
  1.1219 +                 ((op mem::bool list => bool list list => bool)
  1.1220 +                   ([]::bool list) l2)))
  1.1221 +             ((op &::bool => bool => bool)
  1.1222 +               ((alg_twinfree::bool list list => bool) l1)
  1.1223 +               ((alg_twinfree::bool list list => bool) l2)))
  1.1224 +           ((alg_twinfree::bool list list => bool)
  1.1225 +             ((op @::bool list list => bool list list => bool list list)
  1.1226 +               ((map::(bool list => bool list)
  1.1227 +                      => bool list list => bool list list)
  1.1228 +                 ((op #::bool => bool list => bool list) (True::bool)) l1)
  1.1229 +               ((map::(bool list => bool list)
  1.1230 +                      => bool list list => bool list list)
  1.1231 +                 ((op #::bool => bool list => bool list) (False::bool))
  1.1232 +                 l2)))))"
  1.1233 +  by (import prob_canon ALG_TWINFREE_STEP2)
  1.1234 +
  1.1235 +lemma ALG_TWINFREE_STEP: "(All::(bool list list => bool) => bool)
  1.1236 + (%l1::bool list list.
  1.1237 +     (All::(bool list list => bool) => bool)
  1.1238 +      (%l2::bool list list.
  1.1239 +          (op -->::bool => bool => bool)
  1.1240 +           ((op |::bool => bool => bool)
  1.1241 +             ((Not::bool => bool)
  1.1242 +               ((op mem::bool list => bool list list => bool)
  1.1243 +                 ([]::bool list) l1))
  1.1244 +             ((Not::bool => bool)
  1.1245 +               ((op mem::bool list => bool list list => bool)
  1.1246 +                 ([]::bool list) l2)))
  1.1247 +           ((op =::bool => bool => bool)
  1.1248 +             ((alg_twinfree::bool list list => bool)
  1.1249 +               ((op @::bool list list => bool list list => bool list list)
  1.1250 +                 ((map::(bool list => bool list)
  1.1251 +                        => bool list list => bool list list)
  1.1252 +                   ((op #::bool => bool list => bool list) (True::bool)) l1)
  1.1253 +                 ((map::(bool list => bool list)
  1.1254 +                        => bool list list => bool list list)
  1.1255 +                   ((op #::bool => bool list => bool list) (False::bool))
  1.1256 +                   l2)))
  1.1257 +             ((op &::bool => bool => bool)
  1.1258 +               ((alg_twinfree::bool list list => bool) l1)
  1.1259 +               ((alg_twinfree::bool list list => bool) l2)))))"
  1.1260 +  by (import prob_canon ALG_TWINFREE_STEP)
  1.1261 +
  1.1262 +lemma ALG_LONGEST_HD: "ALL h t. length h <= alg_longest (h # t)"
  1.1263 +  by (import prob_canon ALG_LONGEST_HD)
  1.1264 +
  1.1265 +lemma ALG_LONGEST_TL: "ALL h t. alg_longest t <= alg_longest (h # t)"
  1.1266 +  by (import prob_canon ALG_LONGEST_TL)
  1.1267 +
  1.1268 +lemma ALG_LONGEST_TLS: "ALL h t b. alg_longest (map (op # b) (h # t)) = Suc (alg_longest (h # t))"
  1.1269 +  by (import prob_canon ALG_LONGEST_TLS)
  1.1270 +
  1.1271 +lemma ALG_LONGEST_APPEND: "ALL l1 l2.
  1.1272 +   alg_longest l1 <= alg_longest (l1 @ l2) &
  1.1273 +   alg_longest l2 <= alg_longest (l1 @ l2)"
  1.1274 +  by (import prob_canon ALG_LONGEST_APPEND)
  1.1275 +
  1.1276 +lemma ALG_CANON_PREFS_HD: "ALL l b. hd (alg_canon_prefs l b) = l"
  1.1277 +  by (import prob_canon ALG_CANON_PREFS_HD)
  1.1278 +
  1.1279 +lemma ALG_CANON_PREFS_DELETES: "(All::(bool list => bool) => bool)
  1.1280 + (%l::bool list.
  1.1281 +     (All::(bool list list => bool) => bool)
  1.1282 +      (%b::bool list list.
  1.1283 +          (All::(bool list => bool) => bool)
  1.1284 +           (%x::bool list.
  1.1285 +               (op -->::bool => bool => bool)
  1.1286 +                ((op mem::bool list => bool list list => bool) x
  1.1287 +                  ((alg_canon_prefs::bool list
  1.1288 +                                     => bool list list => bool list list)
  1.1289 +                    l b))
  1.1290 +                ((op mem::bool list => bool list list => bool) x
  1.1291 +                  ((op #::bool list => bool list list => bool list list) l
  1.1292 +                    b)))))"
  1.1293 +  by (import prob_canon ALG_CANON_PREFS_DELETES)
  1.1294 +
  1.1295 +lemma ALG_CANON_PREFS_SORTED: "(All::(bool list => bool) => bool)
  1.1296 + (%l::bool list.
  1.1297 +     (All::(bool list list => bool) => bool)
  1.1298 +      (%b::bool list list.
  1.1299 +          (op -->::bool => bool => bool)
  1.1300 +           ((alg_sorted::bool list list => bool)
  1.1301 +             ((op #::bool list => bool list list => bool list list) l b))
  1.1302 +           ((alg_sorted::bool list list => bool)
  1.1303 +             ((alg_canon_prefs::bool list
  1.1304 +                                => bool list list => bool list list)
  1.1305 +               l b))))"
  1.1306 +  by (import prob_canon ALG_CANON_PREFS_SORTED)
  1.1307 +
  1.1308 +lemma ALG_CANON_PREFS_PREFIXFREE: "(All::(bool list => bool) => bool)
  1.1309 + (%l::bool list.
  1.1310 +     (All::(bool list list => bool) => bool)
  1.1311 +      (%b::bool list list.
  1.1312 +          (op -->::bool => bool => bool)
  1.1313 +           ((op &::bool => bool => bool)
  1.1314 +             ((alg_sorted::bool list list => bool) b)
  1.1315 +             ((alg_prefixfree::bool list list => bool) b))
  1.1316 +           ((alg_prefixfree::bool list list => bool)
  1.1317 +             ((alg_canon_prefs::bool list
  1.1318 +                                => bool list list => bool list list)
  1.1319 +               l b))))"
  1.1320 +  by (import prob_canon ALG_CANON_PREFS_PREFIXFREE)
  1.1321 +
  1.1322 +lemma ALG_CANON_PREFS_CONSTANT: "(All::(bool list => bool) => bool)
  1.1323 + (%l::bool list.
  1.1324 +     (All::(bool list list => bool) => bool)
  1.1325 +      (%b::bool list list.
  1.1326 +          (op -->::bool => bool => bool)
  1.1327 +           ((alg_prefixfree::bool list list => bool)
  1.1328 +             ((op #::bool list => bool list list => bool list list) l b))
  1.1329 +           ((op =::bool list list => bool list list => bool)
  1.1330 +             ((alg_canon_prefs::bool list
  1.1331 +                                => bool list list => bool list list)
  1.1332 +               l b)
  1.1333 +             ((op #::bool list => bool list list => bool list list) l b))))"
  1.1334 +  by (import prob_canon ALG_CANON_PREFS_CONSTANT)
  1.1335 +
  1.1336 +lemma ALG_CANON_FIND_HD: "ALL l h t.
  1.1337 +   hd (alg_canon_find l (h # t)) = l | hd (alg_canon_find l (h # t)) = h"
  1.1338 +  by (import prob_canon ALG_CANON_FIND_HD)
  1.1339 +
  1.1340 +lemma ALG_CANON_FIND_DELETES: "(All::(bool list => bool) => bool)
  1.1341 + (%l::bool list.
  1.1342 +     (All::(bool list list => bool) => bool)
  1.1343 +      (%b::bool list list.
  1.1344 +          (All::(bool list => bool) => bool)
  1.1345 +           (%x::bool list.
  1.1346 +               (op -->::bool => bool => bool)
  1.1347 +                ((op mem::bool list => bool list list => bool) x
  1.1348 +                  ((alg_canon_find::bool list
  1.1349 +                                    => bool list list => bool list list)
  1.1350 +                    l b))
  1.1351 +                ((op mem::bool list => bool list list => bool) x
  1.1352 +                  ((op #::bool list => bool list list => bool list list) l
  1.1353 +                    b)))))"
  1.1354 +  by (import prob_canon ALG_CANON_FIND_DELETES)
  1.1355 +
  1.1356 +lemma ALG_CANON_FIND_SORTED: "(All::(bool list => bool) => bool)
  1.1357 + (%l::bool list.
  1.1358 +     (All::(bool list list => bool) => bool)
  1.1359 +      (%b::bool list list.
  1.1360 +          (op -->::bool => bool => bool)
  1.1361 +           ((alg_sorted::bool list list => bool) b)
  1.1362 +           ((alg_sorted::bool list list => bool)
  1.1363 +             ((alg_canon_find::bool list
  1.1364 +                               => bool list list => bool list list)
  1.1365 +               l b))))"
  1.1366 +  by (import prob_canon ALG_CANON_FIND_SORTED)
  1.1367 +
  1.1368 +lemma ALG_CANON_FIND_PREFIXFREE: "(All::(bool list => bool) => bool)
  1.1369 + (%l::bool list.
  1.1370 +     (All::(bool list list => bool) => bool)
  1.1371 +      (%b::bool list list.
  1.1372 +          (op -->::bool => bool => bool)
  1.1373 +           ((op &::bool => bool => bool)
  1.1374 +             ((alg_sorted::bool list list => bool) b)
  1.1375 +             ((alg_prefixfree::bool list list => bool) b))
  1.1376 +           ((alg_prefixfree::bool list list => bool)
  1.1377 +             ((alg_canon_find::bool list
  1.1378 +                               => bool list list => bool list list)
  1.1379 +               l b))))"
  1.1380 +  by (import prob_canon ALG_CANON_FIND_PREFIXFREE)
  1.1381 +
  1.1382 +lemma ALG_CANON_FIND_CONSTANT: "(All::(bool list => bool) => bool)
  1.1383 + (%l::bool list.
  1.1384 +     (All::(bool list list => bool) => bool)
  1.1385 +      (%b::bool list list.
  1.1386 +          (op -->::bool => bool => bool)
  1.1387 +           ((op &::bool => bool => bool)
  1.1388 +             ((alg_sorted::bool list list => bool)
  1.1389 +               ((op #::bool list => bool list list => bool list list) l b))
  1.1390 +             ((alg_prefixfree::bool list list => bool)
  1.1391 +               ((op #::bool list => bool list list => bool list list) l b)))
  1.1392 +           ((op =::bool list list => bool list list => bool)
  1.1393 +             ((alg_canon_find::bool list
  1.1394 +                               => bool list list => bool list list)
  1.1395 +               l b)
  1.1396 +             ((op #::bool list => bool list list => bool list list) l b))))"
  1.1397 +  by (import prob_canon ALG_CANON_FIND_CONSTANT)
  1.1398 +
  1.1399 +lemma ALG_CANON1_SORTED: "ALL x. alg_sorted (alg_canon1 x)"
  1.1400 +  by (import prob_canon ALG_CANON1_SORTED)
  1.1401 +
  1.1402 +lemma ALG_CANON1_PREFIXFREE: "ALL l. alg_prefixfree (alg_canon1 l)"
  1.1403 +  by (import prob_canon ALG_CANON1_PREFIXFREE)
  1.1404 +
  1.1405 +lemma ALG_CANON1_CONSTANT: "(All::(bool list list => bool) => bool)
  1.1406 + (%l::bool list list.
  1.1407 +     (op -->::bool => bool => bool)
  1.1408 +      ((op &::bool => bool => bool) ((alg_sorted::bool list list => bool) l)
  1.1409 +        ((alg_prefixfree::bool list list => bool) l))
  1.1410 +      ((op =::bool list list => bool list list => bool)
  1.1411 +        ((alg_canon1::bool list list => bool list list) l) l))"
  1.1412 +  by (import prob_canon ALG_CANON1_CONSTANT)
  1.1413 +
  1.1414 +lemma ALG_CANON_MERGE_SORTED_PREFIXFREE_TWINFREE: "(All::(bool list => bool) => bool)
  1.1415 + (%l::bool list.
  1.1416 +     (All::(bool list list => bool) => bool)
  1.1417 +      (%b::bool list list.
  1.1418 +          (op -->::bool => bool => bool)
  1.1419 +           ((op &::bool => bool => bool)
  1.1420 +             ((alg_sorted::bool list list => bool)
  1.1421 +               ((op #::bool list => bool list list => bool list list) l b))
  1.1422 +             ((op &::bool => bool => bool)
  1.1423 +               ((alg_prefixfree::bool list list => bool)
  1.1424 +                 ((op #::bool list => bool list list => bool list list) l
  1.1425 +                   b))
  1.1426 +               ((alg_twinfree::bool list list => bool) b)))
  1.1427 +           ((op &::bool => bool => bool)
  1.1428 +             ((alg_sorted::bool list list => bool)
  1.1429 +               ((alg_canon_merge::bool list
  1.1430 +                                  => bool list list => bool list list)
  1.1431 +                 l b))
  1.1432 +             ((op &::bool => bool => bool)
  1.1433 +               ((alg_prefixfree::bool list list => bool)
  1.1434 +                 ((alg_canon_merge::bool list
  1.1435 +                                    => bool list list => bool list list)
  1.1436 +                   l b))
  1.1437 +               ((alg_twinfree::bool list list => bool)
  1.1438 +                 ((alg_canon_merge::bool list
  1.1439 +                                    => bool list list => bool list list)
  1.1440 +                   l b))))))"
  1.1441 +  by (import prob_canon ALG_CANON_MERGE_SORTED_PREFIXFREE_TWINFREE)
  1.1442 +
  1.1443 +lemma ALG_CANON_MERGE_PREFIXFREE_PRESERVE: "(All::(bool list => bool) => bool)
  1.1444 + (%l::bool list.
  1.1445 +     (All::(bool list list => bool) => bool)
  1.1446 +      (%b::bool list list.
  1.1447 +          (All::(bool list => bool) => bool)
  1.1448 +           (%h::bool list.
  1.1449 +               (op -->::bool => bool => bool)
  1.1450 +                ((All::(bool list => bool) => bool)
  1.1451 +                  (%x::bool list.
  1.1452 +                      (op -->::bool => bool => bool)
  1.1453 +                       ((op mem::bool list => bool list list => bool) x
  1.1454 +                         ((op #::bool list
  1.1455 +                                 => bool list list => bool list list)
  1.1456 +                           l b))
  1.1457 +                       ((op &::bool => bool => bool)
  1.1458 +                         ((Not::bool => bool)
  1.1459 +                           ((IS_PREFIX::bool list => bool list => bool) h
  1.1460 +                             x))
  1.1461 +                         ((Not::bool => bool)
  1.1462 +                           ((IS_PREFIX::bool list => bool list => bool) x
  1.1463 +                             h)))))
  1.1464 +                ((All::(bool list => bool) => bool)
  1.1465 +                  (%x::bool list.
  1.1466 +                      (op -->::bool => bool => bool)
  1.1467 +                       ((op mem::bool list => bool list list => bool) x
  1.1468 +                         ((alg_canon_merge::bool list
  1.1469 +      => bool list list => bool list list)
  1.1470 +                           l b))
  1.1471 +                       ((op &::bool => bool => bool)
  1.1472 +                         ((Not::bool => bool)
  1.1473 +                           ((IS_PREFIX::bool list => bool list => bool) h
  1.1474 +                             x))
  1.1475 +                         ((Not::bool => bool)
  1.1476 +                           ((IS_PREFIX::bool list => bool list => bool) x
  1.1477 +                             h))))))))"
  1.1478 +  by (import prob_canon ALG_CANON_MERGE_PREFIXFREE_PRESERVE)
  1.1479 +
  1.1480 +lemma ALG_CANON_MERGE_SHORTENS: "(All::(bool list => bool) => bool)
  1.1481 + (%l::bool list.
  1.1482 +     (All::(bool list list => bool) => bool)
  1.1483 +      (%b::bool list list.
  1.1484 +          (All::(bool list => bool) => bool)
  1.1485 +           (%x::bool list.
  1.1486 +               (op -->::bool => bool => bool)
  1.1487 +                ((op mem::bool list => bool list list => bool) x
  1.1488 +                  ((alg_canon_merge::bool list
  1.1489 +                                     => bool list list => bool list list)
  1.1490 +                    l b))
  1.1491 +                ((Ex::(bool list => bool) => bool)
  1.1492 +                  (%y::bool list.
  1.1493 +                      (op &::bool => bool => bool)
  1.1494 +                       ((op mem::bool list => bool list list => bool) y
  1.1495 +                         ((op #::bool list
  1.1496 +                                 => bool list list => bool list list)
  1.1497 +                           l b))
  1.1498 +                       ((IS_PREFIX::bool list => bool list => bool) y
  1.1499 +                         x))))))"
  1.1500 +  by (import prob_canon ALG_CANON_MERGE_SHORTENS)
  1.1501 +
  1.1502 +lemma ALG_CANON_MERGE_CONSTANT: "(All::(bool list => bool) => bool)
  1.1503 + (%l::bool list.
  1.1504 +     (All::(bool list list => bool) => bool)
  1.1505 +      (%b::bool list list.
  1.1506 +          (op -->::bool => bool => bool)
  1.1507 +           ((alg_twinfree::bool list list => bool)
  1.1508 +             ((op #::bool list => bool list list => bool list list) l b))
  1.1509 +           ((op =::bool list list => bool list list => bool)
  1.1510 +             ((alg_canon_merge::bool list
  1.1511 +                                => bool list list => bool list list)
  1.1512 +               l b)
  1.1513 +             ((op #::bool list => bool list list => bool list list) l b))))"
  1.1514 +  by (import prob_canon ALG_CANON_MERGE_CONSTANT)
  1.1515 +
  1.1516 +lemma ALG_CANON2_PREFIXFREE_PRESERVE: "(All::(bool list list => bool) => bool)
  1.1517 + (%x::bool list list.
  1.1518 +     (All::(bool list => bool) => bool)
  1.1519 +      (%xa::bool list.
  1.1520 +          (op -->::bool => bool => bool)
  1.1521 +           ((All::(bool list => bool) => bool)
  1.1522 +             (%xb::bool list.
  1.1523 +                 (op -->::bool => bool => bool)
  1.1524 +                  ((op mem::bool list => bool list list => bool) xb x)
  1.1525 +                  ((op &::bool => bool => bool)
  1.1526 +                    ((Not::bool => bool)
  1.1527 +                      ((IS_PREFIX::bool list => bool list => bool) xa xb))
  1.1528 +                    ((Not::bool => bool)
  1.1529 +                      ((IS_PREFIX::bool list => bool list => bool) xb
  1.1530 +                        xa)))))
  1.1531 +           ((All::(bool list => bool) => bool)
  1.1532 +             (%xb::bool list.
  1.1533 +                 (op -->::bool => bool => bool)
  1.1534 +                  ((op mem::bool list => bool list list => bool) xb
  1.1535 +                    ((alg_canon2::bool list list => bool list list) x))
  1.1536 +                  ((op &::bool => bool => bool)
  1.1537 +                    ((Not::bool => bool)
  1.1538 +                      ((IS_PREFIX::bool list => bool list => bool) xa xb))
  1.1539 +                    ((Not::bool => bool)
  1.1540 +                      ((IS_PREFIX::bool list => bool list => bool) xb
  1.1541 +                        xa)))))))"
  1.1542 +  by (import prob_canon ALG_CANON2_PREFIXFREE_PRESERVE)
  1.1543 +
  1.1544 +lemma ALG_CANON2_SHORTENS: "(All::(bool list list => bool) => bool)
  1.1545 + (%x::bool list list.
  1.1546 +     (All::(bool list => bool) => bool)
  1.1547 +      (%xa::bool list.
  1.1548 +          (op -->::bool => bool => bool)
  1.1549 +           ((op mem::bool list => bool list list => bool) xa
  1.1550 +             ((alg_canon2::bool list list => bool list list) x))
  1.1551 +           ((Ex::(bool list => bool) => bool)
  1.1552 +             (%y::bool list.
  1.1553 +                 (op &::bool => bool => bool)
  1.1554 +                  ((op mem::bool list => bool list list => bool) y x)
  1.1555 +                  ((IS_PREFIX::bool list => bool list => bool) y xa)))))"
  1.1556 +  by (import prob_canon ALG_CANON2_SHORTENS)
  1.1557 +
  1.1558 +lemma ALG_CANON2_SORTED_PREFIXFREE_TWINFREE: "(All::(bool list list => bool) => bool)
  1.1559 + (%x::bool list list.
  1.1560 +     (op -->::bool => bool => bool)
  1.1561 +      ((op &::bool => bool => bool) ((alg_sorted::bool list list => bool) x)
  1.1562 +        ((alg_prefixfree::bool list list => bool) x))
  1.1563 +      ((op &::bool => bool => bool)
  1.1564 +        ((alg_sorted::bool list list => bool)
  1.1565 +          ((alg_canon2::bool list list => bool list list) x))
  1.1566 +        ((op &::bool => bool => bool)
  1.1567 +          ((alg_prefixfree::bool list list => bool)
  1.1568 +            ((alg_canon2::bool list list => bool list list) x))
  1.1569 +          ((alg_twinfree::bool list list => bool)
  1.1570 +            ((alg_canon2::bool list list => bool list list) x)))))"
  1.1571 +  by (import prob_canon ALG_CANON2_SORTED_PREFIXFREE_TWINFREE)
  1.1572 +
  1.1573 +lemma ALG_CANON2_CONSTANT: "(All::(bool list list => bool) => bool)
  1.1574 + (%l::bool list list.
  1.1575 +     (op -->::bool => bool => bool)
  1.1576 +      ((alg_twinfree::bool list list => bool) l)
  1.1577 +      ((op =::bool list list => bool list list => bool)
  1.1578 +        ((alg_canon2::bool list list => bool list list) l) l))"
  1.1579 +  by (import prob_canon ALG_CANON2_CONSTANT)
  1.1580 +
  1.1581 +lemma ALG_CANON_SORTED_PREFIXFREE_TWINFREE: "ALL l.
  1.1582 +   alg_sorted (alg_canon l) &
  1.1583 +   alg_prefixfree (alg_canon l) & alg_twinfree (alg_canon l)"
  1.1584 +  by (import prob_canon ALG_CANON_SORTED_PREFIXFREE_TWINFREE)
  1.1585 +
  1.1586 +lemma ALG_CANON_CONSTANT: "(All::(bool list list => bool) => bool)
  1.1587 + (%l::bool list list.
  1.1588 +     (op -->::bool => bool => bool)
  1.1589 +      ((op &::bool => bool => bool) ((alg_sorted::bool list list => bool) l)
  1.1590 +        ((op &::bool => bool => bool)
  1.1591 +          ((alg_prefixfree::bool list list => bool) l)
  1.1592 +          ((alg_twinfree::bool list list => bool) l)))
  1.1593 +      ((op =::bool list list => bool list list => bool)
  1.1594 +        ((alg_canon::bool list list => bool list list) l) l))"
  1.1595 +  by (import prob_canon ALG_CANON_CONSTANT)
  1.1596 +
  1.1597 +lemma ALG_CANON_IDEMPOT: "ALL l. alg_canon (alg_canon l) = alg_canon l"
  1.1598 +  by (import prob_canon ALG_CANON_IDEMPOT)
  1.1599 +
  1.1600 +lemma ALGEBRA_CANON_DEF_ALT: "ALL l. algebra_canon l = (alg_sorted l & alg_prefixfree l & alg_twinfree l)"
  1.1601 +  by (import prob_canon ALGEBRA_CANON_DEF_ALT)
  1.1602 +
  1.1603 +lemma ALGEBRA_CANON_BASIC: "algebra_canon [] & algebra_canon [[]] & (ALL x. algebra_canon [x])"
  1.1604 +  by (import prob_canon ALGEBRA_CANON_BASIC)
  1.1605 +
  1.1606 +lemma ALG_CANON_BASIC: "alg_canon [] = [] & alg_canon [[]] = [[]] & (ALL x. alg_canon [x] = [x])"
  1.1607 +  by (import prob_canon ALG_CANON_BASIC)
  1.1608 +
  1.1609 +lemma ALGEBRA_CANON_TL: "(All::(bool list => bool) => bool)
  1.1610 + (%h::bool list.
  1.1611 +     (All::(bool list list => bool) => bool)
  1.1612 +      (%t::bool list list.
  1.1613 +          (op -->::bool => bool => bool)
  1.1614 +           ((algebra_canon::bool list list => bool)
  1.1615 +             ((op #::bool list => bool list list => bool list list) h t))
  1.1616 +           ((algebra_canon::bool list list => bool) t)))"
  1.1617 +  by (import prob_canon ALGEBRA_CANON_TL)
  1.1618 +
  1.1619 +lemma ALGEBRA_CANON_NIL_MEM: "ALL l. (algebra_canon l & [] mem l) = (l = [[]])"
  1.1620 +  by (import prob_canon ALGEBRA_CANON_NIL_MEM)
  1.1621 +
  1.1622 +lemma ALGEBRA_CANON_TLS: "ALL l b. algebra_canon (map (op # b) l) = algebra_canon l"
  1.1623 +  by (import prob_canon ALGEBRA_CANON_TLS)
  1.1624 +
  1.1625 +lemma ALGEBRA_CANON_STEP1: "(All::(bool list list => bool) => bool)
  1.1626 + (%l1::bool list list.
  1.1627 +     (All::(bool list list => bool) => bool)
  1.1628 +      (%l2::bool list list.
  1.1629 +          (op -->::bool => bool => bool)
  1.1630 +           ((algebra_canon::bool list list => bool)
  1.1631 +             ((op @::bool list list => bool list list => bool list list)
  1.1632 +               ((map::(bool list => bool list)
  1.1633 +                      => bool list list => bool list list)
  1.1634 +                 ((op #::bool => bool list => bool list) (True::bool)) l1)
  1.1635 +               ((map::(bool list => bool list)
  1.1636 +                      => bool list list => bool list list)
  1.1637 +                 ((op #::bool => bool list => bool list) (False::bool))
  1.1638 +                 l2)))
  1.1639 +           ((op &::bool => bool => bool)
  1.1640 +             ((algebra_canon::bool list list => bool) l1)
  1.1641 +             ((algebra_canon::bool list list => bool) l2))))"
  1.1642 +  by (import prob_canon ALGEBRA_CANON_STEP1)
  1.1643 +
  1.1644 +lemma ALGEBRA_CANON_STEP2: "(All::(bool list list => bool) => bool)
  1.1645 + (%l1::bool list list.
  1.1646 +     (All::(bool list list => bool) => bool)
  1.1647 +      (%l2::bool list list.
  1.1648 +          (op -->::bool => bool => bool)
  1.1649 +           ((op &::bool => bool => bool)
  1.1650 +             ((op |::bool => bool => bool)
  1.1651 +               ((Not::bool => bool)
  1.1652 +                 ((op =::bool list list => bool list list => bool) l1
  1.1653 +                   ((op #::bool list => bool list list => bool list list)
  1.1654 +                     ([]::bool list) ([]::bool list list))))
  1.1655 +               ((Not::bool => bool)
  1.1656 +                 ((op =::bool list list => bool list list => bool) l2
  1.1657 +                   ((op #::bool list => bool list list => bool list list)
  1.1658 +                     ([]::bool list) ([]::bool list list)))))
  1.1659 +             ((op &::bool => bool => bool)
  1.1660 +               ((algebra_canon::bool list list => bool) l1)
  1.1661 +               ((algebra_canon::bool list list => bool) l2)))
  1.1662 +           ((algebra_canon::bool list list => bool)
  1.1663 +             ((op @::bool list list => bool list list => bool list list)
  1.1664 +               ((map::(bool list => bool list)
  1.1665 +                      => bool list list => bool list list)
  1.1666 +                 ((op #::bool => bool list => bool list) (True::bool)) l1)
  1.1667 +               ((map::(bool list => bool list)
  1.1668 +                      => bool list list => bool list list)
  1.1669 +                 ((op #::bool => bool list => bool list) (False::bool))
  1.1670 +                 l2)))))"
  1.1671 +  by (import prob_canon ALGEBRA_CANON_STEP2)
  1.1672 +
  1.1673 +lemma ALGEBRA_CANON_STEP: "(All::(bool list list => bool) => bool)
  1.1674 + (%l1::bool list list.
  1.1675 +     (All::(bool list list => bool) => bool)
  1.1676 +      (%l2::bool list list.
  1.1677 +          (op -->::bool => bool => bool)
  1.1678 +           ((op |::bool => bool => bool)
  1.1679 +             ((Not::bool => bool)
  1.1680 +               ((op =::bool list list => bool list list => bool) l1
  1.1681 +                 ((op #::bool list => bool list list => bool list list)
  1.1682 +                   ([]::bool list) ([]::bool list list))))
  1.1683 +             ((Not::bool => bool)
  1.1684 +               ((op =::bool list list => bool list list => bool) l2
  1.1685 +                 ((op #::bool list => bool list list => bool list list)
  1.1686 +                   ([]::bool list) ([]::bool list list)))))
  1.1687 +           ((op =::bool => bool => bool)
  1.1688 +             ((algebra_canon::bool list list => bool)
  1.1689 +               ((op @::bool list list => bool list list => bool list list)
  1.1690 +                 ((map::(bool list => bool list)
  1.1691 +                        => bool list list => bool list list)
  1.1692 +                   ((op #::bool => bool list => bool list) (True::bool)) l1)
  1.1693 +                 ((map::(bool list => bool list)
  1.1694 +                        => bool list list => bool list list)
  1.1695 +                   ((op #::bool => bool list => bool list) (False::bool))
  1.1696 +                   l2)))
  1.1697 +             ((op &::bool => bool => bool)
  1.1698 +               ((algebra_canon::bool list list => bool) l1)
  1.1699 +               ((algebra_canon::bool list list => bool) l2)))))"
  1.1700 +  by (import prob_canon ALGEBRA_CANON_STEP)
  1.1701 +
  1.1702 +lemma ALGEBRA_CANON_CASES_THM: "(All::(bool list list => bool) => bool)
  1.1703 + (%l::bool list list.
  1.1704 +     (op -->::bool => bool => bool)
  1.1705 +      ((algebra_canon::bool list list => bool) l)
  1.1706 +      ((op |::bool => bool => bool)
  1.1707 +        ((op =::bool list list => bool list list => bool) l
  1.1708 +          ([]::bool list list))
  1.1709 +        ((op |::bool => bool => bool)
  1.1710 +          ((op =::bool list list => bool list list => bool) l
  1.1711 +            ((op #::bool list => bool list list => bool list list)
  1.1712 +              ([]::bool list) ([]::bool list list)))
  1.1713 +          ((Ex::(bool list list => bool) => bool)
  1.1714 +            (%l1::bool list list.
  1.1715 +                (Ex::(bool list list => bool) => bool)
  1.1716 +                 (%l2::bool list list.
  1.1717 +                     (op &::bool => bool => bool)
  1.1718 +                      ((algebra_canon::bool list list => bool) l1)
  1.1719 +                      ((op &::bool => bool => bool)
  1.1720 +                        ((algebra_canon::bool list list => bool) l2)
  1.1721 +                        ((op =::bool list list => bool list list => bool) l
  1.1722 +                          ((op @::bool list list
  1.1723 +                                  => bool list list => bool list list)
  1.1724 +                            ((map::(bool list => bool list)
  1.1725 +                                   => bool list list => bool list list)
  1.1726 +                              ((op #::bool => bool list => bool list)
  1.1727 +                                (True::bool))
  1.1728 +                              l1)
  1.1729 +                            ((map::(bool list => bool list)
  1.1730 +                                   => bool list list => bool list list)
  1.1731 +                              ((op #::bool => bool list => bool list)
  1.1732 +                                (False::bool))
  1.1733 +                              l2))))))))))"
  1.1734 +  by (import prob_canon ALGEBRA_CANON_CASES_THM)
  1.1735 +
  1.1736 +lemma ALGEBRA_CANON_CASES: "(All::((bool list list => bool) => bool) => bool)
  1.1737 + (%P::bool list list => bool.
  1.1738 +     (op -->::bool => bool => bool)
  1.1739 +      ((op &::bool => bool => bool) (P ([]::bool list list))
  1.1740 +        ((op &::bool => bool => bool)
  1.1741 +          (P ((op #::bool list => bool list list => bool list list)
  1.1742 +               ([]::bool list) ([]::bool list list)))
  1.1743 +          ((All::(bool list list => bool) => bool)
  1.1744 +            (%l1::bool list list.
  1.1745 +                (All::(bool list list => bool) => bool)
  1.1746 +                 (%l2::bool list list.
  1.1747 +                     (op -->::bool => bool => bool)
  1.1748 +                      ((op &::bool => bool => bool)
  1.1749 +                        ((algebra_canon::bool list list => bool) l1)
  1.1750 +                        ((op &::bool => bool => bool)
  1.1751 +                          ((algebra_canon::bool list list => bool) l2)
  1.1752 +                          ((algebra_canon::bool list list => bool)
  1.1753 +                            ((op @::bool list list
  1.1754 +                                    => bool list list => bool list list)
  1.1755 +                              ((map::(bool list => bool list)
  1.1756 +                                     => bool list list => bool list list)
  1.1757 +                                ((op #::bool => bool list => bool list)
  1.1758 +                                  (True::bool))
  1.1759 +                                l1)
  1.1760 +                              ((map::(bool list => bool list)
  1.1761 +                                     => bool list list => bool list list)
  1.1762 +                                ((op #::bool => bool list => bool list)
  1.1763 +                                  (False::bool))
  1.1764 +                                l2)))))
  1.1765 +                      (P ((op @::bool list list
  1.1766 +                                 => bool list list => bool list list)
  1.1767 +                           ((map::(bool list => bool list)
  1.1768 +                                  => bool list list => bool list list)
  1.1769 +                             ((op #::bool => bool list => bool list)
  1.1770 +                               (True::bool))
  1.1771 +                             l1)
  1.1772 +                           ((map::(bool list => bool list)
  1.1773 +                                  => bool list list => bool list list)
  1.1774 +                             ((op #::bool => bool list => bool list)
  1.1775 +                               (False::bool))
  1.1776 +                             l2))))))))
  1.1777 +      ((All::(bool list list => bool) => bool)
  1.1778 +        (%l::bool list list.
  1.1779 +            (op -->::bool => bool => bool)
  1.1780 +             ((algebra_canon::bool list list => bool) l) (P l))))"
  1.1781 +  by (import prob_canon ALGEBRA_CANON_CASES)
  1.1782 +
  1.1783 +lemma ALGEBRA_CANON_INDUCTION: "(All::((bool list list => bool) => bool) => bool)
  1.1784 + (%P::bool list list => bool.
  1.1785 +     (op -->::bool => bool => bool)
  1.1786 +      ((op &::bool => bool => bool) (P ([]::bool list list))
  1.1787 +        ((op &::bool => bool => bool)
  1.1788 +          (P ((op #::bool list => bool list list => bool list list)
  1.1789 +               ([]::bool list) ([]::bool list list)))
  1.1790 +          ((All::(bool list list => bool) => bool)
  1.1791 +            (%l1::bool list list.
  1.1792 +                (All::(bool list list => bool) => bool)
  1.1793 +                 (%l2::bool list list.
  1.1794 +                     (op -->::bool => bool => bool)
  1.1795 +                      ((op &::bool => bool => bool)
  1.1796 +                        ((algebra_canon::bool list list => bool) l1)
  1.1797 +                        ((op &::bool => bool => bool)
  1.1798 +                          ((algebra_canon::bool list list => bool) l2)
  1.1799 +                          ((op &::bool => bool => bool) (P l1)
  1.1800 +                            ((op &::bool => bool => bool) (P l2)
  1.1801 +                              ((algebra_canon::bool list list => bool)
  1.1802 +                                ((op @::bool list list
  1.1803 +  => bool list list => bool list list)
  1.1804 +                                  ((map::(bool list => bool list)
  1.1805 +   => bool list list => bool list list)
  1.1806 +                                    ((op #::bool => bool list => bool list)
  1.1807 +(True::bool))
  1.1808 +                                    l1)
  1.1809 +                                  ((map::(bool list => bool list)
  1.1810 +   => bool list list => bool list list)
  1.1811 +                                    ((op #::bool => bool list => bool list)
  1.1812 +(False::bool))
  1.1813 +                                    l2)))))))
  1.1814 +                      (P ((op @::bool list list
  1.1815 +                                 => bool list list => bool list list)
  1.1816 +                           ((map::(bool list => bool list)
  1.1817 +                                  => bool list list => bool list list)
  1.1818 +                             ((op #::bool => bool list => bool list)
  1.1819 +                               (True::bool))
  1.1820 +                             l1)
  1.1821 +                           ((map::(bool list => bool list)
  1.1822 +                                  => bool list list => bool list list)
  1.1823 +                             ((op #::bool => bool list => bool list)
  1.1824 +                               (False::bool))
  1.1825 +                             l2))))))))
  1.1826 +      ((All::(bool list list => bool) => bool)
  1.1827 +        (%l::bool list list.
  1.1828 +            (op -->::bool => bool => bool)
  1.1829 +             ((algebra_canon::bool list list => bool) l) (P l))))"
  1.1830 +  by (import prob_canon ALGEBRA_CANON_INDUCTION)
  1.1831 +
  1.1832 +lemma MEM_NIL_STEP: "ALL l1 l2. ~ [] mem map (op # True) l1 @ map (op # False) l2"
  1.1833 +  by (import prob_canon MEM_NIL_STEP)
  1.1834 +
  1.1835 +lemma ALG_SORTED_PREFIXFREE_MEM_NIL: "ALL l. (alg_sorted l & alg_prefixfree l & [] mem l) = (l = [[]])"
  1.1836 +  by (import prob_canon ALG_SORTED_PREFIXFREE_MEM_NIL)
  1.1837 +
  1.1838 +lemma ALG_SORTED_PREFIXFREE_EQUALITY: "(All::(bool list list => bool) => bool)
  1.1839 + (%l::bool list list.
  1.1840 +     (All::(bool list list => bool) => bool)
  1.1841 +      (%l'::bool list list.
  1.1842 +          (op -->::bool => bool => bool)
  1.1843 +           ((op &::bool => bool => bool)
  1.1844 +             ((All::(bool list => bool) => bool)
  1.1845 +               (%x::bool list.
  1.1846 +                   (op =::bool => bool => bool)
  1.1847 +                    ((op mem::bool list => bool list list => bool) x l)
  1.1848 +                    ((op mem::bool list => bool list list => bool) x l')))
  1.1849 +             ((op &::bool => bool => bool)
  1.1850 +               ((alg_sorted::bool list list => bool) l)
  1.1851 +               ((op &::bool => bool => bool)
  1.1852 +                 ((alg_sorted::bool list list => bool) l')
  1.1853 +                 ((op &::bool => bool => bool)
  1.1854 +                   ((alg_prefixfree::bool list list => bool) l)
  1.1855 +                   ((alg_prefixfree::bool list list => bool) l')))))
  1.1856 +           ((op =::bool list list => bool list list => bool) l l')))"
  1.1857 +  by (import prob_canon ALG_SORTED_PREFIXFREE_EQUALITY)
  1.1858 +
  1.1859 +;end_setup
  1.1860 +
  1.1861 +;setup_theory boolean_sequence
  1.1862 +
  1.1863 +consts
  1.1864 +  SHD :: "(nat => bool) => bool" 
  1.1865 +
  1.1866 +defs
  1.1867 +  SHD_primdef: "SHD == %f. f 0"
  1.1868 +
  1.1869 +lemma SHD_def: "ALL f. SHD f = f 0"
  1.1870 +  by (import boolean_sequence SHD_def)
  1.1871 +
  1.1872 +consts
  1.1873 +  STL :: "(nat => bool) => nat => bool" 
  1.1874 +
  1.1875 +defs
  1.1876 +  STL_primdef: "STL == %f n. f (Suc n)"
  1.1877 +
  1.1878 +lemma STL_def: "ALL f n. STL f n = f (Suc n)"
  1.1879 +  by (import boolean_sequence STL_def)
  1.1880 +
  1.1881 +consts
  1.1882 +  SCONS :: "bool => (nat => bool) => nat => bool" 
  1.1883 +
  1.1884 +specification (SCONS_primdef: SCONS) SCONS_def: "(ALL h t. SCONS h t 0 = h) & (ALL h t n. SCONS h t (Suc n) = t n)"
  1.1885 +  by (import boolean_sequence SCONS_def)
  1.1886 +
  1.1887 +consts
  1.1888 +  SDEST :: "(nat => bool) => bool * (nat => bool)" 
  1.1889 +
  1.1890 +defs
  1.1891 +  SDEST_primdef: "SDEST == %s. (SHD s, STL s)"
  1.1892 +
  1.1893 +lemma SDEST_def: "SDEST = (%s. (SHD s, STL s))"
  1.1894 +  by (import boolean_sequence SDEST_def)
  1.1895 +
  1.1896 +consts
  1.1897 +  SCONST :: "bool => nat => bool" 
  1.1898 +
  1.1899 +defs
  1.1900 +  SCONST_primdef: "SCONST == K"
  1.1901 +
  1.1902 +lemma SCONST_def: "SCONST = K"
  1.1903 +  by (import boolean_sequence SCONST_def)
  1.1904 +
  1.1905 +consts
  1.1906 +  STAKE :: "nat => (nat => bool) => bool list" 
  1.1907 +
  1.1908 +specification (STAKE_primdef: STAKE) STAKE_def: "(ALL s. STAKE 0 s = []) &
  1.1909 +(ALL n s. STAKE (Suc n) s = SHD s # STAKE n (STL s))"
  1.1910 +  by (import boolean_sequence STAKE_def)
  1.1911 +
  1.1912 +consts
  1.1913 +  SDROP :: "nat => (nat => bool) => nat => bool" 
  1.1914 +
  1.1915 +specification (SDROP_primdef: SDROP) SDROP_def: "SDROP 0 = I & (ALL n. SDROP (Suc n) = SDROP n o STL)"
  1.1916 +  by (import boolean_sequence SDROP_def)
  1.1917 +
  1.1918 +lemma SCONS_SURJ: "ALL x. EX xa t. x = SCONS xa t"
  1.1919 +  by (import boolean_sequence SCONS_SURJ)
  1.1920 +
  1.1921 +lemma SHD_STL_ISO: "ALL h t. EX x. SHD x = h & STL x = t"
  1.1922 +  by (import boolean_sequence SHD_STL_ISO)
  1.1923 +
  1.1924 +lemma SHD_SCONS: "ALL h t. SHD (SCONS h t) = h"
  1.1925 +  by (import boolean_sequence SHD_SCONS)
  1.1926 +
  1.1927 +lemma STL_SCONS: "ALL h t. STL (SCONS h t) = t"
  1.1928 +  by (import boolean_sequence STL_SCONS)
  1.1929 +
  1.1930 +lemma SHD_SCONST: "ALL b. SHD (SCONST b) = b"
  1.1931 +  by (import boolean_sequence SHD_SCONST)
  1.1932 +
  1.1933 +lemma STL_SCONST: "ALL b. STL (SCONST b) = SCONST b"
  1.1934 +  by (import boolean_sequence STL_SCONST)
  1.1935 +
  1.1936 +;end_setup
  1.1937 +
  1.1938 +;setup_theory prob_algebra
  1.1939 +
  1.1940 +consts
  1.1941 +  alg_embed :: "bool list => (nat => bool) => bool" 
  1.1942 +
  1.1943 +specification (alg_embed_primdef: alg_embed) alg_embed_def: "(ALL s. alg_embed [] s = True) &
  1.1944 +(ALL h t s. alg_embed (h # t) s = (h = SHD s & alg_embed t (STL s)))"
  1.1945 +  by (import prob_algebra alg_embed_def)
  1.1946 +
  1.1947 +consts
  1.1948 +  algebra_embed :: "bool list list => (nat => bool) => bool" 
  1.1949 +
  1.1950 +specification (algebra_embed_primdef: algebra_embed) algebra_embed_def: "algebra_embed [] = EMPTY &
  1.1951 +(ALL h t.
  1.1952 +    algebra_embed (h # t) = pred_set.UNION (alg_embed h) (algebra_embed t))"
  1.1953 +  by (import prob_algebra algebra_embed_def)
  1.1954 +
  1.1955 +consts
  1.1956 +  measurable :: "((nat => bool) => bool) => bool" 
  1.1957 +
  1.1958 +defs
  1.1959 +  measurable_primdef: "measurable == %s. EX b. s = algebra_embed b"
  1.1960 +
  1.1961 +lemma measurable_def: "ALL s. measurable s = (EX b. s = algebra_embed b)"
  1.1962 +  by (import prob_algebra measurable_def)
  1.1963 +
  1.1964 +lemma HALVES_INTER: "pred_set.INTER (%x. SHD x = True) (%x. SHD x = False) = EMPTY"
  1.1965 +  by (import prob_algebra HALVES_INTER)
  1.1966 +
  1.1967 +lemma INTER_STL: "ALL p q. pred_set.INTER p q o STL = pred_set.INTER (p o STL) (q o STL)"
  1.1968 +  by (import prob_algebra INTER_STL)
  1.1969 +
  1.1970 +lemma COMPL_SHD: "ALL b. COMPL (%x. SHD x = b) = (%x. SHD x = (~ b))"
  1.1971 +  by (import prob_algebra COMPL_SHD)
  1.1972 +
  1.1973 +lemma ALG_EMBED_BASIC: "alg_embed [] = pred_set.UNIV &
  1.1974 +(ALL h t.
  1.1975 +    alg_embed (h # t) = pred_set.INTER (%x. SHD x = h) (alg_embed t o STL))"
  1.1976 +  by (import prob_algebra ALG_EMBED_BASIC)
  1.1977 +
  1.1978 +lemma ALG_EMBED_NIL: "ALL c. All (alg_embed c) = (c = [])"
  1.1979 +  by (import prob_algebra ALG_EMBED_NIL)
  1.1980 +
  1.1981 +lemma ALG_EMBED_POPULATED: "ALL b. Ex (alg_embed b)"
  1.1982 +  by (import prob_algebra ALG_EMBED_POPULATED)
  1.1983 +
  1.1984 +lemma ALG_EMBED_PREFIX: "(All::(bool list => bool) => bool)
  1.1985 + (%b::bool list.
  1.1986 +     (All::(bool list => bool) => bool)
  1.1987 +      (%c::bool list.
  1.1988 +          (All::((nat => bool) => bool) => bool)
  1.1989 +           (%s::nat => bool.
  1.1990 +               (op -->::bool => bool => bool)
  1.1991 +                ((op &::bool => bool => bool)
  1.1992 +                  ((alg_embed::bool list => (nat => bool) => bool) b s)
  1.1993 +                  ((alg_embed::bool list => (nat => bool) => bool) c s))
  1.1994 +                ((op |::bool => bool => bool)
  1.1995 +                  ((IS_PREFIX::bool list => bool list => bool) b c)
  1.1996 +                  ((IS_PREFIX::bool list => bool list => bool) c b)))))"
  1.1997 +  by (import prob_algebra ALG_EMBED_PREFIX)
  1.1998 +
  1.1999 +lemma ALG_EMBED_PREFIX_SUBSET: "ALL b c. SUBSET (alg_embed b) (alg_embed c) = IS_PREFIX b c"
  1.2000 +  by (import prob_algebra ALG_EMBED_PREFIX_SUBSET)
  1.2001 +
  1.2002 +lemma ALG_EMBED_TWINS: "ALL l.
  1.2003 +   pred_set.UNION (alg_embed (SNOC True l)) (alg_embed (SNOC False l)) =
  1.2004 +   alg_embed l"
  1.2005 +  by (import prob_algebra ALG_EMBED_TWINS)
  1.2006 +
  1.2007 +lemma ALGEBRA_EMBED_BASIC: "algebra_embed [] = EMPTY &
  1.2008 +algebra_embed [[]] = pred_set.UNIV &
  1.2009 +(ALL b. algebra_embed [[b]] = (%s. SHD s = b))"
  1.2010 +  by (import prob_algebra ALGEBRA_EMBED_BASIC)
  1.2011 +
  1.2012 +lemma ALGEBRA_EMBED_MEM: "(All::(bool list list => bool) => bool)
  1.2013 + (%b::bool list list.
  1.2014 +     (All::((nat => bool) => bool) => bool)
  1.2015 +      (%x::nat => bool.
  1.2016 +          (op -->::bool => bool => bool)
  1.2017 +           ((algebra_embed::bool list list => (nat => bool) => bool) b x)
  1.2018 +           ((Ex::(bool list => bool) => bool)
  1.2019 +             (%l::bool list.
  1.2020 +                 (op &::bool => bool => bool)
  1.2021 +                  ((op mem::bool list => bool list list => bool) l b)
  1.2022 +                  ((alg_embed::bool list => (nat => bool) => bool) l x)))))"
  1.2023 +  by (import prob_algebra ALGEBRA_EMBED_MEM)
  1.2024 +
  1.2025 +lemma ALGEBRA_EMBED_APPEND: "ALL l1 l2.
  1.2026 +   algebra_embed (l1 @ l2) =
  1.2027 +   pred_set.UNION (algebra_embed l1) (algebra_embed l2)"
  1.2028 +  by (import prob_algebra ALGEBRA_EMBED_APPEND)
  1.2029 +
  1.2030 +lemma ALGEBRA_EMBED_TLS: "ALL l b.
  1.2031 +   algebra_embed (map (op # b) l) (SCONS h t) = (h = b & algebra_embed l t)"
  1.2032 +  by (import prob_algebra ALGEBRA_EMBED_TLS)
  1.2033 +
  1.2034 +lemma ALG_CANON_PREFS_EMBED: "ALL l b. algebra_embed (alg_canon_prefs l b) = algebra_embed (l # b)"
  1.2035 +  by (import prob_algebra ALG_CANON_PREFS_EMBED)
  1.2036 +
  1.2037 +lemma ALG_CANON_FIND_EMBED: "ALL l b. algebra_embed (alg_canon_find l b) = algebra_embed (l # b)"
  1.2038 +  by (import prob_algebra ALG_CANON_FIND_EMBED)
  1.2039 +
  1.2040 +lemma ALG_CANON1_EMBED: "ALL x. algebra_embed (alg_canon1 x) = algebra_embed x"
  1.2041 +  by (import prob_algebra ALG_CANON1_EMBED)
  1.2042 +
  1.2043 +lemma ALG_CANON_MERGE_EMBED: "ALL l b. algebra_embed (alg_canon_merge l b) = algebra_embed (l # b)"
  1.2044 +  by (import prob_algebra ALG_CANON_MERGE_EMBED)
  1.2045 +
  1.2046 +lemma ALG_CANON2_EMBED: "ALL x. algebra_embed (alg_canon2 x) = algebra_embed x"
  1.2047 +  by (import prob_algebra ALG_CANON2_EMBED)
  1.2048 +
  1.2049 +lemma ALG_CANON_EMBED: "ALL l. algebra_embed (alg_canon l) = algebra_embed l"
  1.2050 +  by (import prob_algebra ALG_CANON_EMBED)
  1.2051 +
  1.2052 +lemma ALGEBRA_CANON_UNIV: "(All::(bool list list => bool) => bool)
  1.2053 + (%l::bool list list.
  1.2054 +     (op -->::bool => bool => bool)
  1.2055 +      ((algebra_canon::bool list list => bool) l)
  1.2056 +      ((op -->::bool => bool => bool)
  1.2057 +        ((op =::((nat => bool) => bool) => ((nat => bool) => bool) => bool)
  1.2058 +          ((algebra_embed::bool list list => (nat => bool) => bool) l)
  1.2059 +          (pred_set.UNIV::(nat => bool) => bool))
  1.2060 +        ((op =::bool list list => bool list list => bool) l
  1.2061 +          ((op #::bool list => bool list list => bool list list)
  1.2062 +            ([]::bool list) ([]::bool list list)))))"
  1.2063 +  by (import prob_algebra ALGEBRA_CANON_UNIV)
  1.2064 +
  1.2065 +lemma ALG_CANON_REP: "ALL b c. (alg_canon b = alg_canon c) = (algebra_embed b = algebra_embed c)"
  1.2066 +  by (import prob_algebra ALG_CANON_REP)
  1.2067 +
  1.2068 +lemma ALGEBRA_CANON_EMBED_EMPTY: "(All::(bool list list => bool) => bool)
  1.2069 + (%l::bool list list.
  1.2070 +     (op -->::bool => bool => bool)
  1.2071 +      ((algebra_canon::bool list list => bool) l)
  1.2072 +      ((op =::bool => bool => bool)
  1.2073 +        ((All::((nat => bool) => bool) => bool)
  1.2074 +          (%v::nat => bool.
  1.2075 +              (Not::bool => bool)
  1.2076 +               ((algebra_embed::bool list list => (nat => bool) => bool) l
  1.2077 +                 v)))
  1.2078 +        ((op =::bool list list => bool list list => bool) l
  1.2079 +          ([]::bool list list))))"
  1.2080 +  by (import prob_algebra ALGEBRA_CANON_EMBED_EMPTY)
  1.2081 +
  1.2082 +lemma ALGEBRA_CANON_EMBED_UNIV: "(All::(bool list list => bool) => bool)
  1.2083 + (%l::bool list list.
  1.2084 +     (op -->::bool => bool => bool)
  1.2085 +      ((algebra_canon::bool list list => bool) l)
  1.2086 +      ((op =::bool => bool => bool)
  1.2087 +        ((All::((nat => bool) => bool) => bool)
  1.2088 +          ((algebra_embed::bool list list => (nat => bool) => bool) l))
  1.2089 +        ((op =::bool list list => bool list list => bool) l
  1.2090 +          ((op #::bool list => bool list list => bool list list)
  1.2091 +            ([]::bool list) ([]::bool list list)))))"
  1.2092 +  by (import prob_algebra ALGEBRA_CANON_EMBED_UNIV)
  1.2093 +
  1.2094 +lemma MEASURABLE_ALGEBRA: "ALL b. measurable (algebra_embed b)"
  1.2095 +  by (import prob_algebra MEASURABLE_ALGEBRA)
  1.2096 +
  1.2097 +lemma MEASURABLE_BASIC: "measurable EMPTY &
  1.2098 +measurable pred_set.UNIV & (ALL b. measurable (%s. SHD s = b))"
  1.2099 +  by (import prob_algebra MEASURABLE_BASIC)
  1.2100 +
  1.2101 +lemma MEASURABLE_SHD: "ALL b. measurable (%s. SHD s = b)"
  1.2102 +  by (import prob_algebra MEASURABLE_SHD)
  1.2103 +
  1.2104 +lemma ALGEBRA_EMBED_COMPL: "ALL l. EX l'. COMPL (algebra_embed l) = algebra_embed l'"
  1.2105 +  by (import prob_algebra ALGEBRA_EMBED_COMPL)
  1.2106 +
  1.2107 +lemma MEASURABLE_COMPL: "ALL s. measurable (COMPL s) = measurable s"
  1.2108 +  by (import prob_algebra MEASURABLE_COMPL)
  1.2109 +
  1.2110 +lemma MEASURABLE_UNION: "(All::(((nat => bool) => bool) => bool) => bool)
  1.2111 + (%s::(nat => bool) => bool.
  1.2112 +     (All::(((nat => bool) => bool) => bool) => bool)
  1.2113 +      (%t::(nat => bool) => bool.
  1.2114 +          (op -->::bool => bool => bool)
  1.2115 +           ((op &::bool => bool => bool)
  1.2116 +             ((measurable::((nat => bool) => bool) => bool) s)
  1.2117 +             ((measurable::((nat => bool) => bool) => bool) t))
  1.2118 +           ((measurable::((nat => bool) => bool) => bool)
  1.2119 +             ((pred_set.UNION::((nat => bool) => bool)
  1.2120 +                               => ((nat => bool) => bool)
  1.2121 +                                  => (nat => bool) => bool)
  1.2122 +               s t))))"
  1.2123 +  by (import prob_algebra MEASURABLE_UNION)
  1.2124 +
  1.2125 +lemma MEASURABLE_INTER: "(All::(((nat => bool) => bool) => bool) => bool)
  1.2126 + (%s::(nat => bool) => bool.
  1.2127 +     (All::(((nat => bool) => bool) => bool) => bool)
  1.2128 +      (%t::(nat => bool) => bool.
  1.2129 +          (op -->::bool => bool => bool)
  1.2130 +           ((op &::bool => bool => bool)
  1.2131 +             ((measurable::((nat => bool) => bool) => bool) s)
  1.2132 +             ((measurable::((nat => bool) => bool) => bool) t))
  1.2133 +           ((measurable::((nat => bool) => bool) => bool)
  1.2134 +             ((pred_set.INTER::((nat => bool) => bool)
  1.2135 +                               => ((nat => bool) => bool)
  1.2136 +                                  => (nat => bool) => bool)
  1.2137 +               s t))))"
  1.2138 +  by (import prob_algebra MEASURABLE_INTER)
  1.2139 +
  1.2140 +lemma MEASURABLE_STL: "ALL p. measurable (p o STL) = measurable p"
  1.2141 +  by (import prob_algebra MEASURABLE_STL)
  1.2142 +
  1.2143 +lemma MEASURABLE_SDROP: "ALL n p. measurable (p o SDROP n) = measurable p"
  1.2144 +  by (import prob_algebra MEASURABLE_SDROP)
  1.2145 +
  1.2146 +lemma MEASURABLE_INTER_HALVES: "ALL p.
  1.2147 +   (measurable (pred_set.INTER (%x. SHD x = True) p) &
  1.2148 +    measurable (pred_set.INTER (%x. SHD x = False) p)) =
  1.2149 +   measurable p"
  1.2150 +  by (import prob_algebra MEASURABLE_INTER_HALVES)
  1.2151 +
  1.2152 +lemma MEASURABLE_HALVES: "ALL p q.
  1.2153 +   measurable
  1.2154 +    (pred_set.UNION (pred_set.INTER (%x. SHD x = True) p)
  1.2155 +      (pred_set.INTER (%x. SHD x = False) q)) =
  1.2156 +   (measurable (pred_set.INTER (%x. SHD x = True) p) &
  1.2157 +    measurable (pred_set.INTER (%x. SHD x = False) q))"
  1.2158 +  by (import prob_algebra MEASURABLE_HALVES)
  1.2159 +
  1.2160 +lemma MEASURABLE_INTER_SHD: "ALL b p.
  1.2161 +   measurable (pred_set.INTER (%x. SHD x = b) (p o STL)) = measurable p"
  1.2162 +  by (import prob_algebra MEASURABLE_INTER_SHD)
  1.2163 +
  1.2164 +;end_setup
  1.2165 +
  1.2166 +;setup_theory prob
  1.2167 +
  1.2168 +consts
  1.2169 +  alg_measure :: "bool list list => real" 
  1.2170 +
  1.2171 +specification (alg_measure_primdef: alg_measure) alg_measure_def: "alg_measure [] = 0 &
  1.2172 +(ALL l rest. alg_measure (l # rest) = (1 / 2) ^ length l + alg_measure rest)"
  1.2173 +  by (import prob alg_measure_def)
  1.2174 +
  1.2175 +consts
  1.2176 +  algebra_measure :: "bool list list => real" 
  1.2177 +
  1.2178 +defs
  1.2179 +  algebra_measure_primdef: "algebra_measure ==
  1.2180 +%b. inf (%r. EX c. algebra_embed b = algebra_embed c & alg_measure c = r)"
  1.2181 +
  1.2182 +lemma algebra_measure_def: "ALL b.
  1.2183 +   algebra_measure b =
  1.2184 +   inf (%r. EX c. algebra_embed b = algebra_embed c & alg_measure c = r)"
  1.2185 +  by (import prob algebra_measure_def)
  1.2186 +
  1.2187 +consts
  1.2188 +  prob :: "((nat => bool) => bool) => real" 
  1.2189 +
  1.2190 +defs
  1.2191 +  prob_primdef: "prob ==
  1.2192 +%s. sup (%r. EX b. algebra_measure b = r & SUBSET (algebra_embed b) s)"
  1.2193 +
  1.2194 +lemma prob_def: "ALL s.
  1.2195 +   prob s =
  1.2196 +   sup (%r. EX b. algebra_measure b = r & SUBSET (algebra_embed b) s)"
  1.2197 +  by (import prob prob_def)
  1.2198 +
  1.2199 +lemma ALG_TWINS_MEASURE: "ALL l::bool list.
  1.2200 +   ((1::real) / (2::real)) ^ length (SNOC True l) +
  1.2201 +   ((1::real) / (2::real)) ^ length (SNOC False l) =
  1.2202 +   ((1::real) / (2::real)) ^ length l"
  1.2203 +  by (import prob ALG_TWINS_MEASURE)
  1.2204 +
  1.2205 +lemma ALG_MEASURE_BASIC: "alg_measure [] = 0 &
  1.2206 +alg_measure [[]] = 1 & (ALL b. alg_measure [[b]] = 1 / 2)"
  1.2207 +  by (import prob ALG_MEASURE_BASIC)
  1.2208 +
  1.2209 +lemma ALG_MEASURE_POS: "ALL l. 0 <= alg_measure l"
  1.2210 +  by (import prob ALG_MEASURE_POS)
  1.2211 +
  1.2212 +lemma ALG_MEASURE_APPEND: "ALL l1 l2. alg_measure (l1 @ l2) = alg_measure l1 + alg_measure l2"
  1.2213 +  by (import prob ALG_MEASURE_APPEND)
  1.2214 +
  1.2215 +lemma ALG_MEASURE_TLS: "ALL l b. 2 * alg_measure (map (op # b) l) = alg_measure l"
  1.2216 +  by (import prob ALG_MEASURE_TLS)
  1.2217 +
  1.2218 +lemma ALG_CANON_PREFS_MONO: "ALL l b. alg_measure (alg_canon_prefs l b) <= alg_measure (l # b)"
  1.2219 +  by (import prob ALG_CANON_PREFS_MONO)
  1.2220 +
  1.2221 +lemma ALG_CANON_FIND_MONO: "ALL l b. alg_measure (alg_canon_find l b) <= alg_measure (l # b)"
  1.2222 +  by (import prob ALG_CANON_FIND_MONO)
  1.2223 +
  1.2224 +lemma ALG_CANON1_MONO: "ALL x. alg_measure (alg_canon1 x) <= alg_measure x"
  1.2225 +  by (import prob ALG_CANON1_MONO)
  1.2226 +
  1.2227 +lemma ALG_CANON_MERGE_MONO: "ALL l b. alg_measure (alg_canon_merge l b) <= alg_measure (l # b)"
  1.2228 +  by (import prob ALG_CANON_MERGE_MONO)
  1.2229 +
  1.2230 +lemma ALG_CANON2_MONO: "ALL x. alg_measure (alg_canon2 x) <= alg_measure x"
  1.2231 +  by (import prob ALG_CANON2_MONO)
  1.2232 +
  1.2233 +lemma ALG_CANON_MONO: "ALL l. alg_measure (alg_canon l) <= alg_measure l"
  1.2234 +  by (import prob ALG_CANON_MONO)
  1.2235 +
  1.2236 +lemma ALGEBRA_MEASURE_DEF_ALT: "ALL l. algebra_measure l = alg_measure (alg_canon l)"
  1.2237 +  by (import prob ALGEBRA_MEASURE_DEF_ALT)
  1.2238 +
  1.2239 +lemma ALGEBRA_MEASURE_BASIC: "algebra_measure [] = 0 &
  1.2240 +algebra_measure [[]] = 1 & (ALL b. algebra_measure [[b]] = 1 / 2)"
  1.2241 +  by (import prob ALGEBRA_MEASURE_BASIC)
  1.2242 +
  1.2243 +lemma ALGEBRA_CANON_MEASURE_MAX: "(All::(bool list list => bool) => bool)
  1.2244 + (%l::bool list list.
  1.2245 +     (op -->::bool => bool => bool)
  1.2246 +      ((algebra_canon::bool list list => bool) l)
  1.2247 +      ((op <=::real => real => bool)
  1.2248 +        ((alg_measure::bool list list => real) l) (1::real)))"
  1.2249 +  by (import prob ALGEBRA_CANON_MEASURE_MAX)
  1.2250 +
  1.2251 +lemma ALGEBRA_MEASURE_MAX: "ALL l. algebra_measure l <= 1"
  1.2252 +  by (import prob ALGEBRA_MEASURE_MAX)
  1.2253 +
  1.2254 +lemma ALGEBRA_MEASURE_MONO_EMBED: "(All::(bool list list => bool) => bool)
  1.2255 + (%x::bool list list.
  1.2256 +     (All::(bool list list => bool) => bool)
  1.2257 +      (%xa::bool list list.
  1.2258 +          (op -->::bool => bool => bool)
  1.2259 +           ((SUBSET::((nat => bool) => bool)
  1.2260 +                     => ((nat => bool) => bool) => bool)
  1.2261 +             ((algebra_embed::bool list list => (nat => bool) => bool) x)
  1.2262 +             ((algebra_embed::bool list list => (nat => bool) => bool) xa))
  1.2263 +           ((op <=::real => real => bool)
  1.2264 +             ((algebra_measure::bool list list => real) x)
  1.2265 +             ((algebra_measure::bool list list => real) xa))))"
  1.2266 +  by (import prob ALGEBRA_MEASURE_MONO_EMBED)
  1.2267 +
  1.2268 +lemma ALG_MEASURE_COMPL: "(All::(bool list list => bool) => bool)
  1.2269 + (%l::bool list list.
  1.2270 +     (op -->::bool => bool => bool)
  1.2271 +      ((algebra_canon::bool list list => bool) l)
  1.2272 +      ((All::(bool list list => bool) => bool)
  1.2273 +        (%c::bool list list.
  1.2274 +            (op -->::bool => bool => bool)
  1.2275 +             ((algebra_canon::bool list list => bool) c)
  1.2276 +             ((op -->::bool => bool => bool)
  1.2277 +               ((op =::((nat => bool) => bool)
  1.2278 +                       => ((nat => bool) => bool) => bool)
  1.2279 +                 ((COMPL::((nat => bool) => bool) => (nat => bool) => bool)
  1.2280 +                   ((algebra_embed::bool list list => (nat => bool) => bool)
  1.2281 +                     l))
  1.2282 +                 ((algebra_embed::bool list list => (nat => bool) => bool)
  1.2283 +                   c))
  1.2284 +               ((op =::real => real => bool)
  1.2285 +                 ((op +::real => real => real)
  1.2286 +                   ((alg_measure::bool list list => real) l)
  1.2287 +                   ((alg_measure::bool list list => real) c))
  1.2288 +                 (1::real))))))"
  1.2289 +  by (import prob ALG_MEASURE_COMPL)
  1.2290 +
  1.2291 +lemma ALG_MEASURE_ADDITIVE: "(All::(bool list list => bool) => bool)
  1.2292 + (%l::bool list list.
  1.2293 +     (op -->::bool => bool => bool)
  1.2294 +      ((algebra_canon::bool list list => bool) l)
  1.2295 +      ((All::(bool list list => bool) => bool)
  1.2296 +        (%c::bool list list.
  1.2297 +            (op -->::bool => bool => bool)
  1.2298 +             ((algebra_canon::bool list list => bool) c)
  1.2299 +             ((All::(bool list list => bool) => bool)
  1.2300 +               (%d::bool list list.
  1.2301 +                   (op -->::bool => bool => bool)
  1.2302 +                    ((algebra_canon::bool list list => bool) d)
  1.2303 +                    ((op -->::bool => bool => bool)
  1.2304 +                      ((op &::bool => bool => bool)
  1.2305 +                        ((op =::((nat => bool) => bool)
  1.2306 +                                => ((nat => bool) => bool) => bool)
  1.2307 +                          ((pred_set.INTER::((nat => bool) => bool)
  1.2308 +      => ((nat => bool) => bool) => (nat => bool) => bool)
  1.2309 +                            ((algebra_embed::bool list list
  1.2310 +       => (nat => bool) => bool)
  1.2311 +                              c)
  1.2312 +                            ((algebra_embed::bool list list
  1.2313 +       => (nat => bool) => bool)
  1.2314 +                              d))
  1.2315 +                          (EMPTY::(nat => bool) => bool))
  1.2316 +                        ((op =::((nat => bool) => bool)
  1.2317 +                                => ((nat => bool) => bool) => bool)
  1.2318 +                          ((algebra_embed::bool list list
  1.2319 +     => (nat => bool) => bool)
  1.2320 +                            l)
  1.2321 +                          ((pred_set.UNION::((nat => bool) => bool)
  1.2322 +      => ((nat => bool) => bool) => (nat => bool) => bool)
  1.2323 +                            ((algebra_embed::bool list list
  1.2324 +       => (nat => bool) => bool)
  1.2325 +                              c)
  1.2326 +                            ((algebra_embed::bool list list
  1.2327 +       => (nat => bool) => bool)
  1.2328 +                              d))))
  1.2329 +                      ((op =::real => real => bool)
  1.2330 +                        ((alg_measure::bool list list => real) l)
  1.2331 +                        ((op +::real => real => real)
  1.2332 +                          ((alg_measure::bool list list => real) c)
  1.2333 +                          ((alg_measure::bool list list => real) d)))))))))"
  1.2334 +  by (import prob ALG_MEASURE_ADDITIVE)
  1.2335 +
  1.2336 +lemma PROB_ALGEBRA: "ALL l. prob (algebra_embed l) = algebra_measure l"
  1.2337 +  by (import prob PROB_ALGEBRA)
  1.2338 +
  1.2339 +lemma PROB_BASIC: "prob EMPTY = 0 &
  1.2340 +prob pred_set.UNIV = 1 & (ALL b. prob (%s. SHD s = b) = 1 / 2)"
  1.2341 +  by (import prob PROB_BASIC)
  1.2342 +
  1.2343 +lemma PROB_ADDITIVE: "(All::(((nat => bool) => bool) => bool) => bool)
  1.2344 + (%s::(nat => bool) => bool.
  1.2345 +     (All::(((nat => bool) => bool) => bool) => bool)
  1.2346 +      (%t::(nat => bool) => bool.
  1.2347 +          (op -->::bool => bool => bool)
  1.2348 +           ((op &::bool => bool => bool)
  1.2349 +             ((measurable::((nat => bool) => bool) => bool) s)
  1.2350 +             ((op &::bool => bool => bool)
  1.2351 +               ((measurable::((nat => bool) => bool) => bool) t)
  1.2352 +               ((op =::((nat => bool) => bool)
  1.2353 +                       => ((nat => bool) => bool) => bool)
  1.2354 +                 ((pred_set.INTER::((nat => bool) => bool)
  1.2355 +                                   => ((nat => bool) => bool)
  1.2356 +=> (nat => bool) => bool)
  1.2357 +                   s t)
  1.2358 +                 (EMPTY::(nat => bool) => bool))))
  1.2359 +           ((op =::real => real => bool)
  1.2360 +             ((prob::((nat => bool) => bool) => real)
  1.2361 +               ((pred_set.UNION::((nat => bool) => bool)
  1.2362 +                                 => ((nat => bool) => bool)
  1.2363 +                                    => (nat => bool) => bool)
  1.2364 +                 s t))
  1.2365 +             ((op +::real => real => real)
  1.2366 +               ((prob::((nat => bool) => bool) => real) s)
  1.2367 +               ((prob::((nat => bool) => bool) => real) t)))))"
  1.2368 +  by (import prob PROB_ADDITIVE)
  1.2369 +
  1.2370 +lemma PROB_COMPL: "(All::(((nat => bool) => bool) => bool) => bool)
  1.2371 + (%s::(nat => bool) => bool.
  1.2372 +     (op -->::bool => bool => bool)
  1.2373 +      ((measurable::((nat => bool) => bool) => bool) s)
  1.2374 +      ((op =::real => real => bool)
  1.2375 +        ((prob::((nat => bool) => bool) => real)
  1.2376 +          ((COMPL::((nat => bool) => bool) => (nat => bool) => bool) s))
  1.2377 +        ((op -::real => real => real) (1::real)
  1.2378 +          ((prob::((nat => bool) => bool) => real) s))))"
  1.2379 +  by (import prob PROB_COMPL)
  1.2380 +
  1.2381 +lemma PROB_SUP_EXISTS1: "ALL s. EX x b. algebra_measure b = x & SUBSET (algebra_embed b) s"
  1.2382 +  by (import prob PROB_SUP_EXISTS1)
  1.2383 +
  1.2384 +lemma PROB_SUP_EXISTS2: "(All::(((nat => bool) => bool) => bool) => bool)
  1.2385 + (%s::(nat => bool) => bool.
  1.2386 +     (Ex::(real => bool) => bool)
  1.2387 +      (%x::real.
  1.2388 +          (All::(real => bool) => bool)
  1.2389 +           (%r::real.
  1.2390 +               (op -->::bool => bool => bool)
  1.2391 +                ((Ex::(bool list list => bool) => bool)
  1.2392 +                  (%b::bool list list.
  1.2393 +                      (op &::bool => bool => bool)
  1.2394 +                       ((op =::real => real => bool)
  1.2395 +                         ((algebra_measure::bool list list => real) b) r)
  1.2396 +                       ((SUBSET::((nat => bool) => bool)
  1.2397 +                                 => ((nat => bool) => bool) => bool)
  1.2398 +                         ((algebra_embed::bool list list
  1.2399 +    => (nat => bool) => bool)
  1.2400 +                           b)
  1.2401 +                         s)))
  1.2402 +                ((op <=::real => real => bool) r x))))"
  1.2403 +  by (import prob PROB_SUP_EXISTS2)
  1.2404 +
  1.2405 +lemma PROB_LE_X: "(All::(((nat => bool) => bool) => bool) => bool)
  1.2406 + (%s::(nat => bool) => bool.
  1.2407 +     (All::(real => bool) => bool)
  1.2408 +      (%x::real.
  1.2409 +          (op -->::bool => bool => bool)
  1.2410 +           ((All::(((nat => bool) => bool) => bool) => bool)
  1.2411 +             (%s'::(nat => bool) => bool.
  1.2412 +                 (op -->::bool => bool => bool)
  1.2413 +                  ((op &::bool => bool => bool)
  1.2414 +                    ((measurable::((nat => bool) => bool) => bool) s')
  1.2415 +                    ((SUBSET::((nat => bool) => bool)
  1.2416 +                              => ((nat => bool) => bool) => bool)
  1.2417 +                      s' s))
  1.2418 +                  ((op <=::real => real => bool)
  1.2419 +                    ((prob::((nat => bool) => bool) => real) s') x)))
  1.2420 +           ((op <=::real => real => bool)
  1.2421 +             ((prob::((nat => bool) => bool) => real) s) x)))"
  1.2422 +  by (import prob PROB_LE_X)
  1.2423 +
  1.2424 +lemma X_LE_PROB: "(All::(((nat => bool) => bool) => bool) => bool)
  1.2425 + (%s::(nat => bool) => bool.
  1.2426 +     (All::(real => bool) => bool)
  1.2427 +      (%x::real.
  1.2428 +          (op -->::bool => bool => bool)
  1.2429 +           ((Ex::(((nat => bool) => bool) => bool) => bool)
  1.2430 +             (%s'::(nat => bool) => bool.
  1.2431 +                 (op &::bool => bool => bool)
  1.2432 +                  ((measurable::((nat => bool) => bool) => bool) s')
  1.2433 +                  ((op &::bool => bool => bool)
  1.2434 +                    ((SUBSET::((nat => bool) => bool)
  1.2435 +                              => ((nat => bool) => bool) => bool)
  1.2436 +                      s' s)
  1.2437 +                    ((op <=::real => real => bool) x
  1.2438 +                      ((prob::((nat => bool) => bool) => real) s')))))
  1.2439 +           ((op <=::real => real => bool) x
  1.2440 +             ((prob::((nat => bool) => bool) => real) s))))"
  1.2441 +  by (import prob X_LE_PROB)
  1.2442 +
  1.2443 +lemma PROB_SUBSET_MONO: "(All::(((nat => bool) => bool) => bool) => bool)
  1.2444 + (%s::(nat => bool) => bool.
  1.2445 +     (All::(((nat => bool) => bool) => bool) => bool)
  1.2446 +      (%t::(nat => bool) => bool.
  1.2447 +          (op -->::bool => bool => bool)
  1.2448 +           ((SUBSET::((nat => bool) => bool)
  1.2449 +                     => ((nat => bool) => bool) => bool)
  1.2450 +             s t)
  1.2451 +           ((op <=::real => real => bool)
  1.2452 +             ((prob::((nat => bool) => bool) => real) s)
  1.2453 +             ((prob::((nat => bool) => bool) => real) t))))"
  1.2454 +  by (import prob PROB_SUBSET_MONO)
  1.2455 +
  1.2456 +lemma PROB_ALG: "ALL x. prob (alg_embed x) = (1 / 2) ^ length x"
  1.2457 +  by (import prob PROB_ALG)
  1.2458 +
  1.2459 +lemma PROB_STL: "(All::(((nat => bool) => bool) => bool) => bool)
  1.2460 + (%p::(nat => bool) => bool.
  1.2461 +     (op -->::bool => bool => bool)
  1.2462 +      ((measurable::((nat => bool) => bool) => bool) p)
  1.2463 +      ((op =::real => real => bool)
  1.2464 +        ((prob::((nat => bool) => bool) => real)
  1.2465 +          ((op o::((nat => bool) => bool)
  1.2466 +                  => ((nat => bool) => nat => bool)
  1.2467 +                     => (nat => bool) => bool)
  1.2468 +            p (STL::(nat => bool) => nat => bool)))
  1.2469 +        ((prob::((nat => bool) => bool) => real) p)))"
  1.2470 +  by (import prob PROB_STL)
  1.2471 +
  1.2472 +lemma PROB_SDROP: "(All::(nat => bool) => bool)
  1.2473 + (%n::nat.
  1.2474 +     (All::(((nat => bool) => bool) => bool) => bool)
  1.2475 +      (%p::(nat => bool) => bool.
  1.2476 +          (op -->::bool => bool => bool)
  1.2477 +           ((measurable::((nat => bool) => bool) => bool) p)
  1.2478 +           ((op =::real => real => bool)
  1.2479 +             ((prob::((nat => bool) => bool) => real)
  1.2480 +               ((op o::((nat => bool) => bool)
  1.2481 +                       => ((nat => bool) => nat => bool)
  1.2482 +                          => (nat => bool) => bool)
  1.2483 +                 p ((SDROP::nat => (nat => bool) => nat => bool) n)))
  1.2484 +             ((prob::((nat => bool) => bool) => real) p))))"
  1.2485 +  by (import prob PROB_SDROP)
  1.2486 +
  1.2487 +lemma PROB_INTER_HALVES: "(All::(((nat => bool) => bool) => bool) => bool)
  1.2488 + (%p::(nat => bool) => bool.
  1.2489 +     (op -->::bool => bool => bool)
  1.2490 +      ((measurable::((nat => bool) => bool) => bool) p)
  1.2491 +      ((op =::real => real => bool)
  1.2492 +        ((op +::real => real => real)
  1.2493 +          ((prob::((nat => bool) => bool) => real)
  1.2494 +            ((pred_set.INTER::((nat => bool) => bool)
  1.2495 +                              => ((nat => bool) => bool)
  1.2496 +                                 => (nat => bool) => bool)
  1.2497 +              (%x::nat => bool.
  1.2498 +                  (op =::bool => bool => bool)
  1.2499 +                   ((SHD::(nat => bool) => bool) x) (True::bool))
  1.2500 +              p))
  1.2501 +          ((prob::((nat => bool) => bool) => real)
  1.2502 +            ((pred_set.INTER::((nat => bool) => bool)
  1.2503 +                              => ((nat => bool) => bool)
  1.2504 +                                 => (nat => bool) => bool)
  1.2505 +              (%x::nat => bool.
  1.2506 +                  (op =::bool => bool => bool)
  1.2507 +                   ((SHD::(nat => bool) => bool) x) (False::bool))
  1.2508 +              p)))
  1.2509 +        ((prob::((nat => bool) => bool) => real) p)))"
  1.2510 +  by (import prob PROB_INTER_HALVES)
  1.2511 +
  1.2512 +lemma PROB_INTER_SHD: "(All::(bool => bool) => bool)
  1.2513 + (%b::bool.
  1.2514 +     (All::(((nat => bool) => bool) => bool) => bool)
  1.2515 +      (%p::(nat => bool) => bool.
  1.2516 +          (op -->::bool => bool => bool)
  1.2517 +           ((measurable::((nat => bool) => bool) => bool) p)
  1.2518 +           ((op =::real => real => bool)
  1.2519 +             ((prob::((nat => bool) => bool) => real)
  1.2520 +               ((pred_set.INTER::((nat => bool) => bool)
  1.2521 +                                 => ((nat => bool) => bool)
  1.2522 +                                    => (nat => bool) => bool)
  1.2523 +                 (%x::nat => bool.
  1.2524 +                     (op =::bool => bool => bool)
  1.2525 +                      ((SHD::(nat => bool) => bool) x) b)
  1.2526 +                 ((op o::((nat => bool) => bool)
  1.2527 +                         => ((nat => bool) => nat => bool)
  1.2528 +                            => (nat => bool) => bool)
  1.2529 +                   p (STL::(nat => bool) => nat => bool))))
  1.2530 +             ((op *::real => real => real)
  1.2531 +               ((op /::real => real => real) (1::real)
  1.2532 +                 ((number_of::bin => real)
  1.2533 +                   ((op BIT::bin => bool => bin)
  1.2534 +                     ((op BIT::bin => bool => bin) (bin.Pls::bin)
  1.2535 +                       (True::bool))
  1.2536 +                     (False::bool))))
  1.2537 +               ((prob::((nat => bool) => bool) => real) p)))))"
  1.2538 +  by (import prob PROB_INTER_SHD)
  1.2539 +
  1.2540 +lemma ALGEBRA_MEASURE_POS: "ALL l. 0 <= algebra_measure l"
  1.2541 +  by (import prob ALGEBRA_MEASURE_POS)
  1.2542 +
  1.2543 +lemma ALGEBRA_MEASURE_RANGE: "ALL l. 0 <= algebra_measure l & algebra_measure l <= 1"
  1.2544 +  by (import prob ALGEBRA_MEASURE_RANGE)
  1.2545 +
  1.2546 +lemma PROB_POS: "ALL p. 0 <= prob p"
  1.2547 +  by (import prob PROB_POS)
  1.2548 +
  1.2549 +lemma PROB_MAX: "ALL p. prob p <= 1"
  1.2550 +  by (import prob PROB_MAX)
  1.2551 +
  1.2552 +lemma PROB_RANGE: "ALL p. 0 <= prob p & prob p <= 1"
  1.2553 +  by (import prob PROB_RANGE)
  1.2554 +
  1.2555 +lemma ABS_PROB: "ALL p. abs (prob p) = prob p"
  1.2556 +  by (import prob ABS_PROB)
  1.2557 +
  1.2558 +lemma PROB_SHD: "ALL b. prob (%s. SHD s = b) = 1 / 2"
  1.2559 +  by (import prob PROB_SHD)
  1.2560 +
  1.2561 +lemma PROB_COMPL_LE1: "(All::(((nat => bool) => bool) => bool) => bool)
  1.2562 + (%p::(nat => bool) => bool.
  1.2563 +     (All::(real => bool) => bool)
  1.2564 +      (%r::real.
  1.2565 +          (op -->::bool => bool => bool)
  1.2566 +           ((measurable::((nat => bool) => bool) => bool) p)
  1.2567 +           ((op =::bool => bool => bool)
  1.2568 +             ((op <=::real => real => bool)
  1.2569 +               ((prob::((nat => bool) => bool) => real)
  1.2570 +                 ((COMPL::((nat => bool) => bool) => (nat => bool) => bool)
  1.2571 +                   p))
  1.2572 +               r)
  1.2573 +             ((op <=::real => real => bool)
  1.2574 +               ((op -::real => real => real) (1::real) r)
  1.2575 +               ((prob::((nat => bool) => bool) => real) p)))))"
  1.2576 +  by (import prob PROB_COMPL_LE1)
  1.2577 +
  1.2578 +;end_setup
  1.2579 +
  1.2580 +;setup_theory prob_pseudo
  1.2581 +
  1.2582 +consts
  1.2583 +  pseudo_linear_hd :: "nat => bool" 
  1.2584 +
  1.2585 +defs
  1.2586 +  pseudo_linear_hd_primdef: "pseudo_linear_hd == EVEN"
  1.2587 +
  1.2588 +lemma pseudo_linear_hd_def: "pseudo_linear_hd = EVEN"
  1.2589 +  by (import prob_pseudo pseudo_linear_hd_def)
  1.2590 +
  1.2591 +consts
  1.2592 +  pseudo_linear_tl :: "nat => nat => nat => nat => nat" 
  1.2593 +
  1.2594 +defs
  1.2595 +  pseudo_linear_tl_primdef: "pseudo_linear_tl == %a b n x. (a * x + b) mod (2 * n + 1)"
  1.2596 +
  1.2597 +lemma pseudo_linear_tl_def: "ALL a b n x. pseudo_linear_tl a b n x = (a * x + b) mod (2 * n + 1)"
  1.2598 +  by (import prob_pseudo pseudo_linear_tl_def)
  1.2599 +
  1.2600 +lemma PSEUDO_LINEAR1_EXECUTE: "EX x. (ALL xa. SHD (x xa) = pseudo_linear_hd xa) &
  1.2601 +      (ALL xa.
  1.2602 +          STL (x xa) =
  1.2603 +          x (pseudo_linear_tl
  1.2604 +              (NUMERAL
  1.2605 +                (NUMERAL_BIT1
  1.2606 +                  (NUMERAL_BIT1
  1.2607 +                    (NUMERAL_BIT1
  1.2608 +                      (NUMERAL_BIT2
  1.2609 +                        (NUMERAL_BIT1 (NUMERAL_BIT2 ALT_ZERO)))))))
  1.2610 +              (NUMERAL
  1.2611 +                (NUMERAL_BIT1
  1.2612 +                  (NUMERAL_BIT1
  1.2613 +                    (NUMERAL_BIT1
  1.2614 +                      (NUMERAL_BIT1
  1.2615 +                        (NUMERAL_BIT1 (NUMERAL_BIT2 ALT_ZERO)))))))
  1.2616 +              (NUMERAL
  1.2617 +                (NUMERAL_BIT1
  1.2618 +                  (NUMERAL_BIT1
  1.2619 +                    (NUMERAL_BIT1
  1.2620 +                      (NUMERAL_BIT1
  1.2621 +                        (NUMERAL_BIT2 (NUMERAL_BIT1 ALT_ZERO)))))))
  1.2622 +              xa))"
  1.2623 +  by (import prob_pseudo PSEUDO_LINEAR1_EXECUTE)
  1.2624 +
  1.2625 +consts
  1.2626 +  pseudo_linear1 :: "nat => nat => bool" 
  1.2627 +
  1.2628 +specification (pseudo_linear1_primdef: pseudo_linear1) pseudo_linear1_def: "(ALL x. SHD (pseudo_linear1 x) = pseudo_linear_hd x) &
  1.2629 +(ALL x.
  1.2630 +    STL (pseudo_linear1 x) =
  1.2631 +    pseudo_linear1
  1.2632 +     (pseudo_linear_tl
  1.2633 +       (NUMERAL
  1.2634 +         (NUMERAL_BIT1
  1.2635 +           (NUMERAL_BIT1
  1.2636 +             (NUMERAL_BIT1
  1.2637 +               (NUMERAL_BIT2 (NUMERAL_BIT1 (NUMERAL_BIT2 ALT_ZERO)))))))
  1.2638 +       (NUMERAL
  1.2639 +         (NUMERAL_BIT1
  1.2640 +           (NUMERAL_BIT1
  1.2641 +             (NUMERAL_BIT1
  1.2642 +               (NUMERAL_BIT1 (NUMERAL_BIT1 (NUMERAL_BIT2 ALT_ZERO)))))))
  1.2643 +       (NUMERAL
  1.2644 +         (NUMERAL_BIT1
  1.2645 +           (NUMERAL_BIT1
  1.2646 +             (NUMERAL_BIT1
  1.2647 +               (NUMERAL_BIT1 (NUMERAL_BIT2 (NUMERAL_BIT1 ALT_ZERO)))))))
  1.2648 +       x))"
  1.2649 +  by (import prob_pseudo pseudo_linear1_def)
  1.2650 +
  1.2651 +consts
  1.2652 +  pseudo :: "nat => nat => bool" 
  1.2653 +
  1.2654 +defs
  1.2655 +  pseudo_primdef: "pseudo == pseudo_linear1"
  1.2656 +
  1.2657 +lemma pseudo_def: "pseudo = pseudo_linear1"
  1.2658 +  by (import prob_pseudo pseudo_def)
  1.2659 +
  1.2660 +;end_setup
  1.2661 +
  1.2662 +;setup_theory prob_indep
  1.2663 +
  1.2664 +consts
  1.2665 +  indep_set :: "((nat => bool) => bool) => ((nat => bool) => bool) => bool" 
  1.2666 +
  1.2667 +defs
  1.2668 +  indep_set_primdef: "indep_set ==
  1.2669 +%p q. measurable p &
  1.2670 +      measurable q & prob (pred_set.INTER p q) = prob p * prob q"
  1.2671 +
  1.2672 +lemma indep_set_def: "ALL p q.
  1.2673 +   indep_set p q =
  1.2674 +   (measurable p &
  1.2675 +    measurable q & prob (pred_set.INTER p q) = prob p * prob q)"
  1.2676 +  by (import prob_indep indep_set_def)
  1.2677 +
  1.2678 +consts
  1.2679 +  alg_cover_set :: "bool list list => bool" 
  1.2680 +
  1.2681 +defs
  1.2682 +  alg_cover_set_primdef: "alg_cover_set ==
  1.2683 +%l. alg_sorted l & alg_prefixfree l & algebra_embed l = pred_set.UNIV"
  1.2684 +
  1.2685 +lemma alg_cover_set_def: "ALL l.
  1.2686 +   alg_cover_set l =
  1.2687 +   (alg_sorted l & alg_prefixfree l & algebra_embed l = pred_set.UNIV)"
  1.2688 +  by (import prob_indep alg_cover_set_def)
  1.2689 +
  1.2690 +consts
  1.2691 +  alg_cover :: "bool list list => (nat => bool) => bool list" 
  1.2692 +
  1.2693 +defs
  1.2694 +  alg_cover_primdef: "alg_cover == %l x. SOME b. b mem l & alg_embed b x"
  1.2695 +
  1.2696 +lemma alg_cover_def: "ALL l x. alg_cover l x = (SOME b. b mem l & alg_embed b x)"
  1.2697 +  by (import prob_indep alg_cover_def)
  1.2698 +
  1.2699 +consts
  1.2700 +  indep :: "((nat => bool) => 'a * (nat => bool)) => bool" 
  1.2701 +
  1.2702 +defs
  1.2703 +  indep_primdef: "indep ==
  1.2704 +%f. EX l r.
  1.2705 +       alg_cover_set l &
  1.2706 +       (ALL s. f s = (let c = alg_cover l s in (r c, SDROP (length c) s)))"
  1.2707 +
  1.2708 +lemma indep_def: "ALL f.
  1.2709 +   indep f =
  1.2710 +   (EX l r.
  1.2711 +       alg_cover_set l &
  1.2712 +       (ALL s. f s = (let c = alg_cover l s in (r c, SDROP (length c) s))))"
  1.2713 +  by (import prob_indep indep_def)
  1.2714 +
  1.2715 +lemma INDEP_SET_BASIC: "(All::(((nat => bool) => bool) => bool) => bool)
  1.2716 + (%p::(nat => bool) => bool.
  1.2717 +     (op -->::bool => bool => bool)
  1.2718 +      ((measurable::((nat => bool) => bool) => bool) p)
  1.2719 +      ((op &::bool => bool => bool)
  1.2720 +        ((indep_set::((nat => bool) => bool)
  1.2721 +                     => ((nat => bool) => bool) => bool)
  1.2722 +          (EMPTY::(nat => bool) => bool) p)
  1.2723 +        ((indep_set::((nat => bool) => bool)
  1.2724 +                     => ((nat => bool) => bool) => bool)
  1.2725 +          (pred_set.UNIV::(nat => bool) => bool) p)))"
  1.2726 +  by (import prob_indep INDEP_SET_BASIC)
  1.2727 +
  1.2728 +lemma INDEP_SET_SYM: "ALL p q. indep_set p q = indep_set p q"
  1.2729 +  by (import prob_indep INDEP_SET_SYM)
  1.2730 +
  1.2731 +lemma INDEP_SET_DISJOINT_DECOMP: "(All::(((nat => bool) => bool) => bool) => bool)
  1.2732 + (%p::(nat => bool) => bool.
  1.2733 +     (All::(((nat => bool) => bool) => bool) => bool)
  1.2734 +      (%q::(nat => bool) => bool.
  1.2735 +          (All::(((nat => bool) => bool) => bool) => bool)
  1.2736 +           (%r::(nat => bool) => bool.
  1.2737 +               (op -->::bool => bool => bool)
  1.2738 +                ((op &::bool => bool => bool)
  1.2739 +                  ((indep_set::((nat => bool) => bool)
  1.2740 +                               => ((nat => bool) => bool) => bool)
  1.2741 +                    p r)
  1.2742 +                  ((op &::bool => bool => bool)
  1.2743 +                    ((indep_set::((nat => bool) => bool)
  1.2744 +                                 => ((nat => bool) => bool) => bool)
  1.2745 +                      q r)
  1.2746 +                    ((op =::((nat => bool) => bool)
  1.2747 +                            => ((nat => bool) => bool) => bool)
  1.2748 +                      ((pred_set.INTER::((nat => bool) => bool)
  1.2749 +  => ((nat => bool) => bool) => (nat => bool) => bool)
  1.2750 +                        p q)
  1.2751 +                      (EMPTY::(nat => bool) => bool))))
  1.2752 +                ((indep_set::((nat => bool) => bool)
  1.2753 +                             => ((nat => bool) => bool) => bool)
  1.2754 +                  ((pred_set.UNION::((nat => bool) => bool)
  1.2755 +                                    => ((nat => bool) => bool)
  1.2756 + => (nat => bool) => bool)
  1.2757 +                    p q)
  1.2758 +                  r))))"
  1.2759 +  by (import prob_indep INDEP_SET_DISJOINT_DECOMP)
  1.2760 +
  1.2761 +lemma ALG_COVER_SET_BASIC: "~ alg_cover_set [] & alg_cover_set [[]] & alg_cover_set [[True], [False]]"
  1.2762 +  by (import prob_indep ALG_COVER_SET_BASIC)
  1.2763 +
  1.2764 +lemma ALG_COVER_WELL_DEFINED: "(All::(bool list list => bool) => bool)
  1.2765 + (%l::bool list list.
  1.2766 +     (All::((nat => bool) => bool) => bool)
  1.2767 +      (%x::nat => bool.
  1.2768 +          (op -->::bool => bool => bool)
  1.2769 +           ((alg_cover_set::bool list list => bool) l)
  1.2770 +           ((op &::bool => bool => bool)
  1.2771 +             ((op mem::bool list => bool list list => bool)
  1.2772 +               ((alg_cover::bool list list => (nat => bool) => bool list) l
  1.2773 +                 x)
  1.2774 +               l)
  1.2775 +             ((alg_embed::bool list => (nat => bool) => bool)
  1.2776 +               ((alg_cover::bool list list => (nat => bool) => bool list) l
  1.2777 +                 x)
  1.2778 +               x))))"
  1.2779 +  by (import prob_indep ALG_COVER_WELL_DEFINED)
  1.2780 +
  1.2781 +lemma ALG_COVER_UNIV: "alg_cover [[]] = K []"
  1.2782 +  by (import prob_indep ALG_COVER_UNIV)
  1.2783 +
  1.2784 +lemma MAP_CONS_TL_FILTER: "(All::(bool list list => bool) => bool)
  1.2785 + (%l::bool list list.
  1.2786 +     (All::(bool => bool) => bool)
  1.2787 +      (%b::bool.
  1.2788 +          (op -->::bool => bool => bool)
  1.2789 +           ((Not::bool => bool)
  1.2790 +             ((op mem::bool list => bool list list => bool) ([]::bool list)
  1.2791 +               l))
  1.2792 +           ((op =::bool list list => bool list list => bool)
  1.2793 +             ((map::(bool list => bool list)
  1.2794 +                    => bool list list => bool list list)
  1.2795 +               ((op #::bool => bool list => bool list) b)
  1.2796 +               ((map::(bool list => bool list)
  1.2797 +                      => bool list list => bool list list)
  1.2798 +                 (tl::bool list => bool list)
  1.2799 +                 ((filter::(bool list => bool)
  1.2800 +                           => bool list list => bool list list)
  1.2801 +                   (%x::bool list.
  1.2802 +                       (op =::bool => bool => bool)
  1.2803 +                        ((hd::bool list => bool) x) b)
  1.2804 +                   l)))
  1.2805 +             ((filter::(bool list => bool)
  1.2806 +                       => bool list list => bool list list)
  1.2807 +               (%x::bool list.
  1.2808 +                   (op =::bool => bool => bool) ((hd::bool list => bool) x)
  1.2809 +                    b)
  1.2810 +               l))))"
  1.2811 +  by (import prob_indep MAP_CONS_TL_FILTER)
  1.2812 +
  1.2813 +lemma ALG_COVER_SET_CASES_THM: "ALL l.
  1.2814 +   alg_cover_set l =
  1.2815 +   (l = [[]] |
  1.2816 +    (EX x xa.
  1.2817 +        alg_cover_set x &
  1.2818 +        alg_cover_set xa & l = map (op # True) x @ map (op # False) xa))"
  1.2819 +  by (import prob_indep ALG_COVER_SET_CASES_THM)
  1.2820 +
  1.2821 +lemma ALG_COVER_SET_CASES: "(All::((bool list list => bool) => bool) => bool)
  1.2822 + (%P::bool list list => bool.
  1.2823 +     (op -->::bool => bool => bool)
  1.2824 +      ((op &::bool => bool => bool)
  1.2825 +        (P ((op #::bool list => bool list list => bool list list)
  1.2826 +             ([]::bool list) ([]::bool list list)))
  1.2827 +        ((All::(bool list list => bool) => bool)
  1.2828 +          (%l1::bool list list.
  1.2829 +              (All::(bool list list => bool) => bool)
  1.2830 +               (%l2::bool list list.
  1.2831 +                   (op -->::bool => bool => bool)
  1.2832 +                    ((op &::bool => bool => bool)
  1.2833 +                      ((alg_cover_set::bool list list => bool) l1)
  1.2834 +                      ((op &::bool => bool => bool)
  1.2835 +                        ((alg_cover_set::bool list list => bool) l2)
  1.2836 +                        ((alg_cover_set::bool list list => bool)
  1.2837 +                          ((op @::bool list list
  1.2838 +                                  => bool list list => bool list list)
  1.2839 +                            ((map::(bool list => bool list)
  1.2840 +                                   => bool list list => bool list list)
  1.2841 +                              ((op #::bool => bool list => bool list)
  1.2842 +                                (True::bool))
  1.2843 +                              l1)
  1.2844 +                            ((map::(bool list => bool list)
  1.2845 +                                   => bool list list => bool list list)
  1.2846 +                              ((op #::bool => bool list => bool list)
  1.2847 +                                (False::bool))
  1.2848 +                              l2)))))
  1.2849 +                    (P ((op @::bool list list
  1.2850 +                               => bool list list => bool list list)
  1.2851 +                         ((map::(bool list => bool list)
  1.2852 +                                => bool list list => bool list list)
  1.2853 +                           ((op #::bool => bool list => bool list)
  1.2854 +                             (True::bool))
  1.2855 +                           l1)
  1.2856 +                         ((map::(bool list => bool list)
  1.2857 +                                => bool list list => bool list list)
  1.2858 +                           ((op #::bool => bool list => bool list)
  1.2859 +                             (False::bool))
  1.2860 +                           l2)))))))
  1.2861 +      ((All::(bool list list => bool) => bool)
  1.2862 +        (%l::bool list list.
  1.2863 +            (op -->::bool => bool => bool)
  1.2864 +             ((alg_cover_set::bool list list => bool) l) (P l))))"
  1.2865 +  by (import prob_indep ALG_COVER_SET_CASES)
  1.2866 +
  1.2867 +lemma ALG_COVER_SET_INDUCTION: "(All::((bool list list => bool) => bool) => bool)
  1.2868 + (%P::bool list list => bool.
  1.2869 +     (op -->::bool => bool => bool)
  1.2870 +      ((op &::bool => bool => bool)
  1.2871 +        (P ((op #::bool list => bool list list => bool list list)
  1.2872 +             ([]::bool list) ([]::bool list list)))
  1.2873 +        ((All::(bool list list => bool) => bool)
  1.2874 +          (%l1::bool list list.
  1.2875 +              (All::(bool list list => bool) => bool)
  1.2876 +               (%l2::bool list list.
  1.2877 +                   (op -->::bool => bool => bool)
  1.2878 +                    ((op &::bool => bool => bool)
  1.2879 +                      ((alg_cover_set::bool list list => bool) l1)
  1.2880 +                      ((op &::bool => bool => bool)
  1.2881 +                        ((alg_cover_set::bool list list => bool) l2)
  1.2882 +                        ((op &::bool => bool => bool) (P l1)
  1.2883 +                          ((op &::bool => bool => bool) (P l2)
  1.2884 +                            ((alg_cover_set::bool list list => bool)
  1.2885 +                              ((op @::bool list list
  1.2886 +=> bool list list => bool list list)
  1.2887 +                                ((map::(bool list => bool list)
  1.2888 + => bool list list => bool list list)
  1.2889 +                                  ((op #::bool => bool list => bool list)
  1.2890 +                                    (True::bool))
  1.2891 +                                  l1)
  1.2892 +                                ((map::(bool list => bool list)
  1.2893 + => bool list list => bool list list)
  1.2894 +                                  ((op #::bool => bool list => bool list)
  1.2895 +                                    (False::bool))
  1.2896 +                                  l2)))))))
  1.2897 +                    (P ((op @::bool list list
  1.2898 +                               => bool list list => bool list list)
  1.2899 +                         ((map::(bool list => bool list)
  1.2900 +                                => bool list list => bool list list)
  1.2901 +                           ((op #::bool => bool list => bool list)
  1.2902 +                             (True::bool))
  1.2903 +                           l1)
  1.2904 +                         ((map::(bool list => bool list)
  1.2905 +                                => bool list list => bool list list)
  1.2906 +                           ((op #::bool => bool list => bool list)
  1.2907 +                             (False::bool))
  1.2908 +                           l2)))))))
  1.2909 +      ((All::(bool list list => bool) => bool)
  1.2910 +        (%l::bool list list.
  1.2911 +            (op -->::bool => bool => bool)
  1.2912 +             ((alg_cover_set::bool list list => bool) l) (P l))))"
  1.2913 +  by (import prob_indep ALG_COVER_SET_INDUCTION)
  1.2914 +
  1.2915 +lemma ALG_COVER_EXISTS_UNIQUE: "(All::(bool list list => bool) => bool)
  1.2916 + (%l::bool list list.
  1.2917 +     (op -->::bool => bool => bool)
  1.2918 +      ((alg_cover_set::bool list list => bool) l)
  1.2919 +      ((All::((nat => bool) => bool) => bool)
  1.2920 +        (%s::nat => bool.
  1.2921 +            (Ex1::(bool list => bool) => bool)
  1.2922 +             (%x::bool list.
  1.2923 +                 (op &::bool => bool => bool)
  1.2924 +                  ((op mem::bool list => bool list list => bool) x l)
  1.2925 +                  ((alg_embed::bool list => (nat => bool) => bool) x s)))))"
  1.2926 +  by (import prob_indep ALG_COVER_EXISTS_UNIQUE)
  1.2927 +
  1.2928 +lemma ALG_COVER_UNIQUE: "(All::(bool list list => bool) => bool)
  1.2929 + (%l::bool list list.
  1.2930 +     (All::(bool list => bool) => bool)
  1.2931 +      (%x::bool list.
  1.2932 +          (All::((nat => bool) => bool) => bool)
  1.2933 +           (%s::nat => bool.
  1.2934 +               (op -->::bool => bool => bool)
  1.2935 +                ((op &::bool => bool => bool)
  1.2936 +                  ((alg_cover_set::bool list list => bool) l)
  1.2937 +                  ((op &::bool => bool => bool)
  1.2938 +                    ((op mem::bool list => bool list list => bool) x l)
  1.2939 +                    ((alg_embed::bool list => (nat => bool) => bool) x s)))
  1.2940 +                ((op =::bool list => bool list => bool)
  1.2941 +                  ((alg_cover::bool list list => (nat => bool) => bool list)
  1.2942 +                    l s)
  1.2943 +                  x))))"
  1.2944 +  by (import prob_indep ALG_COVER_UNIQUE)
  1.2945 +
  1.2946 +lemma ALG_COVER_STEP: "(All::(bool list list => bool) => bool)
  1.2947 + (%l1::bool list list.
  1.2948 +     (All::(bool list list => bool) => bool)
  1.2949 +      (%l2::bool list list.
  1.2950 +          (All::(bool => bool) => bool)
  1.2951 +           (%h::bool.
  1.2952 +               (All::((nat => bool) => bool) => bool)
  1.2953 +                (%t::nat => bool.
  1.2954 +                    (op -->::bool => bool => bool)
  1.2955 +                     ((op &::bool => bool => bool)
  1.2956 +                       ((alg_cover_set::bool list list => bool) l1)
  1.2957 +                       ((alg_cover_set::bool list list => bool) l2))
  1.2958 +                     ((op =::bool list => bool list => bool)
  1.2959 +                       ((alg_cover::bool list list
  1.2960 +                                    => (nat => bool) => bool list)
  1.2961 +                         ((op @::bool list list
  1.2962 +                                 => bool list list => bool list list)
  1.2963 +                           ((map::(bool list => bool list)
  1.2964 +                                  => bool list list => bool list list)
  1.2965 +                             ((op #::bool => bool list => bool list)
  1.2966 +                               (True::bool))
  1.2967 +                             l1)
  1.2968 +                           ((map::(bool list => bool list)
  1.2969 +                                  => bool list list => bool list list)
  1.2970 +                             ((op #::bool => bool list => bool list)
  1.2971 +                               (False::bool))
  1.2972 +                             l2))
  1.2973 +                         ((SCONS::bool => (nat => bool) => nat => bool) h
  1.2974 +                           t))
  1.2975 +                       ((If::bool => bool list => bool list => bool list) h
  1.2976 +                         ((op #::bool => bool list => bool list)
  1.2977 +                           (True::bool)
  1.2978 +                           ((alg_cover::bool list list
  1.2979 +  => (nat => bool) => bool list)
  1.2980 +                             l1 t))
  1.2981 +                         ((op #::bool => bool list => bool list)
  1.2982 +                           (False::bool)
  1.2983 +                           ((alg_cover::bool list list
  1.2984 +  => (nat => bool) => bool list)
  1.2985 +                             l2 t))))))))"
  1.2986 +  by (import prob_indep ALG_COVER_STEP)
  1.2987 +
  1.2988 +lemma ALG_COVER_HEAD: "(All::(bool list list => bool) => bool)
  1.2989 + (%l::bool list list.
  1.2990 +     (op -->::bool => bool => bool)
  1.2991 +      ((alg_cover_set::bool list list => bool) l)
  1.2992 +      ((All::((bool list => bool) => bool) => bool)
  1.2993 +        (%f::bool list => bool.
  1.2994 +            (op =::((nat => bool) => bool)
  1.2995 +                   => ((nat => bool) => bool) => bool)
  1.2996 +             ((op o::(bool list => bool)
  1.2997 +                     => ((nat => bool) => bool list)
  1.2998 +                        => (nat => bool) => bool)
  1.2999 +               f ((alg_cover::bool list list => (nat => bool) => bool list)
  1.3000 +                   l))
  1.3001 +             ((algebra_embed::bool list list => (nat => bool) => bool)
  1.3002 +               ((filter::(bool list => bool)
  1.3003 +                         => bool list list => bool list list)
  1.3004 +                 f l)))))"
  1.3005 +  by (import prob_indep ALG_COVER_HEAD)
  1.3006 +
  1.3007 +lemma ALG_COVER_TAIL_STEP: "(All::(bool list list => bool) => bool)
  1.3008 + (%l1::bool list list.
  1.3009 +     (All::(bool list list => bool) => bool)
  1.3010 +      (%l2::bool list list.
  1.3011 +          (All::(((nat => bool) => bool) => bool) => bool)
  1.3012 +           (%q::(nat => bool) => bool.
  1.3013 +               (op -->::bool => bool => bool)
  1.3014 +                ((op &::bool => bool => bool)
  1.3015 +                  ((alg_cover_set::bool list list => bool) l1)
  1.3016 +                  ((alg_cover_set::bool list list => bool) l2))
  1.3017 +                ((op =::((nat => bool) => bool)
  1.3018 +                        => ((nat => bool) => bool) => bool)
  1.3019 +                  ((op o::((nat => bool) => bool)
  1.3020 +                          => ((nat => bool) => nat => bool)
  1.3021 +                             => (nat => bool) => bool)
  1.3022 +                    q (%x::nat => bool.
  1.3023 +                          (SDROP::nat => (nat => bool) => nat => bool)
  1.3024 +                           ((size::bool list => nat)
  1.3025 +                             ((alg_cover::bool list list
  1.3026 +    => (nat => bool) => bool list)
  1.3027 +                               ((op @::bool list list
  1.3028 + => bool list list => bool list list)
  1.3029 +                                 ((map::(bool list => bool list)
  1.3030 +  => bool list list => bool list list)
  1.3031 +                                   ((op #::bool => bool list => bool list)
  1.3032 +                                     (True::bool))
  1.3033 +                                   l1)
  1.3034 +                                 ((map::(bool list => bool list)
  1.3035 +  => bool list list => bool list list)
  1.3036 +                                   ((op #::bool => bool list => bool list)
  1.3037 +                                     (False::bool))
  1.3038 +                                   l2))
  1.3039 +                               x))
  1.3040 +                           x))
  1.3041 +                  ((pred_set.UNION::((nat => bool) => bool)
  1.3042 +                                    => ((nat => bool) => bool)
  1.3043 + => (nat => bool) => bool)
  1.3044 +                    ((pred_set.INTER::((nat => bool) => bool)
  1.3045 +=> ((nat => bool) => bool) => (nat => bool) => bool)
  1.3046 +                      (%x::nat => bool.
  1.3047 +                          (op =::bool => bool => bool)
  1.3048 +                           ((SHD::(nat => bool) => bool) x) (True::bool))
  1.3049 +                      ((op o::((nat => bool) => bool)
  1.3050 +                              => ((nat => bool) => nat => bool)
  1.3051 +                                 => (nat => bool) => bool)
  1.3052 +                        q ((op o::((nat => bool) => nat => bool)
  1.3053 +                                  => ((nat => bool) => nat => bool)
  1.3054 +                                     => (nat => bool) => nat => bool)
  1.3055 +                            (%x::nat => bool.
  1.3056 +                                (SDROP::nat => (nat => bool) => nat => bool)
  1.3057 +                                 ((size::bool list => nat)
  1.3058 +                                   ((alg_cover::bool list list
  1.3059 +          => (nat => bool) => bool list)
  1.3060 +                                     l1 x))
  1.3061 +                                 x)
  1.3062 +                            (STL::(nat => bool) => nat => bool))))
  1.3063 +                    ((pred_set.INTER::((nat => bool) => bool)
  1.3064 +=> ((nat => bool) => bool) => (nat => bool) => bool)
  1.3065 +                      (%x::nat => bool.
  1.3066 +                          (op =::bool => bool => bool)
  1.3067 +                           ((SHD::(nat => bool) => bool) x) (False::bool))
  1.3068 +                      ((op o::((nat => bool) => bool)
  1.3069 +                              => ((nat => bool) => nat => bool)
  1.3070 +                                 => (nat => bool) => bool)
  1.3071 +                        q ((op o::((nat => bool) => nat => bool)
  1.3072 +                                  => ((nat => bool) => nat => bool)
  1.3073 +                                     => (nat => bool) => nat => bool)
  1.3074 +                            (%x::nat => bool.
  1.3075 +                                (SDROP::nat => (nat => bool) => nat => bool)
  1.3076 +                                 ((size::bool list => nat)
  1.3077 +                                   ((alg_cover::bool list list
  1.3078 +          => (nat => bool) => bool list)
  1.3079 +                                     l2 x))
  1.3080 +                                 x)
  1.3081 +                            (STL::(nat => bool) => nat => bool)))))))))"
  1.3082 +  by (import prob_indep ALG_COVER_TAIL_STEP)
  1.3083 +
  1.3084 +lemma ALG_COVER_TAIL_MEASURABLE: "(All::(bool list list => bool) => bool)
  1.3085 + (%l::bool list list.
  1.3086 +     (op -->::bool => bool => bool)
  1.3087 +      ((alg_cover_set::bool list list => bool) l)
  1.3088 +      ((All::(((nat => bool) => bool) => bool) => bool)
  1.3089 +        (%q::(nat => bool) => bool.
  1.3090 +            (op =::bool => bool => bool)
  1.3091 +             ((measurable::((nat => bool) => bool) => bool)
  1.3092 +               ((op o::((nat => bool) => bool)
  1.3093 +                       => ((nat => bool) => nat => bool)
  1.3094 +                          => (nat => bool) => bool)
  1.3095 +                 q (%x::nat => bool.
  1.3096 +                       (SDROP::nat => (nat => bool) => nat => bool)
  1.3097 +                        ((size::bool list => nat)
  1.3098 +                          ((alg_cover::bool list list
  1.3099 + => (nat => bool) => bool list)
  1.3100 +                            l x))
  1.3101 +                        x)))
  1.3102 +             ((measurable::((nat => bool) => bool) => bool) q))))"
  1.3103 +  by (import prob_indep ALG_COVER_TAIL_MEASURABLE)
  1.3104 +
  1.3105 +lemma ALG_COVER_TAIL_PROB: "(All::(bool list list => bool) => bool)
  1.3106 + (%l::bool list list.
  1.3107 +     (op -->::bool => bool => bool)
  1.3108 +      ((alg_cover_set::bool list list => bool) l)
  1.3109 +      ((All::(((nat => bool) => bool) => bool) => bool)
  1.3110 +        (%q::(nat => bool) => bool.
  1.3111 +            (op -->::bool => bool => bool)
  1.3112 +             ((measurable::((nat => bool) => bool) => bool) q)
  1.3113 +             ((op =::real => real => bool)
  1.3114 +               ((prob::((nat => bool) => bool) => real)
  1.3115 +                 ((op o::((nat => bool) => bool)
  1.3116 +                         => ((nat => bool) => nat => bool)
  1.3117 +                            => (nat => bool) => bool)
  1.3118 +                   q (%x::nat => bool.
  1.3119 +                         (SDROP::nat => (nat => bool) => nat => bool)
  1.3120 +                          ((size::bool list => nat)
  1.3121 +                            ((alg_cover::bool list list
  1.3122 +   => (nat => bool) => bool list)
  1.3123 +                              l x))
  1.3124 +                          x)))
  1.3125 +               ((prob::((nat => bool) => bool) => real) q)))))"
  1.3126 +  by (import prob_indep ALG_COVER_TAIL_PROB)
  1.3127 +
  1.3128 +lemma INDEP_INDEP_SET_LEMMA: "(All::(bool list list => bool) => bool)
  1.3129 + (%l::bool list list.
  1.3130 +     (op -->::bool => bool => bool)
  1.3131 +      ((alg_cover_set::bool list list => bool) l)
  1.3132 +      ((All::(((nat => bool) => bool) => bool) => bool)
  1.3133 +        (%q::(nat => bool) => bool.
  1.3134 +            (op -->::bool => bool => bool)
  1.3135 +             ((measurable::((nat => bool) => bool) => bool) q)
  1.3136 +             ((All::(bool list => bool) => bool)
  1.3137 +               (%x::bool list.
  1.3138 +                   (op -->::bool => bool => bool)
  1.3139 +                    ((op mem::bool list => bool list list => bool) x l)
  1.3140 +                    ((op =::real => real => bool)
  1.3141 +                      ((prob::((nat => bool) => bool) => real)
  1.3142 +                        ((pred_set.INTER::((nat => bool) => bool)
  1.3143 +    => ((nat => bool) => bool) => (nat => bool) => bool)
  1.3144 +                          ((alg_embed::bool list => (nat => bool) => bool)
  1.3145 +                            x)
  1.3146 +                          ((op o::((nat => bool) => bool)
  1.3147 +                                  => ((nat => bool) => nat => bool)
  1.3148 +                                     => (nat => bool) => bool)
  1.3149 +                            q (%x::nat => bool.
  1.3150 +                                  (SDROP::nat
  1.3151 +    => (nat => bool) => nat => bool)
  1.3152 +                                   ((size::bool list => nat)
  1.3153 +                                     ((alg_cover::bool list list
  1.3154 +            => (nat => bool) => bool list)
  1.3155 + l x))
  1.3156 +                                   x))))
  1.3157 +                      ((op *::real => real => real)
  1.3158 +                        ((op ^::real => nat => real)
  1.3159 +                          ((op /::real => real => real) (1::real)
  1.3160 +                            ((number_of::bin => real)
  1.3161 +                              ((op BIT::bin => bool => bin)
  1.3162 +                                ((op BIT::bin => bool => bin) (bin.Pls::bin)
  1.3163 +                                  (True::bool))
  1.3164 +                                (False::bool))))
  1.3165 +                          ((size::bool list => nat) x))
  1.3166 +                        ((prob::((nat => bool) => bool) => real) q))))))))"
  1.3167 +  by (import prob_indep INDEP_INDEP_SET_LEMMA)
  1.3168 +
  1.3169 +lemma INDEP_SET_LIST: "(All::(((nat => bool) => bool) => bool) => bool)
  1.3170 + (%q::(nat => bool) => bool.
  1.3171 +     (All::(bool list list => bool) => bool)
  1.3172 +      (%l::bool list list.
  1.3173 +          (op -->::bool => bool => bool)
  1.3174 +           ((op &::bool => bool => bool)
  1.3175 +             ((alg_sorted::bool list list => bool) l)
  1.3176 +             ((op &::bool => bool => bool)
  1.3177 +               ((alg_prefixfree::bool list list => bool) l)
  1.3178 +               ((op &::bool => bool => bool)
  1.3179 +                 ((measurable::((nat => bool) => bool) => bool) q)
  1.3180 +                 ((All::(bool list => bool) => bool)
  1.3181 +                   (%x::bool list.
  1.3182 +                       (op -->::bool => bool => bool)
  1.3183 +                        ((op mem::bool list => bool list list => bool) x l)
  1.3184 +                        ((indep_set::((nat => bool) => bool)
  1.3185 +                                     => ((nat => bool) => bool) => bool)
  1.3186 +                          ((alg_embed::bool list => (nat => bool) => bool)
  1.3187 +                            x)
  1.3188 +                          q))))))
  1.3189 +           ((indep_set::((nat => bool) => bool)
  1.3190 +                        => ((nat => bool) => bool) => bool)
  1.3191 +             ((algebra_embed::bool list list => (nat => bool) => bool) l)
  1.3192 +             q)))"
  1.3193 +  by (import prob_indep INDEP_SET_LIST)
  1.3194 +
  1.3195 +lemma INDEP_INDEP_SET: "(All::(((nat => bool) => 'a * (nat => bool)) => bool) => bool)
  1.3196 + (%f::(nat => bool) => 'a * (nat => bool).
  1.3197 +     (All::(('a => bool) => bool) => bool)
  1.3198 +      (%p::'a => bool.
  1.3199 +          (All::(((nat => bool) => bool) => bool) => bool)
  1.3200 +           (%q::(nat => bool) => bool.
  1.3201 +               (op -->::bool => bool => bool)
  1.3202 +                ((op &::bool => bool => bool)
  1.3203 +                  ((indep::((nat => bool) => 'a * (nat => bool)) => bool) f)
  1.3204 +                  ((measurable::((nat => bool) => bool) => bool) q))
  1.3205 +                ((indep_set::((nat => bool) => bool)
  1.3206 +                             => ((nat => bool) => bool) => bool)
  1.3207 +                  ((op o::('a => bool)
  1.3208 +                          => ((nat => bool) => 'a) => (nat => bool) => bool)
  1.3209 +                    p ((op o::('a * (nat => bool) => 'a)
  1.3210 +                              => ((nat => bool) => 'a * (nat => bool))
  1.3211 +                                 => (nat => bool) => 'a)
  1.3212 +                        (fst::'a * (nat => bool) => 'a) f))
  1.3213 +                  ((op o::((nat => bool) => bool)
  1.3214 +                          => ((nat => bool) => nat => bool)
  1.3215 +                             => (nat => bool) => bool)
  1.3216 +                    q ((op o::('a * (nat => bool) => nat => bool)
  1.3217 +                              => ((nat => bool) => 'a * (nat => bool))
  1.3218 +                                 => (nat => bool) => nat => bool)
  1.3219 +                        (snd::'a * (nat => bool) => nat => bool) f))))))"
  1.3220 +  by (import prob_indep INDEP_INDEP_SET)
  1.3221 +
  1.3222 +lemma INDEP_UNIT: "ALL x. indep (UNIT x)"
  1.3223 +  by (import prob_indep INDEP_UNIT)
  1.3224 +
  1.3225 +lemma INDEP_SDEST: "indep SDEST"
  1.3226 +  by (import prob_indep INDEP_SDEST)
  1.3227 +
  1.3228 +lemma BIND_STEP: "ALL f. BIND SDEST (%k. f o SCONS k) = f"
  1.3229 +  by (import prob_indep BIND_STEP)
  1.3230 +
  1.3231 +lemma INDEP_BIND_SDEST: "(All::((bool => (nat => bool) => 'a * (nat => bool)) => bool) => bool)
  1.3232 + (%f::bool => (nat => bool) => 'a * (nat => bool).
  1.3233 +     (op -->::bool => bool => bool)
  1.3234 +      ((All::(bool => bool) => bool)
  1.3235 +        (%x::bool.
  1.3236 +            (indep::((nat => bool) => 'a * (nat => bool)) => bool) (f x)))
  1.3237 +      ((indep::((nat => bool) => 'a * (nat => bool)) => bool)
  1.3238 +        ((BIND::((nat => bool) => bool * (nat => bool))
  1.3239 +                => (bool => (nat => bool) => 'a * (nat => bool))
  1.3240 +                   => (nat => bool) => 'a * (nat => bool))
  1.3241 +          (SDEST::(nat => bool) => bool * (nat => bool)) f)))"
  1.3242 +  by (import prob_indep INDEP_BIND_SDEST)
  1.3243 +
  1.3244 +lemma INDEP_BIND: "(All::(((nat => bool) => 'a * (nat => bool)) => bool) => bool)
  1.3245 + (%f::(nat => bool) => 'a * (nat => bool).
  1.3246 +     (All::(('a => (nat => bool) => 'b * (nat => bool)) => bool) => bool)
  1.3247 +      (%g::'a => (nat => bool) => 'b * (nat => bool).
  1.3248 +          (op -->::bool => bool => bool)
  1.3249 +           ((op &::bool => bool => bool)
  1.3250 +             ((indep::((nat => bool) => 'a * (nat => bool)) => bool) f)
  1.3251 +             ((All::('a => bool) => bool)
  1.3252 +               (%x::'a.
  1.3253 +                   (indep::((nat => bool) => 'b * (nat => bool)) => bool)
  1.3254 +                    (g x))))
  1.3255 +           ((indep::((nat => bool) => 'b * (nat => bool)) => bool)
  1.3256 +             ((BIND::((nat => bool) => 'a * (nat => bool))
  1.3257 +                     => ('a => (nat => bool) => 'b * (nat => bool))
  1.3258 +                        => (nat => bool) => 'b * (nat => bool))
  1.3259 +               f g))))"
  1.3260 +  by (import prob_indep INDEP_BIND)
  1.3261 +
  1.3262 +lemma INDEP_PROB: "(All::(((nat => bool) => 'a * (nat => bool)) => bool) => bool)
  1.3263 + (%f::(nat => bool) => 'a * (nat => bool).
  1.3264 +     (All::(('a => bool) => bool) => bool)
  1.3265 +      (%p::'a => bool.
  1.3266 +          (All::(((nat => bool) => bool) => bool) => bool)
  1.3267 +           (%q::(nat => bool) => bool.
  1.3268 +               (op -->::bool => bool => bool)
  1.3269 +                ((op &::bool => bool => bool)
  1.3270 +                  ((indep::((nat => bool) => 'a * (nat => bool)) => bool) f)
  1.3271 +                  ((measurable::((nat => bool) => bool) => bool) q))
  1.3272 +                ((op =::real => real => bool)
  1.3273 +                  ((prob::((nat => bool) => bool) => real)
  1.3274 +                    ((pred_set.INTER::((nat => bool) => bool)
  1.3275 +=> ((nat => bool) => bool) => (nat => bool) => bool)
  1.3276 +                      ((op o::('a => bool)
  1.3277 +                              => ((nat => bool) => 'a)
  1.3278 +                                 => (nat => bool) => bool)
  1.3279 +                        p ((op o::('a * (nat => bool) => 'a)
  1.3280 +                                  => ((nat => bool) => 'a * (nat => bool))
  1.3281 +                                     => (nat => bool) => 'a)
  1.3282 +                            (fst::'a * (nat => bool) => 'a) f))
  1.3283 +                      ((op o::((nat => bool) => bool)
  1.3284 +                              => ((nat => bool) => nat => bool)
  1.3285 +                                 => (nat => bool) => bool)
  1.3286 +                        q ((op o::('a * (nat => bool) => nat => bool)
  1.3287 +                                  => ((nat => bool) => 'a * (nat => bool))
  1.3288 +                                     => (nat => bool) => nat => bool)
  1.3289 +                            (snd::'a * (nat => bool) => nat => bool) f))))
  1.3290 +                  ((op *::real => real => real)
  1.3291 +                    ((prob::((nat => bool) => bool) => real)
  1.3292 +                      ((op o::('a => bool)
  1.3293 +                              => ((nat => bool) => 'a)
  1.3294 +                                 => (nat => bool) => bool)
  1.3295 +                        p ((op o::('a * (nat => bool) => 'a)
  1.3296 +                                  => ((nat => bool) => 'a * (nat => bool))
  1.3297 +                                     => (nat => bool) => 'a)
  1.3298 +                            (fst::'a * (nat => bool) => 'a) f)))
  1.3299 +                    ((prob::((nat => bool) => bool) => real) q))))))"
  1.3300 +  by (import prob_indep INDEP_PROB)
  1.3301 +
  1.3302 +lemma INDEP_MEASURABLE1: "(All::(((nat => bool) => 'a * (nat => bool)) => bool) => bool)
  1.3303 + (%f::(nat => bool) => 'a * (nat => bool).
  1.3304 +     (All::(('a => bool) => bool) => bool)
  1.3305 +      (%p::'a => bool.
  1.3306 +          (op -->::bool => bool => bool)
  1.3307 +           ((indep::((nat => bool) => 'a * (nat => bool)) => bool) f)
  1.3308 +           ((measurable::((nat => bool) => bool) => bool)
  1.3309 +             ((op o::('a => bool)
  1.3310 +                     => ((nat => bool) => 'a) => (nat => bool) => bool)
  1.3311 +               p ((op o::('a * (nat => bool) => 'a)
  1.3312 +                         => ((nat => bool) => 'a * (nat => bool))
  1.3313 +                            => (nat => bool) => 'a)
  1.3314 +                   (fst::'a * (nat => bool) => 'a) f)))))"
  1.3315 +  by (import prob_indep INDEP_MEASURABLE1)
  1.3316 +
  1.3317 +lemma INDEP_MEASURABLE2: "(All::(((nat => bool) => 'a * (nat => bool)) => bool) => bool)
  1.3318 + (%f::(nat => bool) => 'a * (nat => bool).
  1.3319 +     (All::(((nat => bool) => bool) => bool) => bool)
  1.3320 +      (%q::(nat => bool) => bool.
  1.3321 +          (op -->::bool => bool => bool)
  1.3322 +           ((op &::bool => bool => bool)
  1.3323 +             ((indep::((nat => bool) => 'a * (nat => bool)) => bool) f)
  1.3324 +             ((measurable::((nat => bool) => bool) => bool) q))
  1.3325 +           ((measurable::((nat => bool) => bool) => bool)
  1.3326 +             ((op o::((nat => bool) => bool)
  1.3327 +                     => ((nat => bool) => nat => bool)
  1.3328 +                        => (nat => bool) => bool)
  1.3329 +               q ((op o::('a * (nat => bool) => nat => bool)
  1.3330 +                         => ((nat => bool) => 'a * (nat => bool))
  1.3331 +                            => (nat => bool) => nat => bool)
  1.3332 +                   (snd::'a * (nat => bool) => nat => bool) f)))))"
  1.3333 +  by (import prob_indep INDEP_MEASURABLE2)
  1.3334 +
  1.3335 +lemma PROB_INDEP_BOUND: "(All::(((nat => bool) => nat * (nat => bool)) => bool) => bool)
  1.3336 + (%f::(nat => bool) => nat * (nat => bool).
  1.3337 +     (All::(nat => bool) => bool)
  1.3338 +      (%n::nat.
  1.3339 +          (op -->::bool => bool => bool)
  1.3340 +           ((indep::((nat => bool) => nat * (nat => bool)) => bool) f)
  1.3341 +           ((op =::real => real => bool)
  1.3342 +             ((prob::((nat => bool) => bool) => real)
  1.3343 +               (%s::nat => bool.
  1.3344 +                   (op <::nat => nat => bool)
  1.3345 +                    ((fst::nat * (nat => bool) => nat) (f s))
  1.3346 +                    ((Suc::nat => nat) n)))
  1.3347 +             ((op +::real => real => real)
  1.3348 +               ((prob::((nat => bool) => bool) => real)
  1.3349 +                 (%s::nat => bool.
  1.3350 +                     (op <::nat => nat => bool)
  1.3351 +                      ((fst::nat * (nat => bool) => nat) (f s)) n))
  1.3352 +               ((prob::((nat => bool) => bool) => real)
  1.3353 +                 (%s::nat => bool.
  1.3354 +                     (op =::nat => nat => bool)
  1.3355 +                      ((fst::nat * (nat => bool) => nat) (f s)) n))))))"
  1.3356 +  by (import prob_indep PROB_INDEP_BOUND)
  1.3357 +
  1.3358 +;end_setup
  1.3359 +
  1.3360 +;setup_theory prob_uniform
  1.3361 +
  1.3362 +consts
  1.3363 +  unif_bound :: "nat => nat" 
  1.3364 +
  1.3365 +defs
  1.3366 +  unif_bound_primdef: "unif_bound ==
  1.3367 +WFREC (SOME R. WF R & (ALL v. R (Suc v div 2) (Suc v)))
  1.3368 + (%unif_bound. nat_case 0 (%v1. Suc (unif_bound (Suc v1 div 2))))"
  1.3369 +
  1.3370 +lemma unif_bound_primitive_def: "unif_bound =
  1.3371 +WFREC (SOME R. WF R & (ALL v. R (Suc v div 2) (Suc v)))
  1.3372 + (%unif_bound. nat_case 0 (%v1. Suc (unif_bound (Suc v1 div 2))))"
  1.3373 +  by (import prob_uniform unif_bound_primitive_def)
  1.3374 +
  1.3375 +lemma unif_bound_def: "unif_bound 0 = 0 & unif_bound (Suc v) = Suc (unif_bound (Suc v div 2))"
  1.3376 +  by (import prob_uniform unif_bound_def)
  1.3377 +
  1.3378 +lemma unif_bound_ind: "(All::((nat => bool) => bool) => bool)
  1.3379 + (%P::nat => bool.
  1.3380 +     (op -->::bool => bool => bool)
  1.3381 +      ((op &::bool => bool => bool) (P (0::nat))
  1.3382 +        ((All::(nat => bool) => bool)
  1.3383 +          (%v::nat.
  1.3384 +              (op -->::bool => bool => bool)
  1.3385 +               (P ((op div::nat => nat => nat) ((Suc::nat => nat) v)
  1.3386 +                    ((number_of::bin => nat)
  1.3387 +                      ((op BIT::bin => bool => bin)
  1.3388 +                        ((op BIT::bin => bool => bin) (bin.Pls::bin)
  1.3389 +                          (True::bool))
  1.3390 +                        (False::bool)))))
  1.3391 +               (P ((Suc::nat => nat) v)))))
  1.3392 +      ((All::(nat => bool) => bool) P))"
  1.3393 +  by (import prob_uniform unif_bound_ind)
  1.3394 +
  1.3395 +constdefs
  1.3396 +  unif_tupled :: "nat * (nat => bool) => nat * (nat => bool)" 
  1.3397 +  "unif_tupled ==
  1.3398 +WFREC (SOME R. WF R & (ALL s v2. R (Suc v2 div 2, s) (Suc v2, s)))
  1.3399 + (%unif_tupled (v, v1).
  1.3400 +     case v of 0 => (0, v1)
  1.3401 +     | Suc v3 =>
  1.3402 +         let (m, s') = unif_tupled (Suc v3 div 2, v1)
  1.3403 +         in (if SHD s' then 2 * m + 1 else 2 * m, STL s'))"
  1.3404 +
  1.3405 +lemma unif_tupled_primitive_def: "unif_tupled =
  1.3406 +WFREC (SOME R. WF R & (ALL s v2. R (Suc v2 div 2, s) (Suc v2, s)))
  1.3407 + (%unif_tupled (v, v1).
  1.3408 +     case v of 0 => (0, v1)
  1.3409 +     | Suc v3 =>
  1.3410 +         let (m, s') = unif_tupled (Suc v3 div 2, v1)
  1.3411 +         in (if SHD s' then 2 * m + 1 else 2 * m, STL s'))"
  1.3412 +  by (import prob_uniform unif_tupled_primitive_def)
  1.3413 +
  1.3414 +consts
  1.3415 +  unif :: "nat => (nat => bool) => nat * (nat => bool)" 
  1.3416 +
  1.3417 +defs
  1.3418 +  unif_primdef: "unif == %x x1. unif_tupled (x, x1)"
  1.3419 +
  1.3420 +lemma unif_curried_def: "ALL x x1. unif x x1 = unif_tupled (x, x1)"
  1.3421 +  by (import prob_uniform unif_curried_def)
  1.3422 +
  1.3423 +lemma unif_def: "unif 0 s = (0, s) &
  1.3424 +unif (Suc v2) s =
  1.3425 +(let (m, s') = unif (Suc v2 div 2) s
  1.3426 + in (if SHD s' then 2 * m + 1 else 2 * m, STL s'))"
  1.3427 +  by (import prob_uniform unif_def)
  1.3428 +
  1.3429 +lemma unif_ind: "(All::((nat => (nat => bool) => bool) => bool) => bool)
  1.3430 + (%P::nat => (nat => bool) => bool.
  1.3431 +     (op -->::bool => bool => bool)
  1.3432 +      ((op &::bool => bool => bool)
  1.3433 +        ((All::((nat => bool) => bool) => bool) (P (0::nat)))
  1.3434 +        ((All::(nat => bool) => bool)
  1.3435 +          (%v2::nat.
  1.3436 +              (All::((nat => bool) => bool) => bool)
  1.3437 +               (%s::nat => bool.
  1.3438 +                   (op -->::bool => bool => bool)
  1.3439 +                    (P ((op div::nat => nat => nat) ((Suc::nat => nat) v2)
  1.3440 +                         ((number_of::bin => nat)
  1.3441 +                           ((op BIT::bin => bool => bin)
  1.3442 +                             ((op BIT::bin => bool => bin) (bin.Pls::bin)
  1.3443 +                               (True::bool))
  1.3444 +                             (False::bool))))
  1.3445 +                      s)
  1.3446 +                    (P ((Suc::nat => nat) v2) s)))))
  1.3447 +      ((All::(nat => bool) => bool)
  1.3448 +        (%v::nat. (All::((nat => bool) => bool) => bool) (P v))))"
  1.3449 +  by (import prob_uniform unif_ind)
  1.3450 +
  1.3451 +constdefs
  1.3452 +  uniform_tupled :: "nat * nat * (nat => bool) => nat * (nat => bool)" 
  1.3453 +  "(op ==::(nat * nat * (nat => bool) => nat * (nat => bool))
  1.3454 +        => (nat * nat * (nat => bool) => nat * (nat => bool)) => prop)
  1.3455 + (uniform_tupled::nat * nat * (nat => bool) => nat * (nat => bool))
  1.3456 + ((WFREC::(nat * nat * (nat => bool) => nat * nat * (nat => bool) => bool)
  1.3457 +          => ((nat * nat * (nat => bool) => nat * (nat => bool))
  1.3458 +              => nat * nat * (nat => bool) => nat * (nat => bool))
  1.3459 +             => nat * nat * (nat => bool) => nat * (nat => bool))
  1.3460 +   ((Eps::((nat * nat * (nat => bool) => nat * nat * (nat => bool) => bool)
  1.3461 +           => bool)
  1.3462 +          => nat * nat * (nat => bool) => nat * nat * (nat => bool) => bool)
  1.3463 +     (%R::nat * nat * (nat => bool) => nat * nat * (nat => bool) => bool.
  1.3464 +         (op &::bool => bool => bool)
  1.3465 +          ((WF::(nat * nat * (nat => bool)
  1.3466 +                 => nat * nat * (nat => bool) => bool)
  1.3467 +                => bool)
  1.3468 +            R)
  1.3469 +          ((All::(nat => bool) => bool)
  1.3470 +            (%t::nat.
  1.3471 +                (All::((nat => bool) => bool) => bool)
  1.3472 +                 (%s::nat => bool.
  1.3473 +                     (All::(nat => bool) => bool)
  1.3474 +                      (%n::nat.
  1.3475 +                          (All::(nat => bool) => bool)
  1.3476 +                           (%res::nat.
  1.3477 +                               (All::((nat => bool) => bool) => bool)
  1.3478 +                                (%s'::nat => bool.
  1.3479 +                                    (op -->::bool => bool => bool)
  1.3480 +                                     ((op &::bool => bool => bool)
  1.3481 + ((op =::nat * (nat => bool) => nat * (nat => bool) => bool)
  1.3482 +   ((Pair::nat => (nat => bool) => nat * (nat => bool)) res s')
  1.3483 +   ((unif::nat => (nat => bool) => nat * (nat => bool)) n s))
  1.3484 + ((Not::bool => bool)
  1.3485 +   ((op <::nat => nat => bool) res ((Suc::nat => nat) n))))
  1.3486 +                                     (R
  1.3487 + ((Pair::nat => nat * (nat => bool) => nat * nat * (nat => bool)) t
  1.3488 +   ((Pair::nat => (nat => bool) => nat * (nat => bool))
  1.3489 +     ((Suc::nat => nat) n) s'))
  1.3490 + ((Pair::nat => nat * (nat => bool) => nat * nat * (nat => bool))
  1.3491 +   ((Suc::nat => nat) t)
  1.3492 +   ((Pair::nat => (nat => bool) => nat * (nat => bool))
  1.3493 +     ((Suc::nat => nat) n) s)))))))))))
  1.3494 +   (%uniform_tupled::nat * nat * (nat => bool) => nat * (nat => bool).
  1.3495 +       (split::(nat => nat * (nat => bool) => nat * (nat => bool))
  1.3496 +               => nat * nat * (nat => bool) => nat * (nat => bool))
  1.3497 +        (%(v::nat) v1::nat * (nat => bool).
  1.3498 +            (nat_case::nat * (nat => bool)
  1.3499 +                       => (nat => nat * (nat => bool))
  1.3500 +                          => nat => nat * (nat => bool))
  1.3501 +             ((split::(nat => (nat => bool) => nat * (nat => bool))
  1.3502 +                      => nat * (nat => bool) => nat * (nat => bool))
  1.3503 +               (%(v3::nat) v4::nat => bool.
  1.3504 +                   (nat_case::nat * (nat => bool)
  1.3505 +                              => (nat => nat * (nat => bool))
  1.3506 +                                 => nat => nat * (nat => bool))
  1.3507 +                    (ARB::nat * (nat => bool))
  1.3508 +                    (%v5::nat.
  1.3509 +                        (Pair::nat => (nat => bool) => nat * (nat => bool))
  1.3510 +                         (0::nat) v4)
  1.3511 +                    v3)
  1.3512 +               v1)
  1.3513 +             (%v2::nat.
  1.3514 +                 (split::(nat => (nat => bool) => nat * (nat => bool))
  1.3515 +                         => nat * (nat => bool) => nat * (nat => bool))
  1.3516 +                  (%(v7::nat) v8::nat => bool.
  1.3517 +                      (nat_case::nat * (nat => bool)
  1.3518 +                                 => (nat => nat * (nat => bool))
  1.3519 +                                    => nat => nat * (nat => bool))
  1.3520 +                       (ARB::nat * (nat => bool))
  1.3521 +                       (%v9::nat.
  1.3522 +                           (Let::nat * (nat => bool)
  1.3523 +                                 => (nat * (nat => bool)
  1.3524 +                                     => nat * (nat => bool))
  1.3525 +                                    => nat * (nat => bool))
  1.3526 +                            ((unif::nat
  1.3527 +                                    => (nat => bool) => nat * (nat => bool))
  1.3528 +                              v9 v8)
  1.3529 +                            ((split::(nat
  1.3530 +=> (nat => bool) => nat * (nat => bool))
  1.3531 +                                     => nat * (nat => bool)
  1.3532 +  => nat * (nat => bool))
  1.3533 +                              (%(res::nat) s'::nat => bool.
  1.3534 +                                  (If::bool
  1.3535 + => nat * (nat => bool) => nat * (nat => bool) => nat * (nat => bool))
  1.3536 +                                   ((op <::nat => nat => bool) res
  1.3537 +                                     ((Suc::nat => nat) v9))
  1.3538 +                                   ((Pair::nat
  1.3539 +     => (nat => bool) => nat * (nat => bool))
  1.3540 +                                     res s')
  1.3541 +                                   (uniform_tupled
  1.3542 +                                     ((Pair::nat
  1.3543 +       => nat * (nat => bool) => nat * nat * (nat => bool))
  1.3544 + v2 ((Pair::nat => (nat => bool) => nat * (nat => bool))
  1.3545 +      ((Suc::nat => nat) v9) s'))))))
  1.3546 +                       v7)
  1.3547 +                  v1)
  1.3548 +             v)))"
  1.3549 +
  1.3550 +lemma uniform_tupled_primitive_def: "(op =::(nat * nat * (nat => bool) => nat * (nat => bool))
  1.3551 +       => (nat * nat * (nat => bool) => nat * (nat => bool)) => bool)
  1.3552 + (uniform_tupled::nat * nat * (nat => bool) => nat * (nat => bool))
  1.3553 + ((WFREC::(nat * nat * (nat => bool) => nat * nat * (nat => bool) => bool)
  1.3554 +          => ((nat * nat * (nat => bool) => nat * (nat => bool))
  1.3555 +              => nat * nat * (nat => bool) => nat * (nat => bool))
  1.3556 +             => nat * nat * (nat => bool) => nat * (nat => bool))
  1.3557 +   ((Eps::((nat * nat * (nat => bool) => nat * nat * (nat => bool) => bool)
  1.3558 +           => bool)
  1.3559 +          => nat * nat * (nat => bool) => nat * nat * (nat => bool) => bool)
  1.3560 +     (%R::nat * nat * (nat => bool) => nat * nat * (nat => bool) => bool.
  1.3561 +         (op &::bool => bool => bool)
  1.3562 +          ((WF::(nat * nat * (nat => bool)
  1.3563 +                 => nat * nat * (nat => bool) => bool)
  1.3564 +                => bool)
  1.3565 +            R)
  1.3566 +          ((All::(nat => bool) => bool)
  1.3567 +            (%t::nat.
  1.3568 +                (All::((nat => bool) => bool) => bool)
  1.3569 +                 (%s::nat => bool.
  1.3570 +                     (All::(nat => bool) => bool)
  1.3571 +                      (%n::nat.
  1.3572 +                          (All::(nat => bool) => bool)
  1.3573 +                           (%res::nat.
  1.3574 +                               (All::((nat => bool) => bool) => bool)
  1.3575 +                                (%s'::nat => bool.
  1.3576 +                                    (op -->::bool => bool => bool)
  1.3577 +                                     ((op &::bool => bool => bool)
  1.3578 + ((op =::nat * (nat => bool) => nat * (nat => bool) => bool)
  1.3579 +   ((Pair::nat => (nat => bool) => nat * (nat => bool)) res s')
  1.3580 +   ((unif::nat => (nat => bool) => nat * (nat => bool)) n s))
  1.3581 + ((Not::bool => bool)
  1.3582 +   ((op <::nat => nat => bool) res ((Suc::nat => nat) n))))
  1.3583 +                                     (R
  1.3584 + ((Pair::nat => nat * (nat => bool) => nat * nat * (nat => bool)) t
  1.3585 +   ((Pair::nat => (nat => bool) => nat * (nat => bool))
  1.3586 +     ((Suc::nat => nat) n) s'))
  1.3587 + ((Pair::nat => nat * (nat => bool) => nat * nat * (nat => bool))
  1.3588 +   ((Suc::nat => nat) t)
  1.3589 +   ((Pair::nat => (nat => bool) => nat * (nat => bool))
  1.3590 +     ((Suc::nat => nat) n) s)))))))))))
  1.3591 +   (%uniform_tupled::nat * nat * (nat => bool) => nat * (nat => bool).
  1.3592 +       (split::(nat => nat * (nat => bool) => nat * (nat => bool))
  1.3593 +               => nat * nat * (nat => bool) => nat * (nat => bool))
  1.3594 +        (%(v::nat) v1::nat * (nat => bool).
  1.3595 +            (nat_case::nat * (nat => bool)
  1.3596 +                       => (nat => nat * (nat => bool))
  1.3597 +                          => nat => nat * (nat => bool))
  1.3598 +             ((split::(nat => (nat => bool) => nat * (nat => bool))
  1.3599 +                      => nat * (nat => bool) => nat * (nat => bool))
  1.3600 +               (%(v3::nat) v4::nat => bool.
  1.3601 +                   (nat_case::nat * (nat => bool)
  1.3602 +                              => (nat => nat * (nat => bool))
  1.3603 +                                 => nat => nat * (nat => bool))
  1.3604 +                    (ARB::nat * (nat => bool))
  1.3605 +                    (%v5::nat.
  1.3606 +                        (Pair::nat => (nat => bool) => nat * (nat => bool))
  1.3607 +                         (0::nat) v4)
  1.3608 +                    v3)
  1.3609 +               v1)
  1.3610 +             (%v2::nat.
  1.3611 +                 (split::(nat => (nat => bool) => nat * (nat => bool))
  1.3612 +                         => nat * (nat => bool) => nat * (nat => bool))
  1.3613 +                  (%(v7::nat) v8::nat => bool.
  1.3614 +                      (nat_case::nat * (nat => bool)
  1.3615 +                                 => (nat => nat * (nat => bool))
  1.3616 +                                    => nat => nat * (nat => bool))
  1.3617 +                       (ARB::nat * (nat => bool))
  1.3618 +                       (%v9::nat.
  1.3619 +                           (Let::nat * (nat => bool)
  1.3620 +                                 => (nat * (nat => bool)
  1.3621 +                                     => nat * (nat => bool))
  1.3622 +                                    => nat * (nat => bool))
  1.3623 +                            ((unif::nat
  1.3624 +                                    => (nat => bool) => nat * (nat => bool))
  1.3625 +                              v9 v8)
  1.3626 +                            ((split::(nat
  1.3627 +=> (nat => bool) => nat * (nat => bool))
  1.3628 +                                     => nat * (nat => bool)
  1.3629 +  => nat * (nat => bool))
  1.3630 +                              (%(res::nat) s'::nat => bool.
  1.3631 +                                  (If::bool
  1.3632 + => nat * (nat => bool) => nat * (nat => bool) => nat * (nat => bool))
  1.3633 +                                   ((op <::nat => nat => bool) res
  1.3634 +                                     ((Suc::nat => nat) v9))
  1.3635 +                                   ((Pair::nat
  1.3636 +     => (nat => bool) => nat * (nat => bool))
  1.3637 +                                     res s')
  1.3638 +                                   (uniform_tupled
  1.3639 +                                     ((Pair::nat
  1.3640 +       => nat * (nat => bool) => nat * nat * (nat => bool))
  1.3641 + v2 ((Pair::nat => (nat => bool) => nat * (nat => bool))
  1.3642 +      ((Suc::nat => nat) v9) s'))))))
  1.3643 +                       v7)
  1.3644 +                  v1)
  1.3645 +             v)))"
  1.3646 +  by (import prob_uniform uniform_tupled_primitive_def)
  1.3647 +
  1.3648 +consts
  1.3649 +  uniform :: "nat => nat => (nat => bool) => nat * (nat => bool)" 
  1.3650 +
  1.3651 +defs
  1.3652 +  uniform_primdef: "uniform == %x x1 x2. uniform_tupled (x, x1, x2)"
  1.3653 +
  1.3654 +lemma uniform_curried_def: "ALL x x1 x2. uniform x x1 x2 = uniform_tupled (x, x1, x2)"
  1.3655 +  by (import prob_uniform uniform_curried_def)
  1.3656 +
  1.3657 +lemma uniform_ind: "(All::((nat => nat => (nat => bool) => bool) => bool) => bool)
  1.3658 + (%P::nat => nat => (nat => bool) => bool.
  1.3659 +     (op -->::bool => bool => bool)
  1.3660 +      ((op &::bool => bool => bool)
  1.3661 +        ((All::(nat => bool) => bool)
  1.3662 +          (%x::nat.
  1.3663 +              (All::((nat => bool) => bool) => bool)
  1.3664 +               (P ((Suc::nat => nat) x) (0::nat))))
  1.3665 +        ((op &::bool => bool => bool)
  1.3666 +          ((All::((nat => bool) => bool) => bool) (P (0::nat) (0::nat)))
  1.3667 +          ((op &::bool => bool => bool)
  1.3668 +            ((All::(nat => bool) => bool)
  1.3669 +              (%x::nat.
  1.3670 +                  (All::((nat => bool) => bool) => bool)
  1.3671 +                   (P (0::nat) ((Suc::nat => nat) x))))
  1.3672 +            ((All::(nat => bool) => bool)
  1.3673 +              (%x::nat.
  1.3674 +                  (All::(nat => bool) => bool)
  1.3675 +                   (%xa::nat.
  1.3676 +                       (All::((nat => bool) => bool) => bool)
  1.3677 +                        (%xb::nat => bool.
  1.3678 +                            (op -->::bool => bool => bool)
  1.3679 +                             ((All::(nat => bool) => bool)
  1.3680 +                               (%xc::nat.
  1.3681 +                                   (All::((nat => bool) => bool) => bool)
  1.3682 +                                    (%xd::nat => bool.
  1.3683 +  (op -->::bool => bool => bool)
  1.3684 +   ((op &::bool => bool => bool)
  1.3685 +     ((op =::nat * (nat => bool) => nat * (nat => bool) => bool)
  1.3686 +       ((Pair::nat => (nat => bool) => nat * (nat => bool)) xc xd)
  1.3687 +       ((unif::nat => (nat => bool) => nat * (nat => bool)) xa xb))
  1.3688 +     ((Not::bool => bool)
  1.3689 +       ((op <::nat => nat => bool) xc ((Suc::nat => nat) xa))))
  1.3690 +   (P x ((Suc::nat => nat) xa) xd))))
  1.3691 +                             (P ((Suc::nat => nat) x) ((Suc::nat => nat) xa)
  1.3692 +                               xb))))))))
  1.3693 +      ((All::(nat => bool) => bool)
  1.3694 +        (%x::nat.
  1.3695 +            (All::(nat => bool) => bool)
  1.3696 +             (%xa::nat. (All::((nat => bool) => bool) => bool) (P x xa)))))"
  1.3697 +  by (import prob_uniform uniform_ind)
  1.3698 +
  1.3699 +lemma uniform_def: "uniform 0 (Suc n) s = (0, s) &
  1.3700 +uniform (Suc t) (Suc n) s =
  1.3701 +(let (xa, x) = unif n s
  1.3702 + in if xa < Suc n then (xa, x) else uniform t (Suc n) x)"
  1.3703 +  by (import prob_uniform uniform_def)
  1.3704 +
  1.3705 +lemma SUC_DIV_TWO_ZERO: "ALL n. (Suc n div 2 = 0) = (n = 0)"
  1.3706 +  by (import prob_uniform SUC_DIV_TWO_ZERO)
  1.3707 +
  1.3708 +lemma UNIF_BOUND_LOWER: "ALL n. n < 2 ^ unif_bound n"
  1.3709 +  by (import prob_uniform UNIF_BOUND_LOWER)
  1.3710 +
  1.3711 +lemma UNIF_BOUND_LOWER_SUC: "ALL n. Suc n <= 2 ^ unif_bound n"
  1.3712 +  by (import prob_uniform UNIF_BOUND_LOWER_SUC)
  1.3713 +
  1.3714 +lemma UNIF_BOUND_UPPER: "(All::(nat => bool) => bool)
  1.3715 + (%n::nat.
  1.3716 +     (op -->::bool => bool => bool)
  1.3717 +      ((Not::bool => bool) ((op =::nat => nat => bool) n (0::nat)))
  1.3718 +      ((op <=::nat => nat => bool)
  1.3719 +        ((op ^::nat => nat => nat)
  1.3720 +          ((number_of::bin => nat)
  1.3721 +            ((op BIT::bin => bool => bin)
  1.3722 +              ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
  1.3723 +              (False::bool)))
  1.3724 +          ((unif_bound::nat => nat) n))
  1.3725 +        ((op *::nat => nat => nat)
  1.3726 +          ((number_of::bin => nat)
  1.3727 +            ((op BIT::bin => bool => bin)
  1.3728 +              ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
  1.3729 +              (False::bool)))
  1.3730 +          n)))"
  1.3731 +  by (import prob_uniform UNIF_BOUND_UPPER)
  1.3732 +
  1.3733 +lemma UNIF_BOUND_UPPER_SUC: "ALL n. 2 ^ unif_bound n <= Suc (2 * n)"
  1.3734 +  by (import prob_uniform UNIF_BOUND_UPPER_SUC)
  1.3735 +
  1.3736 +lemma UNIF_DEF_MONAD: "unif 0 = UNIT 0 &
  1.3737 +(ALL n.
  1.3738 +    unif (Suc n) =
  1.3739 +    BIND (unif (Suc n div 2))
  1.3740 +     (%m. BIND SDEST (%b. UNIT (if b then 2 * m + 1 else 2 * m))))"
  1.3741 +  by (import prob_uniform UNIF_DEF_MONAD)
  1.3742 +
  1.3743 +lemma UNIFORM_DEF_MONAD: "(ALL x. uniform 0 (Suc x) = UNIT 0) &
  1.3744 +(ALL x xa.
  1.3745 +    uniform (Suc x) (Suc xa) =
  1.3746 +    BIND (unif xa) (%m. if m < Suc xa then UNIT m else uniform x (Suc xa)))"
  1.3747 +  by (import prob_uniform UNIFORM_DEF_MONAD)
  1.3748 +
  1.3749 +lemma INDEP_UNIF: "ALL n. indep (unif n)"
  1.3750 +  by (import prob_uniform INDEP_UNIF)
  1.3751 +
  1.3752 +lemma INDEP_UNIFORM: "ALL t n. indep (uniform t (Suc n))"
  1.3753 +  by (import prob_uniform INDEP_UNIFORM)
  1.3754 +
  1.3755 +lemma PROB_UNIF: "ALL n k.
  1.3756 +   prob (%s. fst (unif n s) = k) =
  1.3757 +   (if k < 2 ^ unif_bound n then (1 / 2) ^ unif_bound n else 0)"
  1.3758 +  by (import prob_uniform PROB_UNIF)
  1.3759 +
  1.3760 +lemma UNIF_RANGE: "ALL n s. fst (unif n s) < 2 ^ unif_bound n"
  1.3761 +  by (import prob_uniform UNIF_RANGE)
  1.3762 +
  1.3763 +lemma PROB_UNIF_PAIR: "ALL n k k'.
  1.3764 +   (prob (%s. fst (unif n s) = k) = prob (%s. fst (unif n s) = k')) =
  1.3765 +   ((k < 2 ^ unif_bound n) = (k' < 2 ^ unif_bound n))"
  1.3766 +  by (import prob_uniform PROB_UNIF_PAIR)
  1.3767 +
  1.3768 +lemma PROB_UNIF_BOUND: "(All::(nat => bool) => bool)
  1.3769 + (%n::nat.
  1.3770 +     (All::(nat => bool) => bool)
  1.3771 +      (%k::nat.
  1.3772 +          (op -->::bool => bool => bool)
  1.3773 +           ((op <=::nat => nat => bool) k
  1.3774 +             ((op ^::nat => nat => nat)
  1.3775 +               ((number_of::bin => nat)
  1.3776 +                 ((op BIT::bin => bool => bin)
  1.3777 +                   ((op BIT::bin => bool => bin) (bin.Pls::bin)
  1.3778 +                     (True::bool))
  1.3779 +                   (False::bool)))
  1.3780 +               ((unif_bound::nat => nat) n)))
  1.3781 +           ((op =::real => real => bool)
  1.3782 +             ((prob::((nat => bool) => bool) => real)
  1.3783 +               (%s::nat => bool.
  1.3784 +                   (op <::nat => nat => bool)
  1.3785 +                    ((fst::nat * (nat => bool) => nat)
  1.3786 +                      ((unif::nat => (nat => bool) => nat * (nat => bool)) n
  1.3787 +                        s))
  1.3788 +                    k))
  1.3789 +             ((op *::real => real => real) ((real::nat => real) k)
  1.3790 +               ((op ^::real => nat => real)
  1.3791 +                 ((op /::real => real => real) (1::real)
  1.3792 +                   ((number_of::bin => real)
  1.3793 +                     ((op BIT::bin => bool => bin)
  1.3794 +                       ((op BIT::bin => bool => bin) (bin.Pls::bin)
  1.3795 +                         (True::bool))
  1.3796 +                       (False::bool))))
  1.3797 +                 ((unif_bound::nat => nat) n))))))"
  1.3798 +  by (import prob_uniform PROB_UNIF_BOUND)
  1.3799 +
  1.3800 +lemma PROB_UNIF_GOOD: "ALL n. 1 / 2 <= prob (%s. fst (unif n s) < Suc n)"
  1.3801 +  by (import prob_uniform PROB_UNIF_GOOD)
  1.3802 +
  1.3803 +lemma UNIFORM_RANGE: "ALL t n s. fst (uniform t (Suc n) s) < Suc n"
  1.3804 +  by (import prob_uniform UNIFORM_RANGE)
  1.3805 +
  1.3806 +lemma PROB_UNIFORM_LOWER_BOUND: "(All::(real => bool) => bool)
  1.3807 + (%b::real.
  1.3808 +     (op -->::bool => bool => bool)
  1.3809 +      ((All::(nat => bool) => bool)
  1.3810 +        (%k::nat.
  1.3811 +            (op -->::bool => bool => bool)
  1.3812 +             ((op <::nat => nat => bool) k ((Suc::nat => nat) (n::nat)))
  1.3813 +             ((op <::real => real => bool)
  1.3814 +               ((prob::((nat => bool) => bool) => real)
  1.3815 +                 (%s::nat => bool.
  1.3816 +                     (op =::nat => nat => bool)
  1.3817 +                      ((fst::nat * (nat => bool) => nat)
  1.3818 +                        ((uniform::nat
  1.3819 +                                   => nat
  1.3820 +=> (nat => bool) => nat * (nat => bool))
  1.3821 +                          (t::nat) ((Suc::nat => nat) n) s))
  1.3822 +                      k))
  1.3823 +               b)))
  1.3824 +      ((All::(nat => bool) => bool)
  1.3825 +        (%m::nat.
  1.3826 +            (op -->::bool => bool => bool)
  1.3827 +             ((op <::nat => nat => bool) m ((Suc::nat => nat) n))
  1.3828 +             ((op <::real => real => bool)
  1.3829 +               ((prob::((nat => bool) => bool) => real)
  1.3830 +                 (%s::nat => bool.
  1.3831 +                     (op <::nat => nat => bool)
  1.3832 +                      ((fst::nat * (nat => bool) => nat)
  1.3833 +                        ((uniform::nat
  1.3834 +                                   => nat
  1.3835 +=> (nat => bool) => nat * (nat => bool))
  1.3836 +                          t ((Suc::nat => nat) n) s))
  1.3837 +                      ((Suc::nat => nat) m)))
  1.3838 +               ((op *::real => real => real)
  1.3839 +                 ((real::nat => real) ((Suc::nat => nat) m)) b)))))"
  1.3840 +  by (import prob_uniform PROB_UNIFORM_LOWER_BOUND)
  1.3841 +
  1.3842 +lemma PROB_UNIFORM_UPPER_BOUND: "(All::(real => bool) => bool)
  1.3843 + (%b::real.
  1.3844 +     (op -->::bool => bool => bool)
  1.3845 +      ((All::(nat => bool) => bool)
  1.3846 +        (%k::nat.
  1.3847 +            (op -->::bool => bool => bool)
  1.3848 +             ((op <::nat => nat => bool) k ((Suc::nat => nat) (n::nat)))
  1.3849 +             ((op <::real => real => bool) b
  1.3850 +               ((prob::((nat => bool) => bool) => real)
  1.3851 +                 (%s::nat => bool.
  1.3852 +                     (op =::nat => nat => bool)
  1.3853 +                      ((fst::nat * (nat => bool) => nat)
  1.3854 +                        ((uniform::nat
  1.3855 +                                   => nat
  1.3856 +=> (nat => bool) => nat * (nat => bool))
  1.3857 +                          (t::nat) ((Suc::nat => nat) n) s))
  1.3858 +                      k)))))
  1.3859 +      ((All::(nat => bool) => bool)
  1.3860 +        (%m::nat.
  1.3861 +            (op -->::bool => bool => bool)
  1.3862 +             ((op <::nat => nat => bool) m ((Suc::nat => nat) n))
  1.3863 +             ((op <::real => real => bool)
  1.3864 +               ((op *::real => real => real)
  1.3865 +                 ((real::nat => real) ((Suc::nat => nat) m)) b)
  1.3866 +               ((prob::((nat => bool) => bool) => real)
  1.3867 +                 (%s::nat => bool.
  1.3868 +                     (op <::nat => nat => bool)
  1.3869 +                      ((fst::nat * (nat => bool) => nat)
  1.3870 +                        ((uniform::nat
  1.3871 +                                   => nat
  1.3872 +=> (nat => bool) => nat * (nat => bool))
  1.3873 +                          t ((Suc::nat => nat) n) s))
  1.3874 +                      ((Suc::nat => nat) m)))))))"
  1.3875 +  by (import prob_uniform PROB_UNIFORM_UPPER_BOUND)
  1.3876 +
  1.3877 +lemma PROB_UNIFORM_PAIR_SUC: "(All::(nat => bool) => bool)
  1.3878 + (%t::nat.
  1.3879 +     (All::(nat => bool) => bool)
  1.3880 +      (%n::nat.
  1.3881 +          (All::(nat => bool) => bool)
  1.3882 +           (%k::nat.
  1.3883 +               (All::(nat => bool) => bool)
  1.3884 +                (%k'::nat.
  1.3885 +                    (op -->::bool => bool => bool)
  1.3886 +                     ((op &::bool => bool => bool)
  1.3887 +                       ((op <::nat => nat => bool) k ((Suc::nat => nat) n))
  1.3888 +                       ((op <::nat => nat => bool) k'
  1.3889 +                         ((Suc::nat => nat) n)))
  1.3890 +                     ((op <=::real => real => bool)
  1.3891 +                       ((abs::real => real)
  1.3892 +                         ((op -::real => real => real)
  1.3893 +                           ((prob::((nat => bool) => bool) => real)
  1.3894 +                             (%s::nat => bool.
  1.3895 +                                 (op =::nat => nat => bool)
  1.3896 +                                  ((fst::nat * (nat => bool) => nat)
  1.3897 +                                    ((uniform::nat
  1.3898 +         => nat => (nat => bool) => nat * (nat => bool))
  1.3899 +t ((Suc::nat => nat) n) s))
  1.3900 +                                  k))
  1.3901 +                           ((prob::((nat => bool) => bool) => real)
  1.3902 +                             (%s::nat => bool.
  1.3903 +                                 (op =::nat => nat => bool)
  1.3904 +                                  ((fst::nat * (nat => bool) => nat)
  1.3905 +                                    ((uniform::nat
  1.3906 +         => nat => (nat => bool) => nat * (nat => bool))
  1.3907 +t ((Suc::nat => nat) n) s))
  1.3908 +                                  k'))))
  1.3909 +                       ((op ^::real => nat => real)
  1.3910 +                         ((op /::real => real => real) (1::real)
  1.3911 +                           ((number_of::bin => real)
  1.3912 +                             ((op BIT::bin => bool => bin)
  1.3913 +                               ((op BIT::bin => bool => bin) (bin.Pls::bin)
  1.3914 +                                 (True::bool))
  1.3915 +                               (False::bool))))
  1.3916 +                         t))))))"
  1.3917 +  by (import prob_uniform PROB_UNIFORM_PAIR_SUC)
  1.3918 +
  1.3919 +lemma PROB_UNIFORM_SUC: "(All::(nat => bool) => bool)
  1.3920 + (%t::nat.
  1.3921 +     (All::(nat => bool) => bool)
  1.3922 +      (%n::nat.
  1.3923 +          (All::(nat => bool) => bool)
  1.3924 +           (%k::nat.
  1.3925 +               (op -->::bool => bool => bool)
  1.3926 +                ((op <::nat => nat => bool) k ((Suc::nat => nat) n))
  1.3927 +                ((op <=::real => real => bool)
  1.3928 +                  ((abs::real => real)
  1.3929 +                    ((op -::real => real => real)
  1.3930 +                      ((prob::((nat => bool) => bool) => real)
  1.3931 +                        (%s::nat => bool.
  1.3932 +                            (op =::nat => nat => bool)
  1.3933 +                             ((fst::nat * (nat => bool) => nat)
  1.3934 +                               ((uniform::nat
  1.3935 +    => nat => (nat => bool) => nat * (nat => bool))
  1.3936 +                                 t ((Suc::nat => nat) n) s))
  1.3937 +                             k))
  1.3938 +                      ((op /::real => real => real) (1::real)
  1.3939 +                        ((real::nat => real) ((Suc::nat => nat) n)))))
  1.3940 +                  ((op ^::real => nat => real)
  1.3941 +                    ((op /::real => real => real) (1::real)
  1.3942 +                      ((number_of::bin => real)
  1.3943 +                        ((op BIT::bin => bool => bin)
  1.3944 +                          ((op BIT::bin => bool => bin) (bin.Pls::bin)
  1.3945 +                            (True::bool))
  1.3946 +                          (False::bool))))
  1.3947 +                    t)))))"
  1.3948 +  by (import prob_uniform PROB_UNIFORM_SUC)
  1.3949 +
  1.3950 +lemma PROB_UNIFORM: "(All::(nat => bool) => bool)
  1.3951 + (%t::nat.
  1.3952 +     (All::(nat => bool) => bool)
  1.3953 +      (%n::nat.
  1.3954 +          (All::(nat => bool) => bool)
  1.3955 +           (%k::nat.
  1.3956 +               (op -->::bool => bool => bool)
  1.3957 +                ((op <::nat => nat => bool) k n)
  1.3958 +                ((op <=::real => real => bool)
  1.3959 +                  ((abs::real => real)
  1.3960 +                    ((op -::real => real => real)
  1.3961 +                      ((prob::((nat => bool) => bool) => real)
  1.3962 +                        (%s::nat => bool.
  1.3963 +                            (op =::nat => nat => bool)
  1.3964 +                             ((fst::nat * (nat => bool) => nat)
  1.3965 +                               ((uniform::nat
  1.3966 +    => nat => (nat => bool) => nat * (nat => bool))
  1.3967 +                                 t n s))
  1.3968 +                             k))
  1.3969 +                      ((op /::real => real => real) (1::real)
  1.3970 +                        ((real::nat => real) n))))
  1.3971 +                  ((op ^::real => nat => real)
  1.3972 +                    ((op /::real => real => real) (1::real)
  1.3973 +                      ((number_of::bin => real)
  1.3974 +                        ((op BIT::bin => bool => bin)
  1.3975 +                          ((op BIT::bin => bool => bin) (bin.Pls::bin)
  1.3976 +                            (True::bool))
  1.3977 +                          (False::bool))))
  1.3978 +                    t)))))"
  1.3979 +  by (import prob_uniform PROB_UNIFORM)
  1.3980 +
  1.3981 +;end_setup
  1.3982 +
  1.3983 +end
  1.3984 +