Theory Omega

⊢ ∀x. fst1 x ⇔ (FST x = 1)

⊢ ∀x. fst_nzero x ⇔ 0 < FST x

⊢ ∀x y. modhat x y = x − y * ((2 * x + y) / (2 * y))

⊢ (∀lowers. real_shadow [] lowers ⇔ T) ∧
  ∀upper ls lowers.
    real_shadow (upper::ls) lowers ⇔
    rshadow_row upper lowers ∧ real_shadow ls lowers

⊢ (∀pad f. MAP2 pad f [] [] = []) ∧
  (∀ys y pad f. MAP2 pad f [] (y::ys) = f pad y::MAP2 pad f [] ys) ∧
  (∀xs x pad f. MAP2 pad f (x::xs) [] = f x pad::MAP2 pad f xs []) ∧
  ∀ys y xs x pad f. MAP2 pad f (x::xs) (y::ys) = f x y::MAP2 pad f xs ys

⊢ ∀P. (∀pad f. P pad f [] []) ∧
      (∀pad f y ys. P pad f [] ys ⇒ P pad f [] (y::ys)) ∧
      (∀pad f x xs. P pad f xs [] ⇒ P pad f (x::xs) []) ∧
      (∀pad f x xs y ys. P pad f xs ys ⇒ P pad f (x::xs) (y::ys)) ⇒
      ∀v v1 v2 v3. P v v1 v2 v3

⊢ ∀xs. (MAP2 0 $+ [] xs = xs) ∧ (MAP2 0 $+ xs [] = xs)

⊢ ∀uppers lowers m.
    EVERY fst_nzero uppers ∧ EVERY fst_nzero lowers ∧
    EVERY (λp. FST p ≤ m) uppers ⇒
    ((∃x. evalupper x uppers ∧ evallower x lowers) ⇔
     dark_shadow uppers lowers ∨ ∃x. nightmare x m uppers lowers lowers)

⊢ ∀uppers lowers.
    EVERY fst_nzero uppers ∧ EVERY fst_nzero lowers ⇒
    ((∃x. evalupper x uppers ∧ evallower x lowers) ⇔
     real_shadow uppers lowers ∧ dark_shadow_condition uppers lowers)

⊢ ∀lowers x y. evallower x lowers ∧ x < y ⇒ evallower y lowers

⊢ (∀x c. calc_nightmare x c [] ⇔ F) ∧
  ∀x rs d c R.
    calc_nightmare x c ((d,R)::rs) ⇔
    (∃i. (0 ≤ i ∧ i ≤ (&c * &d − &c − &d) / &c) ∧ (&d * x = R + i)) ∨
    calc_nightmare x c rs

⊢ ∀P. (∀x c. P x c []) ∧ (∀x c d R rs. P x c rs ⇒ P x c ((d,R)::rs)) ⇒
      ∀v v1 v2. P v v1 v2

⊢ ∀rs.
    nightmare x c uppers lowers rs ⇔
    calc_nightmare x c rs ∧ evalupper x uppers ∧ evallower x lowers

⊢ ∀uppers lowers.
    EVERY fst_nzero uppers ∧ EVERY fst_nzero lowers ∧
    dark_shadow uppers lowers ⇒
    real_shadow uppers lowers

⊢ ∀uppers lowers.
    dark_shadow uppers lowers ⇔
    ∀c d L R.
      MEM (c,L) uppers ∧ MEM (d,R) lowers ⇒
      &d * L − &c * R ≥ (&c − 1) * (&d − 1)

⊢ (∀c L. dark_shadow_cond_row (c,L) [] ⇔ T) ∧
  ∀t d c R L.
    dark_shadow_cond_row (c,L) ((d,R)::t) ⇔
    ¬(∃i. &c * &d * i < &c * R ∧ &c * R ≤ &d * L ∧
         &d * L < &c * &d * (i + 1)) ∧ dark_shadow_cond_row (c,L) t

⊢ ∀P. (∀c L. P (c,L) []) ∧ (∀c L d R t. P (c,L) t ⇒ P (c,L) ((d,R)::t)) ⇒
      ∀v v1 v2. P (v,v1) v2

⊢ (∀lowers. dark_shadow_condition [] lowers ⇔ T) ∧
  ∀uppers lowers c L.
    dark_shadow_condition ((c,L)::uppers) lowers ⇔
    dark_shadow_cond_row (c,L) lowers ∧ dark_shadow_condition uppers lowers

⊢ ∀P. (∀lowers. P [] lowers) ∧
      (∀c L uppers lowers. P uppers lowers ⇒ P ((c,L)::uppers) lowers) ⇒
      ∀v v1. P v v1

⊢ (∀lowers. dark_shadow [] lowers ⇔ T) ∧
  ∀uppers lowers c L.
    dark_shadow ((c,L)::uppers) lowers ⇔
    dark_shadow_row c L lowers ∧ dark_shadow uppers lowers

