<commit_before>------------------------------------------------------------------------------
-- Unproven PA properties
------------------------------------------------------------------------------

{-# OPTIONS --no-universe-polymorphism #-}
{-# OPTIONS --without-K #-}

module PA.Axiomatic.Mendelson.Properties.UnprovedATP where

open import PA.Axiomatic.Mendelson.Base
open import PA.Axiomatic.Mendelson.PropertiesATP

------------------------------------------------------------------------------

+-asocc : ∀ m n o → m + n + o ≈ m + (n + o)
+-asocc m n o = S₉ A A0 is m
  where
  A : ℕ → Set
  A i = i + n + o ≈ i + (n + o)
  {-# ATP definition A #-}

  postulate A0 : A zero
  {-# ATP prove A0 +-leftCong #-}

  -- 31 July 2013: The ATPs could not prove the theorem (240 sec).
  --
  -- After the addition of the inequality _≉_, no ATP proves the
  -- theorem. Before it, only Equinox 5.0alpha (2010-06-29) had proved
  -- the theorem.
  postulate is : ∀ i → A i → A (succ i)
  {-# ATP prove is +-leftCong #-}<commit_msg>Updated doc for an unproven conjecture.<commit_after>------------------------------------------------------------------------------
-- Unproven PA properties
------------------------------------------------------------------------------

{-# OPTIONS --no-universe-polymorphism #-}
{-# OPTIONS --without-K #-}

module PA.Axiomatic.Mendelson.Properties.UnprovedATP where

open import PA.Axiomatic.Mendelson.Base
open import PA.Axiomatic.Mendelson.PropertiesATP

------------------------------------------------------------------------------

+-asocc : ∀ m n o → m + n + o ≈ m + (n + o)
+-asocc m n o = S₉ A A0 is m
  where
  A : ℕ → Set
  A i = i + n + o ≈ i + (n + o)
  {-# ATP definition A #-}

  postulate A0 : A zero
  {-# ATP prove A0 +-leftCong #-}

  -- 25 November 2013: Vampire 0.6 proves the theorem using a time out
  -- of (300 sec).
  postulate is : ∀ i → A i → A (succ i)
  {-# ATP prove is +-leftCong #-}
{'fraction_non_alphanumeric': 0.3487654320987654, 'fraction_numerical': 0.018518518518518517, 'mean_word_length': 1.18785151856018, 'pattern_counts': {'":': 0, '<': 3, '<?xml version=': 0, '>': 3, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 6, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '6813742', 'n_tokens_mistral': 664, 'n_tokens_neox': 579, 'n_words': 212}