Theory: quantHeuristics

Theorems

CONJ_NOT_OR_THM

⊢ ∀A B. A ∧ B ⇔ ¬(¬A ∨ ¬B)

CONS_EQ_REWRITE

⊢ ((x::xs = ys) ⇔ 1 ≤ LENGTH ys ∧ (x = HD ys) ∧ (xs = TL ys)) ∧
  ((ys = x::xs) ⇔ 1 ≤ LENGTH ys ∧ (HD ys = x) ∧ (TL ys = xs)) ∧
  (0 < n ⇒ (n ≤ LENGTH (TL ys) ⇔ n + 1 ≤ LENGTH ys)) ∧
  (n ≤ m ⇒ (n ≤ rhs ∧ m ≤ rhs ⇔ m ≤ rhs)) ∧
  (([] = TL ys) ⇔ LENGTH ys ≤ 1) ∧ ((TL ys = []) ⇔ LENGTH ys ≤ 1) ∧
  (LENGTH (TL ys) ≤ n ⇔ LENGTH ys ≤ n + 1) ∧ (m ≤ n ∧ n ≤ m ⇔ (m = n)) ∧
  (m ≤ LENGTH ys ∧ (n = LENGTH ys) ⇔ m ≤ n ∧ (n = LENGTH ys))

DISJ_IMP_INTRO

⊢ (∀x. P x ∨ Q x) ⇒ (¬P y ⇒ Q y) ∧ (¬Q y ⇒ P y)

EXISTS_NOT_FORALL_THM

⊢ ∀P. (∃x. P x) ⇔ ¬∀x. ¬P x

FST_PAIR_EQ

⊢ ∀p p2. ((FST p,p2) = p) ⇔ (p2 = SND p)

FST_PAIR_EQ_SYM

⊢ ∀p p2. (p = (FST p,p2)) ⇔ (SND p = p2)

GUESSES_NEG_DUALITY

⊢ (GUESS_EXISTS i ($¬ ∘ P) ⇔ GUESS_FORALL i P) ∧
  (GUESS_FORALL i ($¬ ∘ P) ⇔ GUESS_EXISTS i P) ∧
  (GUESS_EXISTS_GAP i ($¬ ∘ P) ⇔ GUESS_FORALL_GAP i P) ∧
  (GUESS_FORALL_GAP i ($¬ ∘ P) ⇔ GUESS_EXISTS_GAP i P) ∧
  (GUESS_EXISTS_POINT i ($¬ ∘ P) ⇔ GUESS_FORALL_POINT i P) ∧
  (GUESS_FORALL_POINT i ($¬ ∘ P) ⇔ GUESS_EXISTS_POINT i P)

GUESSES_NEG_REWRITE

⊢ (GUESS_EXISTS i (λx. ¬P x) ⇔ GUESS_FORALL i (λx. P x)) ∧
  (GUESS_FORALL i (λx. ¬P x) ⇔ GUESS_EXISTS i (λx. P x)) ∧
  (GUESS_EXISTS_GAP i (λx. ¬P x) ⇔ GUESS_FORALL_GAP i (λx. P x)) ∧
  (GUESS_FORALL_GAP i (λx. ¬P x) ⇔ GUESS_EXISTS_GAP i (λx. P x)) ∧
  (GUESS_EXISTS_POINT i (λx. ¬P x) ⇔ GUESS_FORALL_POINT i (λx. P x)) ∧
  (GUESS_FORALL_POINT i (λx. ¬P x) ⇔ GUESS_EXISTS_POINT i (λx. P x))

GUESSES_UEXISTS_THM1

⊢ ∀i P. GUESS_EXISTS (λx. i) P ⇒ ($?! P ⇔ P i ∧ ∀v. P v ⇒ (v = i))

GUESSES_UEXISTS_THM2

⊢ ∀i P. GUESS_EXISTS_GAP (λx. i) P ⇒ ($?! P ⇔ P i)

GUESSES_UEXISTS_THM3

⊢ ∀i P. GUESS_EXISTS_POINT (λx. i) P ⇒ ($?! P ⇔ ∀v. P v ⇒ (v = i))

GUESSES_UEXISTS_THM4

⊢ ∀i P.
    GUESS_EXISTS_POINT (λx. i) P ⇒ GUESS_EXISTS_GAP (λx. i) P ⇒ ($?! P ⇔ T)

GUESSES_WEAKEN_THM

⊢ (GUESS_FORALL_GAP i P ⇒ GUESS_FORALL i P) ∧
  (GUESS_FORALL_POINT i P ⇒ GUESS_FORALL i P) ∧
  (GUESS_EXISTS_POINT i P ⇒ GUESS_EXISTS i P) ∧
  (GUESS_EXISTS_GAP i P ⇒ GUESS_EXISTS i P)

GUESS_EXISTS_FORALL_REWRITES

⊢ (GUESS_EXISTS i P ⇔ ∀v. P v ⇒ ∃fv. P (i fv)) ∧
  (GUESS_FORALL i P ⇔ ∀v. ¬P v ⇒ ∃fv. ¬P (i fv))

GUESS_EXISTS_POINT_THM

⊢ ∀i P. GUESS_EXISTS_POINT i P ⇒ ($? P ⇔ T)

GUESS_EXISTS_THM