⊢ ∀P. (∀lowers. P [] lowers) ∧
      (∀c L uppers lowers. P uppers lowers ⇒ P ((c,L)::uppers) lowers) ⇒
      ∀v v1. P v v1

⊢ (∀c L. dark_shadow_row c L [] ⇔ T) ∧
  ∀rs d c R L.
    dark_shadow_row c L ((d,R)::rs) ⇔
    &d * L − &c * R ≥ (&c − 1) * (&d − 1) ∧ dark_shadow_row c L rs

⊢ ∀P. (∀c L. P c L []) ∧ (∀c L d R rs. P c L rs ⇒ P c L ((d,R)::rs)) ⇒
      ∀v v1 v2. P v v1 v2

⊢ ∀lowers c L.
    0 < c ∧ EVERY fst_nzero lowers ∧ dark_shadow_row c L lowers ⇒
    rshadow_row (c,L) lowers

⊢ ∀c x cs vs.
    0 < c ⇒
    ((0 = c * x + sumc cs vs) ⇔
     ∃s. (x = -(c + 1) * s + sumc (MAP (λx. modhat x (c + 1)) cs) vs) ∧
         (0 = c * x + sumc cs vs))

⊢ p ⇔ ((evalupper x [] ∧ evallower x []) ∧ T) ∧ p

⊢ ((evalupper x ups ∧ evallower x lows) ∧ T) ∧ ex' ⇔
  (evalupper x ups ∧ evallower x lows) ∧ ex'

⊢ ((evalupper x ups ∧ evallower x lows) ∧ ex) ∧ ex' ⇔
  (evalupper x ups ∧ evallower x lows) ∧ ex ∧ ex'

