#u X

#a 5

#q 1

% forall x, y. f(x) == f(y) => x == y
% forall x. f(x) != C

#check NONE

domain{0,1,2,3,...}

%domain is the set of of natural numbers

syntax
c = 0
f(x) = x + 2

M[forall x,y . f(x) == f(y) => x == y]
= forall x,y . M[f(x) == (f(y) => x == y)]
= forall x M[f(x) == f(_y_) => x == y] AND forall y M[f(_x_) == f(y) => _x_ == y]


forall x  M[f(x) == f(_y_) => x == _y_ ]

M[f(0) == f(_y_) => 0 == _y_ ]
= M[f(0) == f(0) => 0 == 0]
= 2 == 2 IMP 0 == 0
= T IMP T

M[f(0) == f(1) => 0 == 1]
= f(0) == f(1) IMP 0 == 1
= 2 == 4 IMP 0 == 1
= F IMP F
= T

....

Continuing for the entire domain we can see that if the values are equal then x == y and other wise it is false implies false which is also true


forall y M[f(_x_) == f(y) => _x_ == y]

M[f(_x_) == f(0) => _x_ == 0]
= M[f(0) == f(0) => 0 == 0]
= 2 == 2 IMP 0 == 0
= T IMP T

M[f(0) == f(1) => 0 == 1]
= f(0) == f(1) IMP 0 == 1
= 2 == 4 IMP 0 == 1
= F IMP F
= T

....

Continuing for the entire domain we can see that if the values are equal then x == y and other wise it is false implies false which is also true



forall x M[f(x) != C]

M[f(0) != _C_ ]
= M[2 != 0]
= T by arith


M[f(1) != _C_ ]
= M[3 != C]
= T by arith

.....

the domain starts at x = 0 and that gives 2
and with each subsequent number, f(x) gives a larger and larger number
since the domain is the set of natural number and we can expand this to infinity
meaning we can always found a x + 2 that's within our domain