⊢ ∀i P. GUESS_EXISTS i P ⇒ ($? P ⇔ ∃fv. P (i fv))

GUESS_FORALL_POINT_THM

⊢ ∀i P. GUESS_FORALL_POINT i P ⇒ ($! P ⇔ F)

GUESS_FORALL_THM

⊢ ∀i P. GUESS_FORALL i P ⇒ ($! P ⇔ ∀fv. P (i fv))

GUESS_POINT_THM

⊢ (GUESS_EXISTS_POINT i P ⇒ ((∃v. P v) ⇔ T)) ∧
  (GUESS_FORALL_POINT i P ⇒ ((∀v. P v) ⇔ F))

GUESS_REWRITES

⊢ ((GUESS_EXISTS i P ⇔ ∀v. P v ⇒ ∃fv. P (i fv)) ∧
   (GUESS_FORALL i P ⇔ ∀v. ¬P v ⇒ ∃fv. ¬P (i fv))) ∧
  (∀i P. GUESS_EXISTS_POINT i P ⇔ ∀fv. P (i fv)) ∧
  (∀i P. GUESS_FORALL_POINT i P ⇔ ∀fv. ¬P (i fv)) ∧
  (∀i P. GUESS_EXISTS_GAP i P ⇔ ∀v. P v ⇒ ∃fv. v = i fv) ∧
  ∀i P. GUESS_FORALL_GAP i P ⇔ ∀v. ¬P v ⇒ ∃fv. v = i fv

GUESS_RULES_BOOL

⊢ GUESS_EXISTS_POINT (λARB. T) (λx. x) ∧
  GUESS_FORALL_POINT (λARB. F) (λx. x) ∧
  GUESS_EXISTS_GAP (λARB. T) (λx. x) ∧ GUESS_FORALL_GAP (λARB. F) (λx. x)

GUESS_RULES_COND

⊢ (GUESS_FORALL_POINT i (λx. P x) ∧ GUESS_FORALL_POINT i (λx. Q x) ⇒
   GUESS_FORALL_POINT i (λx. if b x then P x else Q x)) ∧
  (GUESS_EXISTS_POINT i (λx. P x) ∧ GUESS_EXISTS_POINT i (λx. Q x) ⇒
   GUESS_EXISTS_POINT i (λx. if b x then P x else Q x)) ∧
  (GUESS_EXISTS i (λx. P x) ∧ GUESS_EXISTS i (λx. Q x) ⇒
   GUESS_EXISTS i (λx. if bc then P x else Q x)) ∧
  (GUESS_FORALL i (λx. P x) ∧ GUESS_FORALL i (λx. Q x) ⇒
   GUESS_FORALL i (λx. if bc then P x else Q x)) ∧
  (GUESS_EXISTS_GAP i (λx. P x) ∧ GUESS_EXISTS_GAP i (λx. Q x) ⇒
   GUESS_EXISTS_GAP i (λx. if b x then P x else Q x)) ∧
  (GUESS_FORALL_GAP i (λx. P x) ∧ GUESS_FORALL_GAP i (λx. Q x) ⇒
   GUESS_FORALL_GAP i (λx. if b x then P x else Q x)) ∧
  (GUESS_FORALL_POINT i (λx. b x) ∧ GUESS_FORALL_POINT i (λx. Q x) ⇒
   GUESS_FORALL_POINT i (λx. if b x then P x else Q x)) ∧
  (GUESS_FORALL_POINT i (λx. b x) ∧ GUESS_EXISTS_POINT i (λx. Q x) ⇒
   GUESS_EXISTS_POINT i (λx. if b x then P x else Q x)) ∧
  (GUESS_EXISTS_POINT i (λx. b x) ∧ GUESS_FORALL_POINT i (λx. P x) ⇒
   GUESS_FORALL_POINT i (λx. if b x then P x else Q x)) ∧
  (GUESS_EXISTS_POINT i (λx. b x) ∧ GUESS_EXISTS_POINT i (λx. P x) ⇒
   GUESS_EXISTS_POINT i (λx. if b x then P x else Q x)) ∧
  (GUESS_FORALL_GAP i (λx. b x) ∧ GUESS_EXISTS_GAP i (λx. P x) ⇒
   GUESS_EXISTS_GAP i (λx. if b x then P x else Q x)) ∧
  (GUESS_EXISTS_GAP i (λx. b x) ∧ GUESS_EXISTS_GAP i (λx. Q x) ⇒
   GUESS_EXISTS_GAP i (λx. if b x then P x else Q x)) ∧
  (GUESS_EXISTS_GAP i (λx. b x) ∧ GUESS_FORALL_GAP i (λx. Q x) ⇒
   GUESS_FORALL_GAP i (λx. if b x then P x else Q x)) ∧
  (GUESS_FORALL_GAP i (λx. b x) ∧ GUESS_FORALL_GAP i (λx. P x) ⇒
   GUESS_FORALL_GAP i (λx. if b x then P x else Q x))

GUESS_RULES_CONJ

