%------------------------------------------------------------------------------
% File     : SWX219+1 : TPTP v9.3.0. Released v9.3.0.
% Domain   : Software Verification
% Problem  : Show a specific given type is inhabited
% Version  : Especial.
% English  :

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

% Status   : Theorem
% Rating   : 0.57 v9.3.0
% Syntax   : Number of formulae    :   32 (  27 unt;   0 def)
%            Number of atoms       :   39 (  30 equ)
%            Maximal formula atoms :    3 (   1 avg)
%            Number of connectives :   22 (  15   ~;   0   |;   1   &)
%                                         (   3 <=>;   3  =>;   0  <=;   0 <~>)
%            Maximal formula depth :    8 (   4 avg)
%            Maximal term depth    :    4 (   1 avg)
%            Number of predicates  :    2 (   1 usr;   0 prp; 2-3 aty)
%            Number of functors    :   25 (  25 usr;   6 con; 0-3 aty)
%            Number of variables   :   67 (  66   !;   1   ?)
% SPC      : FOF_THM_RFO_SEQ

% Comments :
%------------------------------------------------------------------------------
fof(axiom_001,axiom,
    ! [X,X2] : head(cons(X,X2)) = X ).

fof(axiom_002,axiom,
    ! [X,X2] : tail(cons(X,X2)) = X2 ).

fof(axiom_003,axiom,
    ! [X,X2] : nil != cons(X,X2) ).

fof(axiom_004,axiom,
    ! [X,X2] : proj1Arr(arr(X,X2)) = X ).

fof(axiom_005,axiom,
    ! [X,X2] : proj2Arr(arr(X,X2)) = X2 ).

fof(axiom_006,axiom,
    ! [X,X2] : arr(X,X2) != a ).

fof(axiom_007,axiom,
    ! [X,X2] : arr(X,X2) != b ).

fof(axiom_008,axiom,
    ! [X,X2] : arr(X,X2) != c ).

fof(axiom_009,axiom,
    a != b ).

fof(axiom_010,axiom,
    a != c ).

fof(axiom_011,axiom,
    b != c ).

fof(axiom_012,axiom,
    ! [X] : proj1Suc(suc(X)) = X ).

fof(axiom_013,axiom,
    ! [X] : zero != suc(X) ).

fof(axiom_014,axiom,
    ! [X] : proj1Just(just(X)) = X ).

fof(axiom_015,axiom,
    ! [X] : nothing != just(X) ).

fof(axiom_016,axiom,
    ! [X,X2,X3] : proj1App(app(X,X2,X3)) = X ).

fof(axiom_017,axiom,
    ! [X,X2,X3] : proj2App(app(X,X2,X3)) = X2 ).

fof(axiom_018,axiom,
    ! [X,X2,X3] : proj3App(app(X,X2,X3)) = X3 ).

fof(axiom_019,axiom,
    ! [X] : proj1Lam(lam(X)) = X ).

fof(axiom_020,axiom,
    ! [X] : proj1Var(var(X)) = X ).

fof(axiom_021,axiom,
    ! [X,X2,X3,X4] : app(X,X2,X3) != lam(X4) ).

fof(axiom_022,axiom,
    ! [X,X2,X3,X4] : app(X,X2,X3) != var(X4) ).

fof(axiom_023,axiom,
    ! [X,X2] : lam(X) != var(X2) ).

fof(axiom_024,axiom,
    ! [Y] : index(nil,Y) = nothing ).

fof(axiom_025,axiom,
    ! [Z,Xs] : index(cons(Z,Xs),zero) = just(Z) ).

fof(axiom_026,axiom,
    ! [Z,Xs,N] : index(cons(Z,Xs),suc(N)) = index(Xs,N) ).

fof(axiom_027,axiom,
    ! [X,Z,F,X2,Tx] :
      ( tc(X,app(F,X2,Tx),Z)
    <=> ( tc(X,F,arr(Tx,Z))
        & tc(X,X2,Tx) ) ) ).

fof(axiom_028,axiom,
    ! [X,Z,E] :
      ( Z != arr(proj1Arr(Z),proj2Arr(Z))
     => ~ tc(X,lam(E),Z) ) ).

fof(axiom_029,axiom,
    ! [X,E,Tx2,T1] :
      ( tc(X,lam(E),arr(Tx2,T1))
    <=> tc(cons(Tx2,X),E,T1) ) ).

fof(axiom_030,axiom,
    ! [X,Z,X3] :
      ( index(X,X3) = nothing
     => ~ tc(X,var(X3),Z) ) ).

fof(axiom_031,axiom,
    ! [X,Z,X3,Tx3] :
      ( index(X,X3) = just(Tx3)
     => ( tc(X,var(X3),Z)
      <=> Tx3 = Z ) ) ).

fof(goal_032,conjecture,
    ? [E] : tc(nil,E,arr(arr(b,c),arr(arr(a,b),arr(a,c)))) ).

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