%------------------------------------------------------------------------------
% File     : SWX238_1 : TPTP v9.3.0. Released v9.3.0.
% Domain   : Software Verification
% Problem  : Find a regular expression with a certain property
% Version  : Especial.
% English  :

% Refs     : [CST26] Claessen et al. (2026), Email to Geoff Sutcliffe
% Source   : [CST26]
% Names    : RegExp_prop_kfind6.p [CST26]

% Status   : Theorem
% Rating   : 1.00 v9.3.0
% Syntax   : Number of formulae    :   77 (  55 unt;   1 typ;   0 def)
%            Number of atoms       :  333 (  77 equ)
%            Maximal formula atoms :    5 (   4 avg)
%            Number of connectives :   88 (  49   ~;   3   |;   3   &)
%                                         (  10 <=>;  23  =>;   0  <=;   0 <~>)
%            Maximal formula depth :    8 (   4 avg)
%            Maximal term depth    :    2 (   1 avg)
%            Number of FOOLs       :  226 ( 220 fml;   6 var)
%            Number of types       :    2 (   0 usr)
%            Number of type conns  :    2 (   1   >;   1   *;   0   +;   0  <<)
%            Number of predicates  :   40 (  39 usr;   8 prp; 0-3 aty)
%            Number of functors    :    1 (   1 usr;   0 con; 2-2 aty)
%            Number of variables   :  136 ( 135   !;   1   ?;   4   :)
% SPC      : TX0_THM_EQU_NAR

% Comments :
%------------------------------------------------------------------------------
tff(type_001,type,
    cons3: ( $o * $i ) > $i ).

tff(axiom_002,axiom,
    ! [X,X2] : ( proj1pair(pair2(X,X2)) = X ) ).

tff(axiom_003,axiom,
    ! [X,X2] : ( proj2pair(pair2(X,X2)) = X2 ) ).

tff(axiom_004,axiom,
    ! [X,X2] : ( head(cons(X,X2)) = X ) ).

tff(axiom_005,axiom,
    ! [X,X2] : ( tail(cons(X,X2)) = X2 ) ).

tff(axiom_006,axiom,
    ! [X,X2] : ( nil != cons(X,X2) ) ).

tff(axiom_007,axiom,
    ! [X,X2] : ( head2(cons2(X,X2)) = X ) ).

tff(axiom_008,axiom,
    ! [X,X2] : ( tail2(cons2(X,X2)) = X2 ) ).

tff(axiom_009,axiom,
    ! [X,X2] : ( nil2 != cons2(X,X2) ) ).

tff(axiom_010,axiom,
    ! [X: $o,X2] :
      ( head3(cons3((X),X2))
    <=> (X) ) ).

tff(axiom_011,axiom,
    ! [X: $o,X2] : ( tail3(cons3((X),X2)) = X2 ) ).

tff(axiom_012,axiom,
    ! [X: $o,X2] : ( nil3 != cons3((X),X2) ) ).

tff(axiom_013,axiom,
    a != b ).

tff(axiom_014,axiom,
    a != c ).

tff(axiom_015,axiom,
    b != c ).

tff(axiom_016,axiom,
    ! [X] : ( proj1Atom(atom(X)) = X ) ).

tff(axiom_017,axiom,
    ! [X,X2] : ( proj1(x(X,X2)) = X ) ).

tff(axiom_018,axiom,
    ! [X,X2] : ( proj2(x(X,X2)) = X2 ) ).

tff(axiom_019,axiom,
    ! [X,X2] : ( proj12(y(X,X2)) = X ) ).

tff(axiom_020,axiom,
    ! [X,X2] : ( proj22(y(X,X2)) = X2 ) ).

tff(axiom_021,axiom,
    ! [X] : ( proj1Star(star(X)) = X ) ).

tff(axiom_022,axiom,
    nil4 != eps ).

tff(axiom_023,axiom,
    ! [X] : ( nil4 != atom(X) ) ).

tff(axiom_024,axiom,
    ! [X,X2] : ( nil4 != x(X,X2) ) ).