⊢ (GUESS_FORALL_POINT i (λx. P x) ⇒ GUESS_FORALL_POINT i (λx. P x ∧ Q x)) ∧
  (GUESS_FORALL_POINT i (λx. Q x) ⇒ GUESS_FORALL_POINT i (λx. P x ∧ Q x)) ∧
  (GUESS_FORALL i (λx. P x) ∧ GUESS_FORALL i (λx. Q x) ⇒
   GUESS_FORALL i (λx. P x ∧ Q x)) ∧
  (GUESS_FORALL_GAP i (λx. P x) ∧ GUESS_FORALL_GAP i (λx. Q x) ⇒
   GUESS_FORALL_GAP i (λx. P x ∧ Q x)) ∧
  (GUESS_EXISTS (λxxx. iK) (λx. P x) ∧ GUESS_EXISTS (λxxx. iK) (λx. Q x) ⇒
   GUESS_EXISTS (λxxx. iK) (λx. P x ∧ Q x)) ∧
  (GUESS_EXISTS i (λx. P x) ⇒ GUESS_EXISTS i (λx. P x ∧ q)) ∧
  (GUESS_EXISTS i (λx. Q x) ⇒ GUESS_EXISTS i (λx. p ∧ Q x)) ∧
  (GUESS_EXISTS_POINT i (λx. P x) ∧ GUESS_EXISTS_POINT i (λx. Q x) ⇒
   GUESS_EXISTS_POINT i (λx. P x ∧ Q x)) ∧
  (GUESS_EXISTS_GAP i (λx. P x) ⇒ GUESS_EXISTS_GAP i (λx. P x ∧ Q x)) ∧
  (GUESS_EXISTS_GAP i (λx. Q x) ⇒ GUESS_EXISTS_GAP i (λx. P x ∧ Q x))

GUESS_RULES_CONSTANT_EXISTS

⊢ GUESS_EXISTS i (λx. p) ⇔ T

GUESS_RULES_CONSTANT_FORALL

⊢ GUESS_FORALL i (λx. p) ⇔ T

GUESS_RULES_DISJ

⊢ (GUESS_EXISTS_POINT i (λx. P x) ⇒ GUESS_EXISTS_POINT i (λx. P x ∨ Q x)) ∧
  (GUESS_EXISTS_POINT i (λx. Q x) ⇒ GUESS_EXISTS_POINT i (λx. P x ∨ Q x)) ∧
  (GUESS_EXISTS i (λx. P x) ∧ GUESS_EXISTS i (λx. Q x) ⇒
   GUESS_EXISTS i (λx. P x ∨ Q x)) ∧
  (GUESS_EXISTS_GAP i (λx. P x) ∧ GUESS_EXISTS_GAP i (λx. Q x) ⇒
   GUESS_EXISTS_GAP i (λx. P x ∨ Q x)) ∧
  (GUESS_FORALL (λxxx. iK) (λx. P x) ∧ GUESS_FORALL (λxxx. iK) (λx. Q x) ⇒
   GUESS_FORALL (λxxx. iK) (λx. P x ∨ Q x)) ∧
  (GUESS_FORALL i (λx. P x) ⇒ GUESS_FORALL i (λx. P x ∨ q)) ∧
  (GUESS_FORALL i (λx. Q x) ⇒ GUESS_FORALL i (λx. p ∨ Q x)) ∧
  (GUESS_FORALL_POINT i (λx. P x) ∧ GUESS_FORALL_POINT i (λx. Q x) ⇒
   GUESS_FORALL_POINT i (λx. P x ∨ Q x)) ∧
  (GUESS_FORALL_GAP i (λx. P x) ⇒ GUESS_FORALL_GAP i (λx. P x ∨ Q x)) ∧
  (GUESS_FORALL_GAP i (λx. Q x) ⇒ GUESS_FORALL_GAP i (λx. P x ∨ Q x))

GUESS_RULES_ELIM_UNIT

⊢ (GUESS_FORALL_POINT i vt ⇔ GUESS_FORALL_POINT (λx. i (x,())) vt) ∧
  (GUESS_EXISTS_POINT i vt ⇔ GUESS_EXISTS_POINT (λx. i (x,())) vt) ∧
  (GUESS_EXISTS i vt ⇔ GUESS_EXISTS (λx. i (x,())) vt) ∧
  (GUESS_FORALL i vt ⇔ GUESS_FORALL (λx. i (x,())) vt) ∧
  (GUESS_EXISTS_GAP i vt ⇔ GUESS_EXISTS_GAP (λx. i (x,())) vt) ∧
  (GUESS_FORALL_GAP i vt ⇔ GUESS_FORALL_GAP (λx. i (x,())) vt)

GUESS_RULES_EQUATION_EXISTS_GAP

⊢ ∀i. GUESS_EXISTS_GAP (λxxx. i) (λx. x = i)

GUESS_RULES_EQUATION_EXISTS_POINT

⊢ ∀i P Q. (P i = Q i) ⇒ GUESS_EXISTS_POINT (λxxx. i) (λx. P x = Q x)

GUESS_RULES_EQUATION_FORALL_POINT

⊢ ∀i P Q. (∀fv. P (i fv) ≠ Q (i fv)) ⇒ GUESS_FORALL_POINT i (λx. P x = Q x)

GUESS_RULES_EQUIV

