Theory "Omega"

Parents integer

Signature

Constant	Type
MAP2	:β -> (β -> β -> α) -> β list -> β list -> α list
calc_nightmare	:int -> num -> (num, int) alist -> bool
dark_shadow	:(num, int) alist reln
dark_shadow_cond_row	:num # int -> (num, int) alist -> bool
dark_shadow_condition	:(num, int) alist reln
dark_shadow_row	:num -> int -> (num, int) alist -> bool
evallower	:int -> (num, int) alist -> bool
evalupper	:int -> (num, int) alist -> bool
fst1	:num # α -> bool
fst_nzero	:num # α -> bool
modhat	:int -> int -> int
nightmare	:int -> num -> (num, int) alist -> (num, int) alist reln
real_shadow	:(num, int) alist reln
rshadow_row	:num # int -> (num, int) alist -> bool
sumc	:int list -> int list -> int

Definitions

modhat_def

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

fst_nzero_def

⊢ ∀x. fst_nzero x ⇔ 0 < FST x

fst1_def

⊢ ∀x. fst1 x ⇔ FST x = 1

real_shadow_def

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

Theorems

MAP2_ind

⊢ ∀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

MAP2_def

⊢ (∀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

MAP2_zero_ADD

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

sumc_ind

⊢ ∀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

sumc_def

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

sumc_thm

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

sumc_ADD

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

sumc_MULT

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

sumc_singleton

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

sumc_nonsingle

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

equality_removal

⊢ ∀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)

evalupper_ind

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

evalupper_def

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

evallower_ind

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

evallower_def

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

smaller_satisfies_uppers

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

bigger_satisfies_lowers

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

onlylowers_satisfiable

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

onlyuppers_satisfiable

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

rshadow_row_ind

⊢ ∀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

rshadow_row_def

⊢ (∀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

singleton_real_shadow

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

real_shadow_revimp_uppers1

⊢ ∀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

real_shadow_revimp_lowers1

⊢ ∀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

real_shadow_always_implied

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

exact_shadow_case

⊢ ∀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)

dark_shadow_cond_row_ind

⊢ ∀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

dark_shadow_cond_row_def

⊢ (∀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

dark_shadow_condition_ind

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

dark_shadow_condition_def

⊢ (∀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

basic_shadow_equivalence

⊢ ∀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)

dark_shadow_row_ind

⊢ ∀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

dark_shadow_row_def

⊢ (∀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

dark_shadow_ind

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

dark_shadow_def

⊢ (∀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

nightmare_ind

⊢ ∀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

nightmare_def

⊢ (∀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

nightmare_implies_LHS

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

dark_shadow_FORALL

⊢ ∀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)

real_shadow_FORALL

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

evalupper_FORALL

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

evallower_FORALL

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

nightmare_EXISTS

⊢ ∀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

final_equivalence

⊢ ∀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))

darkrow_implies_realrow

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

dark_implies_real

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

alternative_equivalence

⊢ ∀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)

eval_base

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

eval_step_upper1

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

eval_step_upper2

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

eval_step_lower1

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

eval_step_lower2

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

eval_step_extra1

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

eval_step_extra2

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

eval_step_extra3

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

eval_step_extra4

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

calc_nightmare_ind

⊢ ∀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

calc_nightmare_def

⊢ (∀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

calculational_nightmare

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