tff(axiom_025,axiom,
    ! [X,X2] : ( nil4 != y(X,X2) ) ).

tff(axiom_026,axiom,
    ! [X] : ( nil4 != star(X) ) ).

tff(axiom_027,axiom,
    ! [X] : ( eps != atom(X) ) ).

tff(axiom_028,axiom,
    ! [X,X2] : ( eps != x(X,X2) ) ).

tff(axiom_029,axiom,
    ! [X,X2] : ( eps != y(X,X2) ) ).

tff(axiom_030,axiom,
    ! [X] : ( eps != star(X) ) ).

tff(axiom_031,axiom,
    ! [X,X2,X3] : ( atom(X) != x(X2,X3) ) ).

tff(axiom_032,axiom,
    ! [X,X2,X3] : ( atom(X) != y(X2,X3) ) ).

tff(axiom_033,axiom,
    ! [X,X2] : ( atom(X) != star(X2) ) ).

tff(axiom_034,axiom,
    ! [X,X2,X3,X4] : ( x(X,X2) != y(X3,X4) ) ).

tff(axiom_035,axiom,
    ! [X,X2,X3] : ( x(X,X2) != star(X3) ) ).

tff(axiom_036,axiom,
    ! [X,X2,X3] : ( y(X,X2) != star(X3) ) ).

tff(axiom_037,axiom,
    ! [X,Y] :
      ( ( X != nil4 )
     => ( ( Y != nil4 )
       => ( ( X != eps )
         => ( ( Y != eps )
           => ( z(X,Y) = y(X,Y) ) ) ) ) ) ).

tff(axiom_038,axiom,
    ! [X] :
      ( ( X != nil4 )
     => ( ( X != eps )
       => ( z(X,eps) = X ) ) ) ).

tff(axiom_039,axiom,
    ! [Y] :
      ( ( Y != nil4 )
     => ( z(eps,Y) = Y ) ) ).

tff(axiom_040,axiom,
    ! [X] :
      ( ( X != nil4 )
     => ( z(X,nil4) = nil4 ) ) ).

tff(axiom_041,axiom,
    ! [Y] : ( z(nil4,Y) = nil4 ) ).

tff(axiom_042,axiom,
    ! [X,Y] :
      ( ( X != nil4 )
     => ( ( Y != nil4 )
       => ( x2(X,Y) = x(X,Y) ) ) ) ).

tff(axiom_043,axiom,
    ! [X] :
      ( ( X != nil4 )
     => ( x2(X,nil4) = X ) ) ).

tff(axiom_044,axiom,
    ! [Y] : ( x2(nil4,Y) = Y ) ).

tff(axiom_045,axiom,
    ! [X] : ( splits(X,nil) = nil ) ).

tff(axiom_046,axiom,
    ! [X,X2,Bs,Cs] : ( splits(X,cons(pair2(Bs,Cs),X2)) = cons(pair2(cons2(X,Bs),Cs),splits(X,X2)) ) ).

tff(axiom_047,axiom,
    splits2(nil2) = cons(pair2(nil2,nil2),nil) ).

tff(axiom_048,axiom,
    ! [Y,Xs] : ( splits2(cons2(Y,Xs)) = cons(pair2(nil2,cons2(Y,Xs)),splits(Y,splits2(Xs))) ) ).

tff(axiom_049,axiom,
    ~ or2(nil3) ).

tff(axiom_050,axiom,
    ! [Y: $o,Xs] :
      ( or2(cons3((Y),Xs))
    <=> ( (Y)
        | or2(Xs) ) ) ).

tff(axiom_051,axiom,
    ! [X] :
      ( ( X != eps )
     => ( ( X != x(proj1(X),proj2(X)) )
       => ( ( X != y(proj12(X),proj22(X)) )
         => ( ( X != star(proj1Star(X)) )
           => ~ eps2(X) ) ) ) ) ).

tff(axiom_052,axiom,
    eps2(eps) ).

tff(axiom_053,axiom,
    ! [P,Q] :
      ( eps2(x(P,Q))
    <=> ( eps2(P)
        | eps2(Q) ) ) ).