⊢ (GUESS_EXISTS_POINT i (λx. P x) ∧ GUESS_EXISTS_POINT i (λx. Q x) ⇒
   GUESS_EXISTS_POINT i (λx. P x ⇔ Q x)) ∧
  (GUESS_FORALL_POINT i (λx. P x) ∧ GUESS_FORALL_POINT i (λx. Q x) ⇒
   GUESS_EXISTS_POINT i (λx. P x ⇔ Q x)) ∧
  (GUESS_EXISTS_POINT i (λx. P x) ∧ GUESS_FORALL_POINT i (λx. Q x) ⇒
   GUESS_FORALL_POINT i (λx. P x ⇔ Q x)) ∧
  (GUESS_FORALL_POINT i (λx. P x) ∧ GUESS_EXISTS_POINT i (λx. Q x) ⇒
   GUESS_FORALL_POINT i (λx. P x ⇔ Q x)) ∧
  (GUESS_FORALL_GAP i (λx. P1 x) ∧ GUESS_FORALL_GAP i (λx. P2 x) ⇒
   GUESS_FORALL_GAP i (λx. P1 x ⇔ P2 x)) ∧
  (GUESS_EXISTS_GAP i (λx. P1 x) ∧ GUESS_EXISTS_GAP i (λx. P2 x) ⇒
   GUESS_FORALL_GAP i (λx. P1 x ⇔ P2 x)) ∧
  (GUESS_EXISTS_GAP i (λx. P1 x) ∧ GUESS_FORALL_GAP i (λx. P2 x) ⇒
   GUESS_EXISTS_GAP i (λx. P1 x ⇔ P2 x)) ∧
  (GUESS_FORALL_GAP i (λx. P1 x) ∧ GUESS_EXISTS_GAP i (λx. P2 x) ⇒
   GUESS_EXISTS_GAP i (λx. P1 x ⇔ P2 x))

GUESS_RULES_EXISTS

⊢ ((∀y. GUESS_EXISTS_POINT i (λx. P x y)) ⇒
   GUESS_EXISTS_POINT i (λx. ∃y. P x y)) ∧
  ((∀y. GUESS_EXISTS i (λx. P x y)) ⇒ GUESS_EXISTS i (λx. ∃y. P x y)) ∧
  ((∀y. GUESS_EXISTS_GAP i (λx. P x y)) ⇒
   GUESS_EXISTS_GAP i (λx. ∃y. P x y)) ∧
  ((∀y. GUESS_FORALL_POINT i (λx. P x y)) ⇒
   GUESS_FORALL_POINT i (λx. ∃y. P x y)) ∧
  ((∀y. GUESS_FORALL (λxxx. iK) (λx. P x y)) ⇒
   GUESS_FORALL (λxxx. iK) (λx. ∃y. P x y)) ∧
  ((∀y. GUESS_FORALL_GAP i (λx. P x y)) ⇒
   GUESS_FORALL_GAP i (λx. ∃y. P x y))

GUESS_RULES_EXISTS_UNIQUE

⊢ ((∀y. GUESS_FORALL_POINT i (λx. P x y)) ⇒
   GUESS_FORALL_POINT i (λx. ∃!y. P x y)) ∧
  ((∀y. GUESS_EXISTS_GAP i (λx. P x y)) ⇒
   GUESS_EXISTS_GAP i (λx. ∃!y. P x y))

GUESS_RULES_EXISTS___NEW_FV

⊢ ((∀y. GUESS_EXISTS_POINT (iy y) (λx. P x y)) ⇒
   GUESS_EXISTS_POINT (λfv. iy (FST fv) (SND fv)) (λx. ∃y. P x y)) ∧
  ((∀y. GUESS_EXISTS (iy y) (λx. P x y)) ⇒
   GUESS_EXISTS (λfv. iy (FST fv) (SND fv)) (λx. ∃y. P x y)) ∧
  ((∀y. GUESS_EXISTS_GAP (iy y) (λx. P x y)) ⇒
   GUESS_EXISTS_GAP (λfv. iy (FST fv) (SND fv)) (λx. ∃y. P x y)) ∧
  ((∀y. GUESS_FORALL_GAP (iy y) (λx. P x y)) ⇒
   GUESS_FORALL_GAP (λfv. iy (FST fv) (SND fv)) (λx. ∃y. P x y))

GUESS_RULES_EXISTS___NEW_FV_1

⊢ ((∀y. GUESS_EXISTS_POINT (λxxx. i y) (λx. P x y)) ⇒
   GUESS_EXISTS_POINT i (λx. ∃y. P x y)) ∧
  ((∀y. GUESS_EXISTS (λxxx. i y) (λx. P x y)) ⇒
   GUESS_EXISTS i (λx. ∃y. P x y)) ∧
  ((∀y. GUESS_EXISTS_GAP (λxxx. i y) (λx. P x y)) ⇒
   GUESS_EXISTS_GAP i (λx. ∃y. P x y)) ∧
  ((∀y. GUESS_FORALL_GAP (λxxx. i y) (λx. P x y)) ⇒
   GUESS_FORALL_GAP i (λx. ∃y. P x y))

GUESS_RULES_FORALL

