% Saved by Prover9-Mace4 Version 0.5, December 2007.

set(ignore_option_dependencies). % GUI handles dependencies

if(Prover9). % Options for Prover9
  assign(max_seconds, 310).
end_if.

if(Mace4).   % Options for Mace4
  assign(max_seconds, 120).
end_if.

formulas(assumptions).

%Theory of quantities

%Basic axioms of quantities

%Axiom: partial order 
x <= x #label(A_reflexivity_po).
(x <= y & x >= y) -> x = y #label(A_antisymmetry_po).
(x <= y & y <= z) -> x <= z #label(A_transitivity_po).

%Def
x <= y <-> y >= x #label(A_gtlt_po).
(x <= y & -(y <= x)) <-> x < y #label(Def_so).
x < y <-> y > x #label(A_gtlt_so).
O(x,y) <-> exists z (z <= x & z <= y) #label(definition_overlap).

% Axiom: sums
x + 0 = x #label(A_identity_element_add).
x + y = y + x  #label(A_symmetry_add).
(x + y) + z = x + (y + z) #label(A_associativity_add).
x + -x = 0  #label(A_inverse_add).
x <= y -> x+z <= y+z #label(translation_invariance).

% Basic Theorems provable for quantities
x <= y <- x+z <= y+z #label(A_ordered_add).
x + y = z & 0 <= y -> x <= z #label(A_ordered2_add).
x + -y = z <-> x = z + y #label(negativity_add).
x + y = z & y > 0 -> x < z #label(strict_order_add).
x + y = z -> y + x = z #label(symmetry_of_sums).

%Subtheory 1
%Mereological quantity (non-total extensional mereology) (= amount)

%Mereological axioms
-(y <= x) -> (exists v  (v <= y & -O(v,x))) #label(strong_supplementation).
%-P(y,x) & P(y,y) & P(x,x) -> (exists v  (P(v,y) & -O(v,x))) #label(strong_supplementation).

%Axiom: non-totality
exists x exists y -(x <= y | y <= x ) #label(non_totality).

%Mereological theorems
(x <= y & 0 <= x) -> x + y = y #label(reflexivity_of_sums).
%P(x,y) -> SUM(x,y,y).
0 <= x -> x + x = x #label(reflexivity_of_sums).
%P(x,x) -> SUM(x,x,x) 
(0 <= x & 0 <= y) -> (x + y = z -> x <= z & y <= z).
%SUM(x,y,z) -> (P(x,z) & P(y,z)).
x <= y -> (y + -x = z -> y + -z = x).
%P(x,y) -> (MIN(y,x,z)->MIN(y,z,x)).
x + y = z & -O(x,y) -> z + -x = y.
%SUM(x,y,z) & -O(x,y) -> MIN(z,x,y).
(0 < x | 0 < y) -> (all z (z < x <-> z < y)-> x = y) #label(mereological_extensionality).
%non-atomic entities with the same parts are identical

%Axiom: Domain closure, to make sure quantities with equivalent measures exist
all x all y m(x) <= m(y) -> (exists z z <= y & m(z) = m(x)).

%Extensive Measurement theory
-O(x,y) -> m(x) + m(y) = m(x + y).

%Theorems about extensive measures
y <= x -> m(x) + -m(y) = m(x + -y).
-(z <= x) -> exists w (w <= z & m(x) + m(w) = m(x + w)). % 222.42 seconds

%Subtheory 2
%Totally ordered quantity (= magnitude)

%x <= y | y <= x #label(totality).
m(x) <= m(y) | m(y) <= m(x) #label(totality_of_range).

%Theorem: in this case, m must be non-injective (Proven in 290.11 second)
exists x exists y -(x = y) & m(x) = m(y).

end_of_list.

formulas(goals).

end_of_list.