tff(axiom_054,axiom,
    ! [R,Q2] :
      ( eps2(y(R,Q2))
    <=> ( eps2(R)
        & eps2(Q2) ) ) ).

tff(axiom_055,axiom,
    ! [Y] : eps2(star(Y)) ).

tff(axiom_056,axiom,
    ! [X,Y] :
      ( ( X != atom(proj1Atom(X)) )
     => ( ( X != x(proj1(X),proj2(X)) )
       => ( ( X != y(proj12(X),proj22(X)) )
         => ( ( X != star(proj1Star(X)) )
           => ( step(X,Y) = nil4 ) ) ) ) ) ).

tff(axiom_057,axiom,
    ! [Y,B] :
      ( ( B = Y )
     => ( step(atom(B),Y) = eps ) ) ).

tff(axiom_058,axiom,
    ! [Y,B] :
      ( ( B != Y )
     => ( step(atom(B),Y) = nil4 ) ) ).

tff(axiom_059,axiom,
    ! [Y,P,Q] : ( step(x(P,Q),Y) = x(step(P,Y),step(Q,Y)) ) ).

tff(axiom_060,axiom,
    ! [Y,R,Q2] :
      ( eps2(R)
     => ( step(y(R,Q2),Y) = x(y(step(R,Y),Q2),step(Q2,Y)) ) ) ).

tff(axiom_061,axiom,
    ! [Y,R,Q2] :
      ( ~ eps2(R)
     => ( step(y(R,Q2),Y) = x(y(step(R,Y),Q2),nil4) ) ) ).

tff(axiom_062,axiom,
    ! [Y,P2] : ( step(star(P2),Y) = y(step(P2,Y),star(P2)) ) ).

tff(axiom_063,axiom,
    ! [X] :
      ( rec(X,nil2)
    <=> eps2(X) ) ).

tff(axiom_064,axiom,
    ! [X,Z,Xs] :
      ( rec(X,cons2(Z,Xs))
    <=> rec(step(X,Z),Xs) ) ).

tff(axiom_065,axiom,
    ! [Y] : ~ reck2(nil4,Y) ).

tff(axiom_066,axiom,
    reck2(eps,nil2) ).

tff(axiom_067,axiom,
    ! [Z,X2] : ~ reck2(eps,cons2(Z,X2)) ).

tff(axiom_068,axiom,
    ! [C] : ~ reck2(atom(C),nil2) ).

tff(axiom_069,axiom,
    ! [C,B2] :
      ( reck2(atom(C),cons2(B2,nil2))
    <=> ( C = B2 ) ) ).

tff(axiom_070,axiom,
    ! [C,B2,X4,X5] : ~ reck2(atom(C),cons2(B2,cons2(X4,X5))) ).

tff(axiom_071,axiom,
    ! [Y,P,Q] :
      ( reck2(x(P,Q),Y)
    <=> ( reck2(P,Y)
        | reck2(Q,Y) ) ) ).

tff(axiom_072,axiom,
    ! [Y,R,Q2] :
      ( reck2(y(R,Q2),Y)
    <=> or2(reck(R,Q2,splits2(Y))) ) ).

tff(axiom_073,axiom,
    ! [P2] : reck2(star(P2),nil2) ).

tff(axiom_074,axiom,
    ! [P2,X6,X7] :
      ( reck2(star(P2),cons2(X6,X7))
    <=> ( ~ eps2(P2)
        & rec(y(P2,star(P2)),cons2(X6,X7)) ) ) ).

tff(axiom_075,axiom,
    ! [P,Q] : ( reck(P,Q,nil) = nil3 ) ).

tff(axiom_076,axiom,
    ! [P,Q,Z,L,R] :
      ( reck(P,Q,cons(pair2(L,R),Z)) = cons3(( reck2(P,L)
          & rec(Q,R) ),reck(P,Q,Z)) ) ).

tff(goal_077,conjecture,
    ? [P] : reck2(P,cons2(a,cons2(b,cons2(a,cons2(b,cons2(b,nil2)))))) ).

%------------------------------------------------------------------------------