⊢ ((∀y. GUESS_FORALL_POINT i (λx. P x y)) ⇒
   GUESS_FORALL_POINT i (λx. ∀y. P x y)) ∧
  ((∀y. GUESS_FORALL i (λx. P x y)) ⇒ GUESS_FORALL i (λx. ∀y. P x y)) ∧
  ((∀y. GUESS_FORALL_GAP i (λx. P x y)) ⇒
   GUESS_FORALL_GAP i (λx. ∀y. P x y)) ∧
  ((∀y. GUESS_EXISTS_POINT i (λx. P x y)) ⇒
   GUESS_EXISTS_POINT i (λx. ∀y. P x y)) ∧
  ((∀y. GUESS_EXISTS (λxxx. iK) (λx. P x y)) ⇒
   GUESS_EXISTS (λxxx. iK) (λx. ∀y. P x y)) ∧
  ((∀y. GUESS_EXISTS_GAP i (λx. P x y)) ⇒
   GUESS_EXISTS_GAP i (λx. ∀y. P x y))

GUESS_RULES_FORALL___NEW_FV

⊢ ((∀y. GUESS_FORALL_POINT (iy y) (λx. P x y)) ⇒
   GUESS_FORALL_POINT (λfv. iy (FST fv) (SND fv)) (λx. ∀y. P x y)) ∧
  ((∀y. GUESS_FORALL (iy y) (λx. P x y)) ⇒
   GUESS_FORALL (λfv. iy (FST fv) (SND fv)) (λx. ∀y. P x y)) ∧
  ((∀y. GUESS_FORALL_GAP (iy y) (λx. P x y)) ⇒
   GUESS_FORALL_GAP (λfv. iy (FST fv) (SND fv)) (λx. ∀y. P x y)) ∧
  ((∀y. GUESS_EXISTS_GAP (iy y) (λx. P x y)) ⇒
   GUESS_EXISTS_GAP (λfv. iy (FST fv) (SND fv)) (λx. ∀y. P x y))

GUESS_RULES_FORALL___NEW_FV_1

⊢ ((∀y. GUESS_FORALL_POINT (λxxx. i y) (λx. P x y)) ⇒
   GUESS_FORALL_POINT i (λx. ∀y. P x y)) ∧
  ((∀y. GUESS_FORALL (λxxx. i y) (λx. P x y)) ⇒
   GUESS_FORALL i (λx. ∀y. P x y)) ∧
  ((∀y. GUESS_FORALL_GAP (λxxx. i y) (λx. P x y)) ⇒
   GUESS_FORALL_GAP i (λx. ∀y. P x y)) ∧
  ((∀y. GUESS_EXISTS_GAP (λxxx. i y) (λx. P x y)) ⇒
   GUESS_EXISTS_GAP i (λx. ∀y. P x y))

GUESS_RULES_IMP

⊢ (GUESS_FORALL_POINT i (λx. P x) ⇒ GUESS_EXISTS_POINT i (λx. P x ⇒ Q x)) ∧
  (GUESS_EXISTS_POINT i (λx. Q x) ⇒ GUESS_EXISTS_POINT i (λx. P x ⇒ Q x)) ∧
  (GUESS_FORALL i (λx. P x) ∧ GUESS_EXISTS i (λx. Q x) ⇒
   GUESS_EXISTS i (λx. P x ⇒ Q x)) ∧
  (GUESS_FORALL_GAP i (λx. P x) ∧ GUESS_EXISTS_GAP i (λx. Q x) ⇒
   GUESS_EXISTS_GAP i (λx. P x ⇒ Q x)) ∧
  (GUESS_EXISTS (λxxx. iK) (λx. P x) ∧ GUESS_FORALL (λxxx. iK) (λx. Q x) ⇒
   GUESS_FORALL (λxxx. iK) (λx. P x ⇒ Q x)) ∧
  (GUESS_EXISTS i (λx. P x) ⇒ GUESS_FORALL i (λx. P x ⇒ q)) ∧
  (GUESS_FORALL i (λx. Q x) ⇒ GUESS_FORALL i (λx. p ⇒ Q x)) ∧
  (GUESS_EXISTS_POINT i (λx. P x) ∧ GUESS_FORALL_POINT i (λx. Q x) ⇒
   GUESS_FORALL_POINT i (λx. P x ⇒ Q x)) ∧
  (GUESS_EXISTS_GAP i (λx. P x) ⇒ GUESS_FORALL_GAP i (λx. P x ⇒ Q x)) ∧
  (GUESS_FORALL_GAP i (λx. Q x) ⇒ GUESS_FORALL_GAP i (λx. P x ⇒ Q x))

GUESS_RULES_NEG

⊢ (GUESS_EXISTS i (λx. P x) ⇒ GUESS_FORALL i (λx. ¬P x)) ∧
  (GUESS_EXISTS_GAP i (λx. P x) ⇒ GUESS_FORALL_GAP i (λx. ¬P x)) ∧
  (GUESS_EXISTS_POINT i (λx. P x) ⇒ GUESS_FORALL_POINT i (λx. ¬P x)) ∧
  (GUESS_FORALL i (λx. P x) ⇒ GUESS_EXISTS i (λx. ¬P x)) ∧
  (GUESS_FORALL_GAP i (λx. P x) ⇒ GUESS_EXISTS_GAP i (λx. ¬P x)) ∧
  (GUESS_FORALL_POINT i (λx. P x) ⇒ GUESS_EXISTS_POINT i (λx. ¬P x))

GUESS_RULES_ONE_CASE___EXISTS_GAP

⊢ ∀P Q. (∀x. ∃fv. x = Q fv) ⇒ GUESS_EXISTS_GAP Q P

GUESS_RULES_ONE_CASE___FORALL_GAP

