Tales of Tails

Description

From "Anarchy Proof".

Definitions (download)

module Definitions where

open import Data.List
open import Data.List.Any
open import Data.Product
open import Function.Equivalence
open import Relation.Binary.PropositionalEquality
open Data.List.Any.Membership-≡


_isSuffixOf_ : ∀ {a} {A : Set a} → List A → List A → Set a
_isSuffixOf_ {a} {A} xs ys = Σ[ zs ∈ List A ] zs ++ xs ≡ ys

_isAllSuffixOf_ : ∀ {a} {A : Set a} → List (List A) → List A → Set a
_isAllSuffixOf_ xss ys = ∀ xs → xs isSuffixOf ys ⇔ xs ∈ xss

Theorem (download)

module Theorem where

open import Definitions
open import Data.List
open import Data.Product

postulate
  mytails : ∀ {a} {A : Set a} (ys : List A) → Σ[ xss ∈ List (List A) ] xss isAllSuffixOf ys

Verifier

module Verifier where

open import Definitions
open import Theorem
open import Data.List
open import Data.Product

checkTails : ∀ {a} {A : Set a} (ys : List A) → Σ[ xss ∈ List (List A) ] xss isAllSuffixOf ys
checkTails = mytails

Proofs

Rank Prover Size Date
1 notogawa 1053 2013-06-02 11:38:17 JST
2 Rotsor 1115 2013-12-29 03:22:35 JST
3 masahiro_sakai 1221 2014-11-27 20:51:36 JST
4 Lost_dog_ 1257 2013-06-02 12:09:17 JST
5 trigott 1594 2014-11-19 16:37:58 JST