matitaB/matita/contribs/ng_TPTP/COL058-3.ma

   1 include "logic/equality.ma".
   2
   3 (* Inclusion of: COL058-3.p *)
   4
   5 (* -------------------------------------------------------------------------- *)
   6
   7 (*  File     : COL058-3 : TPTP v3.7.0. Released v1.0.0. *)
   8
   9 (*  Domain   : Combinatory Logic *)
  10
  11 (*  Problem  : If there's a lark, then there's an egocentric bird. *)
  12
  13 (*  Version  : Especial. *)
  14
  15 (*             Theorem formulation : The egocentric bird is provided and  *)
  16
  17 (*             checked. *)
  18
  19 (*  English  : Suppose we are given a forest that conrtains a lark, and  *)
  20
  21 (*             we are not given any other information. Prove that at least  *)
  22
  23 (*             one bird in the forest must be egocentric. *)
  24
  25 (*  Refs     : [Smu85] Smullyan (1978), To Mock a Mocking Bird and Other Logi *)
  26
  27 (*           : [GO86]  Glickfield & Overbeek (1986), A Foray into Combinatory *)
  28
  29 (*  Source   : [GO86] *)
  30
  31 (*  Names    : - [GO86] *)
  32
  33 (*  Status   : Unsatisfiable *)
  34
  35 (*  Rating   : 0.00 v2.2.1, 0.11 v2.2.0, 0.14 v2.1.0, 0.00 v2.0.0 *)
  36
  37 (*  Syntax   : Number of clauses     :    2 (   0 non-Horn;   2 unit;   1 RR) *)
  38
  39 (*             Number of atoms       :    2 (   2 equality) *)
  40
  41 (*             Maximal clause size   :    1 (   1 average) *)
  42
  43 (*             Number of predicates  :    1 (   0 propositional; 2-2 arity) *)
  44
  45 (*             Number of functors    :    2 (   1 constant; 0-2 arity) *)
  46
  47 (*             Number of variables   :    2 (   0 singleton) *)
  48
  49 (*             Maximal term depth    :    6 (   4 average) *)
  50
  51 (*  Comments :  *)
  52
  53 (* -------------------------------------------------------------------------- *)
  54
  55 (* ---- There exists a lark  *)
  56
  57 (* ---- Hypothesis: This bird is egocentric  *)
  58 ntheorem prove_the_bird_exists:
  59  (∀Univ:Type.∀X1:Univ.∀X2:Univ.
  60 ∀lark:Univ.
  61 ∀response:∀_:Univ.∀_:Univ.Univ.
  62 ∀H0:∀X1:Univ.∀X2:Univ.eq Univ (response (response lark X1) X2) (response X1 (response X2 X2)).eq Univ (response (response (response (response lark lark) (response lark (response lark lark))) (response lark (response lark lark))) (response (response (response lark lark) (response lark (response lark lark))) (response lark (response lark lark)))) (response (response (response lark lark) (response lark (response lark lark))) (response lark (response lark lark))))
  63 .
  64 #Univ ##.
  65 #X1 ##.
  66 #X2 ##.
  67 #lark ##.
  68 #response ##.
  69 #H0 ##.
  70 nauto by H0 ##;
  71 ntry (nassumption) ##;
  72 nqed.
  73
  74 (* -------------------------------------------------------------------------- *)