⊢ ∀P Q. (∀x. ∃fv. x = Q fv) ⇒ GUESS_FORALL_GAP Q P

GUESS_RULES_STRENGTHEN_EXISTS_POINT

⊢ ∀P Q. (∀x. P x ⇒ Q x) ⇒ GUESS_EXISTS_POINT i P ⇒ GUESS_EXISTS_POINT i Q

GUESS_RULES_STRENGTHEN_FORALL_GAP

⊢ ∀P Q. (∀x. P x ⇒ Q x) ⇒ GUESS_FORALL_GAP i P ⇒ GUESS_FORALL_GAP i Q

GUESS_RULES_TRIVIAL_EXISTS_POINT

⊢ ∀i P. P i ⇒ GUESS_EXISTS_POINT (λxxx. i) P

GUESS_RULES_TRIVIAL_FORALL_POINT

⊢ ∀i P. ¬P i ⇒ GUESS_FORALL_POINT (λxxx. i) P

GUESS_RULES_TWO_CASES

⊢ ∀y Q. (∀x. (x = y) ∨ ∃fv. x = Q fv) ⇒ GUESS_FORALL_GAP Q (λx. x = y)

GUESS_RULES_WEAKEN_EXISTS_GAP

⊢ ∀P Q. (∀x. Q x ⇒ P x) ⇒ GUESS_EXISTS_GAP i P ⇒ GUESS_EXISTS_GAP i Q

GUESS_RULES_WEAKEN_FORALL_POINT

⊢ ∀P Q. (∀x. Q x ⇒ P x) ⇒ GUESS_FORALL_POINT i P ⇒ GUESS_FORALL_POINT i Q

HD_TL_EQ_1

⊢ ∀l. (HD l::TL l = l) ⇔ l ≠ []

HD_TL_EQ_NIL_1_bothways

⊢ (∀l. ([HD l] = l) ⇔ (LENGTH l = 1)) ∧ ∀l. (l = [HD l]) ⇔ (LENGTH l = 1)

IMP_NEG_CONTRA

⊢ ∀P i x. ¬P i ⇒ P x ⇒ x ≠ i

INL_NEQ_ELIM

⊢ ((∀l. x ≠ INL l) ⇔ ISR x) ∧ ((∀l. INL l ≠ x) ⇔ ISR x)

INR_NEQ_ELIM

⊢ ((∀r. x ≠ INR r) ⇔ ISL x) ∧ ((∀r. INR r ≠ x) ⇔ ISL x)

ISL_exists

⊢ ISL x ⇔ ∃l. x = INL l

ISR_exists

⊢ ISR x ⇔ ∃r. x = INR r

IS_REMOVABLE_QUANT_FUN___EXISTS_THM

⊢ ∀f P. IS_REMOVABLE_QUANT_FUN f ⇒ ((∃x. P (f x)) ⇔ ∃x'. P x')

IS_REMOVABLE_QUANT_FUN___FORALL_THM

⊢ ∀f P. IS_REMOVABLE_QUANT_FUN f ⇒ ((∀x. P (f x)) ⇔ ∀x'. P x')

IS_SOME_EQ_NOT_NONE

⊢ ∀x. IS_SOME x ⇔ x ≠ NONE

LEFT_IMP_AND_INTRO

⊢ ∀x t1 t2. (t1 ⇒ t2) ⇒ x ∧ t1 ⇒ x ∧ t2

LEFT_IMP_OR_INTRO

⊢ ∀x t1 t2. (t1 ⇒ t2) ⇒ x ∨ t1 ⇒ x ∨ t2

LENGTH_LE_NUM

⊢ n ≤ LENGTH l ⇔ ∃l1 l2. (LENGTH l1 = n) ∧ (l = l1 ⧺ l2)

LENGTH_LE_PLUS

⊢ n + m ≤ LENGTH l ⇔
  ∃l1 l2. (LENGTH l1 = n) ∧ m ≤ LENGTH l2 ∧ (l = l1 ⧺ l2)

LENGTH_NIL_SYM

⊢ (0 = LENGTH l) ⇔ (l = [])

LENGTH_TO_EXISTS_CONS

⊢ (n < LENGTH xs ⇔ ∃y ys. (xs = y::ys) ∧ n ≤ LENGTH ys) ∧
  (LENGTH xs > n ⇔ ∃y ys. (xs = y::ys) ∧ n ≤ LENGTH ys) ∧
  (0 < n ⇒ ((LENGTH xs = n) ⇔ ∃y ys. (xs = y::ys) ∧ (LENGTH ys = PRE n))) ∧
  (0 < n ⇒ ((n = LENGTH xs) ⇔ ∃y ys. (xs = y::ys) ∧ (LENGTH ys = PRE n))) ∧
  (0 < n ⇒ (n ≤ LENGTH xs ⇔ ∃y ys. (xs = y::ys) ∧ PRE n ≤ LENGTH ys)) ∧
  (0 < n ⇒ (LENGTH xs ≥ n ⇔ ∃y ys. (xs = y::ys) ∧ PRE n ≤ LENGTH ys)) ∧
  (0 < x ⇒ (PRE (x + y) = PRE x + y)) ∧ (0 < y ⇒ (PRE (x + y) = x + PRE y))

LIST_LENGTH_0

