%--------------------------------------------------------------------------
% File     : MGT070+1 : TPTP v9.3.0. Released v9.3.0.
% Domain   : Management
% Problem  : Sharpness of Unknown in the Compatible direction
% Version  : Especial.
% English  : For every Unknown scenario with domain bounds [ninf, nsup], 
%            there exists a value V (namely V=n0) for which a Compatible 
%            completion holds. This is thm:unknown-sound (compatible 
%            direction): Unknown is sharp - it does not collapse to 
%            Conflict, because a Compatible completion always exists.

% Refs     : [MC+26] Mustafa et al. (2026), Axis Decomposition for ODRL
% Source   : [MC+26]
% Names    : HARD002+1.p [MC+26]

% Status   : Theorem
% Rating   : 0.00 v9.3.0
% Syntax   : Number of formulae    :   40 (  12 unt;   0 def)
%            Number of atoms       :  113 (  24 equ)
%            Maximal formula atoms :    7 (   2 avg)
%            Number of connectives :   80 (   7   ~;   9   |;  36   &)
%                                         (   8 <=>;  20  =>;   0  <=;   0 <~>)
%            Maximal formula depth :   10 (   5 avg)
%            Maximal term depth    :    2 (   1 avg)
%            Number of predicates  :   13 (  12 usr;   0 prp; 1-4 aty)
%            Number of functors    :    7 (   7 usr;   6 con; 0-2 aty)
%            Number of variables   :   89 (  85   !;   4   ?)
% SPC      : FOF_THM_RFO_SEQ

% Comments : 
%--------------------------------------------------------------------------
include('Axioms/MGT002+0.ax').
include('Axioms/MGT002+1.ax').
include('Axioms/MGT002+2.ax').
include('Axioms/MGT002+4.ax').
%--------------------------------------------------------------------------
%----Setup: a concrete Unknown scenario.
%----P1 constrains width with gteq n0 (interval [n0, nsup]).
%----P2 does not constrain width at all.
%----The height axis is unconstrained by both policies.
%----box_verdict = Unknown (both axes unconstrained by at least one policy)
fof(h_inf_0,hypothesis,
    less(ninf,n0) ).

fof(h_0_sup,hypothesis,
    less(n0,nsup) ).

fof(h_inf_lb,hypothesis,
    ! [X] : leq(ninf,X) ).

fof(h_sup_ub,hypothesis,
    ! [X] : leq(X,nsup) ).

%----The box verdict is Unknown (both axes have at least one policy absent).
fof(h_unknown,hypothesis,
    box_verdict(unknown,unknown) = unknown ).

%----Sharpness of Unknown in the Compatible direction.
%----There exists a value V in [ninf, nsup] for which a Compatible
%----completion holds. This shows Unknown is NOT uniformly Conflict - 
%----the Compatible direction is reachable.
fof(unknown_sound_compatible,conjecture,
    ? [V] :
      ( leq(ninf,V)
      & leq(V,nsup)
      & completion_compatible(V,ninf,nsup) ) ).

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