Упражнения по теме Триггеры

1. Перечислите все триггеры в каждой из формул.

   1. forall x y. x > 0 ∧ y > 0 → x + y > 0
   2. forall x y. x > 0 ∧ y > 0 → f x + f y > 0
   3. forall x. x > 0 → exists y. y < x
   4. exists x. forall y. y > x → y * x = y

2. Докажите утверждение-цель (Ц) из исходных утверждений (1-3) как бы это сделал солвер. Если это сделать невозможно, обоснуйте это.

   1. 1) forall x. x < f x
      Ц) forall x. x < f (f x)

   2. 1) f 0 ≥ 0
      2) forall x y. x ≤ y → f x ≤ f y
      Ц) forall x. x ≥ 0 → f x ≥ 0

   3. 1) forall x. x < 0 → f 0 > x
      2) forall x y. x ≤ y → f x ≤ f y
      Ц) forall x. x ≥ 0 → f x ≥ 0

   4. 1) forall x. x < 0 → f 0 > x
      2) forall x y. x ≤ y → f x ≤ f y
      3) forall x. f (f x + f x) < f (f x)
      Ц) forall x. x ≥ 0 → f x ≥ 0

   5. 1) forall x. x < 0 → f (x + 1) > x
      2) forall x y. x ≤ y → f x ≤ f y
      Ц) forall x. x ≥ 0 → f x ≥ 0

   6. 1) forall x. x < 0 ∧ (exists y. x = 2 * y + 1) → f (x + 1) > x
      2) forall x y. x ≤ y → f x ≤ f y
      Ц) forall x. x ≥ 0 → f x ≥ 0