⊢ ((evalupper x ups ∧ evallower x lows) ∧ T) ∧ ex' ∧ p ⇔
  ((evalupper x ups ∧ evallower x lows) ∧ ex') ∧ p

⊢ ((evalupper x ups ∧ evallower x lows) ∧ ex) ∧ ex' ∧ p ⇔
  ((evalupper x ups ∧ evallower x lows) ∧ ex ∧ ex') ∧ p

⊢ ((evalupper x ups ∧ evallower x lows) ∧ ex) ∧ r ≤ &c * x ⇔
  (evalupper x ups ∧ evallower x ((c,r)::lows)) ∧ ex

⊢ ((evalupper x ups ∧ evallower x lows) ∧ ex) ∧ r ≤ &c * x ∧ p ⇔
  ((evalupper x ups ∧ evallower x ((c,r)::lows)) ∧ ex) ∧ p

⊢ ((evalupper x ups ∧ evallower x lows) ∧ ex) ∧ &c * x ≤ r ⇔
  (evalupper x ((c,r)::ups) ∧ evallower x lows) ∧ ex

⊢ ((evalupper x ups ∧ evallower x lows) ∧ ex) ∧ &c * x ≤ r ∧ p ⇔
  ((evalupper x ((c,r)::ups) ∧ evallower x lows) ∧ ex) ∧ p

⊢ ∀lowers x. evallower x lowers ⇔ ∀d R. MEM (d,R) lowers ⇒ R ≤ &d * x

⊢ (∀x. evallower x [] ⇔ T) ∧
  ∀y x cs c. evallower x ((c,y)::cs) ⇔ y ≤ &c * x ∧ evallower x cs

⊢ ∀P. (∀x. P x []) ∧ (∀x c y cs. P x cs ⇒ P x ((c,y)::cs)) ⇒ ∀v v1. P v v1

⊢ ∀uppers x. evalupper x uppers ⇔ ∀c L. MEM (c,L) uppers ⇒ &c * x ≤ L

⊢ (∀x. evalupper x [] ⇔ T) ∧
  ∀y x cs c. evalupper x ((c,y)::cs) ⇔ &c * x ≤ y ∧ evalupper x cs

⊢ ∀P. (∀x. P x []) ∧ (∀x c y cs. P x cs ⇒ P x ((c,y)::cs)) ⇒ ∀v v1. P v v1

⊢ ∀uppers lowers.
    EVERY fst_nzero uppers ∧ EVERY fst_nzero lowers ⇒
    EVERY fst1 uppers ∨ EVERY fst1 lowers ⇒
    ((∃x. evalupper x uppers ∧ evallower x lowers) ⇔
     real_shadow uppers lowers)

⊢ ∀uppers lowers m.
    EVERY fst_nzero uppers ∧ EVERY fst_nzero lowers ∧
    EVERY (λp. FST p ≤ m) uppers ⇒
    ((∃x. evalupper x uppers ∧ evallower x lowers) ⇔
     real_shadow uppers lowers ∧
     (dark_shadow uppers lowers ∨ ∃x. nightmare x m uppers lowers lowers))

⊢ ∀rs x c uppers lowers.
    nightmare x c uppers lowers rs ⇔
    ∃i d R.
      0 ≤ i ∧ i ≤ (&d * &c − &c − &d) / &c ∧ MEM (d,R) rs ∧
      evalupper x uppers ∧ evallower x lowers ∧ (&d * x = R + i)

⊢ (∀x uppers lowers c. nightmare x c uppers lowers [] ⇔ F) ∧
  ∀x uppers rs lowers d c R.
    nightmare x c uppers lowers ((d,R)::rs) ⇔
    (∃i. (0 ≤ i ∧ i ≤ (&c * &d − &c − &d) / &c) ∧ (&d * x = R + i) ∧
         evalupper x uppers ∧ evallower x lowers) ∨
    nightmare x c uppers lowers rs

⊢ ∀rs x uppers lowers c.
    nightmare x c uppers lowers rs ⇒
    evalupper x uppers ∧ evallower x lowers

⊢ ∀P. (∀x c uppers lowers. P x c uppers lowers []) ∧
      (∀x c uppers lowers d R rs.
         P x c uppers lowers rs ⇒ P x c uppers lowers ((d,R)::rs)) ⇒
      ∀v v1 v2 v3 v4. P v v1 v2 v3 v4

⊢ ∀lowers. EVERY fst_nzero lowers ⇒ ∃x. evallower x lowers

⊢ ∀uppers. EVERY fst_nzero uppers ⇒ ∃x. evalupper x uppers

⊢ ∀uppers lowers.
    real_shadow uppers lowers ⇔
    ∀c d L R. MEM (c,L) uppers ∧ MEM (d,R) lowers ⇒ &c * R ≤ &d * L

⊢ ∀uppers lowers x.
    evalupper x uppers ∧ evallower x lowers ∧ EVERY fst_nzero uppers ∧
    EVERY fst_nzero lowers ⇒
    real_shadow uppers lowers

⊢ ∀uppers lowers c L x.
    0 < c ∧ rshadow_row (c,L) lowers ∧ evalupper x uppers ∧
    evallower x lowers ∧ EVERY fst_nzero uppers ∧ EVERY fst1 lowers ⇒
    ∃x. &c * x ≤ L ∧ evalupper x uppers ∧ evallower x lowers

⊢ ∀uppers lowers L x.
    rshadow_row (1,L) lowers ∧ evallower x lowers ∧ evalupper x uppers ∧
    EVERY fst_nzero lowers ∧ EVERY fst1 uppers ⇒
    ∃x. x ≤ L ∧ evalupper x uppers ∧ evallower x lowers

⊢ (∀uppery upperc. rshadow_row (upperc,uppery) [] ⇔ T) ∧
  ∀uppery upperc rs lowery lowerc.
    rshadow_row (upperc,uppery) ((lowerc,lowery)::rs) ⇔
    &upperc * lowery ≤ &lowerc * uppery ∧ rshadow_row (upperc,uppery) rs

⊢ ∀P. (∀upperc uppery. P (upperc,uppery) []) ∧
      (∀upperc uppery lowerc lowery rs.
         P (upperc,uppery) rs ⇒ P (upperc,uppery) ((lowerc,lowery)::rs)) ⇒
      ∀v v1 v2. P (v,v1) v2

⊢ ∀c L x.
    &c * x ≤ L ∧ 0 < c ⇒
    ∀lowers.
      EVERY fst_nzero lowers ∧ evallower x lowers ⇒
      rshadow_row (c,L) lowers

⊢ ∀uppers x y. evalupper x uppers ∧ y < x ⇒ evalupper y uppers

⊢ ∀cs vs ds. sumc cs vs + sumc ds vs = sumc (MAP2 0 $+ cs ds) vs

⊢ ∀cs vs f. f * sumc cs vs = sumc (MAP (λx. f * x) cs) vs

⊢ (∀v0. sumc v0 [] = 0) ∧ (∀v5 v4. sumc [] (v4::v5) = 0) ∧
  ∀vs v cs c. sumc (c::cs) (v::vs) = c * v + sumc cs vs

⊢ ∀P. (∀v0. P v0 []) ∧ (∀v4 v5. P [] (v4::v5)) ∧
      (∀c cs v vs. P cs vs ⇒ P (c::cs) (v::vs)) ⇒
      ∀v v1. P v v1

⊢ ∀f cs c v vs. sumc (MAP f (c::cs)) (v::vs) = f c * v + sumc (MAP f cs) vs

⊢ ∀f c. sumc (MAP f [c]) [1] = f c

⊢ ∀cs vs c v.
    (sumc [] vs = 0) ∧ (sumc cs [] = 0) ∧
    (sumc (c::cs) (v::vs) = c * v + sumc cs vs)