⊢ ((LENGTH l = 0) ⇔ (l = [])) ∧ ((0 = LENGTH l) ⇔ (l = [])) ∧
  (LENGTH l < 1 ⇔ (l = [])) ∧ (1 > LENGTH l ⇔ (l = [])) ∧
  (0 ≥ LENGTH l ⇔ (l = [])) ∧ (LENGTH l ≤ 0 ⇔ (l = []))

LIST_LENGTH_1

⊢ ((LENGTH l = 1) ⇔ ∃e1. l = [e1]) ∧ ((1 = LENGTH l) ⇔ ∃e1. l = [e1]) ∧
  (0 < LENGTH l ⇔ ∃l' e1. l = e1::l') ∧
  (LENGTH l > 0 ⇔ ∃l' e1. l = e1::l') ∧
  (1 ≤ LENGTH l ⇔ ∃l' e1. l = e1::l') ∧
  (LENGTH l ≥ 1 ⇔ ∃l' e1. l = e1::l') ∧
  (1 + x ≤ LENGTH l ⇔ ∃l' e1. x ≤ LENGTH l' ∧ (l = e1::l')) ∧
  (LENGTH l ≥ 1 + x ⇔ ∃l' e1. x ≤ LENGTH l' ∧ (l = e1::l')) ∧
  (x + 1 ≤ LENGTH l ⇔ ∃l' e1. x ≤ LENGTH l' ∧ (l = e1::l')) ∧
  (LENGTH l ≥ x + 1 ⇔ ∃l' e1. x ≤ LENGTH l' ∧ (l = e1::l')) ∧
  ((LENGTH l = 1 + x) ⇔ ∃l' e1. (LENGTH l' = x) ∧ (l = e1::l')) ∧
  ((1 + x = LENGTH l) ⇔ ∃l' e1. (LENGTH l' = x) ∧ (l = e1::l')) ∧
  ((LENGTH l = x + 1) ⇔ ∃l' e1. (LENGTH l' = x) ∧ (l = e1::l')) ∧
  ((x + 1 = LENGTH l) ⇔ ∃l' e1. (LENGTH l' = x) ∧ (l = e1::l')) ∧
  ((LENGTH l = 0) ⇔ (l = [])) ∧ ((0 = LENGTH l) ⇔ (l = [])) ∧
  (LENGTH l < 1 ⇔ (l = [])) ∧ (1 > LENGTH l ⇔ (l = [])) ∧
  (0 ≥ LENGTH l ⇔ (l = [])) ∧ (LENGTH l ≤ 0 ⇔ (l = []))

LIST_LENGTH_COMPARE_1

⊢ (LENGTH l < 1 ⇔ (l = [])) ∧ (1 > LENGTH l ⇔ (l = [])) ∧
  (0 ≥ LENGTH l ⇔ (l = [])) ∧ (LENGTH l ≤ 0 ⇔ (l = []))

LIST_LENGTH_COMPARE_SUC

⊢ (SUC x ≤ LENGTH l ⇔ ∃l' e1. x ≤ LENGTH l' ∧ (l = e1::l')) ∧
  (LENGTH l ≥ SUC x ⇔ ∃l' e1. x ≤ LENGTH l' ∧ (l = e1::l')) ∧
  ((LENGTH l = SUC x) ⇔ ∃l' e1. (LENGTH l' = x) ∧ (l = e1::l')) ∧
  ((SUC x = LENGTH l) ⇔ ∃l' e1. (LENGTH l' = x) ∧ (l = e1::l'))

MOVE_EXISTS_IMP_THM

⊢ (∃x. (∀y. ¬P x y ⇒ R y) ⇒ Q x) ⇔ (∀y. ¬(∀x. P x y) ⇒ R y) ⇒ ∃x. Q x

PAIR_EQ_EXPAND

⊢ (((x,y) = X) ⇔ (x = FST X) ∧ (y = SND X)) ∧
  ((X = (x,y)) ⇔ (FST X = x) ∧ (SND X = y))

PAIR_EQ_SIMPLE_EXPAND

⊢ (((x,y) = (x,y')) ⇔ (y = y')) ∧ (((y,x) = (y',x)) ⇔ (y = y')) ∧
  (((FST X,y) = X) ⇔ (y = SND X)) ∧ (((x,SND X) = X) ⇔ (x = FST X)) ∧
  ((X = (FST X,y)) ⇔ (SND X = y)) ∧ ((X = (x,SND X)) ⇔ (FST X = x))

RIGHT_IMP_AND_INTRO

⊢ ∀x t1 t2. (t1 ⇒ t2) ⇒ t1 ∧ x ⇒ t2 ∧ x

RIGHT_IMP_OR_INTRO

⊢ ∀x t1 t2. (t1 ⇒ t2) ⇒ t1 ∨ x ⇒ t2 ∨ x

SIMPLE_GUESS_EXISTS_ALT_DEF

⊢ (∀v. SIMPLE_GUESS_EXISTS v i (P v)) ⇔ GUESS_EXISTS_GAP (K i) (λv. P v)

SIMPLE_GUESS_EXISTS_AND_1

⊢ ∀v i P1 P2.
    SIMPLE_GUESS_EXISTS v i P1 ⇒ SIMPLE_GUESS_EXISTS v i (P1 ∧ P2)

SIMPLE_GUESS_EXISTS_AND_2

⊢ ∀v i P1 P2.
    SIMPLE_GUESS_EXISTS v i P2 ⇒ SIMPLE_GUESS_EXISTS v i (P1 ∧ P2)

SIMPLE_GUESS_EXISTS_EQ_1

⊢ ∀v i. SIMPLE_GUESS_EXISTS v i (v = i)

SIMPLE_GUESS_EXISTS_EQ_2

⊢ ∀v i. SIMPLE_GUESS_EXISTS v i (i = v)

SIMPLE_GUESS_EXISTS_EQ_FUN

⊢ ∀v i t1 t2 f.
    SIMPLE_GUESS_EXISTS v i (f t1 = f t2) ⇒
    SIMPLE_GUESS_EXISTS v i (t1 = t2)

SIMPLE_GUESS_EXISTS_EQ_T

⊢ ∀v. SIMPLE_GUESS_EXISTS v T v

SIMPLE_GUESS_EXISTS_EXISTS

⊢ ∀v i P.
    (∀v2. SIMPLE_GUESS_EXISTS v i (P v2)) ⇒
    SIMPLE_GUESS_EXISTS v i (∃v2. P v2)

SIMPLE_GUESS_EXISTS_FORALL

⊢ ∀v i P.
    (∀v2. SIMPLE_GUESS_EXISTS v i (P v2)) ⇒
    SIMPLE_GUESS_EXISTS v i (∀v2. P v2)

SIMPLE_GUESS_EXISTS_NEG

⊢ ∀v i P. SIMPLE_GUESS_FORALL v i P ⇒ SIMPLE_GUESS_EXISTS v i (¬P)

SIMPLE_GUESS_EXISTS_THM

⊢ ∀i P. (∀v. SIMPLE_GUESS_EXISTS v i (P v)) ⇒ ((∃v. P v) ⇔ P i)

SIMPLE_GUESS_FORALL_ALT_DEF

⊢ (∀v. SIMPLE_GUESS_FORALL v i (P v)) ⇔ GUESS_FORALL_GAP (K i) (λv. P v)

SIMPLE_GUESS_FORALL_EXISTS

⊢ ∀v i P.
    (∀v2. SIMPLE_GUESS_FORALL v i (P v2)) ⇒
    SIMPLE_GUESS_FORALL v i (∃v2. P v2)

SIMPLE_GUESS_FORALL_FORALL

⊢ ∀v i P.
    (∀v2. SIMPLE_GUESS_FORALL v i (P v2)) ⇒
    SIMPLE_GUESS_FORALL v i (∀v2. P v2)

SIMPLE_GUESS_FORALL_IMP_1

⊢ ∀v i P1 P2.
    SIMPLE_GUESS_EXISTS v i P1 ⇒ SIMPLE_GUESS_FORALL v i (P1 ⇒ P2)

SIMPLE_GUESS_FORALL_IMP_2

⊢ ∀v i P1 P2.
    SIMPLE_GUESS_FORALL v i P2 ⇒ SIMPLE_GUESS_FORALL v i (P1 ⇒ P2)

SIMPLE_GUESS_FORALL_NEG

⊢ ∀v i P. SIMPLE_GUESS_EXISTS v i P ⇒ SIMPLE_GUESS_FORALL v i (¬P)

SIMPLE_GUESS_FORALL_OR_1

⊢ ∀v i P1 P2.
    SIMPLE_GUESS_FORALL v i P1 ⇒ SIMPLE_GUESS_FORALL v i (P1 ∨ P2)

SIMPLE_GUESS_FORALL_OR_2

⊢ ∀v i P1 P2.
    SIMPLE_GUESS_FORALL v i P2 ⇒ SIMPLE_GUESS_FORALL v i (P1 ∨ P2)

SIMPLE_GUESS_FORALL_THM

⊢ ∀i P. (∀v. SIMPLE_GUESS_FORALL v i (P v)) ⇒ ((∀v. P v) ⇔ P i)

SIMPLE_GUESS_SELECT_THM

⊢ ∀i P.
    (∀v. SIMPLE_GUESS_EXISTS v i (P v)) ⇒
    ((@v. P v) = if P i then i else @v. F)

SIMPLE_GUESS_SOME_THM

⊢ ∀i P.
    (∀v. SIMPLE_GUESS_EXISTS v i (P v)) ⇒
    ((some v. P v) = if P i then SOME i else NONE)

SIMPLE_GUESS_UEXISTS_THM

⊢ ∀i P. (∀v. SIMPLE_GUESS_EXISTS v i (P v)) ⇒ ((∃!v. P v) ⇔ P i)

SND_PAIR_EQ

⊢ ∀p p1. ((p1,SND p) = p) ⇔ (p1 = FST p)

SND_PAIR_EQ_SYM

⊢ ∀p p1. (p = (p1,SND p)) ⇔ (FST p = p1)

SOME_THE_EQ

⊢ ∀opt. (SOME (THE opt) = opt) ⇔ IS_SOME opt

SOME_THE_EQ_SYM

⊢ ∀opt. (opt = SOME (THE opt)) ⇔ IS_SOME opt

UNWIND_EXISTS_THM

⊢ ∀a P. (∃x. P x) ⇔ (∀x. x ≠ a ⇒ ¬P x) ⇒ P a

Theory quantHeuristics

Parents

Contents

Type operators

Constants

Definitions

Theorems

Definitions

Theorems