src/HOL/Import/HOL/HOL4Prob.thy
 author paulson Thu Jul 01 12:29:53 2004 +0200 (2004-07-01) changeset 15013 34264f5e4691 parent 14516 a183dec876ab child 15071 b65fc0787fbe permissions -rw-r--r--
new treatment of binary numerals
```     1 theory HOL4Prob = HOL4Real:
```
```     2
```
```     3 ;setup_theory prob_extra
```
```     4
```
```     5 lemma BOOL_BOOL_CASES_THM: "ALL f. f = (%b. False) | f = (%b. True) | f = (%b. b) | f = Not"
```
```     6   by (import prob_extra BOOL_BOOL_CASES_THM)
```
```     7
```
```     8 lemma EVEN_ODD_BASIC: "EVEN 0 & ~ EVEN 1 & EVEN 2 & ~ ODD 0 & ODD 1 & ~ ODD 2"
```
```     9   by (import prob_extra EVEN_ODD_BASIC)
```
```    10
```
```    11 lemma EVEN_ODD_EXISTS_EQ: "ALL n. EVEN n = (EX m. n = 2 * m) & ODD n = (EX m. n = Suc (2 * m))"
```
```    12   by (import prob_extra EVEN_ODD_EXISTS_EQ)
```
```    13
```
```    14 lemma DIV_THEN_MULT: "ALL p q. Suc q * (p div Suc q) <= p"
```
```    15   by (import prob_extra DIV_THEN_MULT)
```
```    16
```
```    17 lemma DIV_TWO_UNIQUE: "(All::(nat => bool) => bool)
```
```    18  (%n::nat.
```
```    19      (All::(nat => bool) => bool)
```
```    20       (%q::nat.
```
```    21           (All::(nat => bool) => bool)
```
```    22            (%r::nat.
```
```    23                (op -->::bool => bool => bool)
```
```    24                 ((op &::bool => bool => bool)
```
```    25                   ((op =::nat => nat => bool) n
```
```    26                     ((op +::nat => nat => nat)
```
```    27                       ((op *::nat => nat => nat)
```
```    28                         ((number_of::bin => nat)
```
```    29                           ((op BIT::bin => bool => bin)
```
```    30                             ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
```
```    31                               (True::bool))
```
```    32                             (False::bool)))
```
```    33                         q)
```
```    34                       r))
```
```    35                   ((op |::bool => bool => bool)
```
```    36                     ((op =::nat => nat => bool) r (0::nat))
```
```    37                     ((op =::nat => nat => bool) r (1::nat))))
```
```    38                 ((op &::bool => bool => bool)
```
```    39                   ((op =::nat => nat => bool) q
```
```    40                     ((op div::nat => nat => nat) n
```
```    41                       ((number_of::bin => nat)
```
```    42                         ((op BIT::bin => bool => bin)
```
```    43                           ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
```
```    44                             (True::bool))
```
```    45                           (False::bool)))))
```
```    46                   ((op =::nat => nat => bool) r
```
```    47                     ((op mod::nat => nat => nat) n
```
```    48                       ((number_of::bin => nat)
```
```    49                         ((op BIT::bin => bool => bin)
```
```    50                           ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
```
```    51                             (True::bool))
```
```    52                           (False::bool)))))))))"
```
```    53   by (import prob_extra DIV_TWO_UNIQUE)
```
```    54
```
```    55 lemma DIVISION_TWO: "ALL n::nat.
```
```    56    n = (2::nat) * (n div (2::nat)) + n mod (2::nat) &
```
```    57    (n mod (2::nat) = (0::nat) | n mod (2::nat) = (1::nat))"
```
```    58   by (import prob_extra DIVISION_TWO)
```
```    59
```
```    60 lemma DIV_TWO: "ALL n::nat. n = (2::nat) * (n div (2::nat)) + n mod (2::nat)"
```
```    61   by (import prob_extra DIV_TWO)
```
```    62
```
```    63 lemma MOD_TWO: "ALL n. n mod 2 = (if EVEN n then 0 else 1)"
```
```    64   by (import prob_extra MOD_TWO)
```
```    65
```
```    66 lemma DIV_TWO_BASIC: "(0::nat) div (2::nat) = (0::nat) &
```
```    67 (1::nat) div (2::nat) = (0::nat) & (2::nat) div (2::nat) = (1::nat)"
```
```    68   by (import prob_extra DIV_TWO_BASIC)
```
```    69
```
```    70 lemma DIV_TWO_MONO: "(All::(nat => bool) => bool)
```
```    71  (%m::nat.
```
```    72      (All::(nat => bool) => bool)
```
```    73       (%n::nat.
```
```    74           (op -->::bool => bool => bool)
```
```    75            ((op <::nat => nat => bool)
```
```    76              ((op div::nat => nat => nat) m
```
```    77                ((number_of::bin => nat)
```
```    78                  ((op BIT::bin => bool => bin)
```
```    79                    ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
```
```    80                      (True::bool))
```
```    81                    (False::bool))))
```
```    82              ((op div::nat => nat => nat) n
```
```    83                ((number_of::bin => nat)
```
```    84                  ((op BIT::bin => bool => bin)
```
```    85                    ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
```
```    86                      (True::bool))
```
```    87                    (False::bool)))))
```
```    88            ((op <::nat => nat => bool) m n)))"
```
```    89   by (import prob_extra DIV_TWO_MONO)
```
```    90
```
```    91 lemma DIV_TWO_MONO_EVEN: "(All::(nat => bool) => bool)
```
```    92  (%m::nat.
```
```    93      (All::(nat => bool) => bool)
```
```    94       (%n::nat.
```
```    95           (op -->::bool => bool => bool) ((EVEN::nat => bool) n)
```
```    96            ((op =::bool => bool => bool)
```
```    97              ((op <::nat => nat => bool)
```
```    98                ((op div::nat => nat => nat) m
```
```    99                  ((number_of::bin => nat)
```
```   100                    ((op BIT::bin => bool => bin)
```
```   101                      ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
```
```   102                        (True::bool))
```
```   103                      (False::bool))))
```
```   104                ((op div::nat => nat => nat) n
```
```   105                  ((number_of::bin => nat)
```
```   106                    ((op BIT::bin => bool => bin)
```
```   107                      ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
```
```   108                        (True::bool))
```
```   109                      (False::bool)))))
```
```   110              ((op <::nat => nat => bool) m n))))"
```
```   111   by (import prob_extra DIV_TWO_MONO_EVEN)
```
```   112
```
```   113 lemma DIV_TWO_CANCEL: "ALL n. 2 * n div 2 = n & Suc (2 * n) div 2 = n"
```
```   114   by (import prob_extra DIV_TWO_CANCEL)
```
```   115
```
```   116 lemma EXP_DIV_TWO: "ALL n::nat. (2::nat) ^ Suc n div (2::nat) = (2::nat) ^ n"
```
```   117   by (import prob_extra EXP_DIV_TWO)
```
```   118
```
```   119 lemma EVEN_EXP_TWO: "ALL n. EVEN (2 ^ n) = (n ~= 0)"
```
```   120   by (import prob_extra EVEN_EXP_TWO)
```
```   121
```
```   122 lemma DIV_TWO_EXP: "ALL (n::nat) k::nat.
```
```   123    (k div (2::nat) < (2::nat) ^ n) = (k < (2::nat) ^ Suc n)"
```
```   124   by (import prob_extra DIV_TWO_EXP)
```
```   125
```
```   126 consts
```
```   127   inf :: "(real => bool) => real"
```
```   128
```
```   129 defs
```
```   130   inf_primdef: "inf == %P. - sup (IMAGE uminus P)"
```
```   131
```
```   132 lemma inf_def: "ALL P. inf P = - sup (IMAGE uminus P)"
```
```   133   by (import prob_extra inf_def)
```
```   134
```
```   135 lemma INF_DEF_ALT: "ALL P. inf P = - sup (%r. P (- r))"
```
```   136   by (import prob_extra INF_DEF_ALT)
```
```   137
```
```   138 lemma REAL_SUP_EXISTS_UNIQUE: "(All::((real => bool) => bool) => bool)
```
```   139  (%P::real => bool.
```
```   140      (op -->::bool => bool => bool)
```
```   141       ((op &::bool => bool => bool) ((Ex::(real => bool) => bool) P)
```
```   142         ((Ex::(real => bool) => bool)
```
```   143           (%z::real.
```
```   144               (All::(real => bool) => bool)
```
```   145                (%x::real.
```
```   146                    (op -->::bool => bool => bool) (P x)
```
```   147                     ((op <=::real => real => bool) x z)))))
```
```   148       ((Ex1::(real => bool) => bool)
```
```   149         (%s::real.
```
```   150             (All::(real => bool) => bool)
```
```   151              (%y::real.
```
```   152                  (op =::bool => bool => bool)
```
```   153                   ((Ex::(real => bool) => bool)
```
```   154                     (%x::real.
```
```   155                         (op &::bool => bool => bool) (P x)
```
```   156                          ((op <::real => real => bool) y x)))
```
```   157                   ((op <::real => real => bool) y s)))))"
```
```   158   by (import prob_extra REAL_SUP_EXISTS_UNIQUE)
```
```   159
```
```   160 lemma REAL_SUP_MAX: "(All::((real => bool) => bool) => bool)
```
```   161  (%P::real => bool.
```
```   162      (All::(real => bool) => bool)
```
```   163       (%z::real.
```
```   164           (op -->::bool => bool => bool)
```
```   165            ((op &::bool => bool => bool) (P z)
```
```   166              ((All::(real => bool) => bool)
```
```   167                (%x::real.
```
```   168                    (op -->::bool => bool => bool) (P x)
```
```   169                     ((op <=::real => real => bool) x z))))
```
```   170            ((op =::real => real => bool) ((sup::(real => bool) => real) P)
```
```   171              z)))"
```
```   172   by (import prob_extra REAL_SUP_MAX)
```
```   173
```
```   174 lemma REAL_INF_MIN: "(All::((real => bool) => bool) => bool)
```
```   175  (%P::real => bool.
```
```   176      (All::(real => bool) => bool)
```
```   177       (%z::real.
```
```   178           (op -->::bool => bool => bool)
```
```   179            ((op &::bool => bool => bool) (P z)
```
```   180              ((All::(real => bool) => bool)
```
```   181                (%x::real.
```
```   182                    (op -->::bool => bool => bool) (P x)
```
```   183                     ((op <=::real => real => bool) z x))))
```
```   184            ((op =::real => real => bool) ((inf::(real => bool) => real) P)
```
```   185              z)))"
```
```   186   by (import prob_extra REAL_INF_MIN)
```
```   187
```
```   188 lemma HALF_POS: "(0::real) < (1::real) / (2::real)"
```
```   189   by (import prob_extra HALF_POS)
```
```   190
```
```   191 lemma HALF_CANCEL: "(2::real) * ((1::real) / (2::real)) = (1::real)"
```
```   192   by (import prob_extra HALF_CANCEL)
```
```   193
```
```   194 lemma POW_HALF_POS: "ALL n::nat. (0::real) < ((1::real) / (2::real)) ^ n"
```
```   195   by (import prob_extra POW_HALF_POS)
```
```   196
```
```   197 lemma POW_HALF_MONO: "(All::(nat => bool) => bool)
```
```   198  (%m::nat.
```
```   199      (All::(nat => bool) => bool)
```
```   200       (%n::nat.
```
```   201           (op -->::bool => bool => bool) ((op <=::nat => nat => bool) m n)
```
```   202            ((op <=::real => real => bool)
```
```   203              ((op ^::real => nat => real)
```
```   204                ((op /::real => real => real) (1::real)
```
```   205                  ((number_of::bin => real)
```
```   206                    ((op BIT::bin => bool => bin)
```
```   207                      ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
```
```   208                        (True::bool))
```
```   209                      (False::bool))))
```
```   210                n)
```
```   211              ((op ^::real => nat => real)
```
```   212                ((op /::real => real => real) (1::real)
```
```   213                  ((number_of::bin => real)
```
```   214                    ((op BIT::bin => bool => bin)
```
```   215                      ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
```
```   216                        (True::bool))
```
```   217                      (False::bool))))
```
```   218                m))))"
```
```   219   by (import prob_extra POW_HALF_MONO)
```
```   220
```
```   221 lemma POW_HALF_TWICE: "ALL n::nat.
```
```   222    ((1::real) / (2::real)) ^ n = (2::real) * ((1::real) / (2::real)) ^ Suc n"
```
```   223   by (import prob_extra POW_HALF_TWICE)
```
```   224
```
```   225 lemma X_HALF_HALF: "ALL x::real. (1::real) / (2::real) * x + (1::real) / (2::real) * x = x"
```
```   226   by (import prob_extra X_HALF_HALF)
```
```   227
```
```   228 lemma REAL_SUP_LE_X: "(All::((real => bool) => bool) => bool)
```
```   229  (%P::real => bool.
```
```   230      (All::(real => bool) => bool)
```
```   231       (%x::real.
```
```   232           (op -->::bool => bool => bool)
```
```   233            ((op &::bool => bool => bool) ((Ex::(real => bool) => bool) P)
```
```   234              ((All::(real => bool) => bool)
```
```   235                (%r::real.
```
```   236                    (op -->::bool => bool => bool) (P r)
```
```   237                     ((op <=::real => real => bool) r x))))
```
```   238            ((op <=::real => real => bool) ((sup::(real => bool) => real) P)
```
```   239              x)))"
```
```   240   by (import prob_extra REAL_SUP_LE_X)
```
```   241
```
```   242 lemma REAL_X_LE_SUP: "(All::((real => bool) => bool) => bool)
```
```   243  (%P::real => bool.
```
```   244      (All::(real => bool) => bool)
```
```   245       (%x::real.
```
```   246           (op -->::bool => bool => bool)
```
```   247            ((op &::bool => bool => bool) ((Ex::(real => bool) => bool) P)
```
```   248              ((op &::bool => bool => bool)
```
```   249                ((Ex::(real => bool) => bool)
```
```   250                  (%z::real.
```
```   251                      (All::(real => bool) => bool)
```
```   252                       (%r::real.
```
```   253                           (op -->::bool => bool => bool) (P r)
```
```   254                            ((op <=::real => real => bool) r z))))
```
```   255                ((Ex::(real => bool) => bool)
```
```   256                  (%r::real.
```
```   257                      (op &::bool => bool => bool) (P r)
```
```   258                       ((op <=::real => real => bool) x r)))))
```
```   259            ((op <=::real => real => bool) x
```
```   260              ((sup::(real => bool) => real) P))))"
```
```   261   by (import prob_extra REAL_X_LE_SUP)
```
```   262
```
```   263 lemma ABS_BETWEEN_LE: "ALL (x::real) (y::real) d::real.
```
```   264    ((0::real) <= d & x - d <= y & y <= x + d) = (abs (y - x) <= d)"
```
```   265   by (import prob_extra ABS_BETWEEN_LE)
```
```   266
```
```   267 lemma ONE_MINUS_HALF: "(1::real) - (1::real) / (2::real) = (1::real) / (2::real)"
```
```   268   by (import prob_extra ONE_MINUS_HALF)
```
```   269
```
```   270 lemma HALF_LT_1: "(1::real) / (2::real) < (1::real)"
```
```   271   by (import prob_extra HALF_LT_1)
```
```   272
```
```   273 lemma POW_HALF_EXP: "ALL n::nat. ((1::real) / (2::real)) ^ n = inverse (real ((2::nat) ^ n))"
```
```   274   by (import prob_extra POW_HALF_EXP)
```
```   275
```
```   276 lemma INV_SUC_POS: "ALL n. 0 < 1 / real (Suc n)"
```
```   277   by (import prob_extra INV_SUC_POS)
```
```   278
```
```   279 lemma INV_SUC_MAX: "ALL x. 1 / real (Suc x) <= 1"
```
```   280   by (import prob_extra INV_SUC_MAX)
```
```   281
```
```   282 lemma INV_SUC: "ALL n. 0 < 1 / real (Suc n) & 1 / real (Suc n) <= 1"
```
```   283   by (import prob_extra INV_SUC)
```
```   284
```
```   285 lemma ABS_UNIT_INTERVAL: "(All::(real => bool) => bool)
```
```   286  (%x::real.
```
```   287      (All::(real => bool) => bool)
```
```   288       (%y::real.
```
```   289           (op -->::bool => bool => bool)
```
```   290            ((op &::bool => bool => bool)
```
```   291              ((op <=::real => real => bool) (0::real) x)
```
```   292              ((op &::bool => bool => bool)
```
```   293                ((op <=::real => real => bool) x (1::real))
```
```   294                ((op &::bool => bool => bool)
```
```   295                  ((op <=::real => real => bool) (0::real) y)
```
```   296                  ((op <=::real => real => bool) y (1::real)))))
```
```   297            ((op <=::real => real => bool)
```
```   298              ((abs::real => real) ((op -::real => real => real) x y))
```
```   299              (1::real))))"
```
```   300   by (import prob_extra ABS_UNIT_INTERVAL)
```
```   301
```
```   302 lemma MEM_NIL: "ALL l. (ALL x. ~ x mem l) = (l = [])"
```
```   303   by (import prob_extra MEM_NIL)
```
```   304
```
```   305 lemma MAP_MEM: "ALL f l x. x mem map f l = (EX y. y mem l & x = f y)"
```
```   306   by (import prob_extra MAP_MEM)
```
```   307
```
```   308 lemma MEM_NIL_MAP_CONS: "ALL x l. ~ [] mem map (op # x) l"
```
```   309   by (import prob_extra MEM_NIL_MAP_CONS)
```
```   310
```
```   311 lemma FILTER_TRUE: "ALL l. [x:l. True] = l"
```
```   312   by (import prob_extra FILTER_TRUE)
```
```   313
```
```   314 lemma FILTER_FALSE: "ALL l. [x:l. False] = []"
```
```   315   by (import prob_extra FILTER_FALSE)
```
```   316
```
```   317 lemma FILTER_MEM: "(All::(('a => bool) => bool) => bool)
```
```   318  (%P::'a => bool.
```
```   319      (All::('a => bool) => bool)
```
```   320       (%x::'a.
```
```   321           (All::('a list => bool) => bool)
```
```   322            (%l::'a list.
```
```   323                (op -->::bool => bool => bool)
```
```   324                 ((op mem::'a => 'a list => bool) x
```
```   325                   ((filter::('a => bool) => 'a list => 'a list) P l))
```
```   326                 (P x))))"
```
```   327   by (import prob_extra FILTER_MEM)
```
```   328
```
```   329 lemma MEM_FILTER: "(All::(('a => bool) => bool) => bool)
```
```   330  (%P::'a => bool.
```
```   331      (All::('a list => bool) => bool)
```
```   332       (%l::'a list.
```
```   333           (All::('a => bool) => bool)
```
```   334            (%x::'a.
```
```   335                (op -->::bool => bool => bool)
```
```   336                 ((op mem::'a => 'a list => bool) x
```
```   337                   ((filter::('a => bool) => 'a list => 'a list) P l))
```
```   338                 ((op mem::'a => 'a list => bool) x l))))"
```
```   339   by (import prob_extra MEM_FILTER)
```
```   340
```
```   341 lemma FILTER_OUT_ELT: "ALL x l. x mem l | [y:l. y ~= x] = l"
```
```   342   by (import prob_extra FILTER_OUT_ELT)
```
```   343
```
```   344 lemma IS_PREFIX_NIL: "ALL x. IS_PREFIX x [] & IS_PREFIX [] x = (x = [])"
```
```   345   by (import prob_extra IS_PREFIX_NIL)
```
```   346
```
```   347 lemma IS_PREFIX_REFL: "ALL x. IS_PREFIX x x"
```
```   348   by (import prob_extra IS_PREFIX_REFL)
```
```   349
```
```   350 lemma IS_PREFIX_ANTISYM: "(All::('a list => bool) => bool)
```
```   351  (%x::'a list.
```
```   352      (All::('a list => bool) => bool)
```
```   353       (%y::'a list.
```
```   354           (op -->::bool => bool => bool)
```
```   355            ((op &::bool => bool => bool)
```
```   356              ((IS_PREFIX::'a list => 'a list => bool) y x)
```
```   357              ((IS_PREFIX::'a list => 'a list => bool) x y))
```
```   358            ((op =::'a list => 'a list => bool) x y)))"
```
```   359   by (import prob_extra IS_PREFIX_ANTISYM)
```
```   360
```
```   361 lemma IS_PREFIX_TRANS: "(All::('a list => bool) => bool)
```
```   362  (%x::'a list.
```
```   363      (All::('a list => bool) => bool)
```
```   364       (%y::'a list.
```
```   365           (All::('a list => bool) => bool)
```
```   366            (%z::'a list.
```
```   367                (op -->::bool => bool => bool)
```
```   368                 ((op &::bool => bool => bool)
```
```   369                   ((IS_PREFIX::'a list => 'a list => bool) x y)
```
```   370                   ((IS_PREFIX::'a list => 'a list => bool) y z))
```
```   371                 ((IS_PREFIX::'a list => 'a list => bool) x z))))"
```
```   372   by (import prob_extra IS_PREFIX_TRANS)
```
```   373
```
```   374 lemma IS_PREFIX_BUTLAST: "ALL x y. IS_PREFIX (x # y) (butlast (x # y))"
```
```   375   by (import prob_extra IS_PREFIX_BUTLAST)
```
```   376
```
```   377 lemma IS_PREFIX_LENGTH: "(All::('a list => bool) => bool)
```
```   378  (%x::'a list.
```
```   379      (All::('a list => bool) => bool)
```
```   380       (%y::'a list.
```
```   381           (op -->::bool => bool => bool)
```
```   382            ((IS_PREFIX::'a list => 'a list => bool) y x)
```
```   383            ((op <=::nat => nat => bool) ((size::'a list => nat) x)
```
```   384              ((size::'a list => nat) y))))"
```
```   385   by (import prob_extra IS_PREFIX_LENGTH)
```
```   386
```
```   387 lemma IS_PREFIX_LENGTH_ANTI: "(All::('a list => bool) => bool)
```
```   388  (%x::'a list.
```
```   389      (All::('a list => bool) => bool)
```
```   390       (%y::'a list.
```
```   391           (op -->::bool => bool => bool)
```
```   392            ((op &::bool => bool => bool)
```
```   393              ((IS_PREFIX::'a list => 'a list => bool) y x)
```
```   394              ((op =::nat => nat => bool) ((size::'a list => nat) x)
```
```   395                ((size::'a list => nat) y)))
```
```   396            ((op =::'a list => 'a list => bool) x y)))"
```
```   397   by (import prob_extra IS_PREFIX_LENGTH_ANTI)
```
```   398
```
```   399 lemma IS_PREFIX_SNOC: "ALL x y z. IS_PREFIX (SNOC x y) z = (IS_PREFIX y z | z = SNOC x y)"
```
```   400   by (import prob_extra IS_PREFIX_SNOC)
```
```   401
```
```   402 lemma FOLDR_MAP: "ALL (f::'b => 'c => 'c) (e::'c) (g::'a => 'b) l::'a list.
```
```   403    foldr f (map g l) e = foldr (%x::'a. f (g x)) l e"
```
```   404   by (import prob_extra FOLDR_MAP)
```
```   405
```
```   406 lemma LAST_MEM: "ALL h t. last (h # t) mem h # t"
```
```   407   by (import prob_extra LAST_MEM)
```
```   408
```
```   409 lemma LAST_MAP_CONS: "ALL (b::bool) (h::bool list) t::bool list list.
```
```   410    EX x::bool list. last (map (op # b) (h # t)) = b # x"
```
```   411   by (import prob_extra LAST_MAP_CONS)
```
```   412
```
```   413 lemma EXISTS_LONGEST: "(All::('a list => bool) => bool)
```
```   414  (%x::'a list.
```
```   415      (All::('a list list => bool) => bool)
```
```   416       (%y::'a list list.
```
```   417           (Ex::('a list => bool) => bool)
```
```   418            (%z::'a list.
```
```   419                (op &::bool => bool => bool)
```
```   420                 ((op mem::'a list => 'a list list => bool) z
```
```   421                   ((op #::'a list => 'a list list => 'a list list) x y))
```
```   422                 ((All::('a list => bool) => bool)
```
```   423                   (%w::'a list.
```
```   424                       (op -->::bool => bool => bool)
```
```   425                        ((op mem::'a list => 'a list list => bool) w
```
```   426                          ((op #::'a list => 'a list list => 'a list list) x
```
```   427                            y))
```
```   428                        ((op <=::nat => nat => bool)
```
```   429                          ((size::'a list => nat) w)
```
```   430                          ((size::'a list => nat) z)))))))"
```
```   431   by (import prob_extra EXISTS_LONGEST)
```
```   432
```
```   433 lemma UNION_DEF_ALT: "ALL s t. pred_set.UNION s t = (%x. s x | t x)"
```
```   434   by (import prob_extra UNION_DEF_ALT)
```
```   435
```
```   436 lemma INTER_UNION_RDISTRIB: "ALL p q r.
```
```   437    pred_set.INTER (pred_set.UNION p q) r =
```
```   438    pred_set.UNION (pred_set.INTER p r) (pred_set.INTER q r)"
```
```   439   by (import prob_extra INTER_UNION_RDISTRIB)
```
```   440
```
```   441 lemma SUBSET_EQ: "ALL x xa. (x = xa) = (SUBSET x xa & SUBSET xa x)"
```
```   442   by (import prob_extra SUBSET_EQ)
```
```   443
```
```   444 lemma INTER_IS_EMPTY: "ALL s t. (pred_set.INTER s t = EMPTY) = (ALL x. ~ s x | ~ t x)"
```
```   445   by (import prob_extra INTER_IS_EMPTY)
```
```   446
```
```   447 lemma UNION_DISJOINT_SPLIT: "(All::(('a => bool) => bool) => bool)
```
```   448  (%s::'a => bool.
```
```   449      (All::(('a => bool) => bool) => bool)
```
```   450       (%t::'a => bool.
```
```   451           (All::(('a => bool) => bool) => bool)
```
```   452            (%u::'a => bool.
```
```   453                (op -->::bool => bool => bool)
```
```   454                 ((op &::bool => bool => bool)
```
```   455                   ((op =::('a => bool) => ('a => bool) => bool)
```
```   456                     ((pred_set.UNION::('a => bool)
```
```   457 => ('a => bool) => 'a => bool)
```
```   458                       s t)
```
```   459                     ((pred_set.UNION::('a => bool)
```
```   460 => ('a => bool) => 'a => bool)
```
```   461                       s u))
```
```   462                   ((op &::bool => bool => bool)
```
```   463                     ((op =::('a => bool) => ('a => bool) => bool)
```
```   464                       ((pred_set.INTER::('a => bool)
```
```   465   => ('a => bool) => 'a => bool)
```
```   466                         s t)
```
```   467                       (EMPTY::'a => bool))
```
```   468                     ((op =::('a => bool) => ('a => bool) => bool)
```
```   469                       ((pred_set.INTER::('a => bool)
```
```   470   => ('a => bool) => 'a => bool)
```
```   471                         s u)
```
```   472                       (EMPTY::'a => bool))))
```
```   473                 ((op =::('a => bool) => ('a => bool) => bool) t u))))"
```
```   474   by (import prob_extra UNION_DISJOINT_SPLIT)
```
```   475
```
```   476 lemma GSPEC_DEF_ALT: "ALL f. GSPEC f = (%v. EX x. (v, True) = f x)"
```
```   477   by (import prob_extra GSPEC_DEF_ALT)
```
```   478
```
```   479 ;end_setup
```
```   480
```
```   481 ;setup_theory prob_canon
```
```   482
```
```   483 consts
```
```   484   alg_twin :: "bool list => bool list => bool"
```
```   485
```
```   486 defs
```
```   487   alg_twin_primdef: "alg_twin == %x y. EX l. x = SNOC True l & y = SNOC False l"
```
```   488
```
```   489 lemma alg_twin_def: "ALL x y. alg_twin x y = (EX l. x = SNOC True l & y = SNOC False l)"
```
```   490   by (import prob_canon alg_twin_def)
```
```   491
```
```   492 constdefs
```
```   493   alg_order_tupled :: "bool list * bool list => bool"
```
```   494   "(op ==::(bool list * bool list => bool)
```
```   495         => (bool list * bool list => bool) => prop)
```
```   496  (alg_order_tupled::bool list * bool list => bool)
```
```   497  ((WFREC::(bool list * bool list => bool list * bool list => bool)
```
```   498           => ((bool list * bool list => bool)
```
```   499               => bool list * bool list => bool)
```
```   500              => bool list * bool list => bool)
```
```   501    ((Eps::((bool list * bool list => bool list * bool list => bool) => bool)
```
```   502           => bool list * bool list => bool list * bool list => bool)
```
```   503      (%R::bool list * bool list => bool list * bool list => bool.
```
```   504          (op &::bool => bool => bool)
```
```   505           ((WF::(bool list * bool list => bool list * bool list => bool)
```
```   506                 => bool)
```
```   507             R)
```
```   508           ((All::(bool => bool) => bool)
```
```   509             (%h'::bool.
```
```   510                 (All::(bool => bool) => bool)
```
```   511                  (%h::bool.
```
```   512                      (All::(bool list => bool) => bool)
```
```   513                       (%t'::bool list.
```
```   514                           (All::(bool list => bool) => bool)
```
```   515                            (%t::bool list.
```
```   516                                R ((Pair::bool list
```
```   517    => bool list => bool list * bool list)
```
```   518                                    t t')
```
```   519                                 ((Pair::bool list
```
```   520   => bool list => bool list * bool list)
```
```   521                                   ((op #::bool => bool list => bool list) h
```
```   522                                     t)
```
```   523                                   ((op #::bool => bool list => bool list) h'
```
```   524                                     t')))))))))
```
```   525    (%alg_order_tupled::bool list * bool list => bool.
```
```   526        (split::(bool list => bool list => bool)
```
```   527                => bool list * bool list => bool)
```
```   528         (%(v::bool list) v1::bool list.
```
```   529             (list_case::bool
```
```   530                         => (bool => bool list => bool) => bool list => bool)
```
```   531              ((list_case::bool
```
```   532                           => (bool => bool list => bool)
```
```   533                              => bool list => bool)
```
```   534                (True::bool) (%(v8::bool) v9::bool list. True::bool) v1)
```
```   535              (%(v4::bool) v5::bool list.
```
```   536                  (list_case::bool
```
```   537                              => (bool => bool list => bool)
```
```   538                                 => bool list => bool)
```
```   539                   (False::bool)
```
```   540                   (%(v10::bool) v11::bool list.
```
```   541                       (op |::bool => bool => bool)
```
```   542                        ((op &::bool => bool => bool)
```
```   543                          ((op =::bool => bool => bool) v4 (True::bool))
```
```   544                          ((op =::bool => bool => bool) v10 (False::bool)))
```
```   545                        ((op &::bool => bool => bool)
```
```   546                          ((op =::bool => bool => bool) v4 v10)
```
```   547                          (alg_order_tupled
```
```   548                            ((Pair::bool list
```
```   549                                    => bool list => bool list * bool list)
```
```   550                              v5 v11))))
```
```   551                   v1)
```
```   552              v)))"
```
```   553
```
```   554 lemma alg_order_tupled_primitive_def: "(op =::(bool list * bool list => bool)
```
```   555        => (bool list * bool list => bool) => bool)
```
```   556  (alg_order_tupled::bool list * bool list => bool)
```
```   557  ((WFREC::(bool list * bool list => bool list * bool list => bool)
```
```   558           => ((bool list * bool list => bool)
```
```   559               => bool list * bool list => bool)
```
```   560              => bool list * bool list => bool)
```
```   561    ((Eps::((bool list * bool list => bool list * bool list => bool) => bool)
```
```   562           => bool list * bool list => bool list * bool list => bool)
```
```   563      (%R::bool list * bool list => bool list * bool list => bool.
```
```   564          (op &::bool => bool => bool)
```
```   565           ((WF::(bool list * bool list => bool list * bool list => bool)
```
```   566                 => bool)
```
```   567             R)
```
```   568           ((All::(bool => bool) => bool)
```
```   569             (%h'::bool.
```
```   570                 (All::(bool => bool) => bool)
```
```   571                  (%h::bool.
```
```   572                      (All::(bool list => bool) => bool)
```
```   573                       (%t'::bool list.
```
```   574                           (All::(bool list => bool) => bool)
```
```   575                            (%t::bool list.
```
```   576                                R ((Pair::bool list
```
```   577    => bool list => bool list * bool list)
```
```   578                                    t t')
```
```   579                                 ((Pair::bool list
```
```   580   => bool list => bool list * bool list)
```
```   581                                   ((op #::bool => bool list => bool list) h
```
```   582                                     t)
```
```   583                                   ((op #::bool => bool list => bool list) h'
```
```   584                                     t')))))))))
```
```   585    (%alg_order_tupled::bool list * bool list => bool.
```
```   586        (split::(bool list => bool list => bool)
```
```   587                => bool list * bool list => bool)
```
```   588         (%(v::bool list) v1::bool list.
```
```   589             (list_case::bool
```
```   590                         => (bool => bool list => bool) => bool list => bool)
```
```   591              ((list_case::bool
```
```   592                           => (bool => bool list => bool)
```
```   593                              => bool list => bool)
```
```   594                (True::bool) (%(v8::bool) v9::bool list. True::bool) v1)
```
```   595              (%(v4::bool) v5::bool list.
```
```   596                  (list_case::bool
```
```   597                              => (bool => bool list => bool)
```
```   598                                 => bool list => bool)
```
```   599                   (False::bool)
```
```   600                   (%(v10::bool) v11::bool list.
```
```   601                       (op |::bool => bool => bool)
```
```   602                        ((op &::bool => bool => bool)
```
```   603                          ((op =::bool => bool => bool) v4 (True::bool))
```
```   604                          ((op =::bool => bool => bool) v10 (False::bool)))
```
```   605                        ((op &::bool => bool => bool)
```
```   606                          ((op =::bool => bool => bool) v4 v10)
```
```   607                          (alg_order_tupled
```
```   608                            ((Pair::bool list
```
```   609                                    => bool list => bool list * bool list)
```
```   610                              v5 v11))))
```
```   611                   v1)
```
```   612              v)))"
```
```   613   by (import prob_canon alg_order_tupled_primitive_def)
```
```   614
```
```   615 consts
```
```   616   alg_order :: "bool list => bool list => bool"
```
```   617
```
```   618 defs
```
```   619   alg_order_primdef: "alg_order == %x x1. alg_order_tupled (x, x1)"
```
```   620
```
```   621 lemma alg_order_curried_def: "ALL x x1. alg_order x x1 = alg_order_tupled (x, x1)"
```
```   622   by (import prob_canon alg_order_curried_def)
```
```   623
```
```   624 lemma alg_order_ind: "(All::((bool list => bool list => bool) => bool) => bool)
```
```   625  (%P::bool list => bool list => bool.
```
```   626      (op -->::bool => bool => bool)
```
```   627       ((op &::bool => bool => bool)
```
```   628         ((All::(bool => bool) => bool)
```
```   629           (%x::bool.
```
```   630               (All::(bool list => bool) => bool)
```
```   631                (%xa::bool list.
```
```   632                    P ([]::bool list)
```
```   633                     ((op #::bool => bool list => bool list) x xa))))
```
```   634         ((op &::bool => bool => bool) (P ([]::bool list) ([]::bool list))
```
```   635           ((op &::bool => bool => bool)
```
```   636             ((All::(bool => bool) => bool)
```
```   637               (%x::bool.
```
```   638                   (All::(bool list => bool) => bool)
```
```   639                    (%xa::bool list.
```
```   640                        P ((op #::bool => bool list => bool list) x xa)
```
```   641                         ([]::bool list))))
```
```   642             ((All::(bool => bool) => bool)
```
```   643               (%x::bool.
```
```   644                   (All::(bool list => bool) => bool)
```
```   645                    (%xa::bool list.
```
```   646                        (All::(bool => bool) => bool)
```
```   647                         (%xb::bool.
```
```   648                             (All::(bool list => bool) => bool)
```
```   649                              (%xc::bool list.
```
```   650                                  (op -->::bool => bool => bool) (P xa xc)
```
```   651                                   (P ((op #::bool => bool list => bool list)
```
```   652  x xa)
```
```   653                                     ((op #::bool => bool list => bool list)
```
```   654 xb xc))))))))))
```
```   655       ((All::(bool list => bool) => bool)
```
```   656         (%x::bool list. (All::(bool list => bool) => bool) (P x))))"
```
```   657   by (import prob_canon alg_order_ind)
```
```   658
```
```   659 lemma alg_order_def: "alg_order [] (v6 # v7) = True &
```
```   660 alg_order [] [] = True &
```
```   661 alg_order (v2 # v3) [] = False &
```
```   662 alg_order (h # t) (h' # t') =
```
```   663 (h = True & h' = False | h = h' & alg_order t t')"
```
```   664   by (import prob_canon alg_order_def)
```
```   665
```
```   666 consts
```
```   667   alg_sorted :: "bool list list => bool"
```
```   668
```
```   669 defs
```
```   670   alg_sorted_primdef: "alg_sorted ==
```
```   671 WFREC (SOME R. WF R & (ALL x z y. R (y # z) (x # y # z)))
```
```   672  (%alg_sorted.
```
```   673      list_case True
```
```   674       (%v2. list_case True
```
```   675              (%v6 v7. alg_order v2 v6 & alg_sorted (v6 # v7))))"
```
```   676
```
```   677 lemma alg_sorted_primitive_def: "alg_sorted =
```
```   678 WFREC (SOME R. WF R & (ALL x z y. R (y # z) (x # y # z)))
```
```   679  (%alg_sorted.
```
```   680      list_case True
```
```   681       (%v2. list_case True
```
```   682              (%v6 v7. alg_order v2 v6 & alg_sorted (v6 # v7))))"
```
```   683   by (import prob_canon alg_sorted_primitive_def)
```
```   684
```
```   685 lemma alg_sorted_ind: "(All::((bool list list => bool) => bool) => bool)
```
```   686  (%P::bool list list => bool.
```
```   687      (op -->::bool => bool => bool)
```
```   688       ((op &::bool => bool => bool)
```
```   689         ((All::(bool list => bool) => bool)
```
```   690           (%x::bool list.
```
```   691               (All::(bool list => bool) => bool)
```
```   692                (%y::bool list.
```
```   693                    (All::(bool list list => bool) => bool)
```
```   694                     (%z::bool list list.
```
```   695                         (op -->::bool => bool => bool)
```
```   696                          (P ((op #::bool list
```
```   697                                     => bool list list => bool list list)
```
```   698                               y z))
```
```   699                          (P ((op #::bool list
```
```   700                                     => bool list list => bool list list)
```
```   701                               x ((op #::bool list
```
```   702   => bool list list => bool list list)
```
```   703                                   y z)))))))
```
```   704         ((op &::bool => bool => bool)
```
```   705           ((All::(bool list => bool) => bool)
```
```   706             (%v::bool list.
```
```   707                 P ((op #::bool list => bool list list => bool list list) v
```
```   708                     ([]::bool list list))))
```
```   709           (P ([]::bool list list))))
```
```   710       ((All::(bool list list => bool) => bool) P))"
```
```   711   by (import prob_canon alg_sorted_ind)
```
```   712
```
```   713 lemma alg_sorted_def: "alg_sorted (x # y # z) = (alg_order x y & alg_sorted (y # z)) &
```
```   714 alg_sorted [v] = True & alg_sorted [] = True"
```
```   715   by (import prob_canon alg_sorted_def)
```
```   716
```
```   717 consts
```
```   718   alg_prefixfree :: "bool list list => bool"
```
```   719
```
```   720 defs
```
```   721   alg_prefixfree_primdef: "alg_prefixfree ==
```
```   722 WFREC (SOME R. WF R & (ALL x z y. R (y # z) (x # y # z)))
```
```   723  (%alg_prefixfree.
```
```   724      list_case True
```
```   725       (%v2. list_case True
```
```   726              (%v6 v7. ~ IS_PREFIX v6 v2 & alg_prefixfree (v6 # v7))))"
```
```   727
```
```   728 lemma alg_prefixfree_primitive_def: "alg_prefixfree =
```
```   729 WFREC (SOME R. WF R & (ALL x z y. R (y # z) (x # y # z)))
```
```   730  (%alg_prefixfree.
```
```   731      list_case True
```
```   732       (%v2. list_case True
```
```   733              (%v6 v7. ~ IS_PREFIX v6 v2 & alg_prefixfree (v6 # v7))))"
```
```   734   by (import prob_canon alg_prefixfree_primitive_def)
```
```   735
```
```   736 lemma alg_prefixfree_ind: "(All::((bool list list => bool) => bool) => bool)
```
```   737  (%P::bool list list => bool.
```
```   738      (op -->::bool => bool => bool)
```
```   739       ((op &::bool => bool => bool)
```
```   740         ((All::(bool list => bool) => bool)
```
```   741           (%x::bool list.
```
```   742               (All::(bool list => bool) => bool)
```
```   743                (%y::bool list.
```
```   744                    (All::(bool list list => bool) => bool)
```
```   745                     (%z::bool list list.
```
```   746                         (op -->::bool => bool => bool)
```
```   747                          (P ((op #::bool list
```
```   748                                     => bool list list => bool list list)
```
```   749                               y z))
```
```   750                          (P ((op #::bool list
```
```   751                                     => bool list list => bool list list)
```
```   752                               x ((op #::bool list
```
```   753   => bool list list => bool list list)
```
```   754                                   y z)))))))
```
```   755         ((op &::bool => bool => bool)
```
```   756           ((All::(bool list => bool) => bool)
```
```   757             (%v::bool list.
```
```   758                 P ((op #::bool list => bool list list => bool list list) v
```
```   759                     ([]::bool list list))))
```
```   760           (P ([]::bool list list))))
```
```   761       ((All::(bool list list => bool) => bool) P))"
```
```   762   by (import prob_canon alg_prefixfree_ind)
```
```   763
```
```   764 lemma alg_prefixfree_def: "alg_prefixfree (x # y # z) = (~ IS_PREFIX y x & alg_prefixfree (y # z)) &
```
```   765 alg_prefixfree [v] = True & alg_prefixfree [] = True"
```
```   766   by (import prob_canon alg_prefixfree_def)
```
```   767
```
```   768 consts
```
```   769   alg_twinfree :: "bool list list => bool"
```
```   770
```
```   771 defs
```
```   772   alg_twinfree_primdef: "alg_twinfree ==
```
```   773 WFREC (SOME R. WF R & (ALL x z y. R (y # z) (x # y # z)))
```
```   774  (%alg_twinfree.
```
```   775      list_case True
```
```   776       (%v2. list_case True
```
```   777              (%v6 v7. ~ alg_twin v2 v6 & alg_twinfree (v6 # v7))))"
```
```   778
```
```   779 lemma alg_twinfree_primitive_def: "alg_twinfree =
```
```   780 WFREC (SOME R. WF R & (ALL x z y. R (y # z) (x # y # z)))
```
```   781  (%alg_twinfree.
```
```   782      list_case True
```
```   783       (%v2. list_case True
```
```   784              (%v6 v7. ~ alg_twin v2 v6 & alg_twinfree (v6 # v7))))"
```
```   785   by (import prob_canon alg_twinfree_primitive_def)
```
```   786
```
```   787 lemma alg_twinfree_ind: "(All::((bool list list => bool) => bool) => bool)
```
```   788  (%P::bool list list => bool.
```
```   789      (op -->::bool => bool => bool)
```
```   790       ((op &::bool => bool => bool)
```
```   791         ((All::(bool list => bool) => bool)
```
```   792           (%x::bool list.
```
```   793               (All::(bool list => bool) => bool)
```
```   794                (%y::bool list.
```
```   795                    (All::(bool list list => bool) => bool)
```
```   796                     (%z::bool list list.
```
```   797                         (op -->::bool => bool => bool)
```
```   798                          (P ((op #::bool list
```
```   799                                     => bool list list => bool list list)
```
```   800                               y z))
```
```   801                          (P ((op #::bool list
```
```   802                                     => bool list list => bool list list)
```
```   803                               x ((op #::bool list
```
```   804   => bool list list => bool list list)
```
```   805                                   y z)))))))
```
```   806         ((op &::bool => bool => bool)
```
```   807           ((All::(bool list => bool) => bool)
```
```   808             (%v::bool list.
```
```   809                 P ((op #::bool list => bool list list => bool list list) v
```
```   810                     ([]::bool list list))))
```
```   811           (P ([]::bool list list))))
```
```   812       ((All::(bool list list => bool) => bool) P))"
```
```   813   by (import prob_canon alg_twinfree_ind)
```
```   814
```
```   815 lemma alg_twinfree_def: "alg_twinfree (x # y # z) = (~ alg_twin x y & alg_twinfree (y # z)) &
```
```   816 alg_twinfree [v] = True & alg_twinfree [] = True"
```
```   817   by (import prob_canon alg_twinfree_def)
```
```   818
```
```   819 consts
```
```   820   alg_longest :: "bool list list => nat"
```
```   821
```
```   822 defs
```
```   823   alg_longest_primdef: "alg_longest == FOLDR (%h t. if t <= length h then length h else t) 0"
```
```   824
```
```   825 lemma alg_longest_def: "alg_longest = FOLDR (%h t. if t <= length h then length h else t) 0"
```
```   826   by (import prob_canon alg_longest_def)
```
```   827
```
```   828 consts
```
```   829   alg_canon_prefs :: "bool list => bool list list => bool list list"
```
```   830
```
```   831 specification (alg_canon_prefs_primdef: alg_canon_prefs) alg_canon_prefs_def: "(ALL l. alg_canon_prefs l [] = [l]) &
```
```   832 (ALL l h t.
```
```   833     alg_canon_prefs l (h # t) =
```
```   834     (if IS_PREFIX h l then alg_canon_prefs l t else l # h # t))"
```
```   835   by (import prob_canon alg_canon_prefs_def)
```
```   836
```
```   837 consts
```
```   838   alg_canon_find :: "bool list => bool list list => bool list list"
```
```   839
```
```   840 specification (alg_canon_find_primdef: alg_canon_find) alg_canon_find_def: "(ALL l. alg_canon_find l [] = [l]) &
```
```   841 (ALL l h t.
```
```   842     alg_canon_find l (h # t) =
```
```   843     (if alg_order h l
```
```   844      then if IS_PREFIX l h then h # t else h # alg_canon_find l t
```
```   845      else alg_canon_prefs l (h # t)))"
```
```   846   by (import prob_canon alg_canon_find_def)
```
```   847
```
```   848 consts
```
```   849   alg_canon1 :: "bool list list => bool list list"
```
```   850
```
```   851 defs
```
```   852   alg_canon1_primdef: "alg_canon1 == FOLDR alg_canon_find []"
```
```   853
```
```   854 lemma alg_canon1_def: "alg_canon1 = FOLDR alg_canon_find []"
```
```   855   by (import prob_canon alg_canon1_def)
```
```   856
```
```   857 consts
```
```   858   alg_canon_merge :: "bool list => bool list list => bool list list"
```
```   859
```
```   860 specification (alg_canon_merge_primdef: alg_canon_merge) alg_canon_merge_def: "(ALL l. alg_canon_merge l [] = [l]) &
```
```   861 (ALL l h t.
```
```   862     alg_canon_merge l (h # t) =
```
```   863     (if alg_twin l h then alg_canon_merge (butlast h) t else l # h # t))"
```
```   864   by (import prob_canon alg_canon_merge_def)
```
```   865
```
```   866 consts
```
```   867   alg_canon2 :: "bool list list => bool list list"
```
```   868
```
```   869 defs
```
```   870   alg_canon2_primdef: "alg_canon2 == FOLDR alg_canon_merge []"
```
```   871
```
```   872 lemma alg_canon2_def: "alg_canon2 = FOLDR alg_canon_merge []"
```
```   873   by (import prob_canon alg_canon2_def)
```
```   874
```
```   875 consts
```
```   876   alg_canon :: "bool list list => bool list list"
```
```   877
```
```   878 defs
```
```   879   alg_canon_primdef: "alg_canon == %l. alg_canon2 (alg_canon1 l)"
```
```   880
```
```   881 lemma alg_canon_def: "ALL l. alg_canon l = alg_canon2 (alg_canon1 l)"
```
```   882   by (import prob_canon alg_canon_def)
```
```   883
```
```   884 consts
```
```   885   algebra_canon :: "bool list list => bool"
```
```   886
```
```   887 defs
```
```   888   algebra_canon_primdef: "algebra_canon == %l. alg_canon l = l"
```
```   889
```
```   890 lemma algebra_canon_def: "ALL l. algebra_canon l = (alg_canon l = l)"
```
```   891   by (import prob_canon algebra_canon_def)
```
```   892
```
```   893 lemma ALG_TWIN_NIL: "ALL l. ~ alg_twin l [] & ~ alg_twin [] l"
```
```   894   by (import prob_canon ALG_TWIN_NIL)
```
```   895
```
```   896 lemma ALG_TWIN_SING: "ALL x l.
```
```   897    alg_twin [x] l = (x = True & l = [False]) &
```
```   898    alg_twin l [x] = (l = [True] & x = False)"
```
```   899   by (import prob_canon ALG_TWIN_SING)
```
```   900
```
```   901 lemma ALG_TWIN_CONS: "ALL x y z h t.
```
```   902    alg_twin (x # y # z) (h # t) = (x = h & alg_twin (y # z) t) &
```
```   903    alg_twin (h # t) (x # y # z) = (x = h & alg_twin t (y # z))"
```
```   904   by (import prob_canon ALG_TWIN_CONS)
```
```   905
```
```   906 lemma ALG_TWIN_REDUCE: "ALL h t t'. alg_twin (h # t) (h # t') = alg_twin t t'"
```
```   907   by (import prob_canon ALG_TWIN_REDUCE)
```
```   908
```
```   909 lemma ALG_TWINS_PREFIX: "(All::(bool list => bool) => bool)
```
```   910  (%x::bool list.
```
```   911      (All::(bool list => bool) => bool)
```
```   912       (%l::bool list.
```
```   913           (op -->::bool => bool => bool)
```
```   914            ((IS_PREFIX::bool list => bool list => bool) x l)
```
```   915            ((op |::bool => bool => bool)
```
```   916              ((op =::bool list => bool list => bool) x l)
```
```   917              ((op |::bool => bool => bool)
```
```   918                ((IS_PREFIX::bool list => bool list => bool) x
```
```   919                  ((SNOC::bool => bool list => bool list) (True::bool) l))
```
```   920                ((IS_PREFIX::bool list => bool list => bool) x
```
```   921                  ((SNOC::bool => bool list => bool list) (False::bool)
```
```   922                    l))))))"
```
```   923   by (import prob_canon ALG_TWINS_PREFIX)
```
```   924
```
```   925 lemma ALG_ORDER_NIL: "ALL x. alg_order [] x & alg_order x [] = (x = [])"
```
```   926   by (import prob_canon ALG_ORDER_NIL)
```
```   927
```
```   928 lemma ALG_ORDER_REFL: "ALL x. alg_order x x"
```
```   929   by (import prob_canon ALG_ORDER_REFL)
```
```   930
```
```   931 lemma ALG_ORDER_ANTISYM: "(All::(bool list => bool) => bool)
```
```   932  (%x::bool list.
```
```   933      (All::(bool list => bool) => bool)
```
```   934       (%y::bool list.
```
```   935           (op -->::bool => bool => bool)
```
```   936            ((op &::bool => bool => bool)
```
```   937              ((alg_order::bool list => bool list => bool) x y)
```
```   938              ((alg_order::bool list => bool list => bool) y x))
```
```   939            ((op =::bool list => bool list => bool) x y)))"
```
```   940   by (import prob_canon ALG_ORDER_ANTISYM)
```
```   941
```
```   942 lemma ALG_ORDER_TRANS: "(All::(bool list => bool) => bool)
```
```   943  (%x::bool list.
```
```   944      (All::(bool list => bool) => bool)
```
```   945       (%y::bool list.
```
```   946           (All::(bool list => bool) => bool)
```
```   947            (%z::bool list.
```
```   948                (op -->::bool => bool => bool)
```
```   949                 ((op &::bool => bool => bool)
```
```   950                   ((alg_order::bool list => bool list => bool) x y)
```
```   951                   ((alg_order::bool list => bool list => bool) y z))
```
```   952                 ((alg_order::bool list => bool list => bool) x z))))"
```
```   953   by (import prob_canon ALG_ORDER_TRANS)
```
```   954
```
```   955 lemma ALG_ORDER_TOTAL: "ALL x y. alg_order x y | alg_order y x"
```
```   956   by (import prob_canon ALG_ORDER_TOTAL)
```
```   957
```
```   958 lemma ALG_ORDER_PREFIX: "(All::(bool list => bool) => bool)
```
```   959  (%x::bool list.
```
```   960      (All::(bool list => bool) => bool)
```
```   961       (%y::bool list.
```
```   962           (op -->::bool => bool => bool)
```
```   963            ((IS_PREFIX::bool list => bool list => bool) y x)
```
```   964            ((alg_order::bool list => bool list => bool) x y)))"
```
```   965   by (import prob_canon ALG_ORDER_PREFIX)
```
```   966
```
```   967 lemma ALG_ORDER_PREFIX_ANTI: "(All::(bool list => bool) => bool)
```
```   968  (%x::bool list.
```
```   969      (All::(bool list => bool) => bool)
```
```   970       (%y::bool list.
```
```   971           (op -->::bool => bool => bool)
```
```   972            ((op &::bool => bool => bool)
```
```   973              ((alg_order::bool list => bool list => bool) x y)
```
```   974              ((IS_PREFIX::bool list => bool list => bool) x y))
```
```   975            ((op =::bool list => bool list => bool) x y)))"
```
```   976   by (import prob_canon ALG_ORDER_PREFIX_ANTI)
```
```   977
```
```   978 lemma ALG_ORDER_PREFIX_MONO: "(All::(bool list => bool) => bool)
```
```   979  (%x::bool list.
```
```   980      (All::(bool list => bool) => bool)
```
```   981       (%y::bool list.
```
```   982           (All::(bool list => bool) => bool)
```
```   983            (%z::bool list.
```
```   984                (op -->::bool => bool => bool)
```
```   985                 ((op &::bool => bool => bool)
```
```   986                   ((alg_order::bool list => bool list => bool) x y)
```
```   987                   ((op &::bool => bool => bool)
```
```   988                     ((alg_order::bool list => bool list => bool) y z)
```
```   989                     ((IS_PREFIX::bool list => bool list => bool) z x)))
```
```   990                 ((IS_PREFIX::bool list => bool list => bool) y x))))"
```
```   991   by (import prob_canon ALG_ORDER_PREFIX_MONO)
```
```   992
```
```   993 lemma ALG_ORDER_PREFIX_TRANS: "(All::(bool list => bool) => bool)
```
```   994  (%x::bool list.
```
```   995      (All::(bool list => bool) => bool)
```
```   996       (%y::bool list.
```
```   997           (All::(bool list => bool) => bool)
```
```   998            (%z::bool list.
```
```   999                (op -->::bool => bool => bool)
```
```  1000                 ((op &::bool => bool => bool)
```
```  1001                   ((alg_order::bool list => bool list => bool) x y)
```
```  1002                   ((IS_PREFIX::bool list => bool list => bool) y z))
```
```  1003                 ((op |::bool => bool => bool)
```
```  1004                   ((alg_order::bool list => bool list => bool) x z)
```
```  1005                   ((IS_PREFIX::bool list => bool list => bool) x z)))))"
```
```  1006   by (import prob_canon ALG_ORDER_PREFIX_TRANS)
```
```  1007
```
```  1008 lemma ALG_ORDER_SNOC: "ALL x l. ~ alg_order (SNOC x l) l"
```
```  1009   by (import prob_canon ALG_ORDER_SNOC)
```
```  1010
```
```  1011 lemma ALG_SORTED_MIN: "(All::(bool list => bool) => bool)
```
```  1012  (%h::bool list.
```
```  1013      (All::(bool list list => bool) => bool)
```
```  1014       (%t::bool list list.
```
```  1015           (op -->::bool => bool => bool)
```
```  1016            ((alg_sorted::bool list list => bool)
```
```  1017              ((op #::bool list => bool list list => bool list list) h t))
```
```  1018            ((All::(bool list => bool) => bool)
```
```  1019              (%x::bool list.
```
```  1020                  (op -->::bool => bool => bool)
```
```  1021                   ((op mem::bool list => bool list list => bool) x t)
```
```  1022                   ((alg_order::bool list => bool list => bool) h x)))))"
```
```  1023   by (import prob_canon ALG_SORTED_MIN)
```
```  1024
```
```  1025 lemma ALG_SORTED_DEF_ALT: "(All::(bool list => bool) => bool)
```
```  1026  (%h::bool list.
```
```  1027      (All::(bool list list => bool) => bool)
```
```  1028       (%t::bool list list.
```
```  1029           (op =::bool => bool => bool)
```
```  1030            ((alg_sorted::bool list list => bool)
```
```  1031              ((op #::bool list => bool list list => bool list list) h t))
```
```  1032            ((op &::bool => bool => bool)
```
```  1033              ((All::(bool list => bool) => bool)
```
```  1034                (%x::bool list.
```
```  1035                    (op -->::bool => bool => bool)
```
```  1036                     ((op mem::bool list => bool list list => bool) x t)
```
```  1037                     ((alg_order::bool list => bool list => bool) h x)))
```
```  1038              ((alg_sorted::bool list list => bool) t))))"
```
```  1039   by (import prob_canon ALG_SORTED_DEF_ALT)
```
```  1040
```
```  1041 lemma ALG_SORTED_TL: "(All::(bool list => bool) => bool)
```
```  1042  (%h::bool list.
```
```  1043      (All::(bool list list => bool) => bool)
```
```  1044       (%t::bool list list.
```
```  1045           (op -->::bool => bool => bool)
```
```  1046            ((alg_sorted::bool list list => bool)
```
```  1047              ((op #::bool list => bool list list => bool list list) h t))
```
```  1048            ((alg_sorted::bool list list => bool) t)))"
```
```  1049   by (import prob_canon ALG_SORTED_TL)
```
```  1050
```
```  1051 lemma ALG_SORTED_MONO: "(All::(bool list => bool) => bool)
```
```  1052  (%x::bool list.
```
```  1053      (All::(bool list => bool) => bool)
```
```  1054       (%y::bool list.
```
```  1055           (All::(bool list list => bool) => bool)
```
```  1056            (%z::bool list list.
```
```  1057                (op -->::bool => bool => bool)
```
```  1058                 ((alg_sorted::bool list list => bool)
```
```  1059                   ((op #::bool list => bool list list => bool list list) x
```
```  1060                     ((op #::bool list => bool list list => bool list list) y
```
```  1061                       z)))
```
```  1062                 ((alg_sorted::bool list list => bool)
```
```  1063                   ((op #::bool list => bool list list => bool list list) x
```
```  1064                     z)))))"
```
```  1065   by (import prob_canon ALG_SORTED_MONO)
```
```  1066
```
```  1067 lemma ALG_SORTED_TLS: "ALL l b. alg_sorted (map (op # b) l) = alg_sorted l"
```
```  1068   by (import prob_canon ALG_SORTED_TLS)
```
```  1069
```
```  1070 lemma ALG_SORTED_STEP: "ALL l1 l2.
```
```  1071    alg_sorted (map (op # True) l1 @ map (op # False) l2) =
```
```  1072    (alg_sorted l1 & alg_sorted l2)"
```
```  1073   by (import prob_canon ALG_SORTED_STEP)
```
```  1074
```
```  1075 lemma ALG_SORTED_APPEND: "ALL h h' t t'.
```
```  1076    alg_sorted ((h # t) @ h' # t') =
```
```  1077    (alg_sorted (h # t) & alg_sorted (h' # t') & alg_order (last (h # t)) h')"
```
```  1078   by (import prob_canon ALG_SORTED_APPEND)
```
```  1079
```
```  1080 lemma ALG_SORTED_FILTER: "(All::((bool list => bool) => bool) => bool)
```
```  1081  (%P::bool list => bool.
```
```  1082      (All::(bool list list => bool) => bool)
```
```  1083       (%b::bool list list.
```
```  1084           (op -->::bool => bool => bool)
```
```  1085            ((alg_sorted::bool list list => bool) b)
```
```  1086            ((alg_sorted::bool list list => bool)
```
```  1087              ((filter::(bool list => bool)
```
```  1088                        => bool list list => bool list list)
```
```  1089                P b))))"
```
```  1090   by (import prob_canon ALG_SORTED_FILTER)
```
```  1091
```
```  1092 lemma ALG_PREFIXFREE_TL: "(All::(bool list => bool) => bool)
```
```  1093  (%h::bool list.
```
```  1094      (All::(bool list list => bool) => bool)
```
```  1095       (%t::bool list list.
```
```  1096           (op -->::bool => bool => bool)
```
```  1097            ((alg_prefixfree::bool list list => bool)
```
```  1098              ((op #::bool list => bool list list => bool list list) h t))
```
```  1099            ((alg_prefixfree::bool list list => bool) t)))"
```
```  1100   by (import prob_canon ALG_PREFIXFREE_TL)
```
```  1101
```
```  1102 lemma ALG_PREFIXFREE_MONO: "(All::(bool list => bool) => bool)
```
```  1103  (%x::bool list.
```
```  1104      (All::(bool list => bool) => bool)
```
```  1105       (%y::bool list.
```
```  1106           (All::(bool list list => bool) => bool)
```
```  1107            (%z::bool list list.
```
```  1108                (op -->::bool => bool => bool)
```
```  1109                 ((op &::bool => bool => bool)
```
```  1110                   ((alg_sorted::bool list list => bool)
```
```  1111                     ((op #::bool list => bool list list => bool list list) x
```
```  1112                       ((op #::bool list => bool list list => bool list list)
```
```  1113                         y z)))
```
```  1114                   ((alg_prefixfree::bool list list => bool)
```
```  1115                     ((op #::bool list => bool list list => bool list list) x
```
```  1116                       ((op #::bool list => bool list list => bool list list)
```
```  1117                         y z))))
```
```  1118                 ((alg_prefixfree::bool list list => bool)
```
```  1119                   ((op #::bool list => bool list list => bool list list) x
```
```  1120                     z)))))"
```
```  1121   by (import prob_canon ALG_PREFIXFREE_MONO)
```
```  1122
```
```  1123 lemma ALG_PREFIXFREE_ELT: "(All::(bool list => bool) => bool)
```
```  1124  (%h::bool list.
```
```  1125      (All::(bool list list => bool) => bool)
```
```  1126       (%t::bool list list.
```
```  1127           (op -->::bool => bool => bool)
```
```  1128            ((op &::bool => bool => bool)
```
```  1129              ((alg_sorted::bool list list => bool)
```
```  1130                ((op #::bool list => bool list list => bool list list) h t))
```
```  1131              ((alg_prefixfree::bool list list => bool)
```
```  1132                ((op #::bool list => bool list list => bool list list) h t)))
```
```  1133            ((All::(bool list => bool) => bool)
```
```  1134              (%x::bool list.
```
```  1135                  (op -->::bool => bool => bool)
```
```  1136                   ((op mem::bool list => bool list list => bool) x t)
```
```  1137                   ((op &::bool => bool => bool)
```
```  1138                     ((Not::bool => bool)
```
```  1139                       ((IS_PREFIX::bool list => bool list => bool) x h))
```
```  1140                     ((Not::bool => bool)
```
```  1141                       ((IS_PREFIX::bool list => bool list => bool) h
```
```  1142                         x)))))))"
```
```  1143   by (import prob_canon ALG_PREFIXFREE_ELT)
```
```  1144
```
```  1145 lemma ALG_PREFIXFREE_TLS: "ALL l b. alg_prefixfree (map (op # b) l) = alg_prefixfree l"
```
```  1146   by (import prob_canon ALG_PREFIXFREE_TLS)
```
```  1147
```
```  1148 lemma ALG_PREFIXFREE_STEP: "ALL l1 l2.
```
```  1149    alg_prefixfree (map (op # True) l1 @ map (op # False) l2) =
```
```  1150    (alg_prefixfree l1 & alg_prefixfree l2)"
```
```  1151   by (import prob_canon ALG_PREFIXFREE_STEP)
```
```  1152
```
```  1153 lemma ALG_PREFIXFREE_APPEND: "ALL h h' t t'.
```
```  1154    alg_prefixfree ((h # t) @ h' # t') =
```
```  1155    (alg_prefixfree (h # t) &
```
```  1156     alg_prefixfree (h' # t') & ~ IS_PREFIX h' (last (h # t)))"
```
```  1157   by (import prob_canon ALG_PREFIXFREE_APPEND)
```
```  1158
```
```  1159 lemma ALG_PREFIXFREE_FILTER: "(All::((bool list => bool) => bool) => bool)
```
```  1160  (%P::bool list => bool.
```
```  1161      (All::(bool list list => bool) => bool)
```
```  1162       (%b::bool list list.
```
```  1163           (op -->::bool => bool => bool)
```
```  1164            ((op &::bool => bool => bool)
```
```  1165              ((alg_sorted::bool list list => bool) b)
```
```  1166              ((alg_prefixfree::bool list list => bool) b))
```
```  1167            ((alg_prefixfree::bool list list => bool)
```
```  1168              ((filter::(bool list => bool)
```
```  1169                        => bool list list => bool list list)
```
```  1170                P b))))"
```
```  1171   by (import prob_canon ALG_PREFIXFREE_FILTER)
```
```  1172
```
```  1173 lemma ALG_TWINFREE_TL: "(All::(bool list => bool) => bool)
```
```  1174  (%h::bool list.
```
```  1175      (All::(bool list list => bool) => bool)
```
```  1176       (%t::bool list list.
```
```  1177           (op -->::bool => bool => bool)
```
```  1178            ((alg_twinfree::bool list list => bool)
```
```  1179              ((op #::bool list => bool list list => bool list list) h t))
```
```  1180            ((alg_twinfree::bool list list => bool) t)))"
```
```  1181   by (import prob_canon ALG_TWINFREE_TL)
```
```  1182
```
```  1183 lemma ALG_TWINFREE_TLS: "ALL l b. alg_twinfree (map (op # b) l) = alg_twinfree l"
```
```  1184   by (import prob_canon ALG_TWINFREE_TLS)
```
```  1185
```
```  1186 lemma ALG_TWINFREE_STEP1: "(All::(bool list list => bool) => bool)
```
```  1187  (%l1::bool list list.
```
```  1188      (All::(bool list list => bool) => bool)
```
```  1189       (%l2::bool list list.
```
```  1190           (op -->::bool => bool => bool)
```
```  1191            ((alg_twinfree::bool list list => bool)
```
```  1192              ((op @::bool list list => bool list list => bool list list)
```
```  1193                ((map::(bool list => bool list)
```
```  1194                       => bool list list => bool list list)
```
```  1195                  ((op #::bool => bool list => bool list) (True::bool)) l1)
```
```  1196                ((map::(bool list => bool list)
```
```  1197                       => bool list list => bool list list)
```
```  1198                  ((op #::bool => bool list => bool list) (False::bool))
```
```  1199                  l2)))
```
```  1200            ((op &::bool => bool => bool)
```
```  1201              ((alg_twinfree::bool list list => bool) l1)
```
```  1202              ((alg_twinfree::bool list list => bool) l2))))"
```
```  1203   by (import prob_canon ALG_TWINFREE_STEP1)
```
```  1204
```
```  1205 lemma ALG_TWINFREE_STEP2: "(All::(bool list list => bool) => bool)
```
```  1206  (%l1::bool list list.
```
```  1207      (All::(bool list list => bool) => bool)
```
```  1208       (%l2::bool list list.
```
```  1209           (op -->::bool => bool => bool)
```
```  1210            ((op &::bool => bool => bool)
```
```  1211              ((op |::bool => bool => bool)
```
```  1212                ((Not::bool => bool)
```
```  1213                  ((op mem::bool list => bool list list => bool)
```
```  1214                    ([]::bool list) l1))
```
```  1215                ((Not::bool => bool)
```
```  1216                  ((op mem::bool list => bool list list => bool)
```
```  1217                    ([]::bool list) l2)))
```
```  1218              ((op &::bool => bool => bool)
```
```  1219                ((alg_twinfree::bool list list => bool) l1)
```
```  1220                ((alg_twinfree::bool list list => bool) l2)))
```
```  1221            ((alg_twinfree::bool list list => bool)
```
```  1222              ((op @::bool list list => bool list list => bool list list)
```
```  1223                ((map::(bool list => bool list)
```
```  1224                       => bool list list => bool list list)
```
```  1225                  ((op #::bool => bool list => bool list) (True::bool)) l1)
```
```  1226                ((map::(bool list => bool list)
```
```  1227                       => bool list list => bool list list)
```
```  1228                  ((op #::bool => bool list => bool list) (False::bool))
```
```  1229                  l2)))))"
```
```  1230   by (import prob_canon ALG_TWINFREE_STEP2)
```
```  1231
```
```  1232 lemma ALG_TWINFREE_STEP: "(All::(bool list list => bool) => bool)
```
```  1233  (%l1::bool list list.
```
```  1234      (All::(bool list list => bool) => bool)
```
```  1235       (%l2::bool list list.
```
```  1236           (op -->::bool => bool => bool)
```
```  1237            ((op |::bool => bool => bool)
```
```  1238              ((Not::bool => bool)
```
```  1239                ((op mem::bool list => bool list list => bool)
```
```  1240                  ([]::bool list) l1))
```
```  1241              ((Not::bool => bool)
```
```  1242                ((op mem::bool list => bool list list => bool)
```
```  1243                  ([]::bool list) l2)))
```
```  1244            ((op =::bool => bool => bool)
```
```  1245              ((alg_twinfree::bool list list => bool)
```
```  1246                ((op @::bool list list => bool list list => bool list list)
```
```  1247                  ((map::(bool list => bool list)
```
```  1248                         => bool list list => bool list list)
```
```  1249                    ((op #::bool => bool list => bool list) (True::bool)) l1)
```
```  1250                  ((map::(bool list => bool list)
```
```  1251                         => bool list list => bool list list)
```
```  1252                    ((op #::bool => bool list => bool list) (False::bool))
```
```  1253                    l2)))
```
```  1254              ((op &::bool => bool => bool)
```
```  1255                ((alg_twinfree::bool list list => bool) l1)
```
```  1256                ((alg_twinfree::bool list list => bool) l2)))))"
```
```  1257   by (import prob_canon ALG_TWINFREE_STEP)
```
```  1258
```
```  1259 lemma ALG_LONGEST_HD: "ALL h t. length h <= alg_longest (h # t)"
```
```  1260   by (import prob_canon ALG_LONGEST_HD)
```
```  1261
```
```  1262 lemma ALG_LONGEST_TL: "ALL h t. alg_longest t <= alg_longest (h # t)"
```
```  1263   by (import prob_canon ALG_LONGEST_TL)
```
```  1264
```
```  1265 lemma ALG_LONGEST_TLS: "ALL h t b. alg_longest (map (op # b) (h # t)) = Suc (alg_longest (h # t))"
```
```  1266   by (import prob_canon ALG_LONGEST_TLS)
```
```  1267
```
```  1268 lemma ALG_LONGEST_APPEND: "ALL l1 l2.
```
```  1269    alg_longest l1 <= alg_longest (l1 @ l2) &
```
```  1270    alg_longest l2 <= alg_longest (l1 @ l2)"
```
```  1271   by (import prob_canon ALG_LONGEST_APPEND)
```
```  1272
```
```  1273 lemma ALG_CANON_PREFS_HD: "ALL l b. hd (alg_canon_prefs l b) = l"
```
```  1274   by (import prob_canon ALG_CANON_PREFS_HD)
```
```  1275
```
```  1276 lemma ALG_CANON_PREFS_DELETES: "(All::(bool list => bool) => bool)
```
```  1277  (%l::bool list.
```
```  1278      (All::(bool list list => bool) => bool)
```
```  1279       (%b::bool list list.
```
```  1280           (All::(bool list => bool) => bool)
```
```  1281            (%x::bool list.
```
```  1282                (op -->::bool => bool => bool)
```
```  1283                 ((op mem::bool list => bool list list => bool) x
```
```  1284                   ((alg_canon_prefs::bool list
```
```  1285                                      => bool list list => bool list list)
```
```  1286                     l b))
```
```  1287                 ((op mem::bool list => bool list list => bool) x
```
```  1288                   ((op #::bool list => bool list list => bool list list) l
```
```  1289                     b)))))"
```
```  1290   by (import prob_canon ALG_CANON_PREFS_DELETES)
```
```  1291
```
```  1292 lemma ALG_CANON_PREFS_SORTED: "(All::(bool list => bool) => bool)
```
```  1293  (%l::bool list.
```
```  1294      (All::(bool list list => bool) => bool)
```
```  1295       (%b::bool list list.
```
```  1296           (op -->::bool => bool => bool)
```
```  1297            ((alg_sorted::bool list list => bool)
```
```  1298              ((op #::bool list => bool list list => bool list list) l b))
```
```  1299            ((alg_sorted::bool list list => bool)
```
```  1300              ((alg_canon_prefs::bool list
```
```  1301                                 => bool list list => bool list list)
```
```  1302                l b))))"
```
```  1303   by (import prob_canon ALG_CANON_PREFS_SORTED)
```
```  1304
```
```  1305 lemma ALG_CANON_PREFS_PREFIXFREE: "(All::(bool list => bool) => bool)
```
```  1306  (%l::bool list.
```
```  1307      (All::(bool list list => bool) => bool)
```
```  1308       (%b::bool list list.
```
```  1309           (op -->::bool => bool => bool)
```
```  1310            ((op &::bool => bool => bool)
```
```  1311              ((alg_sorted::bool list list => bool) b)
```
```  1312              ((alg_prefixfree::bool list list => bool) b))
```
```  1313            ((alg_prefixfree::bool list list => bool)
```
```  1314              ((alg_canon_prefs::bool list
```
```  1315                                 => bool list list => bool list list)
```
```  1316                l b))))"
```
```  1317   by (import prob_canon ALG_CANON_PREFS_PREFIXFREE)
```
```  1318
```
```  1319 lemma ALG_CANON_PREFS_CONSTANT: "(All::(bool list => bool) => bool)
```
```  1320  (%l::bool list.
```
```  1321      (All::(bool list list => bool) => bool)
```
```  1322       (%b::bool list list.
```
```  1323           (op -->::bool => bool => bool)
```
```  1324            ((alg_prefixfree::bool list list => bool)
```
```  1325              ((op #::bool list => bool list list => bool list list) l b))
```
```  1326            ((op =::bool list list => bool list list => bool)
```
```  1327              ((alg_canon_prefs::bool list
```
```  1328                                 => bool list list => bool list list)
```
```  1329                l b)
```
```  1330              ((op #::bool list => bool list list => bool list list) l b))))"
```
```  1331   by (import prob_canon ALG_CANON_PREFS_CONSTANT)
```
```  1332
```
```  1333 lemma ALG_CANON_FIND_HD: "ALL l h t.
```
```  1334    hd (alg_canon_find l (h # t)) = l | hd (alg_canon_find l (h # t)) = h"
```
```  1335   by (import prob_canon ALG_CANON_FIND_HD)
```
```  1336
```
```  1337 lemma ALG_CANON_FIND_DELETES: "(All::(bool list => bool) => bool)
```
```  1338  (%l::bool list.
```
```  1339      (All::(bool list list => bool) => bool)
```
```  1340       (%b::bool list list.
```
```  1341           (All::(bool list => bool) => bool)
```
```  1342            (%x::bool list.
```
```  1343                (op -->::bool => bool => bool)
```
```  1344                 ((op mem::bool list => bool list list => bool) x
```
```  1345                   ((alg_canon_find::bool list
```
```  1346                                     => bool list list => bool list list)
```
```  1347                     l b))
```
```  1348                 ((op mem::bool list => bool list list => bool) x
```
```  1349                   ((op #::bool list => bool list list => bool list list) l
```
```  1350                     b)))))"
```
```  1351   by (import prob_canon ALG_CANON_FIND_DELETES)
```
```  1352
```
```  1353 lemma ALG_CANON_FIND_SORTED: "(All::(bool list => bool) => bool)
```
```  1354  (%l::bool list.
```
```  1355      (All::(bool list list => bool) => bool)
```
```  1356       (%b::bool list list.
```
```  1357           (op -->::bool => bool => bool)
```
```  1358            ((alg_sorted::bool list list => bool) b)
```
```  1359            ((alg_sorted::bool list list => bool)
```
```  1360              ((alg_canon_find::bool list
```
```  1361                                => bool list list => bool list list)
```
```  1362                l b))))"
```
```  1363   by (import prob_canon ALG_CANON_FIND_SORTED)
```
```  1364
```
```  1365 lemma ALG_CANON_FIND_PREFIXFREE: "(All::(bool list => bool) => bool)
```
```  1366  (%l::bool list.
```
```  1367      (All::(bool list list => bool) => bool)
```
```  1368       (%b::bool list list.
```
```  1369           (op -->::bool => bool => bool)
```
```  1370            ((op &::bool => bool => bool)
```
```  1371              ((alg_sorted::bool list list => bool) b)
```
```  1372              ((alg_prefixfree::bool list list => bool) b))
```
```  1373            ((alg_prefixfree::bool list list => bool)
```
```  1374              ((alg_canon_find::bool list
```
```  1375                                => bool list list => bool list list)
```
```  1376                l b))))"
```
```  1377   by (import prob_canon ALG_CANON_FIND_PREFIXFREE)
```
```  1378
```
```  1379 lemma ALG_CANON_FIND_CONSTANT: "(All::(bool list => bool) => bool)
```
```  1380  (%l::bool list.
```
```  1381      (All::(bool list list => bool) => bool)
```
```  1382       (%b::bool list list.
```
```  1383           (op -->::bool => bool => bool)
```
```  1384            ((op &::bool => bool => bool)
```
```  1385              ((alg_sorted::bool list list => bool)
```
```  1386                ((op #::bool list => bool list list => bool list list) l b))
```
```  1387              ((alg_prefixfree::bool list list => bool)
```
```  1388                ((op #::bool list => bool list list => bool list list) l b)))
```
```  1389            ((op =::bool list list => bool list list => bool)
```
```  1390              ((alg_canon_find::bool list
```
```  1391                                => bool list list => bool list list)
```
```  1392                l b)
```
```  1393              ((op #::bool list => bool list list => bool list list) l b))))"
```
```  1394   by (import prob_canon ALG_CANON_FIND_CONSTANT)
```
```  1395
```
```  1396 lemma ALG_CANON1_SORTED: "ALL x. alg_sorted (alg_canon1 x)"
```
```  1397   by (import prob_canon ALG_CANON1_SORTED)
```
```  1398
```
```  1399 lemma ALG_CANON1_PREFIXFREE: "ALL l. alg_prefixfree (alg_canon1 l)"
```
```  1400   by (import prob_canon ALG_CANON1_PREFIXFREE)
```
```  1401
```
```  1402 lemma ALG_CANON1_CONSTANT: "(All::(bool list list => bool) => bool)
```
```  1403  (%l::bool list list.
```
```  1404      (op -->::bool => bool => bool)
```
```  1405       ((op &::bool => bool => bool) ((alg_sorted::bool list list => bool) l)
```
```  1406         ((alg_prefixfree::bool list list => bool) l))
```
```  1407       ((op =::bool list list => bool list list => bool)
```
```  1408         ((alg_canon1::bool list list => bool list list) l) l))"
```
```  1409   by (import prob_canon ALG_CANON1_CONSTANT)
```
```  1410
```
```  1411 lemma ALG_CANON_MERGE_SORTED_PREFIXFREE_TWINFREE: "(All::(bool list => bool) => bool)
```
```  1412  (%l::bool list.
```
```  1413      (All::(bool list list => bool) => bool)
```
```  1414       (%b::bool list list.
```
```  1415           (op -->::bool => bool => bool)
```
```  1416            ((op &::bool => bool => bool)
```
```  1417              ((alg_sorted::bool list list => bool)
```
```  1418                ((op #::bool list => bool list list => bool list list) l b))
```
```  1419              ((op &::bool => bool => bool)
```
```  1420                ((alg_prefixfree::bool list list => bool)
```
```  1421                  ((op #::bool list => bool list list => bool list list) l
```
```  1422                    b))
```
```  1423                ((alg_twinfree::bool list list => bool) b)))
```
```  1424            ((op &::bool => bool => bool)
```
```  1425              ((alg_sorted::bool list list => bool)
```
```  1426                ((alg_canon_merge::bool list
```
```  1427                                   => bool list list => bool list list)
```
```  1428                  l b))
```
```  1429              ((op &::bool => bool => bool)
```
```  1430                ((alg_prefixfree::bool list list => bool)
```
```  1431                  ((alg_canon_merge::bool list
```
```  1432                                     => bool list list => bool list list)
```
```  1433                    l b))
```
```  1434                ((alg_twinfree::bool list list => bool)
```
```  1435                  ((alg_canon_merge::bool list
```
```  1436                                     => bool list list => bool list list)
```
```  1437                    l b))))))"
```
```  1438   by (import prob_canon ALG_CANON_MERGE_SORTED_PREFIXFREE_TWINFREE)
```
```  1439
```
```  1440 lemma ALG_CANON_MERGE_PREFIXFREE_PRESERVE: "(All::(bool list => bool) => bool)
```
```  1441  (%l::bool list.
```
```  1442      (All::(bool list list => bool) => bool)
```
```  1443       (%b::bool list list.
```
```  1444           (All::(bool list => bool) => bool)
```
```  1445            (%h::bool list.
```
```  1446                (op -->::bool => bool => bool)
```
```  1447                 ((All::(bool list => bool) => bool)
```
```  1448                   (%x::bool list.
```
```  1449                       (op -->::bool => bool => bool)
```
```  1450                        ((op mem::bool list => bool list list => bool) x
```
```  1451                          ((op #::bool list
```
```  1452                                  => bool list list => bool list list)
```
```  1453                            l b))
```
```  1454                        ((op &::bool => bool => bool)
```
```  1455                          ((Not::bool => bool)
```
```  1456                            ((IS_PREFIX::bool list => bool list => bool) h
```
```  1457                              x))
```
```  1458                          ((Not::bool => bool)
```
```  1459                            ((IS_PREFIX::bool list => bool list => bool) x
```
```  1460                              h)))))
```
```  1461                 ((All::(bool list => bool) => bool)
```
```  1462                   (%x::bool list.
```
```  1463                       (op -->::bool => bool => bool)
```
```  1464                        ((op mem::bool list => bool list list => bool) x
```
```  1465                          ((alg_canon_merge::bool list
```
```  1466       => bool list list => bool list list)
```
```  1467                            l b))
```
```  1468                        ((op &::bool => bool => bool)
```
```  1469                          ((Not::bool => bool)
```
```  1470                            ((IS_PREFIX::bool list => bool list => bool) h
```
```  1471                              x))
```
```  1472                          ((Not::bool => bool)
```
```  1473                            ((IS_PREFIX::bool list => bool list => bool) x
```
```  1474                              h))))))))"
```
```  1475   by (import prob_canon ALG_CANON_MERGE_PREFIXFREE_PRESERVE)
```
```  1476
```
```  1477 lemma ALG_CANON_MERGE_SHORTENS: "(All::(bool list => bool) => bool)
```
```  1478  (%l::bool list.
```
```  1479      (All::(bool list list => bool) => bool)
```
```  1480       (%b::bool list list.
```
```  1481           (All::(bool list => bool) => bool)
```
```  1482            (%x::bool list.
```
```  1483                (op -->::bool => bool => bool)
```
```  1484                 ((op mem::bool list => bool list list => bool) x
```
```  1485                   ((alg_canon_merge::bool list
```
```  1486                                      => bool list list => bool list list)
```
```  1487                     l b))
```
```  1488                 ((Ex::(bool list => bool) => bool)
```
```  1489                   (%y::bool list.
```
```  1490                       (op &::bool => bool => bool)
```
```  1491                        ((op mem::bool list => bool list list => bool) y
```
```  1492                          ((op #::bool list
```
```  1493                                  => bool list list => bool list list)
```
```  1494                            l b))
```
```  1495                        ((IS_PREFIX::bool list => bool list => bool) y
```
```  1496                          x))))))"
```
```  1497   by (import prob_canon ALG_CANON_MERGE_SHORTENS)
```
```  1498
```
```  1499 lemma ALG_CANON_MERGE_CONSTANT: "(All::(bool list => bool) => bool)
```
```  1500  (%l::bool list.
```
```  1501      (All::(bool list list => bool) => bool)
```
```  1502       (%b::bool list list.
```
```  1503           (op -->::bool => bool => bool)
```
```  1504            ((alg_twinfree::bool list list => bool)
```
```  1505              ((op #::bool list => bool list list => bool list list) l b))
```
```  1506            ((op =::bool list list => bool list list => bool)
```
```  1507              ((alg_canon_merge::bool list
```
```  1508                                 => bool list list => bool list list)
```
```  1509                l b)
```
```  1510              ((op #::bool list => bool list list => bool list list) l b))))"
```
```  1511   by (import prob_canon ALG_CANON_MERGE_CONSTANT)
```
```  1512
```
```  1513 lemma ALG_CANON2_PREFIXFREE_PRESERVE: "(All::(bool list list => bool) => bool)
```
```  1514  (%x::bool list list.
```
```  1515      (All::(bool list => bool) => bool)
```
```  1516       (%xa::bool list.
```
```  1517           (op -->::bool => bool => bool)
```
```  1518            ((All::(bool list => bool) => bool)
```
```  1519              (%xb::bool list.
```
```  1520                  (op -->::bool => bool => bool)
```
```  1521                   ((op mem::bool list => bool list list => bool) xb x)
```
```  1522                   ((op &::bool => bool => bool)
```
```  1523                     ((Not::bool => bool)
```
```  1524                       ((IS_PREFIX::bool list => bool list => bool) xa xb))
```
```  1525                     ((Not::bool => bool)
```
```  1526                       ((IS_PREFIX::bool list => bool list => bool) xb
```
```  1527                         xa)))))
```
```  1528            ((All::(bool list => bool) => bool)
```
```  1529              (%xb::bool list.
```
```  1530                  (op -->::bool => bool => bool)
```
```  1531                   ((op mem::bool list => bool list list => bool) xb
```
```  1532                     ((alg_canon2::bool list list => bool list list) x))
```
```  1533                   ((op &::bool => bool => bool)
```
```  1534                     ((Not::bool => bool)
```
```  1535                       ((IS_PREFIX::bool list => bool list => bool) xa xb))
```
```  1536                     ((Not::bool => bool)
```
```  1537                       ((IS_PREFIX::bool list => bool list => bool) xb
```
```  1538                         xa)))))))"
```
```  1539   by (import prob_canon ALG_CANON2_PREFIXFREE_PRESERVE)
```
```  1540
```
```  1541 lemma ALG_CANON2_SHORTENS: "(All::(bool list list => bool) => bool)
```
```  1542  (%x::bool list list.
```
```  1543      (All::(bool list => bool) => bool)
```
```  1544       (%xa::bool list.
```
```  1545           (op -->::bool => bool => bool)
```
```  1546            ((op mem::bool list => bool list list => bool) xa
```
```  1547              ((alg_canon2::bool list list => bool list list) x))
```
```  1548            ((Ex::(bool list => bool) => bool)
```
```  1549              (%y::bool list.
```
```  1550                  (op &::bool => bool => bool)
```
```  1551                   ((op mem::bool list => bool list list => bool) y x)
```
```  1552                   ((IS_PREFIX::bool list => bool list => bool) y xa)))))"
```
```  1553   by (import prob_canon ALG_CANON2_SHORTENS)
```
```  1554
```
```  1555 lemma ALG_CANON2_SORTED_PREFIXFREE_TWINFREE: "(All::(bool list list => bool) => bool)
```
```  1556  (%x::bool list list.
```
```  1557      (op -->::bool => bool => bool)
```
```  1558       ((op &::bool => bool => bool) ((alg_sorted::bool list list => bool) x)
```
```  1559         ((alg_prefixfree::bool list list => bool) x))
```
```  1560       ((op &::bool => bool => bool)
```
```  1561         ((alg_sorted::bool list list => bool)
```
```  1562           ((alg_canon2::bool list list => bool list list) x))
```
```  1563         ((op &::bool => bool => bool)
```
```  1564           ((alg_prefixfree::bool list list => bool)
```
```  1565             ((alg_canon2::bool list list => bool list list) x))
```
```  1566           ((alg_twinfree::bool list list => bool)
```
```  1567             ((alg_canon2::bool list list => bool list list) x)))))"
```
```  1568   by (import prob_canon ALG_CANON2_SORTED_PREFIXFREE_TWINFREE)
```
```  1569
```
```  1570 lemma ALG_CANON2_CONSTANT: "(All::(bool list list => bool) => bool)
```
```  1571  (%l::bool list list.
```
```  1572      (op -->::bool => bool => bool)
```
```  1573       ((alg_twinfree::bool list list => bool) l)
```
```  1574       ((op =::bool list list => bool list list => bool)
```
```  1575         ((alg_canon2::bool list list => bool list list) l) l))"
```
```  1576   by (import prob_canon ALG_CANON2_CONSTANT)
```
```  1577
```
```  1578 lemma ALG_CANON_SORTED_PREFIXFREE_TWINFREE: "ALL l.
```
```  1579    alg_sorted (alg_canon l) &
```
```  1580    alg_prefixfree (alg_canon l) & alg_twinfree (alg_canon l)"
```
```  1581   by (import prob_canon ALG_CANON_SORTED_PREFIXFREE_TWINFREE)
```
```  1582
```
```  1583 lemma ALG_CANON_CONSTANT: "(All::(bool list list => bool) => bool)
```
```  1584  (%l::bool list list.
```
```  1585      (op -->::bool => bool => bool)
```
```  1586       ((op &::bool => bool => bool) ((alg_sorted::bool list list => bool) l)
```
```  1587         ((op &::bool => bool => bool)
```
```  1588           ((alg_prefixfree::bool list list => bool) l)
```
```  1589           ((alg_twinfree::bool list list => bool) l)))
```
```  1590       ((op =::bool list list => bool list list => bool)
```
```  1591         ((alg_canon::bool list list => bool list list) l) l))"
```
```  1592   by (import prob_canon ALG_CANON_CONSTANT)
```
```  1593
```
```  1594 lemma ALG_CANON_IDEMPOT: "ALL l. alg_canon (alg_canon l) = alg_canon l"
```
```  1595   by (import prob_canon ALG_CANON_IDEMPOT)
```
```  1596
```
```  1597 lemma ALGEBRA_CANON_DEF_ALT: "ALL l. algebra_canon l = (alg_sorted l & alg_prefixfree l & alg_twinfree l)"
```
```  1598   by (import prob_canon ALGEBRA_CANON_DEF_ALT)
```
```  1599
```
```  1600 lemma ALGEBRA_CANON_BASIC: "algebra_canon [] & algebra_canon [[]] & (ALL x. algebra_canon [x])"
```
```  1601   by (import prob_canon ALGEBRA_CANON_BASIC)
```
```  1602
```
```  1603 lemma ALG_CANON_BASIC: "alg_canon [] = [] & alg_canon [[]] = [[]] & (ALL x. alg_canon [x] = [x])"
```
```  1604   by (import prob_canon ALG_CANON_BASIC)
```
```  1605
```
```  1606 lemma ALGEBRA_CANON_TL: "(All::(bool list => bool) => bool)
```
```  1607  (%h::bool list.
```
```  1608      (All::(bool list list => bool) => bool)
```
```  1609       (%t::bool list list.
```
```  1610           (op -->::bool => bool => bool)
```
```  1611            ((algebra_canon::bool list list => bool)
```
```  1612              ((op #::bool list => bool list list => bool list list) h t))
```
```  1613            ((algebra_canon::bool list list => bool) t)))"
```
```  1614   by (import prob_canon ALGEBRA_CANON_TL)
```
```  1615
```
```  1616 lemma ALGEBRA_CANON_NIL_MEM: "ALL l. (algebra_canon l & [] mem l) = (l = [[]])"
```
```  1617   by (import prob_canon ALGEBRA_CANON_NIL_MEM)
```
```  1618
```
```  1619 lemma ALGEBRA_CANON_TLS: "ALL l b. algebra_canon (map (op # b) l) = algebra_canon l"
```
```  1620   by (import prob_canon ALGEBRA_CANON_TLS)
```
```  1621
```
```  1622 lemma ALGEBRA_CANON_STEP1: "(All::(bool list list => bool) => bool)
```
```  1623  (%l1::bool list list.
```
```  1624      (All::(bool list list => bool) => bool)
```
```  1625       (%l2::bool list list.
```
```  1626           (op -->::bool => bool => bool)
```
```  1627            ((algebra_canon::bool list list => bool)
```
```  1628              ((op @::bool list list => bool list list => bool list list)
```
```  1629                ((map::(bool list => bool list)
```
```  1630                       => bool list list => bool list list)
```
```  1631                  ((op #::bool => bool list => bool list) (True::bool)) l1)
```
```  1632                ((map::(bool list => bool list)
```
```  1633                       => bool list list => bool list list)
```
```  1634                  ((op #::bool => bool list => bool list) (False::bool))
```
```  1635                  l2)))
```
```  1636            ((op &::bool => bool => bool)
```
```  1637              ((algebra_canon::bool list list => bool) l1)
```
```  1638              ((algebra_canon::bool list list => bool) l2))))"
```
```  1639   by (import prob_canon ALGEBRA_CANON_STEP1)
```
```  1640
```
```  1641 lemma ALGEBRA_CANON_STEP2: "(All::(bool list list => bool) => bool)
```
```  1642  (%l1::bool list list.
```
```  1643      (All::(bool list list => bool) => bool)
```
```  1644       (%l2::bool list list.
```
```  1645           (op -->::bool => bool => bool)
```
```  1646            ((op &::bool => bool => bool)
```
```  1647              ((op |::bool => bool => bool)
```
```  1648                ((Not::bool => bool)
```
```  1649                  ((op =::bool list list => bool list list => bool) l1
```
```  1650                    ((op #::bool list => bool list list => bool list list)
```
```  1651                      ([]::bool list) ([]::bool list list))))
```
```  1652                ((Not::bool => bool)
```
```  1653                  ((op =::bool list list => bool list list => bool) l2
```
```  1654                    ((op #::bool list => bool list list => bool list list)
```
```  1655                      ([]::bool list) ([]::bool list list)))))
```
```  1656              ((op &::bool => bool => bool)
```
```  1657                ((algebra_canon::bool list list => bool) l1)
```
```  1658                ((algebra_canon::bool list list => bool) l2)))
```
```  1659            ((algebra_canon::bool list list => bool)
```
```  1660              ((op @::bool list list => bool list list => bool list list)
```
```  1661                ((map::(bool list => bool list)
```
```  1662                       => bool list list => bool list list)
```
```  1663                  ((op #::bool => bool list => bool list) (True::bool)) l1)
```
```  1664                ((map::(bool list => bool list)
```
```  1665                       => bool list list => bool list list)
```
```  1666                  ((op #::bool => bool list => bool list) (False::bool))
```
```  1667                  l2)))))"
```
```  1668   by (import prob_canon ALGEBRA_CANON_STEP2)
```
```  1669
```
```  1670 lemma ALGEBRA_CANON_STEP: "(All::(bool list list => bool) => bool)
```
```  1671  (%l1::bool list list.
```
```  1672      (All::(bool list list => bool) => bool)
```
```  1673       (%l2::bool list list.
```
```  1674           (op -->::bool => bool => bool)
```
```  1675            ((op |::bool => bool => bool)
```
```  1676              ((Not::bool => bool)
```
```  1677                ((op =::bool list list => bool list list => bool) l1
```
```  1678                  ((op #::bool list => bool list list => bool list list)
```
```  1679                    ([]::bool list) ([]::bool list list))))
```
```  1680              ((Not::bool => bool)
```
```  1681                ((op =::bool list list => bool list list => bool) l2
```
```  1682                  ((op #::bool list => bool list list => bool list list)
```
```  1683                    ([]::bool list) ([]::bool list list)))))
```
```  1684            ((op =::bool => bool => bool)
```
```  1685              ((algebra_canon::bool list list => bool)
```
```  1686                ((op @::bool list list => bool list list => bool list list)
```
```  1687                  ((map::(bool list => bool list)
```
```  1688                         => bool list list => bool list list)
```
```  1689                    ((op #::bool => bool list => bool list) (True::bool)) l1)
```
```  1690                  ((map::(bool list => bool list)
```
```  1691                         => bool list list => bool list list)
```
```  1692                    ((op #::bool => bool list => bool list) (False::bool))
```
```  1693                    l2)))
```
```  1694              ((op &::bool => bool => bool)
```
```  1695                ((algebra_canon::bool list list => bool) l1)
```
```  1696                ((algebra_canon::bool list list => bool) l2)))))"
```
```  1697   by (import prob_canon ALGEBRA_CANON_STEP)
```
```  1698
```
```  1699 lemma ALGEBRA_CANON_CASES_THM: "(All::(bool list list => bool) => bool)
```
```  1700  (%l::bool list list.
```
```  1701      (op -->::bool => bool => bool)
```
```  1702       ((algebra_canon::bool list list => bool) l)
```
```  1703       ((op |::bool => bool => bool)
```
```  1704         ((op =::bool list list => bool list list => bool) l
```
```  1705           ([]::bool list list))
```
```  1706         ((op |::bool => bool => bool)
```
```  1707           ((op =::bool list list => bool list list => bool) l
```
```  1708             ((op #::bool list => bool list list => bool list list)
```
```  1709               ([]::bool list) ([]::bool list list)))
```
```  1710           ((Ex::(bool list list => bool) => bool)
```
```  1711             (%l1::bool list list.
```
```  1712                 (Ex::(bool list list => bool) => bool)
```
```  1713                  (%l2::bool list list.
```
```  1714                      (op &::bool => bool => bool)
```
```  1715                       ((algebra_canon::bool list list => bool) l1)
```
```  1716                       ((op &::bool => bool => bool)
```
```  1717                         ((algebra_canon::bool list list => bool) l2)
```
```  1718                         ((op =::bool list list => bool list list => bool) l
```
```  1719                           ((op @::bool list list
```
```  1720                                   => bool list list => bool list list)
```
```  1721                             ((map::(bool list => bool list)
```
```  1722                                    => bool list list => bool list list)
```
```  1723                               ((op #::bool => bool list => bool list)
```
```  1724                                 (True::bool))
```
```  1725                               l1)
```
```  1726                             ((map::(bool list => bool list)
```
```  1727                                    => bool list list => bool list list)
```
```  1728                               ((op #::bool => bool list => bool list)
```
```  1729                                 (False::bool))
```
```  1730                               l2))))))))))"
```
```  1731   by (import prob_canon ALGEBRA_CANON_CASES_THM)
```
```  1732
```
```  1733 lemma ALGEBRA_CANON_CASES: "(All::((bool list list => bool) => bool) => bool)
```
```  1734  (%P::bool list list => bool.
```
```  1735      (op -->::bool => bool => bool)
```
```  1736       ((op &::bool => bool => bool) (P ([]::bool list list))
```
```  1737         ((op &::bool => bool => bool)
```
```  1738           (P ((op #::bool list => bool list list => bool list list)
```
```  1739                ([]::bool list) ([]::bool list list)))
```
```  1740           ((All::(bool list list => bool) => bool)
```
```  1741             (%l1::bool list list.
```
```  1742                 (All::(bool list list => bool) => bool)
```
```  1743                  (%l2::bool list list.
```
```  1744                      (op -->::bool => bool => bool)
```
```  1745                       ((op &::bool => bool => bool)
```
```  1746                         ((algebra_canon::bool list list => bool) l1)
```
```  1747                         ((op &::bool => bool => bool)
```
```  1748                           ((algebra_canon::bool list list => bool) l2)
```
```  1749                           ((algebra_canon::bool list list => bool)
```
```  1750                             ((op @::bool list list
```
```  1751                                     => bool list list => bool list list)
```
```  1752                               ((map::(bool list => bool list)
```
```  1753                                      => bool list list => bool list list)
```
```  1754                                 ((op #::bool => bool list => bool list)
```
```  1755                                   (True::bool))
```
```  1756                                 l1)
```
```  1757                               ((map::(bool list => bool list)
```
```  1758                                      => bool list list => bool list list)
```
```  1759                                 ((op #::bool => bool list => bool list)
```
```  1760                                   (False::bool))
```
```  1761                                 l2)))))
```
```  1762                       (P ((op @::bool list list
```
```  1763                                  => bool list list => bool list list)
```
```  1764                            ((map::(bool list => bool list)
```
```  1765                                   => bool list list => bool list list)
```
```  1766                              ((op #::bool => bool list => bool list)
```
```  1767                                (True::bool))
```
```  1768                              l1)
```
```  1769                            ((map::(bool list => bool list)
```
```  1770                                   => bool list list => bool list list)
```
```  1771                              ((op #::bool => bool list => bool list)
```
```  1772                                (False::bool))
```
```  1773                              l2))))))))
```
```  1774       ((All::(bool list list => bool) => bool)
```
```  1775         (%l::bool list list.
```
```  1776             (op -->::bool => bool => bool)
```
```  1777              ((algebra_canon::bool list list => bool) l) (P l))))"
```
```  1778   by (import prob_canon ALGEBRA_CANON_CASES)
```
```  1779
```
```  1780 lemma ALGEBRA_CANON_INDUCTION: "(All::((bool list list => bool) => bool) => bool)
```
```  1781  (%P::bool list list => bool.
```
```  1782      (op -->::bool => bool => bool)
```
```  1783       ((op &::bool => bool => bool) (P ([]::bool list list))
```
```  1784         ((op &::bool => bool => bool)
```
```  1785           (P ((op #::bool list => bool list list => bool list list)
```
```  1786                ([]::bool list) ([]::bool list list)))
```
```  1787           ((All::(bool list list => bool) => bool)
```
```  1788             (%l1::bool list list.
```
```  1789                 (All::(bool list list => bool) => bool)
```
```  1790                  (%l2::bool list list.
```
```  1791                      (op -->::bool => bool => bool)
```
```  1792                       ((op &::bool => bool => bool)
```
```  1793                         ((algebra_canon::bool list list => bool) l1)
```
```  1794                         ((op &::bool => bool => bool)
```
```  1795                           ((algebra_canon::bool list list => bool) l2)
```
```  1796                           ((op &::bool => bool => bool) (P l1)
```
```  1797                             ((op &::bool => bool => bool) (P l2)
```
```  1798                               ((algebra_canon::bool list list => bool)
```
```  1799                                 ((op @::bool list list
```
```  1800   => bool list list => bool list list)
```
```  1801                                   ((map::(bool list => bool list)
```
```  1802    => bool list list => bool list list)
```
```  1803                                     ((op #::bool => bool list => bool list)
```
```  1804 (True::bool))
```
```  1805                                     l1)
```
```  1806                                   ((map::(bool list => bool list)
```
```  1807    => bool list list => bool list list)
```
```  1808                                     ((op #::bool => bool list => bool list)
```
```  1809 (False::bool))
```
```  1810                                     l2)))))))
```
```  1811                       (P ((op @::bool list list
```
```  1812                                  => bool list list => bool list list)
```
```  1813                            ((map::(bool list => bool list)
```
```  1814                                   => bool list list => bool list list)
```
```  1815                              ((op #::bool => bool list => bool list)
```
```  1816                                (True::bool))
```
```  1817                              l1)
```
```  1818                            ((map::(bool list => bool list)
```
```  1819                                   => bool list list => bool list list)
```
```  1820                              ((op #::bool => bool list => bool list)
```
```  1821                                (False::bool))
```
```  1822                              l2))))))))
```
```  1823       ((All::(bool list list => bool) => bool)
```
```  1824         (%l::bool list list.
```
```  1825             (op -->::bool => bool => bool)
```
```  1826              ((algebra_canon::bool list list => bool) l) (P l))))"
```
```  1827   by (import prob_canon ALGEBRA_CANON_INDUCTION)
```
```  1828
```
```  1829 lemma MEM_NIL_STEP: "ALL l1 l2. ~ [] mem map (op # True) l1 @ map (op # False) l2"
```
```  1830   by (import prob_canon MEM_NIL_STEP)
```
```  1831
```
```  1832 lemma ALG_SORTED_PREFIXFREE_MEM_NIL: "ALL l. (alg_sorted l & alg_prefixfree l & [] mem l) = (l = [[]])"
```
```  1833   by (import prob_canon ALG_SORTED_PREFIXFREE_MEM_NIL)
```
```  1834
```
```  1835 lemma ALG_SORTED_PREFIXFREE_EQUALITY: "(All::(bool list list => bool) => bool)
```
```  1836  (%l::bool list list.
```
```  1837      (All::(bool list list => bool) => bool)
```
```  1838       (%l'::bool list list.
```
```  1839           (op -->::bool => bool => bool)
```
```  1840            ((op &::bool => bool => bool)
```
```  1841              ((All::(bool list => bool) => bool)
```
```  1842                (%x::bool list.
```
```  1843                    (op =::bool => bool => bool)
```
```  1844                     ((op mem::bool list => bool list list => bool) x l)
```
```  1845                     ((op mem::bool list => bool list list => bool) x l')))
```
```  1846              ((op &::bool => bool => bool)
```
```  1847                ((alg_sorted::bool list list => bool) l)
```
```  1848                ((op &::bool => bool => bool)
```
```  1849                  ((alg_sorted::bool list list => bool) l')
```
```  1850                  ((op &::bool => bool => bool)
```
```  1851                    ((alg_prefixfree::bool list list => bool) l)
```
```  1852                    ((alg_prefixfree::bool list list => bool) l')))))
```
```  1853            ((op =::bool list list => bool list list => bool) l l')))"
```
```  1854   by (import prob_canon ALG_SORTED_PREFIXFREE_EQUALITY)
```
```  1855
```
```  1856 ;end_setup
```
```  1857
```
```  1858 ;setup_theory boolean_sequence
```
```  1859
```
```  1860 consts
```
```  1861   SHD :: "(nat => bool) => bool"
```
```  1862
```
```  1863 defs
```
```  1864   SHD_primdef: "SHD == %f. f 0"
```
```  1865
```
```  1866 lemma SHD_def: "ALL f. SHD f = f 0"
```
```  1867   by (import boolean_sequence SHD_def)
```
```  1868
```
```  1869 consts
```
```  1870   STL :: "(nat => bool) => nat => bool"
```
```  1871
```
```  1872 defs
```
```  1873   STL_primdef: "STL == %f n. f (Suc n)"
```
```  1874
```
```  1875 lemma STL_def: "ALL f n. STL f n = f (Suc n)"
```
```  1876   by (import boolean_sequence STL_def)
```
```  1877
```
```  1878 consts
```
```  1879   SCONS :: "bool => (nat => bool) => nat => bool"
```
```  1880
```
```  1881 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)"
```
```  1882   by (import boolean_sequence SCONS_def)
```
```  1883
```
```  1884 consts
```
```  1885   SDEST :: "(nat => bool) => bool * (nat => bool)"
```
```  1886
```
```  1887 defs
```
```  1888   SDEST_primdef: "SDEST == %s. (SHD s, STL s)"
```
```  1889
```
```  1890 lemma SDEST_def: "SDEST = (%s. (SHD s, STL s))"
```
```  1891   by (import boolean_sequence SDEST_def)
```
```  1892
```
```  1893 consts
```
```  1894   SCONST :: "bool => nat => bool"
```
```  1895
```
```  1896 defs
```
```  1897   SCONST_primdef: "SCONST == K"
```
```  1898
```
```  1899 lemma SCONST_def: "SCONST = K"
```
```  1900   by (import boolean_sequence SCONST_def)
```
```  1901
```
```  1902 consts
```
```  1903   STAKE :: "nat => (nat => bool) => bool list"
```
```  1904
```
```  1905 specification (STAKE_primdef: STAKE) STAKE_def: "(ALL s. STAKE 0 s = []) &
```
```  1906 (ALL n s. STAKE (Suc n) s = SHD s # STAKE n (STL s))"
```
```  1907   by (import boolean_sequence STAKE_def)
```
```  1908
```
```  1909 consts
```
```  1910   SDROP :: "nat => (nat => bool) => nat => bool"
```
```  1911
```
```  1912 specification (SDROP_primdef: SDROP) SDROP_def: "SDROP 0 = I & (ALL n. SDROP (Suc n) = SDROP n o STL)"
```
```  1913   by (import boolean_sequence SDROP_def)
```
```  1914
```
```  1915 lemma SCONS_SURJ: "ALL x. EX xa t. x = SCONS xa t"
```
```  1916   by (import boolean_sequence SCONS_SURJ)
```
```  1917
```
```  1918 lemma SHD_STL_ISO: "ALL h t. EX x. SHD x = h & STL x = t"
```
```  1919   by (import boolean_sequence SHD_STL_ISO)
```
```  1920
```
```  1921 lemma SHD_SCONS: "ALL h t. SHD (SCONS h t) = h"
```
```  1922   by (import boolean_sequence SHD_SCONS)
```
```  1923
```
```  1924 lemma STL_SCONS: "ALL h t. STL (SCONS h t) = t"
```
```  1925   by (import boolean_sequence STL_SCONS)
```
```  1926
```
```  1927 lemma SHD_SCONST: "ALL b. SHD (SCONST b) = b"
```
```  1928   by (import boolean_sequence SHD_SCONST)
```
```  1929
```
```  1930 lemma STL_SCONST: "ALL b. STL (SCONST b) = SCONST b"
```
```  1931   by (import boolean_sequence STL_SCONST)
```
```  1932
```
```  1933 ;end_setup
```
```  1934
```
```  1935 ;setup_theory prob_algebra
```
```  1936
```
```  1937 consts
```
```  1938   alg_embed :: "bool list => (nat => bool) => bool"
```
```  1939
```
```  1940 specification (alg_embed_primdef: alg_embed) alg_embed_def: "(ALL s. alg_embed [] s = True) &
```
```  1941 (ALL h t s. alg_embed (h # t) s = (h = SHD s & alg_embed t (STL s)))"
```
```  1942   by (import prob_algebra alg_embed_def)
```
```  1943
```
```  1944 consts
```
```  1945   algebra_embed :: "bool list list => (nat => bool) => bool"
```
```  1946
```
```  1947 specification (algebra_embed_primdef: algebra_embed) algebra_embed_def: "algebra_embed [] = EMPTY &
```
```  1948 (ALL h t.
```
```  1949     algebra_embed (h # t) = pred_set.UNION (alg_embed h) (algebra_embed t))"
```
```  1950   by (import prob_algebra algebra_embed_def)
```
```  1951
```
```  1952 consts
```
```  1953   measurable :: "((nat => bool) => bool) => bool"
```
```  1954
```
```  1955 defs
```
```  1956   measurable_primdef: "measurable == %s. EX b. s = algebra_embed b"
```
```  1957
```
```  1958 lemma measurable_def: "ALL s. measurable s = (EX b. s = algebra_embed b)"
```
```  1959   by (import prob_algebra measurable_def)
```
```  1960
```
```  1961 lemma HALVES_INTER: "pred_set.INTER (%x. SHD x = True) (%x. SHD x = False) = EMPTY"
```
```  1962   by (import prob_algebra HALVES_INTER)
```
```  1963
```
```  1964 lemma INTER_STL: "ALL p q. pred_set.INTER p q o STL = pred_set.INTER (p o STL) (q o STL)"
```
```  1965   by (import prob_algebra INTER_STL)
```
```  1966
```
```  1967 lemma COMPL_SHD: "ALL b. COMPL (%x. SHD x = b) = (%x. SHD x = (~ b))"
```
```  1968   by (import prob_algebra COMPL_SHD)
```
```  1969
```
```  1970 lemma ALG_EMBED_BASIC: "alg_embed [] = pred_set.UNIV &
```
```  1971 (ALL h t.
```
```  1972     alg_embed (h # t) = pred_set.INTER (%x. SHD x = h) (alg_embed t o STL))"
```
```  1973   by (import prob_algebra ALG_EMBED_BASIC)
```
```  1974
```
```  1975 lemma ALG_EMBED_NIL: "ALL c. All (alg_embed c) = (c = [])"
```
```  1976   by (import prob_algebra ALG_EMBED_NIL)
```
```  1977
```
```  1978 lemma ALG_EMBED_POPULATED: "ALL b. Ex (alg_embed b)"
```
```  1979   by (import prob_algebra ALG_EMBED_POPULATED)
```
```  1980
```
```  1981 lemma ALG_EMBED_PREFIX: "(All::(bool list => bool) => bool)
```
```  1982  (%b::bool list.
```
```  1983      (All::(bool list => bool) => bool)
```
```  1984       (%c::bool list.
```
```  1985           (All::((nat => bool) => bool) => bool)
```
```  1986            (%s::nat => bool.
```
```  1987                (op -->::bool => bool => bool)
```
```  1988                 ((op &::bool => bool => bool)
```
```  1989                   ((alg_embed::bool list => (nat => bool) => bool) b s)
```
```  1990                   ((alg_embed::bool list => (nat => bool) => bool) c s))
```
```  1991                 ((op |::bool => bool => bool)
```
```  1992                   ((IS_PREFIX::bool list => bool list => bool) b c)
```
```  1993                   ((IS_PREFIX::bool list => bool list => bool) c b)))))"
```
```  1994   by (import prob_algebra ALG_EMBED_PREFIX)
```
```  1995
```
```  1996 lemma ALG_EMBED_PREFIX_SUBSET: "ALL b c. SUBSET (alg_embed b) (alg_embed c) = IS_PREFIX b c"
```
```  1997   by (import prob_algebra ALG_EMBED_PREFIX_SUBSET)
```
```  1998
```
```  1999 lemma ALG_EMBED_TWINS: "ALL l.
```
```  2000    pred_set.UNION (alg_embed (SNOC True l)) (alg_embed (SNOC False l)) =
```
```  2001    alg_embed l"
```
```  2002   by (import prob_algebra ALG_EMBED_TWINS)
```
```  2003
```
```  2004 lemma ALGEBRA_EMBED_BASIC: "algebra_embed [] = EMPTY &
```
```  2005 algebra_embed [[]] = pred_set.UNIV &
```
```  2006 (ALL b. algebra_embed [[b]] = (%s. SHD s = b))"
```
```  2007   by (import prob_algebra ALGEBRA_EMBED_BASIC)
```
```  2008
```
```  2009 lemma ALGEBRA_EMBED_MEM: "(All::(bool list list => bool) => bool)
```
```  2010  (%b::bool list list.
```
```  2011      (All::((nat => bool) => bool) => bool)
```
```  2012       (%x::nat => bool.
```
```  2013           (op -->::bool => bool => bool)
```
```  2014            ((algebra_embed::bool list list => (nat => bool) => bool) b x)
```
```  2015            ((Ex::(bool list => bool) => bool)
```
```  2016              (%l::bool list.
```
```  2017                  (op &::bool => bool => bool)
```
```  2018                   ((op mem::bool list => bool list list => bool) l b)
```
```  2019                   ((alg_embed::bool list => (nat => bool) => bool) l x)))))"
```
```  2020   by (import prob_algebra ALGEBRA_EMBED_MEM)
```
```  2021
```
```  2022 lemma ALGEBRA_EMBED_APPEND: "ALL l1 l2.
```
```  2023    algebra_embed (l1 @ l2) =
```
```  2024    pred_set.UNION (algebra_embed l1) (algebra_embed l2)"
```
```  2025   by (import prob_algebra ALGEBRA_EMBED_APPEND)
```
```  2026
```
```  2027 lemma ALGEBRA_EMBED_TLS: "ALL l b.
```
```  2028    algebra_embed (map (op # b) l) (SCONS h t) = (h = b & algebra_embed l t)"
```
```  2029   by (import prob_algebra ALGEBRA_EMBED_TLS)
```
```  2030
```
```  2031 lemma ALG_CANON_PREFS_EMBED: "ALL l b. algebra_embed (alg_canon_prefs l b) = algebra_embed (l # b)"
```
```  2032   by (import prob_algebra ALG_CANON_PREFS_EMBED)
```
```  2033
```
```  2034 lemma ALG_CANON_FIND_EMBED: "ALL l b. algebra_embed (alg_canon_find l b) = algebra_embed (l # b)"
```
```  2035   by (import prob_algebra ALG_CANON_FIND_EMBED)
```
```  2036
```
```  2037 lemma ALG_CANON1_EMBED: "ALL x. algebra_embed (alg_canon1 x) = algebra_embed x"
```
```  2038   by (import prob_algebra ALG_CANON1_EMBED)
```
```  2039
```
```  2040 lemma ALG_CANON_MERGE_EMBED: "ALL l b. algebra_embed (alg_canon_merge l b) = algebra_embed (l # b)"
```
```  2041   by (import prob_algebra ALG_CANON_MERGE_EMBED)
```
```  2042
```
```  2043 lemma ALG_CANON2_EMBED: "ALL x. algebra_embed (alg_canon2 x) = algebra_embed x"
```
```  2044   by (import prob_algebra ALG_CANON2_EMBED)
```
```  2045
```
```  2046 lemma ALG_CANON_EMBED: "ALL l. algebra_embed (alg_canon l) = algebra_embed l"
```
```  2047   by (import prob_algebra ALG_CANON_EMBED)
```
```  2048
```
```  2049 lemma ALGEBRA_CANON_UNIV: "(All::(bool list list => bool) => bool)
```
```  2050  (%l::bool list list.
```
```  2051      (op -->::bool => bool => bool)
```
```  2052       ((algebra_canon::bool list list => bool) l)
```
```  2053       ((op -->::bool => bool => bool)
```
```  2054         ((op =::((nat => bool) => bool) => ((nat => bool) => bool) => bool)
```
```  2055           ((algebra_embed::bool list list => (nat => bool) => bool) l)
```
```  2056           (pred_set.UNIV::(nat => bool) => bool))
```
```  2057         ((op =::bool list list => bool list list => bool) l
```
```  2058           ((op #::bool list => bool list list => bool list list)
```
```  2059             ([]::bool list) ([]::bool list list)))))"
```
```  2060   by (import prob_algebra ALGEBRA_CANON_UNIV)
```
```  2061
```
```  2062 lemma ALG_CANON_REP: "ALL b c. (alg_canon b = alg_canon c) = (algebra_embed b = algebra_embed c)"
```
```  2063   by (import prob_algebra ALG_CANON_REP)
```
```  2064
```
```  2065 lemma ALGEBRA_CANON_EMBED_EMPTY: "(All::(bool list list => bool) => bool)
```
```  2066  (%l::bool list list.
```
```  2067      (op -->::bool => bool => bool)
```
```  2068       ((algebra_canon::bool list list => bool) l)
```
```  2069       ((op =::bool => bool => bool)
```
```  2070         ((All::((nat => bool) => bool) => bool)
```
```  2071           (%v::nat => bool.
```
```  2072               (Not::bool => bool)
```
```  2073                ((algebra_embed::bool list list => (nat => bool) => bool) l
```
```  2074                  v)))
```
```  2075         ((op =::bool list list => bool list list => bool) l
```
```  2076           ([]::bool list list))))"
```
```  2077   by (import prob_algebra ALGEBRA_CANON_EMBED_EMPTY)
```
```  2078
```
```  2079 lemma ALGEBRA_CANON_EMBED_UNIV: "(All::(bool list list => bool) => bool)
```
```  2080  (%l::bool list list.
```
```  2081      (op -->::bool => bool => bool)
```
```  2082       ((algebra_canon::bool list list => bool) l)
```
```  2083       ((op =::bool => bool => bool)
```
```  2084         ((All::((nat => bool) => bool) => bool)
```
```  2085           ((algebra_embed::bool list list => (nat => bool) => bool) l))
```
```  2086         ((op =::bool list list => bool list list => bool) l
```
```  2087           ((op #::bool list => bool list list => bool list list)
```
```  2088             ([]::bool list) ([]::bool list list)))))"
```
```  2089   by (import prob_algebra ALGEBRA_CANON_EMBED_UNIV)
```
```  2090
```
```  2091 lemma MEASURABLE_ALGEBRA: "ALL b. measurable (algebra_embed b)"
```
```  2092   by (import prob_algebra MEASURABLE_ALGEBRA)
```
```  2093
```
```  2094 lemma MEASURABLE_BASIC: "measurable EMPTY &
```
```  2095 measurable pred_set.UNIV & (ALL b. measurable (%s. SHD s = b))"
```
```  2096   by (import prob_algebra MEASURABLE_BASIC)
```
```  2097
```
```  2098 lemma MEASURABLE_SHD: "ALL b. measurable (%s. SHD s = b)"
```
```  2099   by (import prob_algebra MEASURABLE_SHD)
```
```  2100
```
```  2101 lemma ALGEBRA_EMBED_COMPL: "ALL l. EX l'. COMPL (algebra_embed l) = algebra_embed l'"
```
```  2102   by (import prob_algebra ALGEBRA_EMBED_COMPL)
```
```  2103
```
```  2104 lemma MEASURABLE_COMPL: "ALL s. measurable (COMPL s) = measurable s"
```
```  2105   by (import prob_algebra MEASURABLE_COMPL)
```
```  2106
```
```  2107 lemma MEASURABLE_UNION: "(All::(((nat => bool) => bool) => bool) => bool)
```
```  2108  (%s::(nat => bool) => bool.
```
```  2109      (All::(((nat => bool) => bool) => bool) => bool)
```
```  2110       (%t::(nat => bool) => bool.
```
```  2111           (op -->::bool => bool => bool)
```
```  2112            ((op &::bool => bool => bool)
```
```  2113              ((measurable::((nat => bool) => bool) => bool) s)
```
```  2114              ((measurable::((nat => bool) => bool) => bool) t))
```
```  2115            ((measurable::((nat => bool) => bool) => bool)
```
```  2116              ((pred_set.UNION::((nat => bool) => bool)
```
```  2117                                => ((nat => bool) => bool)
```
```  2118                                   => (nat => bool) => bool)
```
```  2119                s t))))"
```
```  2120   by (import prob_algebra MEASURABLE_UNION)
```
```  2121
```
```  2122 lemma MEASURABLE_INTER: "(All::(((nat => bool) => bool) => bool) => bool)
```
```  2123  (%s::(nat => bool) => bool.
```
```  2124      (All::(((nat => bool) => bool) => bool) => bool)
```
```  2125       (%t::(nat => bool) => bool.
```
```  2126           (op -->::bool => bool => bool)
```
```  2127            ((op &::bool => bool => bool)
```
```  2128              ((measurable::((nat => bool) => bool) => bool) s)
```
```  2129              ((measurable::((nat => bool) => bool) => bool) t))
```
```  2130            ((measurable::((nat => bool) => bool) => bool)
```
```  2131              ((pred_set.INTER::((nat => bool) => bool)
```
```  2132                                => ((nat => bool) => bool)
```
```  2133                                   => (nat => bool) => bool)
```
```  2134                s t))))"
```
```  2135   by (import prob_algebra MEASURABLE_INTER)
```
```  2136
```
```  2137 lemma MEASURABLE_STL: "ALL p. measurable (p o STL) = measurable p"
```
```  2138   by (import prob_algebra MEASURABLE_STL)
```
```  2139
```
```  2140 lemma MEASURABLE_SDROP: "ALL n p. measurable (p o SDROP n) = measurable p"
```
```  2141   by (import prob_algebra MEASURABLE_SDROP)
```
```  2142
```
```  2143 lemma MEASURABLE_INTER_HALVES: "ALL p.
```
```  2144    (measurable (pred_set.INTER (%x. SHD x = True) p) &
```
```  2145     measurable (pred_set.INTER (%x. SHD x = False) p)) =
```
```  2146    measurable p"
```
```  2147   by (import prob_algebra MEASURABLE_INTER_HALVES)
```
```  2148
```
```  2149 lemma MEASURABLE_HALVES: "ALL p q.
```
```  2150    measurable
```
```  2151     (pred_set.UNION (pred_set.INTER (%x. SHD x = True) p)
```
```  2152       (pred_set.INTER (%x. SHD x = False) q)) =
```
```  2153    (measurable (pred_set.INTER (%x. SHD x = True) p) &
```
```  2154     measurable (pred_set.INTER (%x. SHD x = False) q))"
```
```  2155   by (import prob_algebra MEASURABLE_HALVES)
```
```  2156
```
```  2157 lemma MEASURABLE_INTER_SHD: "ALL b p.
```
```  2158    measurable (pred_set.INTER (%x. SHD x = b) (p o STL)) = measurable p"
```
```  2159   by (import prob_algebra MEASURABLE_INTER_SHD)
```
```  2160
```
```  2161 ;end_setup
```
```  2162
```
```  2163 ;setup_theory prob
```
```  2164
```
```  2165 consts
```
```  2166   alg_measure :: "bool list list => real"
```
```  2167
```
```  2168 specification (alg_measure_primdef: alg_measure) alg_measure_def: "alg_measure [] = 0 &
```
```  2169 (ALL l rest. alg_measure (l # rest) = (1 / 2) ^ length l + alg_measure rest)"
```
```  2170   by (import prob alg_measure_def)
```
```  2171
```
```  2172 consts
```
```  2173   algebra_measure :: "bool list list => real"
```
```  2174
```
```  2175 defs
```
```  2176   algebra_measure_primdef: "algebra_measure ==
```
```  2177 %b. inf (%r. EX c. algebra_embed b = algebra_embed c & alg_measure c = r)"
```
```  2178
```
```  2179 lemma algebra_measure_def: "ALL b.
```
```  2180    algebra_measure b =
```
```  2181    inf (%r. EX c. algebra_embed b = algebra_embed c & alg_measure c = r)"
```
```  2182   by (import prob algebra_measure_def)
```
```  2183
```
```  2184 consts
```
```  2185   prob :: "((nat => bool) => bool) => real"
```
```  2186
```
```  2187 defs
```
```  2188   prob_primdef: "prob ==
```
```  2189 %s. sup (%r. EX b. algebra_measure b = r & SUBSET (algebra_embed b) s)"
```
```  2190
```
```  2191 lemma prob_def: "ALL s.
```
```  2192    prob s =
```
```  2193    sup (%r. EX b. algebra_measure b = r & SUBSET (algebra_embed b) s)"
```
```  2194   by (import prob prob_def)
```
```  2195
```
```  2196 lemma ALG_TWINS_MEASURE: "ALL l::bool list.
```
```  2197    ((1::real) / (2::real)) ^ length (SNOC True l) +
```
```  2198    ((1::real) / (2::real)) ^ length (SNOC False l) =
```
```  2199    ((1::real) / (2::real)) ^ length l"
```
```  2200   by (import prob ALG_TWINS_MEASURE)
```
```  2201
```
```  2202 lemma ALG_MEASURE_BASIC: "alg_measure [] = 0 &
```
```  2203 alg_measure [[]] = 1 & (ALL b. alg_measure [[b]] = 1 / 2)"
```
```  2204   by (import prob ALG_MEASURE_BASIC)
```
```  2205
```
```  2206 lemma ALG_MEASURE_POS: "ALL l. 0 <= alg_measure l"
```
```  2207   by (import prob ALG_MEASURE_POS)
```
```  2208
```
```  2209 lemma ALG_MEASURE_APPEND: "ALL l1 l2. alg_measure (l1 @ l2) = alg_measure l1 + alg_measure l2"
```
```  2210   by (import prob ALG_MEASURE_APPEND)
```
```  2211
```
```  2212 lemma ALG_MEASURE_TLS: "ALL l b. 2 * alg_measure (map (op # b) l) = alg_measure l"
```
```  2213   by (import prob ALG_MEASURE_TLS)
```
```  2214
```
```  2215 lemma ALG_CANON_PREFS_MONO: "ALL l b. alg_measure (alg_canon_prefs l b) <= alg_measure (l # b)"
```
```  2216   by (import prob ALG_CANON_PREFS_MONO)
```
```  2217
```
```  2218 lemma ALG_CANON_FIND_MONO: "ALL l b. alg_measure (alg_canon_find l b) <= alg_measure (l # b)"
```
```  2219   by (import prob ALG_CANON_FIND_MONO)
```
```  2220
```
```  2221 lemma ALG_CANON1_MONO: "ALL x. alg_measure (alg_canon1 x) <= alg_measure x"
```
```  2222   by (import prob ALG_CANON1_MONO)
```
```  2223
```
```  2224 lemma ALG_CANON_MERGE_MONO: "ALL l b. alg_measure (alg_canon_merge l b) <= alg_measure (l # b)"
```
```  2225   by (import prob ALG_CANON_MERGE_MONO)
```
```  2226
```
```  2227 lemma ALG_CANON2_MONO: "ALL x. alg_measure (alg_canon2 x) <= alg_measure x"
```
```  2228   by (import prob ALG_CANON2_MONO)
```
```  2229
```
```  2230 lemma ALG_CANON_MONO: "ALL l. alg_measure (alg_canon l) <= alg_measure l"
```
```  2231   by (import prob ALG_CANON_MONO)
```
```  2232
```
```  2233 lemma ALGEBRA_MEASURE_DEF_ALT: "ALL l. algebra_measure l = alg_measure (alg_canon l)"
```
```  2234   by (import prob ALGEBRA_MEASURE_DEF_ALT)
```
```  2235
```
```  2236 lemma ALGEBRA_MEASURE_BASIC: "algebra_measure [] = 0 &
```
```  2237 algebra_measure [[]] = 1 & (ALL b. algebra_measure [[b]] = 1 / 2)"
```
```  2238   by (import prob ALGEBRA_MEASURE_BASIC)
```
```  2239
```
```  2240 lemma ALGEBRA_CANON_MEASURE_MAX: "(All::(bool list list => bool) => bool)
```
```  2241  (%l::bool list list.
```
```  2242      (op -->::bool => bool => bool)
```
```  2243       ((algebra_canon::bool list list => bool) l)
```
```  2244       ((op <=::real => real => bool)
```
```  2245         ((alg_measure::bool list list => real) l) (1::real)))"
```
```  2246   by (import prob ALGEBRA_CANON_MEASURE_MAX)
```
```  2247
```
```  2248 lemma ALGEBRA_MEASURE_MAX: "ALL l. algebra_measure l <= 1"
```
```  2249   by (import prob ALGEBRA_MEASURE_MAX)
```
```  2250
```
```  2251 lemma ALGEBRA_MEASURE_MONO_EMBED: "(All::(bool list list => bool) => bool)
```
```  2252  (%x::bool list list.
```
```  2253      (All::(bool list list => bool) => bool)
```
```  2254       (%xa::bool list list.
```
```  2255           (op -->::bool => bool => bool)
```
```  2256            ((SUBSET::((nat => bool) => bool)
```
```  2257                      => ((nat => bool) => bool) => bool)
```
```  2258              ((algebra_embed::bool list list => (nat => bool) => bool) x)
```
```  2259              ((algebra_embed::bool list list => (nat => bool) => bool) xa))
```
```  2260            ((op <=::real => real => bool)
```
```  2261              ((algebra_measure::bool list list => real) x)
```
```  2262              ((algebra_measure::bool list list => real) xa))))"
```
```  2263   by (import prob ALGEBRA_MEASURE_MONO_EMBED)
```
```  2264
```
```  2265 lemma ALG_MEASURE_COMPL: "(All::(bool list list => bool) => bool)
```
```  2266  (%l::bool list list.
```
```  2267      (op -->::bool => bool => bool)
```
```  2268       ((algebra_canon::bool list list => bool) l)
```
```  2269       ((All::(bool list list => bool) => bool)
```
```  2270         (%c::bool list list.
```
```  2271             (op -->::bool => bool => bool)
```
```  2272              ((algebra_canon::bool list list => bool) c)
```
```  2273              ((op -->::bool => bool => bool)
```
```  2274                ((op =::((nat => bool) => bool)
```
```  2275                        => ((nat => bool) => bool) => bool)
```
```  2276                  ((COMPL::((nat => bool) => bool) => (nat => bool) => bool)
```
```  2277                    ((algebra_embed::bool list list => (nat => bool) => bool)
```
```  2278                      l))
```
```  2279                  ((algebra_embed::bool list list => (nat => bool) => bool)
```
```  2280                    c))
```
```  2281                ((op =::real => real => bool)
```
```  2282                  ((op +::real => real => real)
```
```  2283                    ((alg_measure::bool list list => real) l)
```
```  2284                    ((alg_measure::bool list list => real) c))
```
```  2285                  (1::real))))))"
```
```  2286   by (import prob ALG_MEASURE_COMPL)
```
```  2287
```
```  2288 lemma ALG_MEASURE_ADDITIVE: "(All::(bool list list => bool) => bool)
```
```  2289  (%l::bool list list.
```
```  2290      (op -->::bool => bool => bool)
```
```  2291       ((algebra_canon::bool list list => bool) l)
```
```  2292       ((All::(bool list list => bool) => bool)
```
```  2293         (%c::bool list list.
```
```  2294             (op -->::bool => bool => bool)
```
```  2295              ((algebra_canon::bool list list => bool) c)
```
```  2296              ((All::(bool list list => bool) => bool)
```
```  2297                (%d::bool list list.
```
```  2298                    (op -->::bool => bool => bool)
```
```  2299                     ((algebra_canon::bool list list => bool) d)
```
```  2300                     ((op -->::bool => bool => bool)
```
```  2301                       ((op &::bool => bool => bool)
```
```  2302                         ((op =::((nat => bool) => bool)
```
```  2303                                 => ((nat => bool) => bool) => bool)
```
```  2304                           ((pred_set.INTER::((nat => bool) => bool)
```
```  2305       => ((nat => bool) => bool) => (nat => bool) => bool)
```
```  2306                             ((algebra_embed::bool list list
```
```  2307        => (nat => bool) => bool)
```
```  2308                               c)
```
```  2309                             ((algebra_embed::bool list list
```
```  2310        => (nat => bool) => bool)
```
```  2311                               d))
```
```  2312                           (EMPTY::(nat => bool) => bool))
```
```  2313                         ((op =::((nat => bool) => bool)
```
```  2314                                 => ((nat => bool) => bool) => bool)
```
```  2315                           ((algebra_embed::bool list list
```
```  2316      => (nat => bool) => bool)
```
```  2317                             l)
```
```  2318                           ((pred_set.UNION::((nat => bool) => bool)
```
```  2319       => ((nat => bool) => bool) => (nat => bool) => bool)
```
```  2320                             ((algebra_embed::bool list list
```
```  2321        => (nat => bool) => bool)
```
```  2322                               c)
```
```  2323                             ((algebra_embed::bool list list
```
```  2324        => (nat => bool) => bool)
```
```  2325                               d))))
```
```  2326                       ((op =::real => real => bool)
```
```  2327                         ((alg_measure::bool list list => real) l)
```
```  2328                         ((op +::real => real => real)
```
```  2329                           ((alg_measure::bool list list => real) c)
```
```  2330                           ((alg_measure::bool list list => real) d)))))))))"
```
```  2331   by (import prob ALG_MEASURE_ADDITIVE)
```
```  2332
```
```  2333 lemma PROB_ALGEBRA: "ALL l. prob (algebra_embed l) = algebra_measure l"
```
```  2334   by (import prob PROB_ALGEBRA)
```
```  2335
```
```  2336 lemma PROB_BASIC: "prob EMPTY = 0 &
```
```  2337 prob pred_set.UNIV = 1 & (ALL b. prob (%s. SHD s = b) = 1 / 2)"
```
```  2338   by (import prob PROB_BASIC)
```
```  2339
```
```  2340 lemma PROB_ADDITIVE: "(All::(((nat => bool) => bool) => bool) => bool)
```
```  2341  (%s::(nat => bool) => bool.
```
```  2342      (All::(((nat => bool) => bool) => bool) => bool)
```
```  2343       (%t::(nat => bool) => bool.
```
```  2344           (op -->::bool => bool => bool)
```
```  2345            ((op &::bool => bool => bool)
```
```  2346              ((measurable::((nat => bool) => bool) => bool) s)
```
```  2347              ((op &::bool => bool => bool)
```
```  2348                ((measurable::((nat => bool) => bool) => bool) t)
```
```  2349                ((op =::((nat => bool) => bool)
```
```  2350                        => ((nat => bool) => bool) => bool)
```
```  2351                  ((pred_set.INTER::((nat => bool) => bool)
```
```  2352                                    => ((nat => bool) => bool)
```
```  2353 => (nat => bool) => bool)
```
```  2354                    s t)
```
```  2355                  (EMPTY::(nat => bool) => bool))))
```
```  2356            ((op =::real => real => bool)
```
```  2357              ((prob::((nat => bool) => bool) => real)
```
```  2358                ((pred_set.UNION::((nat => bool) => bool)
```
```  2359                                  => ((nat => bool) => bool)
```
```  2360                                     => (nat => bool) => bool)
```
```  2361                  s t))
```
```  2362              ((op +::real => real => real)
```
```  2363                ((prob::((nat => bool) => bool) => real) s)
```
```  2364                ((prob::((nat => bool) => bool) => real) t)))))"
```
```  2365   by (import prob PROB_ADDITIVE)
```
```  2366
```
```  2367 lemma PROB_COMPL: "(All::(((nat => bool) => bool) => bool) => bool)
```
```  2368  (%s::(nat => bool) => bool.
```
```  2369      (op -->::bool => bool => bool)
```
```  2370       ((measurable::((nat => bool) => bool) => bool) s)
```
```  2371       ((op =::real => real => bool)
```
```  2372         ((prob::((nat => bool) => bool) => real)
```
```  2373           ((COMPL::((nat => bool) => bool) => (nat => bool) => bool) s))
```
```  2374         ((op -::real => real => real) (1::real)
```
```  2375           ((prob::((nat => bool) => bool) => real) s))))"
```
```  2376   by (import prob PROB_COMPL)
```
```  2377
```
```  2378 lemma PROB_SUP_EXISTS1: "ALL s. EX x b. algebra_measure b = x & SUBSET (algebra_embed b) s"
```
```  2379   by (import prob PROB_SUP_EXISTS1)
```
```  2380
```
```  2381 lemma PROB_SUP_EXISTS2: "(All::(((nat => bool) => bool) => bool) => bool)
```
```  2382  (%s::(nat => bool) => bool.
```
```  2383      (Ex::(real => bool) => bool)
```
```  2384       (%x::real.
```
```  2385           (All::(real => bool) => bool)
```
```  2386            (%r::real.
```
```  2387                (op -->::bool => bool => bool)
```
```  2388                 ((Ex::(bool list list => bool) => bool)
```
```  2389                   (%b::bool list list.
```
```  2390                       (op &::bool => bool => bool)
```
```  2391                        ((op =::real => real => bool)
```
```  2392                          ((algebra_measure::bool list list => real) b) r)
```
```  2393                        ((SUBSET::((nat => bool) => bool)
```
```  2394                                  => ((nat => bool) => bool) => bool)
```
```  2395                          ((algebra_embed::bool list list
```
```  2396     => (nat => bool) => bool)
```
```  2397                            b)
```
```  2398                          s)))
```
```  2399                 ((op <=::real => real => bool) r x))))"
```
```  2400   by (import prob PROB_SUP_EXISTS2)
```
```  2401
```
```  2402 lemma PROB_LE_X: "(All::(((nat => bool) => bool) => bool) => bool)
```
```  2403  (%s::(nat => bool) => bool.
```
```  2404      (All::(real => bool) => bool)
```
```  2405       (%x::real.
```
```  2406           (op -->::bool => bool => bool)
```
```  2407            ((All::(((nat => bool) => bool) => bool) => bool)
```
```  2408              (%s'::(nat => bool) => bool.
```
```  2409                  (op -->::bool => bool => bool)
```
```  2410                   ((op &::bool => bool => bool)
```
```  2411                     ((measurable::((nat => bool) => bool) => bool) s')
```
```  2412                     ((SUBSET::((nat => bool) => bool)
```
```  2413                               => ((nat => bool) => bool) => bool)
```
```  2414                       s' s))
```
```  2415                   ((op <=::real => real => bool)
```
```  2416                     ((prob::((nat => bool) => bool) => real) s') x)))
```
```  2417            ((op <=::real => real => bool)
```
```  2418              ((prob::((nat => bool) => bool) => real) s) x)))"
```
```  2419   by (import prob PROB_LE_X)
```
```  2420
```
```  2421 lemma X_LE_PROB: "(All::(((nat => bool) => bool) => bool) => bool)
```
```  2422  (%s::(nat => bool) => bool.
```
```  2423      (All::(real => bool) => bool)
```
```  2424       (%x::real.
```
```  2425           (op -->::bool => bool => bool)
```
```  2426            ((Ex::(((nat => bool) => bool) => bool) => bool)
```
```  2427              (%s'::(nat => bool) => bool.
```
```  2428                  (op &::bool => bool => bool)
```
```  2429                   ((measurable::((nat => bool) => bool) => bool) s')
```
```  2430                   ((op &::bool => bool => bool)
```
```  2431                     ((SUBSET::((nat => bool) => bool)
```
```  2432                               => ((nat => bool) => bool) => bool)
```
```  2433                       s' s)
```
```  2434                     ((op <=::real => real => bool) x
```
```  2435                       ((prob::((nat => bool) => bool) => real) s')))))
```
```  2436            ((op <=::real => real => bool) x
```
```  2437              ((prob::((nat => bool) => bool) => real) s))))"
```
```  2438   by (import prob X_LE_PROB)
```
```  2439
```
```  2440 lemma PROB_SUBSET_MONO: "(All::(((nat => bool) => bool) => bool) => bool)
```
```  2441  (%s::(nat => bool) => bool.
```
```  2442      (All::(((nat => bool) => bool) => bool) => bool)
```
```  2443       (%t::(nat => bool) => bool.
```
```  2444           (op -->::bool => bool => bool)
```
```  2445            ((SUBSET::((nat => bool) => bool)
```
```  2446                      => ((nat => bool) => bool) => bool)
```
```  2447              s t)
```
```  2448            ((op <=::real => real => bool)
```
```  2449              ((prob::((nat => bool) => bool) => real) s)
```
```  2450              ((prob::((nat => bool) => bool) => real) t))))"
```
```  2451   by (import prob PROB_SUBSET_MONO)
```
```  2452
```
```  2453 lemma PROB_ALG: "ALL x. prob (alg_embed x) = (1 / 2) ^ length x"
```
```  2454   by (import prob PROB_ALG)
```
```  2455
```
```  2456 lemma PROB_STL: "(All::(((nat => bool) => bool) => bool) => bool)
```
```  2457  (%p::(nat => bool) => bool.
```
```  2458      (op -->::bool => bool => bool)
```
```  2459       ((measurable::((nat => bool) => bool) => bool) p)
```
```  2460       ((op =::real => real => bool)
```
```  2461         ((prob::((nat => bool) => bool) => real)
```
```  2462           ((op o::((nat => bool) => bool)
```
```  2463                   => ((nat => bool) => nat => bool)
```
```  2464                      => (nat => bool) => bool)
```
```  2465             p (STL::(nat => bool) => nat => bool)))
```
```  2466         ((prob::((nat => bool) => bool) => real) p)))"
```
```  2467   by (import prob PROB_STL)
```
```  2468
```
```  2469 lemma PROB_SDROP: "(All::(nat => bool) => bool)
```
```  2470  (%n::nat.
```
```  2471      (All::(((nat => bool) => bool) => bool) => bool)
```
```  2472       (%p::(nat => bool) => bool.
```
```  2473           (op -->::bool => bool => bool)
```
```  2474            ((measurable::((nat => bool) => bool) => bool) p)
```
```  2475            ((op =::real => real => bool)
```
```  2476              ((prob::((nat => bool) => bool) => real)
```
```  2477                ((op o::((nat => bool) => bool)
```
```  2478                        => ((nat => bool) => nat => bool)
```
```  2479                           => (nat => bool) => bool)
```
```  2480                  p ((SDROP::nat => (nat => bool) => nat => bool) n)))
```
```  2481              ((prob::((nat => bool) => bool) => real) p))))"
```
```  2482   by (import prob PROB_SDROP)
```
```  2483
```
```  2484 lemma PROB_INTER_HALVES: "(All::(((nat => bool) => bool) => bool) => bool)
```
```  2485  (%p::(nat => bool) => bool.
```
```  2486      (op -->::bool => bool => bool)
```
```  2487       ((measurable::((nat => bool) => bool) => bool) p)
```
```  2488       ((op =::real => real => bool)
```
```  2489         ((op +::real => real => real)
```
```  2490           ((prob::((nat => bool) => bool) => real)
```
```  2491             ((pred_set.INTER::((nat => bool) => bool)
```
```  2492                               => ((nat => bool) => bool)
```
```  2493                                  => (nat => bool) => bool)
```
```  2494               (%x::nat => bool.
```
```  2495                   (op =::bool => bool => bool)
```
```  2496                    ((SHD::(nat => bool) => bool) x) (True::bool))
```
```  2497               p))
```
```  2498           ((prob::((nat => bool) => bool) => real)
```
```  2499             ((pred_set.INTER::((nat => bool) => bool)
```
```  2500                               => ((nat => bool) => bool)
```
```  2501                                  => (nat => bool) => bool)
```
```  2502               (%x::nat => bool.
```
```  2503                   (op =::bool => bool => bool)
```
```  2504                    ((SHD::(nat => bool) => bool) x) (False::bool))
```
```  2505               p)))
```
```  2506         ((prob::((nat => bool) => bool) => real) p)))"
```
```  2507   by (import prob PROB_INTER_HALVES)
```
```  2508
```
```  2509 lemma PROB_INTER_SHD: "(All::(bool => bool) => bool)
```
```  2510  (%b::bool.
```
```  2511      (All::(((nat => bool) => bool) => bool) => bool)
```
```  2512       (%p::(nat => bool) => bool.
```
```  2513           (op -->::bool => bool => bool)
```
```  2514            ((measurable::((nat => bool) => bool) => bool) p)
```
```  2515            ((op =::real => real => bool)
```
```  2516              ((prob::((nat => bool) => bool) => real)
```
```  2517                ((pred_set.INTER::((nat => bool) => bool)
```
```  2518                                  => ((nat => bool) => bool)
```
```  2519                                     => (nat => bool) => bool)
```
```  2520                  (%x::nat => bool.
```
```  2521                      (op =::bool => bool => bool)
```
```  2522                       ((SHD::(nat => bool) => bool) x) b)
```
```  2523                  ((op o::((nat => bool) => bool)
```
```  2524                          => ((nat => bool) => nat => bool)
```
```  2525                             => (nat => bool) => bool)
```
```  2526                    p (STL::(nat => bool) => nat => bool))))
```
```  2527              ((op *::real => real => real)
```
```  2528                ((op /::real => real => real) (1::real)
```
```  2529                  ((number_of::bin => real)
```
```  2530                    ((op BIT::bin => bool => bin)
```
```  2531                      ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
```
```  2532                        (True::bool))
```
```  2533                      (False::bool))))
```
```  2534                ((prob::((nat => bool) => bool) => real) p)))))"
```
```  2535   by (import prob PROB_INTER_SHD)
```
```  2536
```
```  2537 lemma ALGEBRA_MEASURE_POS: "ALL l. 0 <= algebra_measure l"
```
```  2538   by (import prob ALGEBRA_MEASURE_POS)
```
```  2539
```
```  2540 lemma ALGEBRA_MEASURE_RANGE: "ALL l. 0 <= algebra_measure l & algebra_measure l <= 1"
```
```  2541   by (import prob ALGEBRA_MEASURE_RANGE)
```
```  2542
```
```  2543 lemma PROB_POS: "ALL p. 0 <= prob p"
```
```  2544   by (import prob PROB_POS)
```
```  2545
```
```  2546 lemma PROB_MAX: "ALL p. prob p <= 1"
```
```  2547   by (import prob PROB_MAX)
```
```  2548
```
```  2549 lemma PROB_RANGE: "ALL p. 0 <= prob p & prob p <= 1"
```
```  2550   by (import prob PROB_RANGE)
```
```  2551
```
```  2552 lemma ABS_PROB: "ALL p. abs (prob p) = prob p"
```
```  2553   by (import prob ABS_PROB)
```
```  2554
```
```  2555 lemma PROB_SHD: "ALL b. prob (%s. SHD s = b) = 1 / 2"
```
```  2556   by (import prob PROB_SHD)
```
```  2557
```
```  2558 lemma PROB_COMPL_LE1: "(All::(((nat => bool) => bool) => bool) => bool)
```
```  2559  (%p::(nat => bool) => bool.
```
```  2560      (All::(real => bool) => bool)
```
```  2561       (%r::real.
```
```  2562           (op -->::bool => bool => bool)
```
```  2563            ((measurable::((nat => bool) => bool) => bool) p)
```
```  2564            ((op =::bool => bool => bool)
```
```  2565              ((op <=::real => real => bool)
```
```  2566                ((prob::((nat => bool) => bool) => real)
```
```  2567                  ((COMPL::((nat => bool) => bool) => (nat => bool) => bool)
```
```  2568                    p))
```
```  2569                r)
```
```  2570              ((op <=::real => real => bool)
```
```  2571                ((op -::real => real => real) (1::real) r)
```
```  2572                ((prob::((nat => bool) => bool) => real) p)))))"
```
```  2573   by (import prob PROB_COMPL_LE1)
```
```  2574
```
```  2575 ;end_setup
```
```  2576
```
```  2577 ;setup_theory prob_pseudo
```
```  2578
```
```  2579 consts
```
```  2580   pseudo_linear_hd :: "nat => bool"
```
```  2581
```
```  2582 defs
```
```  2583   pseudo_linear_hd_primdef: "pseudo_linear_hd == EVEN"
```
```  2584
```
```  2585 lemma pseudo_linear_hd_def: "pseudo_linear_hd = EVEN"
```
```  2586   by (import prob_pseudo pseudo_linear_hd_def)
```
```  2587
```
```  2588 consts
```
```  2589   pseudo_linear_tl :: "nat => nat => nat => nat => nat"
```
```  2590
```
```  2591 defs
```
```  2592   pseudo_linear_tl_primdef: "pseudo_linear_tl == %a b n x. (a * x + b) mod (2 * n + 1)"
```
```  2593
```
```  2594 lemma pseudo_linear_tl_def: "ALL a b n x. pseudo_linear_tl a b n x = (a * x + b) mod (2 * n + 1)"
```
```  2595   by (import prob_pseudo pseudo_linear_tl_def)
```
```  2596
```
```  2597 lemma PSEUDO_LINEAR1_EXECUTE: "EX x. (ALL xa. SHD (x xa) = pseudo_linear_hd xa) &
```
```  2598       (ALL xa.
```
```  2599           STL (x xa) =
```
```  2600           x (pseudo_linear_tl
```
```  2601               (NUMERAL
```
```  2602                 (NUMERAL_BIT1
```
```  2603                   (NUMERAL_BIT1
```
```  2604                     (NUMERAL_BIT1
```
```  2605                       (NUMERAL_BIT2
```
```  2606                         (NUMERAL_BIT1 (NUMERAL_BIT2 ALT_ZERO)))))))
```
```  2607               (NUMERAL
```
```  2608                 (NUMERAL_BIT1
```
```  2609                   (NUMERAL_BIT1
```
```  2610                     (NUMERAL_BIT1
```
```  2611                       (NUMERAL_BIT1
```
```  2612                         (NUMERAL_BIT1 (NUMERAL_BIT2 ALT_ZERO)))))))
```
```  2613               (NUMERAL
```
```  2614                 (NUMERAL_BIT1
```
```  2615                   (NUMERAL_BIT1
```
```  2616                     (NUMERAL_BIT1
```
```  2617                       (NUMERAL_BIT1
```
```  2618                         (NUMERAL_BIT2 (NUMERAL_BIT1 ALT_ZERO)))))))
```
```  2619               xa))"
```
```  2620   by (import prob_pseudo PSEUDO_LINEAR1_EXECUTE)
```
```  2621
```
```  2622 consts
```
```  2623   pseudo_linear1 :: "nat => nat => bool"
```
```  2624
```
```  2625 specification (pseudo_linear1_primdef: pseudo_linear1) pseudo_linear1_def: "(ALL x. SHD (pseudo_linear1 x) = pseudo_linear_hd x) &
```
```  2626 (ALL x.
```
```  2627     STL (pseudo_linear1 x) =
```
```  2628     pseudo_linear1
```
```  2629      (pseudo_linear_tl
```
```  2630        (NUMERAL
```
```  2631          (NUMERAL_BIT1
```
```  2632            (NUMERAL_BIT1
```
```  2633              (NUMERAL_BIT1
```
```  2634                (NUMERAL_BIT2 (NUMERAL_BIT1 (NUMERAL_BIT2 ALT_ZERO)))))))
```
```  2635        (NUMERAL
```
```  2636          (NUMERAL_BIT1
```
```  2637            (NUMERAL_BIT1
```
```  2638              (NUMERAL_BIT1
```
```  2639                (NUMERAL_BIT1 (NUMERAL_BIT1 (NUMERAL_BIT2 ALT_ZERO)))))))
```
```  2640        (NUMERAL
```
```  2641          (NUMERAL_BIT1
```
```  2642            (NUMERAL_BIT1
```
```  2643              (NUMERAL_BIT1
```
```  2644                (NUMERAL_BIT1 (NUMERAL_BIT2 (NUMERAL_BIT1 ALT_ZERO)))))))
```
```  2645        x))"
```
```  2646   by (import prob_pseudo pseudo_linear1_def)
```
```  2647
```
```  2648 consts
```
```  2649   pseudo :: "nat => nat => bool"
```
```  2650
```
```  2651 defs
```
```  2652   pseudo_primdef: "pseudo == pseudo_linear1"
```
```  2653
```
```  2654 lemma pseudo_def: "pseudo = pseudo_linear1"
```
```  2655   by (import prob_pseudo pseudo_def)
```
```  2656
```
```  2657 ;end_setup
```
```  2658
```
```  2659 ;setup_theory prob_indep
```
```  2660
```
```  2661 consts
```
```  2662   indep_set :: "((nat => bool) => bool) => ((nat => bool) => bool) => bool"
```
```  2663
```
```  2664 defs
```
```  2665   indep_set_primdef: "indep_set ==
```
```  2666 %p q. measurable p &
```
```  2667       measurable q & prob (pred_set.INTER p q) = prob p * prob q"
```
```  2668
```
```  2669 lemma indep_set_def: "ALL p q.
```
```  2670    indep_set p q =
```
```  2671    (measurable p &
```
```  2672     measurable q & prob (pred_set.INTER p q) = prob p * prob q)"
```
```  2673   by (import prob_indep indep_set_def)
```
```  2674
```
```  2675 consts
```
```  2676   alg_cover_set :: "bool list list => bool"
```
```  2677
```
```  2678 defs
```
```  2679   alg_cover_set_primdef: "alg_cover_set ==
```
```  2680 %l. alg_sorted l & alg_prefixfree l & algebra_embed l = pred_set.UNIV"
```
```  2681
```
```  2682 lemma alg_cover_set_def: "ALL l.
```
```  2683    alg_cover_set l =
```
```  2684    (alg_sorted l & alg_prefixfree l & algebra_embed l = pred_set.UNIV)"
```
```  2685   by (import prob_indep alg_cover_set_def)
```
```  2686
```
```  2687 consts
```
```  2688   alg_cover :: "bool list list => (nat => bool) => bool list"
```
```  2689
```
```  2690 defs
```
```  2691   alg_cover_primdef: "alg_cover == %l x. SOME b. b mem l & alg_embed b x"
```
```  2692
```
```  2693 lemma alg_cover_def: "ALL l x. alg_cover l x = (SOME b. b mem l & alg_embed b x)"
```
```  2694   by (import prob_indep alg_cover_def)
```
```  2695
```
```  2696 consts
```
```  2697   indep :: "((nat => bool) => 'a * (nat => bool)) => bool"
```
```  2698
```
```  2699 defs
```
```  2700   indep_primdef: "indep ==
```
```  2701 %f. EX l r.
```
```  2702        alg_cover_set l &
```
```  2703        (ALL s. f s = (let c = alg_cover l s in (r c, SDROP (length c) s)))"
```
```  2704
```
```  2705 lemma indep_def: "ALL f.
```
```  2706    indep f =
```
```  2707    (EX l r.
```
```  2708        alg_cover_set l &
```
```  2709        (ALL s. f s = (let c = alg_cover l s in (r c, SDROP (length c) s))))"
```
```  2710   by (import prob_indep indep_def)
```
```  2711
```
```  2712 lemma INDEP_SET_BASIC: "(All::(((nat => bool) => bool) => bool) => bool)
```
```  2713  (%p::(nat => bool) => bool.
```
```  2714      (op -->::bool => bool => bool)
```
```  2715       ((measurable::((nat => bool) => bool) => bool) p)
```
```  2716       ((op &::bool => bool => bool)
```
```  2717         ((indep_set::((nat => bool) => bool)
```
```  2718                      => ((nat => bool) => bool) => bool)
```
```  2719           (EMPTY::(nat => bool) => bool) p)
```
```  2720         ((indep_set::((nat => bool) => bool)
```
```  2721                      => ((nat => bool) => bool) => bool)
```
```  2722           (pred_set.UNIV::(nat => bool) => bool) p)))"
```
```  2723   by (import prob_indep INDEP_SET_BASIC)
```
```  2724
```
```  2725 lemma INDEP_SET_SYM: "ALL p q. indep_set p q = indep_set p q"
```
```  2726   by (import prob_indep INDEP_SET_SYM)
```
```  2727
```
```  2728 lemma INDEP_SET_DISJOINT_DECOMP: "(All::(((nat => bool) => bool) => bool) => bool)
```
```  2729  (%p::(nat => bool) => bool.
```
```  2730      (All::(((nat => bool) => bool) => bool) => bool)
```
```  2731       (%q::(nat => bool) => bool.
```
```  2732           (All::(((nat => bool) => bool) => bool) => bool)
```
```  2733            (%r::(nat => bool) => bool.
```
```  2734                (op -->::bool => bool => bool)
```
```  2735                 ((op &::bool => bool => bool)
```
```  2736                   ((indep_set::((nat => bool) => bool)
```
```  2737                                => ((nat => bool) => bool) => bool)
```
```  2738                     p r)
```
```  2739                   ((op &::bool => bool => bool)
```
```  2740                     ((indep_set::((nat => bool) => bool)
```
```  2741                                  => ((nat => bool) => bool) => bool)
```
```  2742                       q r)
```
```  2743                     ((op =::((nat => bool) => bool)
```
```  2744                             => ((nat => bool) => bool) => bool)
```
```  2745                       ((pred_set.INTER::((nat => bool) => bool)
```
```  2746   => ((nat => bool) => bool) => (nat => bool) => bool)
```
```  2747                         p q)
```
```  2748                       (EMPTY::(nat => bool) => bool))))
```
```  2749                 ((indep_set::((nat => bool) => bool)
```
```  2750                              => ((nat => bool) => bool) => bool)
```
```  2751                   ((pred_set.UNION::((nat => bool) => bool)
```
```  2752                                     => ((nat => bool) => bool)
```
```  2753  => (nat => bool) => bool)
```
```  2754                     p q)
```
```  2755                   r))))"
```
```  2756   by (import prob_indep INDEP_SET_DISJOINT_DECOMP)
```
```  2757
```
```  2758 lemma ALG_COVER_SET_BASIC: "~ alg_cover_set [] & alg_cover_set [[]] & alg_cover_set [[True], [False]]"
```
```  2759   by (import prob_indep ALG_COVER_SET_BASIC)
```
```  2760
```
```  2761 lemma ALG_COVER_WELL_DEFINED: "(All::(bool list list => bool) => bool)
```
```  2762  (%l::bool list list.
```
```  2763      (All::((nat => bool) => bool) => bool)
```
```  2764       (%x::nat => bool.
```
```  2765           (op -->::bool => bool => bool)
```
```  2766            ((alg_cover_set::bool list list => bool) l)
```
```  2767            ((op &::bool => bool => bool)
```
```  2768              ((op mem::bool list => bool list list => bool)
```
```  2769                ((alg_cover::bool list list => (nat => bool) => bool list) l
```
```  2770                  x)
```
```  2771                l)
```
```  2772              ((alg_embed::bool list => (nat => bool) => bool)
```
```  2773                ((alg_cover::bool list list => (nat => bool) => bool list) l
```
```  2774                  x)
```
```  2775                x))))"
```
```  2776   by (import prob_indep ALG_COVER_WELL_DEFINED)
```
```  2777
```
```  2778 lemma ALG_COVER_UNIV: "alg_cover [[]] = K []"
```
```  2779   by (import prob_indep ALG_COVER_UNIV)
```
```  2780
```
```  2781 lemma MAP_CONS_TL_FILTER: "(All::(bool list list => bool) => bool)
```
```  2782  (%l::bool list list.
```
```  2783      (All::(bool => bool) => bool)
```
```  2784       (%b::bool.
```
```  2785           (op -->::bool => bool => bool)
```
```  2786            ((Not::bool => bool)
```
```  2787              ((op mem::bool list => bool list list => bool) ([]::bool list)
```
```  2788                l))
```
```  2789            ((op =::bool list list => bool list list => bool)
```
```  2790              ((map::(bool list => bool list)
```
```  2791                     => bool list list => bool list list)
```
```  2792                ((op #::bool => bool list => bool list) b)
```
```  2793                ((map::(bool list => bool list)
```
```  2794                       => bool list list => bool list list)
```
```  2795                  (tl::bool list => bool list)
```
```  2796                  ((filter::(bool list => bool)
```
```  2797                            => bool list list => bool list list)
```
```  2798                    (%x::bool list.
```
```  2799                        (op =::bool => bool => bool)
```
```  2800                         ((hd::bool list => bool) x) b)
```
```  2801                    l)))
```
```  2802              ((filter::(bool list => bool)
```
```  2803                        => bool list list => bool list list)
```
```  2804                (%x::bool list.
```
```  2805                    (op =::bool => bool => bool) ((hd::bool list => bool) x)
```
```  2806                     b)
```
```  2807                l))))"
```
```  2808   by (import prob_indep MAP_CONS_TL_FILTER)
```
```  2809
```
```  2810 lemma ALG_COVER_SET_CASES_THM: "ALL l.
```
```  2811    alg_cover_set l =
```
```  2812    (l = [[]] |
```
```  2813     (EX x xa.
```
```  2814         alg_cover_set x &
```
```  2815         alg_cover_set xa & l = map (op # True) x @ map (op # False) xa))"
```
```  2816   by (import prob_indep ALG_COVER_SET_CASES_THM)
```
```  2817
```
```  2818 lemma ALG_COVER_SET_CASES: "(All::((bool list list => bool) => bool) => bool)
```
```  2819  (%P::bool list list => bool.
```
```  2820      (op -->::bool => bool => bool)
```
```  2821       ((op &::bool => bool => bool)
```
```  2822         (P ((op #::bool list => bool list list => bool list list)
```
```  2823              ([]::bool list) ([]::bool list list)))
```
```  2824         ((All::(bool list list => bool) => bool)
```
```  2825           (%l1::bool list list.
```
```  2826               (All::(bool list list => bool) => bool)
```
```  2827                (%l2::bool list list.
```
```  2828                    (op -->::bool => bool => bool)
```
```  2829                     ((op &::bool => bool => bool)
```
```  2830                       ((alg_cover_set::bool list list => bool) l1)
```
```  2831                       ((op &::bool => bool => bool)
```
```  2832                         ((alg_cover_set::bool list list => bool) l2)
```
```  2833                         ((alg_cover_set::bool list list => bool)
```
```  2834                           ((op @::bool list list
```
```  2835                                   => bool list list => bool list list)
```
```  2836                             ((map::(bool list => bool list)
```
```  2837                                    => bool list list => bool list list)
```
```  2838                               ((op #::bool => bool list => bool list)
```
```  2839                                 (True::bool))
```
```  2840                               l1)
```
```  2841                             ((map::(bool list => bool list)
```
```  2842                                    => bool list list => bool list list)
```
```  2843                               ((op #::bool => bool list => bool list)
```
```  2844                                 (False::bool))
```
```  2845                               l2)))))
```
```  2846                     (P ((op @::bool list list
```
```  2847                                => bool list list => bool list list)
```
```  2848                          ((map::(bool list => bool list)
```
```  2849                                 => bool list list => bool list list)
```
```  2850                            ((op #::bool => bool list => bool list)
```
```  2851                              (True::bool))
```
```  2852                            l1)
```
```  2853                          ((map::(bool list => bool list)
```
```  2854                                 => bool list list => bool list list)
```
```  2855                            ((op #::bool => bool list => bool list)
```
```  2856                              (False::bool))
```
```  2857                            l2)))))))
```
```  2858       ((All::(bool list list => bool) => bool)
```
```  2859         (%l::bool list list.
```
```  2860             (op -->::bool => bool => bool)
```
```  2861              ((alg_cover_set::bool list list => bool) l) (P l))))"
```
```  2862   by (import prob_indep ALG_COVER_SET_CASES)
```
```  2863
```
```  2864 lemma ALG_COVER_SET_INDUCTION: "(All::((bool list list => bool) => bool) => bool)
```
```  2865  (%P::bool list list => bool.
```
```  2866      (op -->::bool => bool => bool)
```
```  2867       ((op &::bool => bool => bool)
```
```  2868         (P ((op #::bool list => bool list list => bool list list)
```
```  2869              ([]::bool list) ([]::bool list list)))
```
```  2870         ((All::(bool list list => bool) => bool)
```
```  2871           (%l1::bool list list.
```
```  2872               (All::(bool list list => bool) => bool)
```
```  2873                (%l2::bool list list.
```
```  2874                    (op -->::bool => bool => bool)
```
```  2875                     ((op &::bool => bool => bool)
```
```  2876                       ((alg_cover_set::bool list list => bool) l1)
```
```  2877                       ((op &::bool => bool => bool)
```
```  2878                         ((alg_cover_set::bool list list => bool) l2)
```
```  2879                         ((op &::bool => bool => bool) (P l1)
```
```  2880                           ((op &::bool => bool => bool) (P l2)
```
```  2881                             ((alg_cover_set::bool list list => bool)
```
```  2882                               ((op @::bool list list
```
```  2883 => bool list list => bool list list)
```
```  2884                                 ((map::(bool list => bool list)
```
```  2885  => bool list list => bool list list)
```
```  2886                                   ((op #::bool => bool list => bool list)
```
```  2887                                     (True::bool))
```
```  2888                                   l1)
```
```  2889                                 ((map::(bool list => bool list)
```
```  2890  => bool list list => bool list list)
```
```  2891                                   ((op #::bool => bool list => bool list)
```
```  2892                                     (False::bool))
```
```  2893                                   l2)))))))
```
```  2894                     (P ((op @::bool list list
```
```  2895                                => bool list list => bool list list)
```
```  2896                          ((map::(bool list => bool list)
```
```  2897                                 => bool list list => bool list list)
```
```  2898                            ((op #::bool => bool list => bool list)
```
```  2899                              (True::bool))
```
```  2900                            l1)
```
```  2901                          ((map::(bool list => bool list)
```
```  2902                                 => bool list list => bool list list)
```
```  2903                            ((op #::bool => bool list => bool list)
```
```  2904                              (False::bool))
```
```  2905                            l2)))))))
```
```  2906       ((All::(bool list list => bool) => bool)
```
```  2907         (%l::bool list list.
```
```  2908             (op -->::bool => bool => bool)
```
```  2909              ((alg_cover_set::bool list list => bool) l) (P l))))"
```
```  2910   by (import prob_indep ALG_COVER_SET_INDUCTION)
```
```  2911
```
```  2912 lemma ALG_COVER_EXISTS_UNIQUE: "(All::(bool list list => bool) => bool)
```
```  2913  (%l::bool list list.
```
```  2914      (op -->::bool => bool => bool)
```
```  2915       ((alg_cover_set::bool list list => bool) l)
```
```  2916       ((All::((nat => bool) => bool) => bool)
```
```  2917         (%s::nat => bool.
```
```  2918             (Ex1::(bool list => bool) => bool)
```
```  2919              (%x::bool list.
```
```  2920                  (op &::bool => bool => bool)
```
```  2921                   ((op mem::bool list => bool list list => bool) x l)
```
```  2922                   ((alg_embed::bool list => (nat => bool) => bool) x s)))))"
```
```  2923   by (import prob_indep ALG_COVER_EXISTS_UNIQUE)
```
```  2924
```
```  2925 lemma ALG_COVER_UNIQUE: "(All::(bool list list => bool) => bool)
```
```  2926  (%l::bool list list.
```
```  2927      (All::(bool list => bool) => bool)
```
```  2928       (%x::bool list.
```
```  2929           (All::((nat => bool) => bool) => bool)
```
```  2930            (%s::nat => bool.
```
```  2931                (op -->::bool => bool => bool)
```
```  2932                 ((op &::bool => bool => bool)
```
```  2933                   ((alg_cover_set::bool list list => bool) l)
```
```  2934                   ((op &::bool => bool => bool)
```
```  2935                     ((op mem::bool list => bool list list => bool) x l)
```
```  2936                     ((alg_embed::bool list => (nat => bool) => bool) x s)))
```
```  2937                 ((op =::bool list => bool list => bool)
```
```  2938                   ((alg_cover::bool list list => (nat => bool) => bool list)
```
```  2939                     l s)
```
```  2940                   x))))"
```
```  2941   by (import prob_indep ALG_COVER_UNIQUE)
```
```  2942
```
```  2943 lemma ALG_COVER_STEP: "(All::(bool list list => bool) => bool)
```
```  2944  (%l1::bool list list.
```
```  2945      (All::(bool list list => bool) => bool)
```
```  2946       (%l2::bool list list.
```
```  2947           (All::(bool => bool) => bool)
```
```  2948            (%h::bool.
```
```  2949                (All::((nat => bool) => bool) => bool)
```
```  2950                 (%t::nat => bool.
```
```  2951                     (op -->::bool => bool => bool)
```
```  2952                      ((op &::bool => bool => bool)
```
```  2953                        ((alg_cover_set::bool list list => bool) l1)
```
```  2954                        ((alg_cover_set::bool list list => bool) l2))
```
```  2955                      ((op =::bool list => bool list => bool)
```
```  2956                        ((alg_cover::bool list list
```
```  2957                                     => (nat => bool) => bool list)
```
```  2958                          ((op @::bool list list
```
```  2959                                  => bool list list => bool list list)
```
```  2960                            ((map::(bool list => bool list)
```
```  2961                                   => bool list list => bool list list)
```
```  2962                              ((op #::bool => bool list => bool list)
```
```  2963                                (True::bool))
```
```  2964                              l1)
```
```  2965                            ((map::(bool list => bool list)
```
```  2966                                   => bool list list => bool list list)
```
```  2967                              ((op #::bool => bool list => bool list)
```
```  2968                                (False::bool))
```
```  2969                              l2))
```
```  2970                          ((SCONS::bool => (nat => bool) => nat => bool) h
```
```  2971                            t))
```
```  2972                        ((If::bool => bool list => bool list => bool list) h
```
```  2973                          ((op #::bool => bool list => bool list)
```
```  2974                            (True::bool)
```
```  2975                            ((alg_cover::bool list list
```
```  2976   => (nat => bool) => bool list)
```
```  2977                              l1 t))
```
```  2978                          ((op #::bool => bool list => bool list)
```
```  2979                            (False::bool)
```
```  2980                            ((alg_cover::bool list list
```
```  2981   => (nat => bool) => bool list)
```
```  2982                              l2 t))))))))"
```
```  2983   by (import prob_indep ALG_COVER_STEP)
```
```  2984
```
```  2985 lemma ALG_COVER_HEAD: "(All::(bool list list => bool) => bool)
```
```  2986  (%l::bool list list.
```
```  2987      (op -->::bool => bool => bool)
```
```  2988       ((alg_cover_set::bool list list => bool) l)
```
```  2989       ((All::((bool list => bool) => bool) => bool)
```
```  2990         (%f::bool list => bool.
```
```  2991             (op =::((nat => bool) => bool)
```
```  2992                    => ((nat => bool) => bool) => bool)
```
```  2993              ((op o::(bool list => bool)
```
```  2994                      => ((nat => bool) => bool list)
```
```  2995                         => (nat => bool) => bool)
```
```  2996                f ((alg_cover::bool list list => (nat => bool) => bool list)
```
```  2997                    l))
```
```  2998              ((algebra_embed::bool list list => (nat => bool) => bool)
```
```  2999                ((filter::(bool list => bool)
```
```  3000                          => bool list list => bool list list)
```
```  3001                  f l)))))"
```
```  3002   by (import prob_indep ALG_COVER_HEAD)
```
```  3003
```
```  3004 lemma ALG_COVER_TAIL_STEP: "(All::(bool list list => bool) => bool)
```
```  3005  (%l1::bool list list.
```
```  3006      (All::(bool list list => bool) => bool)
```
```  3007       (%l2::bool list list.
```
```  3008           (All::(((nat => bool) => bool) => bool) => bool)
```
```  3009            (%q::(nat => bool) => bool.
```
```  3010                (op -->::bool => bool => bool)
```
```  3011                 ((op &::bool => bool => bool)
```
```  3012                   ((alg_cover_set::bool list list => bool) l1)
```
```  3013                   ((alg_cover_set::bool list list => bool) l2))
```
```  3014                 ((op =::((nat => bool) => bool)
```
```  3015                         => ((nat => bool) => bool) => bool)
```
```  3016                   ((op o::((nat => bool) => bool)
```
```  3017                           => ((nat => bool) => nat => bool)
```
```  3018                              => (nat => bool) => bool)
```
```  3019                     q (%x::nat => bool.
```
```  3020                           (SDROP::nat => (nat => bool) => nat => bool)
```
```  3021                            ((size::bool list => nat)
```
```  3022                              ((alg_cover::bool list list
```
```  3023     => (nat => bool) => bool list)
```
```  3024                                ((op @::bool list list
```
```  3025  => bool list list => bool list list)
```
```  3026                                  ((map::(bool list => bool list)
```
```  3027   => bool list list => bool list list)
```
```  3028                                    ((op #::bool => bool list => bool list)
```
```  3029                                      (True::bool))
```
```  3030                                    l1)
```
```  3031                                  ((map::(bool list => bool list)
```
```  3032   => bool list list => bool list list)
```
```  3033                                    ((op #::bool => bool list => bool list)
```
```  3034                                      (False::bool))
```
```  3035                                    l2))
```
```  3036                                x))
```
```  3037                            x))
```
```  3038                   ((pred_set.UNION::((nat => bool) => bool)
```
```  3039                                     => ((nat => bool) => bool)
```
```  3040  => (nat => bool) => bool)
```
```  3041                     ((pred_set.INTER::((nat => bool) => bool)
```
```  3042 => ((nat => bool) => bool) => (nat => bool) => bool)
```
```  3043                       (%x::nat => bool.
```
```  3044                           (op =::bool => bool => bool)
```
```  3045                            ((SHD::(nat => bool) => bool) x) (True::bool))
```
```  3046                       ((op o::((nat => bool) => bool)
```
```  3047                               => ((nat => bool) => nat => bool)
```
```  3048                                  => (nat => bool) => bool)
```
```  3049                         q ((op o::((nat => bool) => nat => bool)
```
```  3050                                   => ((nat => bool) => nat => bool)
```
```  3051                                      => (nat => bool) => nat => bool)
```
```  3052                             (%x::nat => bool.
```
```  3053                                 (SDROP::nat => (nat => bool) => nat => bool)
```
```  3054                                  ((size::bool list => nat)
```
```  3055                                    ((alg_cover::bool list list
```
```  3056           => (nat => bool) => bool list)
```
```  3057                                      l1 x))
```
```  3058                                  x)
```
```  3059                             (STL::(nat => bool) => nat => bool))))
```
```  3060                     ((pred_set.INTER::((nat => bool) => bool)
```
```  3061 => ((nat => bool) => bool) => (nat => bool) => bool)
```
```  3062                       (%x::nat => bool.
```
```  3063                           (op =::bool => bool => bool)
```
```  3064                            ((SHD::(nat => bool) => bool) x) (False::bool))
```
```  3065                       ((op o::((nat => bool) => bool)
```
```  3066                               => ((nat => bool) => nat => bool)
```
```  3067                                  => (nat => bool) => bool)
```
```  3068                         q ((op o::((nat => bool) => nat => bool)
```
```  3069                                   => ((nat => bool) => nat => bool)
```
```  3070                                      => (nat => bool) => nat => bool)
```
```  3071                             (%x::nat => bool.
```
```  3072                                 (SDROP::nat => (nat => bool) => nat => bool)
```
```  3073                                  ((size::bool list => nat)
```
```  3074                                    ((alg_cover::bool list list
```
```  3075           => (nat => bool) => bool list)
```
```  3076                                      l2 x))
```
```  3077                                  x)
```
```  3078                             (STL::(nat => bool) => nat => bool)))))))))"
```
```  3079   by (import prob_indep ALG_COVER_TAIL_STEP)
```
```  3080
```
```  3081 lemma ALG_COVER_TAIL_MEASURABLE: "(All::(bool list list => bool) => bool)
```
```  3082  (%l::bool list list.
```
```  3083      (op -->::bool => bool => bool)
```
```  3084       ((alg_cover_set::bool list list => bool) l)
```
```  3085       ((All::(((nat => bool) => bool) => bool) => bool)
```
```  3086         (%q::(nat => bool) => bool.
```
```  3087             (op =::bool => bool => bool)
```
```  3088              ((measurable::((nat => bool) => bool) => bool)
```
```  3089                ((op o::((nat => bool) => bool)
```
```  3090                        => ((nat => bool) => nat => bool)
```
```  3091                           => (nat => bool) => bool)
```
```  3092                  q (%x::nat => bool.
```
```  3093                        (SDROP::nat => (nat => bool) => nat => bool)
```
```  3094                         ((size::bool list => nat)
```
```  3095                           ((alg_cover::bool list list
```
```  3096  => (nat => bool) => bool list)
```
```  3097                             l x))
```
```  3098                         x)))
```
```  3099              ((measurable::((nat => bool) => bool) => bool) q))))"
```
```  3100   by (import prob_indep ALG_COVER_TAIL_MEASURABLE)
```
```  3101
```
```  3102 lemma ALG_COVER_TAIL_PROB: "(All::(bool list list => bool) => bool)
```
```  3103  (%l::bool list list.
```
```  3104      (op -->::bool => bool => bool)
```
```  3105       ((alg_cover_set::bool list list => bool) l)
```
```  3106       ((All::(((nat => bool) => bool) => bool) => bool)
```
```  3107         (%q::(nat => bool) => bool.
```
```  3108             (op -->::bool => bool => bool)
```
```  3109              ((measurable::((nat => bool) => bool) => bool) q)
```
```  3110              ((op =::real => real => bool)
```
```  3111                ((prob::((nat => bool) => bool) => real)
```
```  3112                  ((op o::((nat => bool) => bool)
```
```  3113                          => ((nat => bool) => nat => bool)
```
```  3114                             => (nat => bool) => bool)
```
```  3115                    q (%x::nat => bool.
```
```  3116                          (SDROP::nat => (nat => bool) => nat => bool)
```
```  3117                           ((size::bool list => nat)
```
```  3118                             ((alg_cover::bool list list
```
```  3119    => (nat => bool) => bool list)
```
```  3120                               l x))
```
```  3121                           x)))
```
```  3122                ((prob::((nat => bool) => bool) => real) q)))))"
```
```  3123   by (import prob_indep ALG_COVER_TAIL_PROB)
```
```  3124
```
```  3125 lemma INDEP_INDEP_SET_LEMMA: "(All::(bool list list => bool) => bool)
```
```  3126  (%l::bool list list.
```
```  3127      (op -->::bool => bool => bool)
```
```  3128       ((alg_cover_set::bool list list => bool) l)
```
```  3129       ((All::(((nat => bool) => bool) => bool) => bool)
```
```  3130         (%q::(nat => bool) => bool.
```
```  3131             (op -->::bool => bool => bool)
```
```  3132              ((measurable::((nat => bool) => bool) => bool) q)
```
```  3133              ((All::(bool list => bool) => bool)
```
```  3134                (%x::bool list.
```
```  3135                    (op -->::bool => bool => bool)
```
```  3136                     ((op mem::bool list => bool list list => bool) x l)
```
```  3137                     ((op =::real => real => bool)
```
```  3138                       ((prob::((nat => bool) => bool) => real)
```
```  3139                         ((pred_set.INTER::((nat => bool) => bool)
```
```  3140     => ((nat => bool) => bool) => (nat => bool) => bool)
```
```  3141                           ((alg_embed::bool list => (nat => bool) => bool)
```
```  3142                             x)
```
```  3143                           ((op o::((nat => bool) => bool)
```
```  3144                                   => ((nat => bool) => nat => bool)
```
```  3145                                      => (nat => bool) => bool)
```
```  3146                             q (%x::nat => bool.
```
```  3147                                   (SDROP::nat
```
```  3148     => (nat => bool) => nat => bool)
```
```  3149                                    ((size::bool list => nat)
```
```  3150                                      ((alg_cover::bool list list
```
```  3151             => (nat => bool) => bool list)
```
```  3152  l x))
```
```  3153                                    x))))
```
```  3154                       ((op *::real => real => real)
```
```  3155                         ((op ^::real => nat => real)
```
```  3156                           ((op /::real => real => real) (1::real)
```
```  3157                             ((number_of::bin => real)
```
```  3158                               ((op BIT::bin => bool => bin)
```
```  3159                                 ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
```
```  3160                                   (True::bool))
```
```  3161                                 (False::bool))))
```
```  3162                           ((size::bool list => nat) x))
```
```  3163                         ((prob::((nat => bool) => bool) => real) q))))))))"
```
```  3164   by (import prob_indep INDEP_INDEP_SET_LEMMA)
```
```  3165
```
```  3166 lemma INDEP_SET_LIST: "(All::(((nat => bool) => bool) => bool) => bool)
```
```  3167  (%q::(nat => bool) => bool.
```
```  3168      (All::(bool list list => bool) => bool)
```
```  3169       (%l::bool list list.
```
```  3170           (op -->::bool => bool => bool)
```
```  3171            ((op &::bool => bool => bool)
```
```  3172              ((alg_sorted::bool list list => bool) l)
```
```  3173              ((op &::bool => bool => bool)
```
```  3174                ((alg_prefixfree::bool list list => bool) l)
```
```  3175                ((op &::bool => bool => bool)
```
```  3176                  ((measurable::((nat => bool) => bool) => bool) q)
```
```  3177                  ((All::(bool list => bool) => bool)
```
```  3178                    (%x::bool list.
```
```  3179                        (op -->::bool => bool => bool)
```
```  3180                         ((op mem::bool list => bool list list => bool) x l)
```
```  3181                         ((indep_set::((nat => bool) => bool)
```
```  3182                                      => ((nat => bool) => bool) => bool)
```
```  3183                           ((alg_embed::bool list => (nat => bool) => bool)
```
```  3184                             x)
```
```  3185                           q))))))
```
```  3186            ((indep_set::((nat => bool) => bool)
```
```  3187                         => ((nat => bool) => bool) => bool)
```
```  3188              ((algebra_embed::bool list list => (nat => bool) => bool) l)
```
```  3189              q)))"
```
```  3190   by (import prob_indep INDEP_SET_LIST)
```
```  3191
```
```  3192 lemma INDEP_INDEP_SET: "(All::(((nat => bool) => 'a * (nat => bool)) => bool) => bool)
```
```  3193  (%f::(nat => bool) => 'a * (nat => bool).
```
```  3194      (All::(('a => bool) => bool) => bool)
```
```  3195       (%p::'a => bool.
```
```  3196           (All::(((nat => bool) => bool) => bool) => bool)
```
```  3197            (%q::(nat => bool) => bool.
```
```  3198                (op -->::bool => bool => bool)
```
```  3199                 ((op &::bool => bool => bool)
```
```  3200                   ((indep::((nat => bool) => 'a * (nat => bool)) => bool) f)
```
```  3201                   ((measurable::((nat => bool) => bool) => bool) q))
```
```  3202                 ((indep_set::((nat => bool) => bool)
```
```  3203                              => ((nat => bool) => bool) => bool)
```
```  3204                   ((op o::('a => bool)
```
```  3205                           => ((nat => bool) => 'a) => (nat => bool) => bool)
```
```  3206                     p ((op o::('a * (nat => bool) => 'a)
```
```  3207                               => ((nat => bool) => 'a * (nat => bool))
```
```  3208                                  => (nat => bool) => 'a)
```
```  3209                         (fst::'a * (nat => bool) => 'a) f))
```
```  3210                   ((op o::((nat => bool) => bool)
```
```  3211                           => ((nat => bool) => nat => bool)
```
```  3212                              => (nat => bool) => bool)
```
```  3213                     q ((op o::('a * (nat => bool) => nat => bool)
```
```  3214                               => ((nat => bool) => 'a * (nat => bool))
```
```  3215                                  => (nat => bool) => nat => bool)
```
```  3216                         (snd::'a * (nat => bool) => nat => bool) f))))))"
```
```  3217   by (import prob_indep INDEP_INDEP_SET)
```
```  3218
```
```  3219 lemma INDEP_UNIT: "ALL x. indep (UNIT x)"
```
```  3220   by (import prob_indep INDEP_UNIT)
```
```  3221
```
```  3222 lemma INDEP_SDEST: "indep SDEST"
```
```  3223   by (import prob_indep INDEP_SDEST)
```
```  3224
```
```  3225 lemma BIND_STEP: "ALL f. BIND SDEST (%k. f o SCONS k) = f"
```
```  3226   by (import prob_indep BIND_STEP)
```
```  3227
```
```  3228 lemma INDEP_BIND_SDEST: "(All::((bool => (nat => bool) => 'a * (nat => bool)) => bool) => bool)
```
```  3229  (%f::bool => (nat => bool) => 'a * (nat => bool).
```
```  3230      (op -->::bool => bool => bool)
```
```  3231       ((All::(bool => bool) => bool)
```
```  3232         (%x::bool.
```
```  3233             (indep::((nat => bool) => 'a * (nat => bool)) => bool) (f x)))
```
```  3234       ((indep::((nat => bool) => 'a * (nat => bool)) => bool)
```
```  3235         ((BIND::((nat => bool) => bool * (nat => bool))
```
```  3236                 => (bool => (nat => bool) => 'a * (nat => bool))
```
```  3237                    => (nat => bool) => 'a * (nat => bool))
```
```  3238           (SDEST::(nat => bool) => bool * (nat => bool)) f)))"
```
```  3239   by (import prob_indep INDEP_BIND_SDEST)
```
```  3240
```
```  3241 lemma INDEP_BIND: "(All::(((nat => bool) => 'a * (nat => bool)) => bool) => bool)
```
```  3242  (%f::(nat => bool) => 'a * (nat => bool).
```
```  3243      (All::(('a => (nat => bool) => 'b * (nat => bool)) => bool) => bool)
```
```  3244       (%g::'a => (nat => bool) => 'b * (nat => bool).
```
```  3245           (op -->::bool => bool => bool)
```
```  3246            ((op &::bool => bool => bool)
```
```  3247              ((indep::((nat => bool) => 'a * (nat => bool)) => bool) f)
```
```  3248              ((All::('a => bool) => bool)
```
```  3249                (%x::'a.
```
```  3250                    (indep::((nat => bool) => 'b * (nat => bool)) => bool)
```
```  3251                     (g x))))
```
```  3252            ((indep::((nat => bool) => 'b * (nat => bool)) => bool)
```
```  3253              ((BIND::((nat => bool) => 'a * (nat => bool))
```
```  3254                      => ('a => (nat => bool) => 'b * (nat => bool))
```
```  3255                         => (nat => bool) => 'b * (nat => bool))
```
```  3256                f g))))"
```
```  3257   by (import prob_indep INDEP_BIND)
```
```  3258
```
```  3259 lemma INDEP_PROB: "(All::(((nat => bool) => 'a * (nat => bool)) => bool) => bool)
```
```  3260  (%f::(nat => bool) => 'a * (nat => bool).
```
```  3261      (All::(('a => bool) => bool) => bool)
```
```  3262       (%p::'a => bool.
```
```  3263           (All::(((nat => bool) => bool) => bool) => bool)
```
```  3264            (%q::(nat => bool) => bool.
```
```  3265                (op -->::bool => bool => bool)
```
```  3266                 ((op &::bool => bool => bool)
```
```  3267                   ((indep::((nat => bool) => 'a * (nat => bool)) => bool) f)
```
```  3268                   ((measurable::((nat => bool) => bool) => bool) q))
```
```  3269                 ((op =::real => real => bool)
```
```  3270                   ((prob::((nat => bool) => bool) => real)
```
```  3271                     ((pred_set.INTER::((nat => bool) => bool)
```
```  3272 => ((nat => bool) => bool) => (nat => bool) => bool)
```
```  3273                       ((op o::('a => bool)
```
```  3274                               => ((nat => bool) => 'a)
```
```  3275                                  => (nat => bool) => bool)
```
```  3276                         p ((op o::('a * (nat => bool) => 'a)
```
```  3277                                   => ((nat => bool) => 'a * (nat => bool))
```
```  3278                                      => (nat => bool) => 'a)
```
```  3279                             (fst::'a * (nat => bool) => 'a) f))
```
```  3280                       ((op o::((nat => bool) => bool)
```
```  3281                               => ((nat => bool) => nat => bool)
```
```  3282                                  => (nat => bool) => bool)
```
```  3283                         q ((op o::('a * (nat => bool) => nat => bool)
```
```  3284                                   => ((nat => bool) => 'a * (nat => bool))
```
```  3285                                      => (nat => bool) => nat => bool)
```
```  3286                             (snd::'a * (nat => bool) => nat => bool) f))))
```
```  3287                   ((op *::real => real => real)
```
```  3288                     ((prob::((nat => bool) => bool) => real)
```
```  3289                       ((op o::('a => bool)
```
```  3290                               => ((nat => bool) => 'a)
```
```  3291                                  => (nat => bool) => bool)
```
```  3292                         p ((op o::('a * (nat => bool) => 'a)
```
```  3293                                   => ((nat => bool) => 'a * (nat => bool))
```
```  3294                                      => (nat => bool) => 'a)
```
```  3295                             (fst::'a * (nat => bool) => 'a) f)))
```
```  3296                     ((prob::((nat => bool) => bool) => real) q))))))"
```
```  3297   by (import prob_indep INDEP_PROB)
```
```  3298
```
```  3299 lemma INDEP_MEASURABLE1: "(All::(((nat => bool) => 'a * (nat => bool)) => bool) => bool)
```
```  3300  (%f::(nat => bool) => 'a * (nat => bool).
```
```  3301      (All::(('a => bool) => bool) => bool)
```
```  3302       (%p::'a => bool.
```
```  3303           (op -->::bool => bool => bool)
```
```  3304            ((indep::((nat => bool) => 'a * (nat => bool)) => bool) f)
```
```  3305            ((measurable::((nat => bool) => bool) => bool)
```
```  3306              ((op o::('a => bool)
```
```  3307                      => ((nat => bool) => 'a) => (nat => bool) => bool)
```
```  3308                p ((op o::('a * (nat => bool) => 'a)
```
```  3309                          => ((nat => bool) => 'a * (nat => bool))
```
```  3310                             => (nat => bool) => 'a)
```
```  3311                    (fst::'a * (nat => bool) => 'a) f)))))"
```
```  3312   by (import prob_indep INDEP_MEASURABLE1)
```
```  3313
```
```  3314 lemma INDEP_MEASURABLE2: "(All::(((nat => bool) => 'a * (nat => bool)) => bool) => bool)
```
```  3315  (%f::(nat => bool) => 'a * (nat => bool).
```
```  3316      (All::(((nat => bool) => bool) => bool) => bool)
```
```  3317       (%q::(nat => bool) => bool.
```
```  3318           (op -->::bool => bool => bool)
```
```  3319            ((op &::bool => bool => bool)
```
```  3320              ((indep::((nat => bool) => 'a * (nat => bool)) => bool) f)
```
```  3321              ((measurable::((nat => bool) => bool) => bool) q))
```
```  3322            ((measurable::((nat => bool) => bool) => bool)
```
```  3323              ((op o::((nat => bool) => bool)
```
```  3324                      => ((nat => bool) => nat => bool)
```
```  3325                         => (nat => bool) => bool)
```
```  3326                q ((op o::('a * (nat => bool) => nat => bool)
```
```  3327                          => ((nat => bool) => 'a * (nat => bool))
```
```  3328                             => (nat => bool) => nat => bool)
```
```  3329                    (snd::'a * (nat => bool) => nat => bool) f)))))"
```
```  3330   by (import prob_indep INDEP_MEASURABLE2)
```
```  3331
```
```  3332 lemma PROB_INDEP_BOUND: "(All::(((nat => bool) => nat * (nat => bool)) => bool) => bool)
```
```  3333  (%f::(nat => bool) => nat * (nat => bool).
```
```  3334      (All::(nat => bool) => bool)
```
```  3335       (%n::nat.
```
```  3336           (op -->::bool => bool => bool)
```
```  3337            ((indep::((nat => bool) => nat * (nat => bool)) => bool) f)
```
```  3338            ((op =::real => real => bool)
```
```  3339              ((prob::((nat => bool) => bool) => real)
```
```  3340                (%s::nat => bool.
```
```  3341                    (op <::nat => nat => bool)
```
```  3342                     ((fst::nat * (nat => bool) => nat) (f s))
```
```  3343                     ((Suc::nat => nat) n)))
```
```  3344              ((op +::real => real => real)
```
```  3345                ((prob::((nat => bool) => bool) => real)
```
```  3346                  (%s::nat => bool.
```
```  3347                      (op <::nat => nat => bool)
```
```  3348                       ((fst::nat * (nat => bool) => nat) (f s)) n))
```
```  3349                ((prob::((nat => bool) => bool) => real)
```
```  3350                  (%s::nat => bool.
```
```  3351                      (op =::nat => nat => bool)
```
```  3352                       ((fst::nat * (nat => bool) => nat) (f s)) n))))))"
```
```  3353   by (import prob_indep PROB_INDEP_BOUND)
```
```  3354
```
```  3355 ;end_setup
```
```  3356
```
```  3357 ;setup_theory prob_uniform
```
```  3358
```
```  3359 consts
```
```  3360   unif_bound :: "nat => nat"
```
```  3361
```
```  3362 defs
```
```  3363   unif_bound_primdef: "unif_bound ==
```
```  3364 WFREC (SOME R. WF R & (ALL v. R (Suc v div 2) (Suc v)))
```
```  3365  (%unif_bound. nat_case 0 (%v1. Suc (unif_bound (Suc v1 div 2))))"
```
```  3366
```
```  3367 lemma unif_bound_primitive_def: "unif_bound =
```
```  3368 WFREC (SOME R. WF R & (ALL v. R (Suc v div 2) (Suc v)))
```
```  3369  (%unif_bound. nat_case 0 (%v1. Suc (unif_bound (Suc v1 div 2))))"
```
```  3370   by (import prob_uniform unif_bound_primitive_def)
```
```  3371
```
```  3372 lemma unif_bound_def: "unif_bound 0 = 0 & unif_bound (Suc v) = Suc (unif_bound (Suc v div 2))"
```
```  3373   by (import prob_uniform unif_bound_def)
```
```  3374
```
```  3375 lemma unif_bound_ind: "(All::((nat => bool) => bool) => bool)
```
```  3376  (%P::nat => bool.
```
```  3377      (op -->::bool => bool => bool)
```
```  3378       ((op &::bool => bool => bool) (P (0::nat))
```
```  3379         ((All::(nat => bool) => bool)
```
```  3380           (%v::nat.
```
```  3381               (op -->::bool => bool => bool)
```
```  3382                (P ((op div::nat => nat => nat) ((Suc::nat => nat) v)
```
```  3383                     ((number_of::bin => nat)
```
```  3384                       ((op BIT::bin => bool => bin)
```
```  3385                         ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
```
```  3386                           (True::bool))
```
```  3387                         (False::bool)))))
```
```  3388                (P ((Suc::nat => nat) v)))))
```
```  3389       ((All::(nat => bool) => bool) P))"
```
```  3390   by (import prob_uniform unif_bound_ind)
```
```  3391
```
```  3392 constdefs
```
```  3393   unif_tupled :: "nat * (nat => bool) => nat * (nat => bool)"
```
```  3394   "unif_tupled ==
```
```  3395 WFREC (SOME R. WF R & (ALL s v2. R (Suc v2 div 2, s) (Suc v2, s)))
```
```  3396  (%unif_tupled (v, v1).
```
```  3397      case v of 0 => (0, v1)
```
```  3398      | Suc v3 =>
```
```  3399          let (m, s') = unif_tupled (Suc v3 div 2, v1)
```
```  3400          in (if SHD s' then 2 * m + 1 else 2 * m, STL s'))"
```
```  3401
```
```  3402 lemma unif_tupled_primitive_def: "unif_tupled =
```
```  3403 WFREC (SOME R. WF R & (ALL s v2. R (Suc v2 div 2, s) (Suc v2, s)))
```
```  3404  (%unif_tupled (v, v1).
```
```  3405      case v of 0 => (0, v1)
```
```  3406      | Suc v3 =>
```
```  3407          let (m, s') = unif_tupled (Suc v3 div 2, v1)
```
```  3408          in (if SHD s' then 2 * m + 1 else 2 * m, STL s'))"
```
```  3409   by (import prob_uniform unif_tupled_primitive_def)
```
```  3410
```
```  3411 consts
```
```  3412   unif :: "nat => (nat => bool) => nat * (nat => bool)"
```
```  3413
```
```  3414 defs
```
```  3415   unif_primdef: "unif == %x x1. unif_tupled (x, x1)"
```
```  3416
```
```  3417 lemma unif_curried_def: "ALL x x1. unif x x1 = unif_tupled (x, x1)"
```
```  3418   by (import prob_uniform unif_curried_def)
```
```  3419
```
```  3420 lemma unif_def: "unif 0 s = (0, s) &
```
```  3421 unif (Suc v2) s =
```
```  3422 (let (m, s') = unif (Suc v2 div 2) s
```
```  3423  in (if SHD s' then 2 * m + 1 else 2 * m, STL s'))"
```
```  3424   by (import prob_uniform unif_def)
```
```  3425
```
```  3426 lemma unif_ind: "(All::((nat => (nat => bool) => bool) => bool) => bool)
```
```  3427  (%P::nat => (nat => bool) => bool.
```
```  3428      (op -->::bool => bool => bool)
```
```  3429       ((op &::bool => bool => bool)
```
```  3430         ((All::((nat => bool) => bool) => bool) (P (0::nat)))
```
```  3431         ((All::(nat => bool) => bool)
```
```  3432           (%v2::nat.
```
```  3433               (All::((nat => bool) => bool) => bool)
```
```  3434                (%s::nat => bool.
```
```  3435                    (op -->::bool => bool => bool)
```
```  3436                     (P ((op div::nat => nat => nat) ((Suc::nat => nat) v2)
```
```  3437                          ((number_of::bin => nat)
```
```  3438                            ((op BIT::bin => bool => bin)
```
```  3439                              ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
```
```  3440                                (True::bool))
```
```  3441                              (False::bool))))
```
```  3442                       s)
```
```  3443                     (P ((Suc::nat => nat) v2) s)))))
```
```  3444       ((All::(nat => bool) => bool)
```
```  3445         (%v::nat. (All::((nat => bool) => bool) => bool) (P v))))"
```
```  3446   by (import prob_uniform unif_ind)
```
```  3447
```
```  3448 constdefs
```
```  3449   uniform_tupled :: "nat * nat * (nat => bool) => nat * (nat => bool)"
```
```  3450   "(op ==::(nat * nat * (nat => bool) => nat * (nat => bool))
```
```  3451         => (nat * nat * (nat => bool) => nat * (nat => bool)) => prop)
```
```  3452  (uniform_tupled::nat * nat * (nat => bool) => nat * (nat => bool))
```
```  3453  ((WFREC::(nat * nat * (nat => bool) => nat * nat * (nat => bool) => bool)
```
```  3454           => ((nat * nat * (nat => bool) => nat * (nat => bool))
```
```  3455               => nat * nat * (nat => bool) => nat * (nat => bool))
```
```  3456              => nat * nat * (nat => bool) => nat * (nat => bool))
```
```  3457    ((Eps::((nat * nat * (nat => bool) => nat * nat * (nat => bool) => bool)
```
```  3458            => bool)
```
```  3459           => nat * nat * (nat => bool) => nat * nat * (nat => bool) => bool)
```
```  3460      (%R::nat * nat * (nat => bool) => nat * nat * (nat => bool) => bool.
```
```  3461          (op &::bool => bool => bool)
```
```  3462           ((WF::(nat * nat * (nat => bool)
```
```  3463                  => nat * nat * (nat => bool) => bool)
```
```  3464                 => bool)
```
```  3465             R)
```
```  3466           ((All::(nat => bool) => bool)
```
```  3467             (%t::nat.
```
```  3468                 (All::((nat => bool) => bool) => bool)
```
```  3469                  (%s::nat => bool.
```
```  3470                      (All::(nat => bool) => bool)
```
```  3471                       (%n::nat.
```
```  3472                           (All::(nat => bool) => bool)
```
```  3473                            (%res::nat.
```
```  3474                                (All::((nat => bool) => bool) => bool)
```
```  3475                                 (%s'::nat => bool.
```
```  3476                                     (op -->::bool => bool => bool)
```
```  3477                                      ((op &::bool => bool => bool)
```
```  3478  ((op =::nat * (nat => bool) => nat * (nat => bool) => bool)
```
```  3479    ((Pair::nat => (nat => bool) => nat * (nat => bool)) res s')
```
```  3480    ((unif::nat => (nat => bool) => nat * (nat => bool)) n s))
```
```  3481  ((Not::bool => bool)
```
```  3482    ((op <::nat => nat => bool) res ((Suc::nat => nat) n))))
```
```  3483                                      (R
```
```  3484  ((Pair::nat => nat * (nat => bool) => nat * nat * (nat => bool)) t
```
```  3485    ((Pair::nat => (nat => bool) => nat * (nat => bool))
```
```  3486      ((Suc::nat => nat) n) s'))
```
```  3487  ((Pair::nat => nat * (nat => bool) => nat * nat * (nat => bool))
```
```  3488    ((Suc::nat => nat) t)
```
```  3489    ((Pair::nat => (nat => bool) => nat * (nat => bool))
```
```  3490      ((Suc::nat => nat) n) s)))))))))))
```
```  3491    (%uniform_tupled::nat * nat * (nat => bool) => nat * (nat => bool).
```
```  3492        (split::(nat => nat * (nat => bool) => nat * (nat => bool))
```
```  3493                => nat * nat * (nat => bool) => nat * (nat => bool))
```
```  3494         (%(v::nat) v1::nat * (nat => bool).
```
```  3495             (nat_case::nat * (nat => bool)
```
```  3496                        => (nat => nat * (nat => bool))
```
```  3497                           => nat => nat * (nat => bool))
```
```  3498              ((split::(nat => (nat => bool) => nat * (nat => bool))
```
```  3499                       => nat * (nat => bool) => nat * (nat => bool))
```
```  3500                (%(v3::nat) v4::nat => bool.
```
```  3501                    (nat_case::nat * (nat => bool)
```
```  3502                               => (nat => nat * (nat => bool))
```
```  3503                                  => nat => nat * (nat => bool))
```
```  3504                     (ARB::nat * (nat => bool))
```
```  3505                     (%v5::nat.
```
```  3506                         (Pair::nat => (nat => bool) => nat * (nat => bool))
```
```  3507                          (0::nat) v4)
```
```  3508                     v3)
```
```  3509                v1)
```
```  3510              (%v2::nat.
```
```  3511                  (split::(nat => (nat => bool) => nat * (nat => bool))
```
```  3512                          => nat * (nat => bool) => nat * (nat => bool))
```
```  3513                   (%(v7::nat) v8::nat => bool.
```
```  3514                       (nat_case::nat * (nat => bool)
```
```  3515                                  => (nat => nat * (nat => bool))
```
```  3516                                     => nat => nat * (nat => bool))
```
```  3517                        (ARB::nat * (nat => bool))
```
```  3518                        (%v9::nat.
```
```  3519                            (Let::nat * (nat => bool)
```
```  3520                                  => (nat * (nat => bool)
```
```  3521                                      => nat * (nat => bool))
```
```  3522                                     => nat * (nat => bool))
```
```  3523                             ((unif::nat
```
```  3524                                     => (nat => bool) => nat * (nat => bool))
```
```  3525                               v9 v8)
```
```  3526                             ((split::(nat
```
```  3527 => (nat => bool) => nat * (nat => bool))
```
```  3528                                      => nat * (nat => bool)
```
```  3529   => nat * (nat => bool))
```
```  3530                               (%(res::nat) s'::nat => bool.
```
```  3531                                   (If::bool
```
```  3532  => nat * (nat => bool) => nat * (nat => bool) => nat * (nat => bool))
```
```  3533                                    ((op <::nat => nat => bool) res
```
```  3534                                      ((Suc::nat => nat) v9))
```
```  3535                                    ((Pair::nat
```
```  3536      => (nat => bool) => nat * (nat => bool))
```
```  3537                                      res s')
```
```  3538                                    (uniform_tupled
```
```  3539                                      ((Pair::nat
```
```  3540        => nat * (nat => bool) => nat * nat * (nat => bool))
```
```  3541  v2 ((Pair::nat => (nat => bool) => nat * (nat => bool))
```
```  3542       ((Suc::nat => nat) v9) s'))))))
```
```  3543                        v7)
```
```  3544                   v1)
```
```  3545              v)))"
```
```  3546
```
```  3547 lemma uniform_tupled_primitive_def: "(op =::(nat * nat * (nat => bool) => nat * (nat => bool))
```
```  3548        => (nat * nat * (nat => bool) => nat * (nat => bool)) => bool)
```
```  3549  (uniform_tupled::nat * nat * (nat => bool) => nat * (nat => bool))
```
```  3550  ((WFREC::(nat * nat * (nat => bool) => nat * nat * (nat => bool) => bool)
```
```  3551           => ((nat * nat * (nat => bool) => nat * (nat => bool))
```
```  3552               => nat * nat * (nat => bool) => nat * (nat => bool))
```
```  3553              => nat * nat * (nat => bool) => nat * (nat => bool))
```
```  3554    ((Eps::((nat * nat * (nat => bool) => nat * nat * (nat => bool) => bool)
```
```  3555            => bool)
```
```  3556           => nat * nat * (nat => bool) => nat * nat * (nat => bool) => bool)
```
```  3557      (%R::nat * nat * (nat => bool) => nat * nat * (nat => bool) => bool.
```
```  3558          (op &::bool => bool => bool)
```
```  3559           ((WF::(nat * nat * (nat => bool)
```
```  3560                  => nat * nat * (nat => bool) => bool)
```
```  3561                 => bool)
```
```  3562             R)
```
```  3563           ((All::(nat => bool) => bool)
```
```  3564             (%t::nat.
```
```  3565                 (All::((nat => bool) => bool) => bool)
```
```  3566                  (%s::nat => bool.
```
```  3567                      (All::(nat => bool) => bool)
```
```  3568                       (%n::nat.
```
```  3569                           (All::(nat => bool) => bool)
```
```  3570                            (%res::nat.
```
```  3571                                (All::((nat => bool) => bool) => bool)
```
```  3572                                 (%s'::nat => bool.
```
```  3573                                     (op -->::bool => bool => bool)
```
```  3574                                      ((op &::bool => bool => bool)
```
```  3575  ((op =::nat * (nat => bool) => nat * (nat => bool) => bool)
```
```  3576    ((Pair::nat => (nat => bool) => nat * (nat => bool)) res s')
```
```  3577    ((unif::nat => (nat => bool) => nat * (nat => bool)) n s))
```
```  3578  ((Not::bool => bool)
```
```  3579    ((op <::nat => nat => bool) res ((Suc::nat => nat) n))))
```
```  3580                                      (R
```
```  3581  ((Pair::nat => nat * (nat => bool) => nat * nat * (nat => bool)) t
```
```  3582    ((Pair::nat => (nat => bool) => nat * (nat => bool))
```
```  3583      ((Suc::nat => nat) n) s'))
```
```  3584  ((Pair::nat => nat * (nat => bool) => nat * nat * (nat => bool))
```
```  3585    ((Suc::nat => nat) t)
```
```  3586    ((Pair::nat => (nat => bool) => nat * (nat => bool))
```
```  3587      ((Suc::nat => nat) n) s)))))))))))
```
```  3588    (%uniform_tupled::nat * nat * (nat => bool) => nat * (nat => bool).
```
```  3589        (split::(nat => nat * (nat => bool) => nat * (nat => bool))
```
```  3590                => nat * nat * (nat => bool) => nat * (nat => bool))
```
```  3591         (%(v::nat) v1::nat * (nat => bool).
```
```  3592             (nat_case::nat * (nat => bool)
```
```  3593                        => (nat => nat * (nat => bool))
```
```  3594                           => nat => nat * (nat => bool))
```
```  3595              ((split::(nat => (nat => bool) => nat * (nat => bool))
```
```  3596                       => nat * (nat => bool) => nat * (nat => bool))
```
```  3597                (%(v3::nat) v4::nat => bool.
```
```  3598                    (nat_case::nat * (nat => bool)
```
```  3599                               => (nat => nat * (nat => bool))
```
```  3600                                  => nat => nat * (nat => bool))
```
```  3601                     (ARB::nat * (nat => bool))
```
```  3602                     (%v5::nat.
```
```  3603                         (Pair::nat => (nat => bool) => nat * (nat => bool))
```
```  3604                          (0::nat) v4)
```
```  3605                     v3)
```
```  3606                v1)
```
```  3607              (%v2::nat.
```
```  3608                  (split::(nat => (nat => bool) => nat * (nat => bool))
```
```  3609                          => nat * (nat => bool) => nat * (nat => bool))
```
```  3610                   (%(v7::nat) v8::nat => bool.
```
```  3611                       (nat_case::nat * (nat => bool)
```
```  3612                                  => (nat => nat * (nat => bool))
```
```  3613                                     => nat => nat * (nat => bool))
```
```  3614                        (ARB::nat * (nat => bool))
```
```  3615                        (%v9::nat.
```
```  3616                            (Let::nat * (nat => bool)
```
```  3617                                  => (nat * (nat => bool)
```
```  3618                                      => nat * (nat => bool))
```
```  3619                                     => nat * (nat => bool))
```
```  3620                             ((unif::nat
```
```  3621                                     => (nat => bool) => nat * (nat => bool))
```
```  3622                               v9 v8)
```
```  3623                             ((split::(nat
```
```  3624 => (nat => bool) => nat * (nat => bool))
```
```  3625                                      => nat * (nat => bool)
```
```  3626   => nat * (nat => bool))
```
```  3627                               (%(res::nat) s'::nat => bool.
```
```  3628                                   (If::bool
```
```  3629  => nat * (nat => bool) => nat * (nat => bool) => nat * (nat => bool))
```
```  3630                                    ((op <::nat => nat => bool) res
```
```  3631                                      ((Suc::nat => nat) v9))
```
```  3632                                    ((Pair::nat
```
```  3633      => (nat => bool) => nat * (nat => bool))
```
```  3634                                      res s')
```
```  3635                                    (uniform_tupled
```
```  3636                                      ((Pair::nat
```
```  3637        => nat * (nat => bool) => nat * nat * (nat => bool))
```
```  3638  v2 ((Pair::nat => (nat => bool) => nat * (nat => bool))
```
```  3639       ((Suc::nat => nat) v9) s'))))))
```
```  3640                        v7)
```
```  3641                   v1)
```
```  3642              v)))"
```
```  3643   by (import prob_uniform uniform_tupled_primitive_def)
```
```  3644
```
```  3645 consts
```
```  3646   uniform :: "nat => nat => (nat => bool) => nat * (nat => bool)"
```
```  3647
```
```  3648 defs
```
```  3649   uniform_primdef: "uniform == %x x1 x2. uniform_tupled (x, x1, x2)"
```
```  3650
```
```  3651 lemma uniform_curried_def: "ALL x x1 x2. uniform x x1 x2 = uniform_tupled (x, x1, x2)"
```
```  3652   by (import prob_uniform uniform_curried_def)
```
```  3653
```
```  3654 lemma uniform_ind: "(All::((nat => nat => (nat => bool) => bool) => bool) => bool)
```
```  3655  (%P::nat => nat => (nat => bool) => bool.
```
```  3656      (op -->::bool => bool => bool)
```
```  3657       ((op &::bool => bool => bool)
```
```  3658         ((All::(nat => bool) => bool)
```
```  3659           (%x::nat.
```
```  3660               (All::((nat => bool) => bool) => bool)
```
```  3661                (P ((Suc::nat => nat) x) (0::nat))))
```
```  3662         ((op &::bool => bool => bool)
```
```  3663           ((All::((nat => bool) => bool) => bool) (P (0::nat) (0::nat)))
```
```  3664           ((op &::bool => bool => bool)
```
```  3665             ((All::(nat => bool) => bool)
```
```  3666               (%x::nat.
```
```  3667                   (All::((nat => bool) => bool) => bool)
```
```  3668                    (P (0::nat) ((Suc::nat => nat) x))))
```
```  3669             ((All::(nat => bool) => bool)
```
```  3670               (%x::nat.
```
```  3671                   (All::(nat => bool) => bool)
```
```  3672                    (%xa::nat.
```
```  3673                        (All::((nat => bool) => bool) => bool)
```
```  3674                         (%xb::nat => bool.
```
```  3675                             (op -->::bool => bool => bool)
```
```  3676                              ((All::(nat => bool) => bool)
```
```  3677                                (%xc::nat.
```
```  3678                                    (All::((nat => bool) => bool) => bool)
```
```  3679                                     (%xd::nat => bool.
```
```  3680   (op -->::bool => bool => bool)
```
```  3681    ((op &::bool => bool => bool)
```
```  3682      ((op =::nat * (nat => bool) => nat * (nat => bool) => bool)
```
```  3683        ((Pair::nat => (nat => bool) => nat * (nat => bool)) xc xd)
```
```  3684        ((unif::nat => (nat => bool) => nat * (nat => bool)) xa xb))
```
```  3685      ((Not::bool => bool)
```
```  3686        ((op <::nat => nat => bool) xc ((Suc::nat => nat) xa))))
```
```  3687    (P x ((Suc::nat => nat) xa) xd))))
```
```  3688                              (P ((Suc::nat => nat) x) ((Suc::nat => nat) xa)
```
```  3689                                xb))))))))
```
```  3690       ((All::(nat => bool) => bool)
```
```  3691         (%x::nat.
```
```  3692             (All::(nat => bool) => bool)
```
```  3693              (%xa::nat. (All::((nat => bool) => bool) => bool) (P x xa)))))"
```
```  3694   by (import prob_uniform uniform_ind)
```
```  3695
```
```  3696 lemma uniform_def: "uniform 0 (Suc n) s = (0, s) &
```
```  3697 uniform (Suc t) (Suc n) s =
```
```  3698 (let (xa, x) = unif n s
```
```  3699  in if xa < Suc n then (xa, x) else uniform t (Suc n) x)"
```
```  3700   by (import prob_uniform uniform_def)
```
```  3701
```
```  3702 lemma SUC_DIV_TWO_ZERO: "ALL n. (Suc n div 2 = 0) = (n = 0)"
```
```  3703   by (import prob_uniform SUC_DIV_TWO_ZERO)
```
```  3704
```
```  3705 lemma UNIF_BOUND_LOWER: "ALL n. n < 2 ^ unif_bound n"
```
```  3706   by (import prob_uniform UNIF_BOUND_LOWER)
```
```  3707
```
```  3708 lemma UNIF_BOUND_LOWER_SUC: "ALL n. Suc n <= 2 ^ unif_bound n"
```
```  3709   by (import prob_uniform UNIF_BOUND_LOWER_SUC)
```
```  3710
```
```  3711 lemma UNIF_BOUND_UPPER: "(All::(nat => bool) => bool)
```
```  3712  (%n::nat.
```
```  3713      (op -->::bool => bool => bool)
```
```  3714       ((Not::bool => bool) ((op =::nat => nat => bool) n (0::nat)))
```
```  3715       ((op <=::nat => nat => bool)
```
```  3716         ((op ^::nat => nat => nat)
```
```  3717           ((number_of::bin => nat)
```
```  3718             ((op BIT::bin => bool => bin)
```
```  3719               ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
```
```  3720               (False::bool)))
```
```  3721           ((unif_bound::nat => nat) n))
```
```  3722         ((op *::nat => nat => nat)
```
```  3723           ((number_of::bin => nat)
```
```  3724             ((op BIT::bin => bool => bin)
```
```  3725               ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
```
```  3726               (False::bool)))
```
```  3727           n)))"
```
```  3728   by (import prob_uniform UNIF_BOUND_UPPER)
```
```  3729
```
```  3730 lemma UNIF_BOUND_UPPER_SUC: "ALL n. 2 ^ unif_bound n <= Suc (2 * n)"
```
```  3731   by (import prob_uniform UNIF_BOUND_UPPER_SUC)
```
```  3732
```
```  3733 lemma UNIF_DEF_MONAD: "unif 0 = UNIT 0 &
```
```  3734 (ALL n.
```
```  3735     unif (Suc n) =
```
```  3736     BIND (unif (Suc n div 2))
```
```  3737      (%m. BIND SDEST (%b. UNIT (if b then 2 * m + 1 else 2 * m))))"
```
```  3738   by (import prob_uniform UNIF_DEF_MONAD)
```
```  3739
```
```  3740 lemma UNIFORM_DEF_MONAD: "(ALL x. uniform 0 (Suc x) = UNIT 0) &
```
```  3741 (ALL x xa.
```
```  3742     uniform (Suc x) (Suc xa) =
```
```  3743     BIND (unif xa) (%m. if m < Suc xa then UNIT m else uniform x (Suc xa)))"
```
```  3744   by (import prob_uniform UNIFORM_DEF_MONAD)
```
```  3745
```
```  3746 lemma INDEP_UNIF: "ALL n. indep (unif n)"
```
```  3747   by (import prob_uniform INDEP_UNIF)
```
```  3748
```
```  3749 lemma INDEP_UNIFORM: "ALL t n. indep (uniform t (Suc n))"
```
```  3750   by (import prob_uniform INDEP_UNIFORM)
```
```  3751
```
```  3752 lemma PROB_UNIF: "ALL n k.
```
```  3753    prob (%s. fst (unif n s) = k) =
```
```  3754    (if k < 2 ^ unif_bound n then (1 / 2) ^ unif_bound n else 0)"
```
```  3755   by (import prob_uniform PROB_UNIF)
```
```  3756
```
```  3757 lemma UNIF_RANGE: "ALL n s. fst (unif n s) < 2 ^ unif_bound n"
```
```  3758   by (import prob_uniform UNIF_RANGE)
```
```  3759
```
```  3760 lemma PROB_UNIF_PAIR: "ALL n k k'.
```
```  3761    (prob (%s. fst (unif n s) = k) = prob (%s. fst (unif n s) = k')) =
```
```  3762    ((k < 2 ^ unif_bound n) = (k' < 2 ^ unif_bound n))"
```
```  3763   by (import prob_uniform PROB_UNIF_PAIR)
```
```  3764
```
```  3765 lemma PROB_UNIF_BOUND: "(All::(nat => bool) => bool)
```
```  3766  (%n::nat.
```
```  3767      (All::(nat => bool) => bool)
```
```  3768       (%k::nat.
```
```  3769           (op -->::bool => bool => bool)
```
```  3770            ((op <=::nat => nat => bool) k
```
```  3771              ((op ^::nat => nat => nat)
```
```  3772                ((number_of::bin => nat)
```
```  3773                  ((op BIT::bin => bool => bin)
```
```  3774                    ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
```
```  3775                      (True::bool))
```
```  3776                    (False::bool)))
```
```  3777                ((unif_bound::nat => nat) n)))
```
```  3778            ((op =::real => real => bool)
```
```  3779              ((prob::((nat => bool) => bool) => real)
```
```  3780                (%s::nat => bool.
```
```  3781                    (op <::nat => nat => bool)
```
```  3782                     ((fst::nat * (nat => bool) => nat)
```
```  3783                       ((unif::nat => (nat => bool) => nat * (nat => bool)) n
```
```  3784                         s))
```
```  3785                     k))
```
```  3786              ((op *::real => real => real) ((real::nat => real) k)
```
```  3787                ((op ^::real => nat => real)
```
```  3788                  ((op /::real => real => real) (1::real)
```
```  3789                    ((number_of::bin => real)
```
```  3790                      ((op BIT::bin => bool => bin)
```
```  3791                        ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
```
```  3792                          (True::bool))
```
```  3793                        (False::bool))))
```
```  3794                  ((unif_bound::nat => nat) n))))))"
```
```  3795   by (import prob_uniform PROB_UNIF_BOUND)
```
```  3796
```
```  3797 lemma PROB_UNIF_GOOD: "ALL n. 1 / 2 <= prob (%s. fst (unif n s) < Suc n)"
```
```  3798   by (import prob_uniform PROB_UNIF_GOOD)
```
```  3799
```
```  3800 lemma UNIFORM_RANGE: "ALL t n s. fst (uniform t (Suc n) s) < Suc n"
```
```  3801   by (import prob_uniform UNIFORM_RANGE)
```
```  3802
```
```  3803 lemma PROB_UNIFORM_LOWER_BOUND: "(All::(real => bool) => bool)
```
```  3804  (%b::real.
```
```  3805      (op -->::bool => bool => bool)
```
```  3806       ((All::(nat => bool) => bool)
```
```  3807         (%k::nat.
```
```  3808             (op -->::bool => bool => bool)
```
```  3809              ((op <::nat => nat => bool) k ((Suc::nat => nat) (n::nat)))
```
```  3810              ((op <::real => real => bool)
```
```  3811                ((prob::((nat => bool) => bool) => real)
```
```  3812                  (%s::nat => bool.
```
```  3813                      (op =::nat => nat => bool)
```
```  3814                       ((fst::nat * (nat => bool) => nat)
```
```  3815                         ((uniform::nat
```
```  3816                                    => nat
```
```  3817 => (nat => bool) => nat * (nat => bool))
```
```  3818                           (t::nat) ((Suc::nat => nat) n) s))
```
```  3819                       k))
```
```  3820                b)))
```
```  3821       ((All::(nat => bool) => bool)
```
```  3822         (%m::nat.
```
```  3823             (op -->::bool => bool => bool)
```
```  3824              ((op <::nat => nat => bool) m ((Suc::nat => nat) n))
```
```  3825              ((op <::real => real => bool)
```
```  3826                ((prob::((nat => bool) => bool) => real)
```
```  3827                  (%s::nat => bool.
```
```  3828                      (op <::nat => nat => bool)
```
```  3829                       ((fst::nat * (nat => bool) => nat)
```
```  3830                         ((uniform::nat
```
```  3831                                    => nat
```
```  3832 => (nat => bool) => nat * (nat => bool))
```
```  3833                           t ((Suc::nat => nat) n) s))
```
```  3834                       ((Suc::nat => nat) m)))
```
```  3835                ((op *::real => real => real)
```
```  3836                  ((real::nat => real) ((Suc::nat => nat) m)) b)))))"
```
```  3837   by (import prob_uniform PROB_UNIFORM_LOWER_BOUND)
```
```  3838
```
```  3839 lemma PROB_UNIFORM_UPPER_BOUND: "(All::(real => bool) => bool)
```
```  3840  (%b::real.
```
```  3841      (op -->::bool => bool => bool)
```
```  3842       ((All::(nat => bool) => bool)
```
```  3843         (%k::nat.
```
```  3844             (op -->::bool => bool => bool)
```
```  3845              ((op <::nat => nat => bool) k ((Suc::nat => nat) (n::nat)))
```
```  3846              ((op <::real => real => bool) b
```
```  3847                ((prob::((nat => bool) => bool) => real)
```
```  3848                  (%s::nat => bool.
```
```  3849                      (op =::nat => nat => bool)
```
```  3850                       ((fst::nat * (nat => bool) => nat)
```
```  3851                         ((uniform::nat
```
```  3852                                    => nat
```
```  3853 => (nat => bool) => nat * (nat => bool))
```
```  3854                           (t::nat) ((Suc::nat => nat) n) s))
```
```  3855                       k)))))
```
```  3856       ((All::(nat => bool) => bool)
```
```  3857         (%m::nat.
```
```  3858             (op -->::bool => bool => bool)
```
```  3859              ((op <::nat => nat => bool) m ((Suc::nat => nat) n))
```
```  3860              ((op <::real => real => bool)
```
```  3861                ((op *::real => real => real)
```
```  3862                  ((real::nat => real) ((Suc::nat => nat) m)) b)
```
```  3863                ((prob::((nat => bool) => bool) => real)
```
```  3864                  (%s::nat => bool.
```
```  3865                      (op <::nat => nat => bool)
```
```  3866                       ((fst::nat * (nat => bool) => nat)
```
```  3867                         ((uniform::nat
```
```  3868                                    => nat
```
```  3869 => (nat => bool) => nat * (nat => bool))
```
```  3870                           t ((Suc::nat => nat) n) s))
```
```  3871                       ((Suc::nat => nat) m)))))))"
```
```  3872   by (import prob_uniform PROB_UNIFORM_UPPER_BOUND)
```
```  3873
```
```  3874 lemma PROB_UNIFORM_PAIR_SUC: "(All::(nat => bool) => bool)
```
```  3875  (%t::nat.
```
```  3876      (All::(nat => bool) => bool)
```
```  3877       (%n::nat.
```
```  3878           (All::(nat => bool) => bool)
```
```  3879            (%k::nat.
```
```  3880                (All::(nat => bool) => bool)
```
```  3881                 (%k'::nat.
```
```  3882                     (op -->::bool => bool => bool)
```
```  3883                      ((op &::bool => bool => bool)
```
```  3884                        ((op <::nat => nat => bool) k ((Suc::nat => nat) n))
```
```  3885                        ((op <::nat => nat => bool) k'
```
```  3886                          ((Suc::nat => nat) n)))
```
```  3887                      ((op <=::real => real => bool)
```
```  3888                        ((abs::real => real)
```
```  3889                          ((op -::real => real => real)
```
```  3890                            ((prob::((nat => bool) => bool) => real)
```
```  3891                              (%s::nat => bool.
```
```  3892                                  (op =::nat => nat => bool)
```
```  3893                                   ((fst::nat * (nat => bool) => nat)
```
```  3894                                     ((uniform::nat
```
```  3895          => nat => (nat => bool) => nat * (nat => bool))
```
```  3896 t ((Suc::nat => nat) n) s))
```
```  3897                                   k))
```
```  3898                            ((prob::((nat => bool) => bool) => real)
```
```  3899                              (%s::nat => bool.
```
```  3900                                  (op =::nat => nat => bool)
```
```  3901                                   ((fst::nat * (nat => bool) => nat)
```
```  3902                                     ((uniform::nat
```
```  3903          => nat => (nat => bool) => nat * (nat => bool))
```
```  3904 t ((Suc::nat => nat) n) s))
```
```  3905                                   k'))))
```
```  3906                        ((op ^::real => nat => real)
```
```  3907                          ((op /::real => real => real) (1::real)
```
```  3908                            ((number_of::bin => real)
```
```  3909                              ((op BIT::bin => bool => bin)
```
```  3910                                ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
```
```  3911                                  (True::bool))
```
```  3912                                (False::bool))))
```
```  3913                          t))))))"
```
```  3914   by (import prob_uniform PROB_UNIFORM_PAIR_SUC)
```
```  3915
```
```  3916 lemma PROB_UNIFORM_SUC: "(All::(nat => bool) => bool)
```
```  3917  (%t::nat.
```
```  3918      (All::(nat => bool) => bool)
```
```  3919       (%n::nat.
```
```  3920           (All::(nat => bool) => bool)
```
```  3921            (%k::nat.
```
```  3922                (op -->::bool => bool => bool)
```
```  3923                 ((op <::nat => nat => bool) k ((Suc::nat => nat) n))
```
```  3924                 ((op <=::real => real => bool)
```
```  3925                   ((abs::real => real)
```
```  3926                     ((op -::real => real => real)
```
```  3927                       ((prob::((nat => bool) => bool) => real)
```
```  3928                         (%s::nat => bool.
```
```  3929                             (op =::nat => nat => bool)
```
```  3930                              ((fst::nat * (nat => bool) => nat)
```
```  3931                                ((uniform::nat
```
```  3932     => nat => (nat => bool) => nat * (nat => bool))
```
```  3933                                  t ((Suc::nat => nat) n) s))
```
```  3934                              k))
```
```  3935                       ((op /::real => real => real) (1::real)
```
```  3936                         ((real::nat => real) ((Suc::nat => nat) n)))))
```
```  3937                   ((op ^::real => nat => real)
```
```  3938                     ((op /::real => real => real) (1::real)
```
```  3939                       ((number_of::bin => real)
```
```  3940                         ((op BIT::bin => bool => bin)
```
```  3941                           ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
```
```  3942                             (True::bool))
```
```  3943                           (False::bool))))
```
```  3944                     t)))))"
```
```  3945   by (import prob_uniform PROB_UNIFORM_SUC)
```
```  3946
```
```  3947 lemma PROB_UNIFORM: "(All::(nat => bool) => bool)
```
```  3948  (%t::nat.
```
```  3949      (All::(nat => bool) => bool)
```
```  3950       (%n::nat.
```
```  3951           (All::(nat => bool) => bool)
```
```  3952            (%k::nat.
```
```  3953                (op -->::bool => bool => bool)
```
```  3954                 ((op <::nat => nat => bool) k n)
```
```  3955                 ((op <=::real => real => bool)
```
```  3956                   ((abs::real => real)
```
```  3957                     ((op -::real => real => real)
```
```  3958                       ((prob::((nat => bool) => bool) => real)
```
```  3959                         (%s::nat => bool.
```
```  3960                             (op =::nat => nat => bool)
```
```  3961                              ((fst::nat * (nat => bool) => nat)
```
```  3962                                ((uniform::nat
```
```  3963     => nat => (nat => bool) => nat * (nat => bool))
```
```  3964                                  t n s))
```
```  3965                              k))
```
```  3966                       ((op /::real => real => real) (1::real)
```
```  3967                         ((real::nat => real) n))))
```
```  3968                   ((op ^::real => nat => real)
```
```  3969                     ((op /::real => real => real) (1::real)
```
```  3970                       ((number_of::bin => real)
```
```  3971                         ((op BIT::bin => bool => bin)
```
```  3972                           ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
```
```  3973                             (True::bool))
```
```  3974                           (False::bool))))
```
```  3975                     t)))))"
```
```  3976   by (import prob_uniform PROB_UNIFORM)
```
```  3977
```
```  3978 ;end_setup
```
```  3979
```
```  3980 end
```
```  3981
```