nomin_4.miz
begin
reserve v for
object;
reserve V,A for
set;
reserve f for
SCBinominativeFunction of V, A;
definition
let A;
::
NOMIN_4:def1
attr A is
complex-containing means
COMPLEX
c= A;
end
registration
cluster
complex-containing for
set;
existence
proof
take
COMPLEX ;
thus thesis;
end;
cluster
complex-containing -> non
empty for
set;
coherence by
XBOOLE_1: 3;
end
scheme ::
NOMIN_4:sch1
BinPredToFunEx { X,Y() ->
set , P[
object,
object] } :
ex f be
Function of
[:X(), Y():],
BOOLEAN st for x,y be
object st x
in X() & y
in Y() holds (P[x, y] implies (f
. (x,y))
=
TRUE ) & ( not P[x, y] implies (f
. (x,y))
=
FALSE );
defpred
Q[
object,
object,
object] means (P[$1, $2] & $3
=
TRUE ) or ( not P[$1, $2] & $3
=
FALSE );
A1: for x,y be
object st x
in X() & y
in Y() holds ex z be
object st z
in
BOOLEAN &
Q[x, y, z]
proof
let x,y be
object such that x
in X() & y
in Y();
per cases ;
suppose
A2:
Q[x, y,
TRUE ];
take
TRUE ;
thus thesis by
A2;
end;
suppose
A3:
Q[x, y,
FALSE ];
take
FALSE ;
thus thesis by
A3;
end;
end;
consider f be
Function of
[:X(), Y():],
BOOLEAN such that
A4: for x,y be
object st x
in X() & y
in Y() holds
Q[x, y, (f
. (x,y))] from
BINOP_1:sch 1(
A1);
take f;
thus thesis by
A4;
end;
scheme ::
NOMIN_4:sch2
BinPredToFunUnique { X,Y() ->
set , P[
object,
object] } :
for f,g be
Function of
[:X(), Y():],
BOOLEAN st (for x,y be
object st x
in X() & y
in Y() holds (P[x, y] implies (f
. (x,y))
=
TRUE ) & ( not P[x, y] implies (f
. (x,y))
=
FALSE )) & (for x,y be
object st x
in X() & y
in Y() holds (P[x, y] implies (g
. (x,y))
=
TRUE ) & ( not P[x, y] implies (g
. (x,y))
=
FALSE )) holds f
= g;
let f,g be
Function of
[:X(), Y():],
BOOLEAN such that
A1: (for x,y be
object st x
in X() & y
in Y() holds (P[x, y] implies (f
. (x,y))
=
TRUE ) & ( not P[x, y] implies (f
. (x,y))
=
FALSE )) and
A2: (for x,y be
object st x
in X() & y
in Y() holds (P[x, y] implies (g
. (x,y))
=
TRUE ) & ( not P[x, y] implies (g
. (x,y))
=
FALSE ));
for a,b be
set st a
in X() & b
in Y() holds (f
. (a,b))
= (g
. (a,b))
proof
let a,b be
set such that
A3: a
in X() & b
in Y();
(f
. (a,b))
= (g
. (a,b))
proof
per cases ;
suppose
A4: P[a, b];
hence (f
. (a,b))
=
TRUE by
A1,
A3
.= (g
. (a,b)) by
A2,
A3,
A4;
end;
suppose
A5: not P[a, b];
hence (f
. (a,b))
=
FALSE by
A1,
A3
.= (g
. (a,b)) by
A2,
A3,
A5;
end;
end;
hence thesis;
end;
hence thesis by
BINOP_1: 1;
end;
scheme ::
NOMIN_4:sch3
Lambda2Unique { X,Y,Z() ->
set , F(
object,
object) ->
object } :
for f,g be
Function of
[:X(), Y():], Z() st (for x,y be
object st x
in X() & y
in Y() holds (f
. (x,y))
= F(x,y)) & (for x,y be
object st x
in X() & y
in Y() holds (g
. (x,y))
= F(x,y)) holds f
= g;
let f,g be
Function of
[:X(), Y():], Z() such that
A1: for x,y be
object st x
in X() & y
in Y() holds (f
. (x,y))
= F(x,y) and
A2: for x,y be
object st x
in X() & y
in Y() holds (g
. (x,y))
= F(x,y);
for a,b be
set st a
in X() & b
in Y() holds (f
. (a,b))
= (g
. (a,b))
proof
let a,b be
set such that
A3: a
in X() & b
in Y();
(f
. (a,b))
= F(a,b) by
A1,
A3
.= (g
. (a,b)) by
A2,
A3;
hence thesis;
end;
hence thesis by
BINOP_1: 1;
end;
definition
let V, A;
::
NOMIN_4:def2
func
nonatomicsND (V,A) ->
set equals the set of all d where d be
NonatomicND of V, A;
coherence ;
end
theorem ::
NOMIN_4:1
Th1: for d be
object st d
in (
nonatomicsND (V,A)) holds d is
NonatomicND of V, A
proof
let d be
object;
assume d
in (
nonatomicsND (V,A));
then ex d1 be
NonatomicND of V, A st d
= d1;
hence thesis;
end;
theorem ::
NOMIN_4:2
Th2:
{}
in (
nonatomicsND (V,A))
proof
{} is
NonatomicND of V, A by
NOMIN_1: 30;
hence thesis;
end;
registration
let V, A;
cluster (
nonatomicsND (V,A)) -> non
empty
functional;
coherence
proof
thus (
nonatomicsND (V,A)) is non
empty by
Th2;
let v;
thus thesis by
Th1;
end;
end
definition
let V, A;
::
NOMIN_4:def3
pred A
is_without_nonatomicND_wrt V means A
misses (
nonatomicsND (V,A));
end
theorem ::
NOMIN_4:3
Th3: A
is_without_nonatomicND_wrt V implies for d be
NonatomicND of V, A holds not d
in A
proof
assume
A1: A
is_without_nonatomicND_wrt V;
let d be
NonatomicND of V, A;
d
in (
nonatomicsND (V,A));
hence thesis by
A1,
XBOOLE_0: 3;
end;
theorem ::
NOMIN_4:4
Th4: A
is_without_nonatomicND_wrt V & v
in V implies for d1 be
NonatomicND of V, A holds for d2 be
TypeSCNominativeData of V, A holds (
dom (
local_overlapping (V,A,d1,d2,v)))
= (
{v}
\/ (
dom d1))
proof
assume that
A1: A
is_without_nonatomicND_wrt V and
A2: v
in V;
let d1 be
NonatomicND of V, A;
let d2 be
TypeSCNominativeData of V, A;
not d1
in A & not (
naming (V,A,v,d2))
in A by
A1,
Th3;
hence thesis by
A2,
NOMIN_2: 15;
end;
theorem ::
NOMIN_4:5
A
is_without_nonatomicND_wrt V implies for d be
NonatomicND of V, A holds v
in V & d
in (
dom f) implies (
dom ((
SC_assignment (f,v))
. d))
= ((
dom d)
\/
{v})
proof
assume
A1: A
is_without_nonatomicND_wrt V;
let d be
NonatomicND of V, A;
not d
in A & not (
naming (V,A,v,(f
. d)))
in A by
A1,
Th3;
hence thesis by
NOMIN_2: 33;
end;
reserve d for
TypeSCNominativeData of V, A;
reserve d1 for
NonatomicND of V, A;
theorem ::
NOMIN_4:6
Th6: for d1 be
NonatomicND of V, A holds v
in V & A
is_without_nonatomicND_wrt V implies (
local_overlapping (V,A,d1,d,v))
in (
dom (
denaming (V,A,v)))
proof
let d1 be
NonatomicND of V, A;
set L = (
local_overlapping (V,A,d1,d,v));
set D = (
denaming (V,A,v));
A1: (
dom D)
= { d where d be
NonatomicND of V, A : v
in (
dom d) } by
NOMIN_1:def 18;
A2: L is
NonatomicND of V, A by
NOMIN_2: 9;
assume v
in V & A
is_without_nonatomicND_wrt V;
then
A3: (
dom L)
= (
{v}
\/ (
dom d1)) by
Th4;
v
in
{v} by
TARSKI:def 1;
then v
in (
dom L) by
A3,
XBOOLE_0:def 3;
hence thesis by
A1,
A2;
end;
reserve a,b,c,z for
Element of V;
reserve x,y for
object;
reserve p,q,r,s for
SCPartialNominativePredicate of V, A;
definition
let V, A, d, a;
::
NOMIN_4:def4
pred a
is_ext_real_on d means ((
denaming (V,A,a))
. d) is
ext-real;
::
NOMIN_4:def5
pred a
is_complex_on d means ((
denaming (V,A,a))
. d) is
complex;
::
NOMIN_4:def6
pred a
is_a_value_on d means ((
denaming (V,A,a))
. d)
in A;
end
theorem ::
NOMIN_4:7
Th7: A is
complex-containing & (for d holds a
is_complex_on d) implies for d holds a
is_a_value_on d
proof
assume that
A1:
COMPLEX
c= A and
A2: for d holds a
is_complex_on d;
let d;
a
is_complex_on d by
A2;
then ((
denaming (V,A,a))
. d)
in
COMPLEX by
XCMPLX_0:def 2;
hence ((
denaming (V,A,a))
. d)
in A by
A1;
end;
theorem ::
NOMIN_4:8
Th8: (for d holds a
is_a_value_on d) implies (
rng (
denaming (V,A,a)))
c= A
proof
assume
A1: for d holds a
is_a_value_on d;
set f = (
denaming (V,A,a));
let y be
object;
assume y
in (
rng f);
then
consider x be
object such that
A2: x
in (
dom f) and
A3: (f
. x)
= y by
FUNCT_1:def 3;
(
dom f)
= { d where d be
NonatomicND of V, A : a
in (
dom d) } by
NOMIN_1:def 18;
then
consider d be
NonatomicND of V, A such that
A4: x
= d and a
in (
dom d) by
A2;
a
is_a_value_on d by
A1;
hence thesis by
A3,
A4;
end;
theorem ::
NOMIN_4:9
Th9: (for d holds a
is_a_value_on d) & (for d holds b
is_a_value_on d) implies (
rng
<:(
denaming (V,A,a)), (
denaming (V,A,b)):>)
c=
[:A, A:]
proof
set Da = (
denaming (V,A,a));
set Db = (
denaming (V,A,b));
A1: (
rng
<:Da, Db:>)
c=
[:(
rng Da), (
rng Db):] by
FUNCT_3: 51;
assume (for d holds a
is_a_value_on d) & (for d holds b
is_a_value_on d);
then (
rng Da)
c= A & (
rng Db)
c= A by
Th8;
then
[:(
rng Da), (
rng Db):]
c=
[:A, A:] by
ZFMISC_1: 96;
hence thesis by
A1,
XBOOLE_1: 1;
end;
definition
let V, A;
let a,b be
Element of V;
let p be
Function of
[:A, A:],
BOOLEAN ;
::
NOMIN_4:def7
func
lift_binary_pred (p,a,b) ->
SCPartialNominativePredicate of V, A equals (p
*
<:(
denaming (V,A,a)), (
denaming (V,A,b)):>);
coherence
proof
set ab =
<:(
denaming (V,A,a)), (
denaming (V,A,b)):>;
set P = (p
* ab);
A1: (
dom ab)
= ((
dom (
denaming (V,A,a)))
/\ (
dom (
denaming (V,A,b)))) by
FUNCT_3:def 7;
for o be
object holds o
in (
dom P) implies o
in (
dom ab) by
FUNCT_1: 11;
then (
dom P)
c= (
dom ab) by
TARSKI:def 3;
then
A2: (
dom P)
c= (
ND (V,A)) by
A1,
XBOOLE_1: 1;
(
rng P)
c=
BOOLEAN ;
hence thesis by
A2,
RELSET_1: 4;
end;
end
definition
let V, A;
let a,b be
Element of V;
let op be
Function of
[:A, A:], A;
::
NOMIN_4:def8
func
lift_binary_op (op,a,b) ->
SCBinominativeFunction of V, A equals (op
*
<:(
denaming (V,A,a)), (
denaming (V,A,b)):>);
coherence
proof
set ab =
<:(
denaming (V,A,a)), (
denaming (V,A,b)):>;
set P = (op
* ab);
A1: (
dom ab)
= ((
dom (
denaming (V,A,a)))
/\ (
dom (
denaming (V,A,b)))) by
FUNCT_3:def 7;
for o be
object holds o
in (
dom P) implies o
in (
dom ab) by
FUNCT_1: 11;
then (
dom P)
c= (
dom ab) by
TARSKI:def 3;
then
A2: (
dom P)
c= (
ND (V,A)) by
A1,
XBOOLE_1: 1;
(
rng P)
c= (
ND (V,A))
proof
for o be
object holds o
in A implies o
in (
ND (V,A))
proof
let o be
object;
assume o
in A;
then o is
TypeSCNominativeData of V, A by
NOMIN_1:def 6;
hence o
in (
ND (V,A));
end;
then A
c= (
ND (V,A)) by
TARSKI:def 3;
hence thesis by
XBOOLE_1: 1;
end;
hence thesis by
A2,
RELSET_1: 4;
end;
end
definition
let A;
::
NOMIN_4:def9
func
Equality (A) ->
Function of
[:A, A:],
BOOLEAN means
:
Def9: for a,b be
object st a
in A & b
in A holds (a
= b implies (it
. (a,b))
=
TRUE ) & (a
<> b implies (it
. (a,b))
=
FALSE );
existence
proof
defpred
P[
object,
object] means $1
= $2;
consider f be
Function of
[:A, A:],
BOOLEAN such that
A1: for x,y be
object st x
in A & y
in A holds (
P[x, y] implies (f
. (x,y))
=
TRUE ) & ( not
P[x, y] implies (f
. (x,y))
=
FALSE ) from
BinPredToFunEx;
take f;
thus thesis by
A1;
end;
uniqueness
proof
defpred
P[
object,
object] means $1
= $2;
for f,g be
Function of
[:A, A:],
BOOLEAN st (for x,y be
object st x
in A & y
in A holds (
P[x, y] implies (f
. (x,y))
=
TRUE ) & ( not
P[x, y] implies (f
. (x,y))
=
FALSE )) & (for x,y be
object st x
in A & y
in A holds (
P[x, y] implies (g
. (x,y))
=
TRUE ) & ( not
P[x, y] implies (g
. (x,y))
=
FALSE )) holds f
= g from
BinPredToFunUnique;
hence thesis;
end;
end
definition
let V, A;
let x,y be
Element of V;
::
NOMIN_4:def10
func
Equality (A,x,y) ->
SCPartialNominativePredicate of V, A equals (
lift_binary_pred ((
Equality A),x,y));
coherence ;
end
definition
let x,y be
object;
::
NOMIN_4:def11
pred x
less_pred y means ex x1,y1 be
ExtReal st x1
= x & y1
= y & x1
< y1;
irreflexivity ;
asymmetry ;
end
theorem ::
NOMIN_4:10
Th10: for x,y be
ExtReal holds not x
less_pred y implies y
less_pred x or x
= y
proof
let x,y be
ExtReal;
assume not x
less_pred y & not y
less_pred x;
then x
<= y & x
>= y;
hence thesis by
XXREAL_0: 1;
end;
definition
let A;
::
NOMIN_4:def12
func
less (A) ->
Function of
[:A, A:],
BOOLEAN means
:
Def12: for x,y be
object st x
in A & y
in A holds (x
less_pred y implies (it
. (x,y))
=
TRUE ) & ( not x
less_pred y implies (it
. (x,y))
=
FALSE );
existence
proof
defpred
P[
object,
object] means $1
less_pred $2;
consider f be
Function of
[:A, A:],
BOOLEAN such that
A1: for x,y be
object st x
in A & y
in A holds (
P[x, y] implies (f
. (x,y))
=
TRUE ) & ( not
P[x, y] implies (f
. (x,y))
=
FALSE ) from
BinPredToFunEx;
take f;
thus thesis by
A1;
end;
uniqueness
proof
defpred
P[
object,
object] means $1
less_pred $2;
for f,g be
Function of
[:A, A:],
BOOLEAN st (for x,y be
object st x
in A & y
in A holds (
P[x, y] implies (f
. (x,y))
=
TRUE ) & ( not
P[x, y] implies (f
. (x,y))
=
FALSE )) & (for x,y be
object st x
in A & y
in A holds (
P[x, y] implies (g
. (x,y))
=
TRUE ) & ( not
P[x, y] implies (g
. (x,y))
=
FALSE )) holds f
= g from
BinPredToFunUnique;
hence thesis;
end;
end
definition
let V, A;
let x,y be
Element of V;
::
NOMIN_4:def13
func
less (A,x,y) ->
SCPartialNominativePredicate of V, A equals (
lift_binary_pred ((
less A),x,y));
coherence ;
end
theorem ::
NOMIN_4:11
Th11: (for d holds a
is_a_value_on d) & (for d holds b
is_a_value_on d) implies (
dom (
Equality (A,a,b)))
= ((
dom (
denaming (V,A,a)))
/\ (
dom (
denaming (V,A,b))))
proof
set Da = (
denaming (V,A,a));
set Db = (
denaming (V,A,b));
assume
A1: (for d holds a
is_a_value_on d) & (for d holds b
is_a_value_on d);
(
dom (
Equality A))
=
[:A, A:] by
FUNCT_2:def 1;
then (
rng
<:Da, Db:>)
c= (
dom (
Equality A)) by
A1,
Th9;
then (
dom (
Equality (A,a,b)))
= (
dom
<:Da, Db:>) by
RELAT_1: 27;
hence thesis by
FUNCT_3:def 7;
end;
theorem ::
NOMIN_4:12
Th12: (for d holds a
is_a_value_on d) & (for d holds b
is_a_value_on d) implies (
dom (
less (A,a,b)))
= ((
dom (
denaming (V,A,a)))
/\ (
dom (
denaming (V,A,b))))
proof
set Da = (
denaming (V,A,a));
set Db = (
denaming (V,A,b));
assume
A1: (for d holds a
is_a_value_on d) & (for d holds b
is_a_value_on d);
(
dom (
less A))
=
[:A, A:] by
FUNCT_2:def 1;
then (
rng
<:Da, Db:>)
c= (
dom (
less A)) by
A1,
Th9;
then (
dom (
less (A,a,b)))
= (
dom
<:Da, Db:>) by
RELAT_1: 27;
hence thesis by
FUNCT_3:def 7;
end;
theorem ::
NOMIN_4:13
(for d holds a
is_a_value_on d) & (for d holds b
is_a_value_on d) & (for d holds a
is_ext_real_on d) & (for d holds b
is_ext_real_on d) implies (
PP_not (
Equality (A,a,b)))
= (
PP_or ((
less (A,a,b)),(
less (A,b,a))))
proof
set e = (
Equality (A,a,b));
set p = (
PP_not e);
set q = (
less (A,a,b));
set r = (
less (A,b,a));
set o = (
PP_or (q,r));
set L = (
less A);
set E = (
Equality A);
set Da = (
denaming (V,A,a));
set Db = (
denaming (V,A,b));
assume that
A1: (for d holds a
is_a_value_on d) & (for d holds b
is_a_value_on d) and
A2: (for d holds a
is_ext_real_on d) & (for d holds b
is_ext_real_on d);
A3: (
dom p)
= (
dom e) by
PARTPR_1:def 2;
A4: (
dom o)
= { d where d be
TypeSCNominativeData of V, A : d
in (
dom q) & (q
. d)
=
TRUE or d
in (
dom r) & (r
. d)
=
TRUE or d
in (
dom q) & (q
. d)
=
FALSE & d
in (
dom r) & (r
. d)
=
FALSE } by
NOMIN_2: 16;
A5: (
dom Da)
= { d where d be
NonatomicND of V, A : a
in (
dom d) } by
NOMIN_1:def 18;
A6: (
dom
<:Da, Db:>)
= ((
dom Da)
/\ (
dom Db)) by
FUNCT_3:def 7;
A7: (
dom
<:Db, Da:>)
= ((
dom Db)
/\ (
dom Da)) by
FUNCT_3:def 7;
A8: (
dom e)
= ((
dom Da)
/\ (
dom Db)) by
A1,
Th11;
A9: (
dom q)
= ((
dom Da)
/\ (
dom Db)) by
A1,
Th12;
A10: (
dom r)
= ((
dom Da)
/\ (
dom Db)) by
A1,
Th12;
thus (
dom p)
= (
dom o)
proof
thus (
dom p)
c= (
dom o)
proof
let x be
object;
assume
A11: x
in (
dom p);
then x
in (
dom Da) by
A3,
A8,
XBOOLE_0:def 4;
then ex da be
NonatomicND of V, A st x
= da & a
in (
dom da) by
A5;
then
reconsider x as
TypeSCNominativeData of V, A;
A12: (
<:Da, Db:>
. x)
=
[(Da
. x), (Db
. x)] by
A3,
A6,
A8,
A11,
FUNCT_3:def 7;
A13: (
<:Db, Da:>
. x)
=
[(Db
. x), (Da
. x)] by
A3,
A7,
A8,
A11,
FUNCT_3:def 7;
A14: a
is_a_value_on x & b
is_a_value_on x by
A1;
A15: (q
. x)
= (L
. ((Da
. x),(Db
. x))) by
A3,
A6,
A8,
A11,
A12,
FUNCT_1: 13;
A16: (r
. x)
= (L
. ((Db
. x),(Da
. x))) by
A3,
A7,
A8,
A11,
A13,
FUNCT_1: 13;
A17: a
is_ext_real_on x & b
is_ext_real_on x by
A2;
per cases ;
suppose (Da
. x)
= (Db
. x);
then (q
. x)
=
FALSE & (r
. x)
=
FALSE by
A14,
A15,
A16,
Def12;
hence thesis by
A3,
A4,
A8,
A9,
A10,
A11;
end;
suppose
A18: (Da
. x)
<> (Db
. x);
now
assume (q
. x)
<>
TRUE & (r
. x)
<>
TRUE ;
then not (Da
. x)
less_pred (Db
. x) & not (Db
. x)
less_pred (Da
. x) by
A14,
A15,
A16,
Def12;
hence contradiction by
A17,
A18,
Th10;
end;
hence thesis by
A3,
A4,
A8,
A9,
A10,
A11;
end;
end;
let x be
object;
assume x
in (
dom o);
then ex d be
TypeSCNominativeData of V, A st x
= d & (d
in (
dom q) & (q
. d)
=
TRUE or d
in (
dom r) & (r
. d)
=
TRUE or d
in (
dom q) & (q
. d)
=
FALSE & d
in (
dom r) & (r
. d)
=
FALSE ) by
A4;
hence thesis by
A1,
A3,
A8,
Th12;
end;
let x be
object;
assume
A19: x
in (
dom p);
then x
in (
dom Da) by
A3,
A8,
XBOOLE_0:def 4;
then
consider da be
NonatomicND of V, A such that
A20: x
= da and a
in (
dom da) by
A5;
reconsider x as
TypeSCNominativeData of V, A by
A20;
A21: x
in (
dom q) & x
in (
dom r) by
A1,
A3,
A8,
A19,
Th12;
A22: (
<:Da, Db:>
. x)
=
[(Da
. x), (Db
. x)] by
A3,
A6,
A8,
A19,
FUNCT_3:def 7;
A23: (
<:Db, Da:>
. x)
=
[(Db
. x), (Da
. x)] by
A3,
A7,
A8,
A19,
FUNCT_3:def 7;
A24: a
is_a_value_on x & b
is_a_value_on x by
A1;
A25: (q
. x)
= (L
. ((Da
. x),(Db
. x))) by
A3,
A6,
A8,
A19,
A22,
FUNCT_1: 13;
A26: (r
. x)
= (L
. ((Db
. x),(Da
. x))) by
A3,
A7,
A8,
A19,
A23,
FUNCT_1: 13;
A27: a
is_ext_real_on x & b
is_ext_real_on x by
A2;
per cases ;
suppose
A28: (Da
. x)
= (Db
. x);
then (q
. x)
=
FALSE & (r
. x)
=
FALSE by
A24,
A25,
A26,
Def12;
then
A29: (o
. x)
=
FALSE by
A21,
PARTPR_1:def 4;
(e
. x)
= (E
. ((Da
. x),(Db
. x))) by
A3,
A19,
A22,
FUNCT_1: 12
.=
TRUE by
A24,
A28,
Def9;
hence thesis by
A29,
A3,
A19,
PARTPR_1:def 2;
end;
suppose
A30: (Da
. x)
<> (Db
. x);
now
assume (q
. x)
<>
TRUE & (r
. x)
<>
TRUE ;
then not (Da
. x)
less_pred (Db
. x) & not (Db
. x)
less_pred (Da
. x) by
A24,
A25,
A26,
Def12;
hence contradiction by
A27,
A30,
Th10;
end;
then
A31: (o
. x)
=
TRUE by
A21,
PARTPR_1:def 4;
(e
. x)
= (E
. ((Da
. x),(Db
. x))) by
A3,
A19,
A22,
FUNCT_1: 12
.=
FALSE by
A24,
A30,
Def9;
hence thesis by
A31,
A3,
A19,
PARTPR_1:def 2;
end;
end;
theorem ::
NOMIN_4:14
(for d holds a
is_a_value_on d) & (for d holds b
is_a_value_on d) & a
is_ext_real_on d & b
is_ext_real_on d & d
in (
dom (
PP_not (
Equality (A,a,b)))) & ((
PP_not (
Equality (A,a,b)))
. d)
=
TRUE implies d
in (
dom (
less (A,a,b))) & ((
less (A,a,b))
. d)
=
TRUE or d
in (
dom (
less (A,b,a))) & ((
less (A,b,a))
. d)
=
TRUE
proof
set e = (
Equality (A,a,b));
set E = (
Equality A);
set Da = (
denaming (V,A,a));
set Db = (
denaming (V,A,b));
set L = (
less A);
assume that
A1: (for d holds a
is_a_value_on d) & (for d holds b
is_a_value_on d) and
A2: a
is_ext_real_on d & b
is_ext_real_on d and
A3: d
in (
dom (
PP_not e)) and
A4: ((
PP_not e)
. d)
=
TRUE and
A5: not d
in (
dom (
less (A,a,b))) or ((
less (A,a,b))
. d)
<>
TRUE ;
A6: a
is_a_value_on d by
A1;
A7: b
is_a_value_on d by
A1;
A8: (
dom
<:Db, Da:>)
= ((
dom Db)
/\ (
dom Da)) by
FUNCT_3:def 7;
A9: (
dom (
PP_not e))
= (
dom e) by
PARTPR_1:def 2;
A10: (
dom e)
c= (
dom
<:Da, Db:>) by
RELAT_1: 25;
then d
in (
dom
<:Da, Db:>) by
A3,
A9;
then
A11: d
in (
dom
<:Db, Da:>) by
A8,
FUNCT_3:def 7;
A12: (e
. d)
=
FALSE by
A3,
A4,
A9,
PARTPR_1: 5;
A13: (
<:Da, Db:>
. d)
=
[(Da
. d), (Db
. d)] by
A3,
A9,
A10,
FUNCT_3:def 7;
then (e
. d)
= (E
. ((Da
. d),(Db
. d))) by
A3,
A9,
A10,
FUNCT_1: 13;
then
A14: (Da
. d)
<> (Db
. d) by
A6,
A12,
Def9;
reconsider x = (Da
. d), y = (Db
. d) as
ExtReal by
A2;
A15: d
in (
dom
<:Da, Db:>) by
A3,
A9,
FUNCT_1: 11;
A16: (
dom L)
=
[:A, A:] by
FUNCT_2:def 1;
[(Da
. d), (Db
. d)]
in
[:A, A:] by
A6,
A7,
ZFMISC_1:def 2;
then d
in (
dom (L
*
<:Da, Db:>)) by
A15,
A13,
A16,
FUNCT_1: 11;
then
FALSE
= ((L
*
<:Da, Db:>)
. d) by
A5,
PARTPR_1: 3
.= (L
. ((Da
. d),(Db
. d))) by
A3,
A9,
A10,
A13,
FUNCT_1: 13;
then not x
less_pred y by
A6,
A7,
Def12;
then
A17: (Db
. d)
less_pred (Da
. d) by
A14,
Th10;
((L
*
<:Db, Da:>)
. d)
= (L
. (
<:Db, Da:>
. d)) by
A11,
FUNCT_1: 13
.= (L
. ((Db
. d),(Da
. d))) by
A11,
FUNCT_3:def 7
.=
TRUE by
A6,
A7,
A17,
Def12;
hence thesis by
A1,
A8,
A11,
Th12;
end;
definition
let x,y be
object;
assume
A1: x is
Complex & y is
Complex;
::
NOMIN_4:def14
func
subtraction (x,y) ->
Complex means
:
Def14: ex x1,y1 be
Complex st x1
= x & y1
= y & it
= (x1
- y1);
existence
proof
reconsider x1 = x, y1 = y as
Complex by
A1;
take (x1
- y1);
thus thesis;
end;
uniqueness ;
end
definition
let A;
assume
A1: A is
complex-containing;
::
NOMIN_4:def15
func
subtraction (A) ->
Function of
[:A, A:], A means
:
Def15: for x,y be
object st x
in A & y
in A holds (it
. (x,y))
= (
subtraction (x,y));
existence
proof
deffunc
F(
object,
object) = (
subtraction ($1,$2));
A2: for x,y be
object st x
in A & y
in A holds (
subtraction (x,y))
in A
proof
let x,y be
object such that x
in A & y
in A;
(
subtraction (x,y))
in
COMPLEX by
XCMPLX_0:def 2;
hence thesis by
A1;
end;
consider f be
Function of
[:A, A:], A such that
A3: for x,y be
object st x
in A & y
in A holds (f
. (x,y))
= (
subtraction (x,y)) from
BINOP_1:sch 2(
A2);
take f;
thus thesis by
A3;
end;
uniqueness
proof
deffunc
F(
object,
object) = (
subtraction ($1,$2));
for f,g be
Function of
[:A, A:], A st (for x,y be
object st x
in A & y
in A holds (f
. (x,y))
=
F(x,y)) & (for x,y be
object st x
in A & y
in A holds (g
. (x,y))
=
F(x,y)) holds f
= g from
Lambda2Unique;
hence thesis;
end;
end
definition
let V, A;
let x,y be
Element of V;
::
NOMIN_4:def16
func
subtraction (A,x,y) ->
SCBinominativeFunction of V, A equals (
lift_binary_op ((
subtraction A),x,y));
coherence ;
end
theorem ::
NOMIN_4:15
A is
complex-containing & a
in (
dom d1) & b
in (
dom d1) & d1
in (
dom (
subtraction (A,a,b))) implies for x,y be
Complex st x
= (d1
. a) & y
= (d1
. b) holds ((
subtraction (A,a,b))
. d1)
= (x
- y)
proof
assume that
A1: A is
complex-containing and
A2: a
in (
dom d1) and
A3: b
in (
dom d1) and
A4: d1
in (
dom (
subtraction (A,a,b)));
let x,y be
Complex such that
A5: x
= (d1
. a) & y
= (d1
. b);
set Di = (
denaming (V,A,a));
set Dj = (
denaming (V,A,b));
A6: d1
in (
dom
<:Di, Dj:>) by
A4,
FUNCT_1: 11;
then
A7: (
<:Di, Dj:>
. d1)
=
[(Di
. d1), (Dj
. d1)] by
FUNCT_3:def 7;
A8: (
dom
<:Di, Dj:>)
= ((
dom Di)
/\ (
dom Dj)) by
FUNCT_3:def 7;
then d1
in (
dom Di) by
A6,
XBOOLE_0:def 4;
then
A9: (Di
. d1)
= (
denaming (a,d1)) by
NOMIN_1:def 18
.= (d1
. a) by
A2,
NOMIN_1:def 12;
d1
in (
dom Dj) by
A6,
A8,
XBOOLE_0:def 4;
then
A10: (Dj
. d1)
= (
denaming (b,d1)) by
NOMIN_1:def 18
.= (d1
. b) by
A3,
NOMIN_1:def 12;
A11: x
in
COMPLEX & y
in
COMPLEX by
XCMPLX_0:def 2;
thus ((
subtraction (A,a,b))
. d1)
= ((
subtraction A)
. ((Di
. d1),(Dj
. d1))) by
A4,
A7,
FUNCT_1: 12
.= (
subtraction ((Di
. d1),(Dj
. d1))) by
A1,
A5,
A9,
A10,
A11,
Def15
.= (x
- y) by
A5,
A9,
A10,
Def14;
end;
definition
let V, A, a, b;
::
NOMIN_4:def17
func
gcd_conditional_step (V,A,a,b) ->
SCBinominativeFunction of V, A equals (
PP_IF ((
less (A,b,a)),(
SC_assignment ((
subtraction (A,a,b)),a)),(
PPid (
ND (V,A)))));
coherence ;
end
definition
let V, A, a, b;
::
NOMIN_4:def18
func
gcd_loop_body (V,A,a,b) ->
SCBinominativeFunction of V, A equals (
PP_composition ((
gcd_conditional_step (V,A,a,b)),(
gcd_conditional_step (V,A,b,a))));
coherence ;
end
definition
let V, A, a, b;
::
NOMIN_4:def19
func
gcd_main_loop (V,A,a,b) ->
SCBinominativeFunction of V, A equals (
PP_while ((
PP_not (
Equality (A,a,b))),(
gcd_loop_body (V,A,a,b))));
coherence ;
end
definition
let V, A, a, b, x, y;
::
NOMIN_4:def20
func
gcd_var_init (V,A,a,b,x,y) ->
SCBinominativeFunction of V, A equals (
PP_composition ((
SC_assignment ((
denaming (V,A,x)),a)),(
SC_assignment ((
denaming (V,A,y)),b))));
coherence ;
end
definition
let V, A, a, b, x, y;
::
NOMIN_4:def21
func
gcd_main_part (V,A,a,b,x,y) ->
SCBinominativeFunction of V, A equals (
PP_composition ((
gcd_var_init (V,A,a,b,x,y)),(
gcd_main_loop (V,A,a,b))));
coherence ;
end
definition
let V, A, a, b, x, y, z;
::
NOMIN_4:def22
func
gcd_program (V,A,a,b,x,y,z) ->
SCBinominativeFunction of V, A equals (
PP_composition ((
gcd_main_part (V,A,a,b,x,y)),(
SC_assignment ((
denaming (V,A,a)),z))));
coherence ;
end
reserve x0,y0 for
Nat;
definition
let V, A, x, y, x0, y0;
let d be
object;
::
NOMIN_4:def23
pred
valid_gcd_input_pred V,A,x,y,x0,y0,d means ex d1 be
NonatomicND of V, A st d
= d1 & x
in (
dom d1) & y
in (
dom d1) & (d1
. x)
= x0 & (d1
. y)
= y0;
end
definition
let V, A, x, y, x0, y0;
::
NOMIN_4:def24
func
valid_gcd_input (V,A,x,y,x0,y0) ->
SCPartialNominativePredicate of V, A means
:
Def24: (
dom it )
= (
ND (V,A)) & for d be
object st d
in (
dom it ) holds (
valid_gcd_input_pred (V,A,x,y,x0,y0,d) implies (it
. d)
=
TRUE ) & ( not
valid_gcd_input_pred (V,A,x,y,x0,y0,d) implies (it
. d)
=
FALSE );
existence
proof
A1: (
ND (V,A))
c= (
ND (V,A));
defpred
P[
object] means
valid_gcd_input_pred (V,A,x,y,x0,y0,$1);
consider p be
SCPartialNominativePredicate of V, A such that
A2: (
dom p)
= (
ND (V,A)) & (for d be
object st d
in (
dom p) holds (
P[d] implies (p
. d)
=
TRUE ) & ( not
P[d] implies (p
. d)
=
FALSE )) from
PARTPR_2:sch 1(
A1);
take p;
thus thesis by
A2;
end;
uniqueness
proof
defpred
P[
object] means
valid_gcd_input_pred (V,A,x,y,x0,y0,$1);
for p,q be
SCPartialNominativePredicate of V, A st ((
dom p)
= (
ND (V,A)) & (for d be
object st d
in (
dom p) holds (
P[d] implies (p
. d)
=
TRUE ) & ( not
P[d] implies (p
. d)
=
FALSE ))) & ((
dom q)
= (
ND (V,A)) & (for d be
object st d
in (
dom q) holds (
P[d] implies (q
. d)
=
TRUE ) & ( not
P[d] implies (q
. d)
=
FALSE ))) holds p
= q from
PARTPR_2:sch 2;
hence thesis;
end;
end
registration
let V, A, x, y, x0, y0;
cluster (
valid_gcd_input (V,A,x,y,x0,y0)) ->
total;
coherence by
Def24;
end
definition
let V, A, z, x0, y0;
let d be
object;
::
NOMIN_4:def25
pred
valid_gcd_output_pred V,A,z,x0,y0,d means ex d1 be
NonatomicND of V, A st d
= d1 & z
in (
dom d1) & (d1
. z)
= (x0
gcd y0);
end
definition
let V, A, z, x0, y0;
set D = { d where d be
TypeSCNominativeData of V, A : d
in (
dom (
denaming (V,A,z))) };
::
NOMIN_4:def26
func
valid_gcd_output (V,A,z,x0,y0) ->
SCPartialNominativePredicate of V, A means
:
Def26: (
dom it )
= { d where d be
TypeSCNominativeData of V, A : d
in (
dom (
denaming (V,A,z))) } & for d be
object st d
in (
dom it ) holds (
valid_gcd_output_pred (V,A,z,x0,y0,d) implies (it
. d)
=
TRUE ) & ( not
valid_gcd_output_pred (V,A,z,x0,y0,d) implies (it
. d)
=
FALSE );
existence
proof
A1: D
c= (
ND (V,A))
proof
let v;
assume v
in D;
then ex d be
TypeSCNominativeData of V, A st v
= d & d
in (
dom (
denaming (V,A,z)));
hence thesis;
end;
defpred
P[
object] means
valid_gcd_output_pred (V,A,z,x0,y0,$1);
consider p be
SCPartialNominativePredicate of V, A such that
A2: (
dom p)
= D & (for d be
object st d
in (
dom p) holds (
P[d] implies (p
. d)
=
TRUE ) & ( not
P[d] implies (p
. d)
=
FALSE )) from
PARTPR_2:sch 1(
A1);
take p;
thus thesis by
A2;
end;
uniqueness
proof
defpred
P[
object] means
valid_gcd_output_pred (V,A,z,x0,y0,$1);
for p,q be
SCPartialNominativePredicate of V, A st ((
dom p)
= D & (for d be
object st d
in (
dom p) holds (
P[d] implies (p
. d)
=
TRUE ) & ( not
P[d] implies (p
. d)
=
FALSE ))) & ((
dom q)
= D & (for d be
object st d
in (
dom q) holds (
P[d] implies (q
. d)
=
TRUE ) & ( not
P[d] implies (q
. d)
=
FALSE ))) holds p
= q from
PARTPR_2:sch 2;
hence thesis;
end;
end
definition
let V, A, a, b, x0, y0;
let d be
object;
::
NOMIN_4:def27
pred
gcd_inv_pred V,A,a,b,x0,y0,d means ex d1 be
NonatomicND of V, A st d
= d1 & a
in (
dom d1) & b
in (
dom d1) & ex x,y be
Nat st x
= (d1
. a) & y
= (d1
. b) & (x
gcd y)
= (x0
gcd y0);
end
definition
let V, A, a, b, x0, y0;
::
NOMIN_4:def28
func
gcd_inv (V,A,a,b,x0,y0) ->
SCPartialNominativePredicate of V, A means
:
Def28: (
dom it )
= (
ND (V,A)) & for d be
object st d
in (
dom it ) holds (
gcd_inv_pred (V,A,a,b,x0,y0,d) implies (it
. d)
=
TRUE ) & ( not
gcd_inv_pred (V,A,a,b,x0,y0,d) implies (it
. d)
=
FALSE );
existence
proof
A1: (
ND (V,A))
c= (
ND (V,A));
defpred
P[
object] means
gcd_inv_pred (V,A,a,b,x0,y0,$1);
consider p be
SCPartialNominativePredicate of V, A such that
A2: (
dom p)
= (
ND (V,A)) & (for d be
object st d
in (
dom p) holds (
P[d] implies (p
. d)
=
TRUE ) & ( not
P[d] implies (p
. d)
=
FALSE )) from
PARTPR_2:sch 1(
A1);
take p;
thus thesis by
A2;
end;
uniqueness
proof
defpred
P[
object] means
gcd_inv_pred (V,A,a,b,x0,y0,$1);
for p,q be
SCPartialNominativePredicate of V, A st ((
dom p)
= (
ND (V,A)) & (for d be
object st d
in (
dom p) holds (
P[d] implies (p
. d)
=
TRUE ) & ( not
P[d] implies (p
. d)
=
FALSE ))) & ((
dom q)
= (
ND (V,A)) & (for d be
object st d
in (
dom q) holds (
P[d] implies (q
. d)
=
TRUE ) & ( not
P[d] implies (q
. d)
=
FALSE ))) holds p
= q from
PARTPR_2:sch 2;
hence thesis;
end;
end
registration
let V, A, a, b, x0, y0;
cluster (
gcd_inv (V,A,a,b,x0,y0)) ->
total;
coherence by
Def28;
end
theorem ::
NOMIN_4:16
Th15:
<*(
PP_inversion (
SC_Psuperpos (p,(
denaming (V,A,x)),a))), (
SC_assignment ((
denaming (V,A,x)),a)), p*> is
SFHT of (
ND (V,A))
proof
set Dx = (
denaming (V,A,x));
set F = (
SC_assignment (Dx,a));
set P = (
SC_Psuperpos (p,Dx,a));
set I = (
PP_inversion P);
for d st d
in (
dom I) & (I
. d)
=
TRUE & d
in (
dom F) & (F
. d)
in (
dom p) holds (p
. (F
. d))
=
TRUE
proof
let d such that
A1: d
in (
dom I) and (I
. d)
=
TRUE and
A2: d
in (
dom F) and
A3: (F
. d)
in (
dom p);
(
dom I)
= { d where d be
Element of (
ND (V,A)) : not d
in (
dom P) } by
PARTPR_2:def 17;
then
A4: ex d1 be
Element of (
ND (V,A)) st d1
= d & not d1
in (
dom P) by
A1;
(
dom F)
= (
dom Dx) by
NOMIN_2:def 7;
then (P,d)
=~ (p,(
local_overlapping (V,A,d,(Dx
. d),a))) by
A2,
NOMIN_2:def 11;
hence thesis by
A2,
A3,
A4,
NOMIN_2:def 7;
end;
hence thesis by
NOMIN_3: 28;
end;
theorem ::
NOMIN_4:17
Th16: V is non
empty & A
is_without_nonatomicND_wrt V & a
<> b & a
<> y implies
<*(
valid_gcd_input (V,A,x,y,x0,y0)), (
gcd_var_init (V,A,a,b,x,y)), (
gcd_inv (V,A,a,b,x0,y0))*> is
SFHT of (
ND (V,A))
proof
assume that
A1: V is non
empty and
A2: A
is_without_nonatomicND_wrt V and
A3: a
<> b and
A4: a
<> y;
set Dx = (
denaming (V,A,x));
set Dy = (
denaming (V,A,y));
set p = (
gcd_inv (V,A,a,b,x0,y0));
set Q = (
SC_Psuperpos (p,Dy,b));
set P = (
SC_Psuperpos (Q,Dx,a));
set F = (
SC_assignment (Dx,a));
set G = (
SC_assignment (Dy,b));
set H = (
gcd_var_init (V,A,a,b,x,y));
set I = (
valid_gcd_input (V,A,x,y,x0,y0));
A5:
<*P, F, Q*> is
SFHT of (
ND (V,A)) by
NOMIN_3: 29;
A6:
<*Q, G, p*> is
SFHT of (
ND (V,A)) by
NOMIN_3: 29;
A7: (
dom Q)
= { d where d be
TypeSCNominativeData of V, A : (
local_overlapping (V,A,d,(Dy
. d),b))
in (
dom p) & d
in (
dom Dy) } by
NOMIN_2:def 11;
A8: (
dom Dy)
= { d where d be
NonatomicND of V, A : y
in (
dom d) } by
NOMIN_1:def 18;
A9: (
dom p)
= (
ND (V,A)) by
Def28;
<*(
PP_inversion Q), G, p*> is
SFHT of (
ND (V,A)) by
Th15;
then
A10:
<*P, H, p*> is
SFHT of (
ND (V,A)) by
A5,
A6,
NOMIN_3: 25;
I
||= P
proof
let d be
Element of (
ND (V,A)) such that
A11: d
in (
dom I) and
A12: (I
. d)
=
TRUE ;
A13:
valid_gcd_input_pred (V,A,x,y,x0,y0,d) by
A11,
A12,
Def24;
then
reconsider d as
NonatomicND of V, A;
A14: (
dom Dx)
= { d where d be
NonatomicND of V, A : x
in (
dom d) } by
NOMIN_1:def 18;
A15: (
dom P)
= { d where d be
TypeSCNominativeData of V, A : (
local_overlapping (V,A,d,(Dx
. d),a))
in (
dom Q) & d
in (
dom Dx) } by
NOMIN_2:def 11;
reconsider Lx = (
local_overlapping (V,A,d,(Dx
. d),a)) as
NonatomicND of V, A by
NOMIN_2: 9;
reconsider Ly = (
local_overlapping (V,A,Lx,(Dy
. Lx),b)) as
NonatomicND of V, A by
NOMIN_2: 9;
A16: Ly
in (
dom p) by
A9;
reconsider GO = (
global_overlapping (V,A,Lx,(
naming (V,A,b,(Dy
. Lx))))) as
Function;
set d1 = (
naming (V,A,a,(Dx
. d)));
set d2 = (b
.--> (Dy
. Lx));
A17: not Lx
in A by
A2,
Th3;
A18: not d
in A by
A2,
Th3;
A19: not d1
in A by
A2,
Th3;
A20: Lx
= (d1
\/ (d
| ((
dom d)
\ (
dom d1)))) by
A18,
A19,
NOMIN_1: 64;
then d1
c= Lx by
XBOOLE_1: 7;
then
A21: (
dom d1)
c= (
dom Lx) by
GRFUNC_1: 2;
A22: d
in (
dom Dx) by
A13,
A14;
then
A23: (Dx
. d) is
TypeSCNominativeData of V, A by
PARTFUN1: 4,
NOMIN_1: 39;
then
A24: d1
= (a
.--> (Dx
. d)) by
A1,
NOMIN_1:def 13;
not y
in (
dom d1) by
A4,
A24,
TARSKI:def 1;
then y
in ((
dom d)
\ (
dom d1)) by
A13,
XBOOLE_0:def 5;
then
A25: y
in (
dom (d
| ((
dom d)
\ (
dom d1)))) by
RELAT_1: 57;
(d
| ((
dom d)
\ (
dom d1)))
c= Lx by
A20,
XBOOLE_1: 7;
then
A26: (
dom (d
| ((
dom d)
\ (
dom d1))))
c= (
dom Lx) by
GRFUNC_1: 2;
then
A27: Lx
in (
dom Dy) by
A8,
A25;
A28: (Dy
. Lx) is
TypeSCNominativeData of V, A by
A27,
PARTFUN1: 4,
NOMIN_1: 39;
then
A29: (
naming (V,A,b,(Dy
. Lx)))
= d2 by
A1,
NOMIN_1:def 13;
then
A30: not d2
in A by
A2,
Th3;
then
A31: Ly
= (d2
\/ (Lx
| ((
dom Lx)
\ (
dom d2)))) by
A29,
A17,
NOMIN_1: 64;
then d2
c= Ly by
XBOOLE_1: 7;
then
A32: (
dom d2)
c= (
dom Ly) by
GRFUNC_1: 2;
A34: not a
in (
dom d2) by
A3,
TARSKI:def 1;
a
in
{a} by
TARSKI:def 1;
then
A35: a
in ((
dom Lx)
\ (
dom d2)) by
A21,
A24,
A34,
XBOOLE_0:def 5;
reconsider G1 = (
global_overlapping (V,A,Lx,d2)) as
Function by
A29;
A36: G1
= (d2
\/ (Lx
| ((
dom Lx)
\ (
dom d2)))) by
A29,
A17,
A30,
NOMIN_1: 64;
A37: a
in (
dom (Lx
| ((
dom Lx)
\ (
dom d2)))) by
A35,
RELAT_1: 57;
(Lx
| ((
dom Lx)
\ (
dom d2)))
c= Ly by
A31,
XBOOLE_1: 7;
then
A38: (
dom (Lx
| ((
dom Lx)
\ (
dom d2))))
c= (
dom Ly) by
GRFUNC_1: 2;
A39: b
in
{b} by
TARSKI:def 1;
A41: (Ly
. a)
= (G1
. a) by
A28,
A1,
NOMIN_1:def 13
.= ((Lx
| ((
dom Lx)
\ (
dom d2)))
. a) by
A36,
A37,
GRFUNC_1: 15
.= (Lx
. a) by
A37,
FUNCT_1: 47
.= (Dx
. d) by
A1,
A23,
NOMIN_2: 10
.= (
denaming (x,d)) by
A22,
NOMIN_1:def 18
.= x0 by
A13,
NOMIN_1:def 12;
(Ly
. b)
= (Dy
. Lx) by
A1,
A28,
NOMIN_2: 10
.= (
denaming (y,Lx)) by
A27,
NOMIN_1:def 18
.= (Lx
. y) by
A26,
A25,
NOMIN_1:def 12
.= y0 by
A13,
A19,
A23,
A1,
A4,
A18,
NOMIN_2: 12;
then
A42:
gcd_inv_pred (V,A,a,b,x0,y0,Ly) by
A38,
A37,
A39,
A32,
A41;
A43: Lx
in (
dom Q) by
A7,
A16,
A27;
then d
in (
dom P) by
A15,
A22;
then (P
. d)
= (Q
. Lx) by
NOMIN_2: 35
.= (p
. Ly) by
A43,
NOMIN_2: 35
.=
TRUE by
A16,
A42,
Def28;
hence thesis by
A15,
A43,
A22;
end;
hence thesis by
A10,
NOMIN_3: 15;
end;
theorem ::
NOMIN_4:18
Th17: V is non
empty & A
is_without_nonatomicND_wrt V & a
<> b & A is
complex-containing & (for d holds a
is_complex_on d) & (for d holds b
is_complex_on d) implies
<*(
PP_and ((
less (A,b,a)),(
gcd_inv (V,A,a,b,x0,y0)))), (
SC_assignment ((
subtraction (A,a,b)),a)), (
gcd_inv (V,A,a,b,x0,y0))*> is
SFHT of (
ND (V,A))
proof
assume that
A1: V is non
empty and
A2: A
is_without_nonatomicND_wrt V and
A3: a
<> b and
A4: A is
complex-containing and
A5: for d holds a
is_complex_on d and
A6: for d holds b
is_complex_on d;
set i = (
gcd_inv (V,A,a,b,x0,y0));
set l = (
less (A,b,a));
set D = (
subtraction (A,a,b));
set Da = (
denaming (V,A,a));
set Db = (
denaming (V,A,b));
set f = (
SC_assignment (D,a));
set p = (
PP_and (l,i));
set S = (
SC_Psuperpos (i,D,a));
A7:
<*S, f, i*> is
SFHT of (
ND (V,A)) by
NOMIN_3: 29;
for d holds d
in (
dom p) & (p
. d)
=
TRUE & d
in (
dom f) & (f
. d)
in (
dom i) implies (i
. (f
. d))
=
TRUE
proof
let d such that
A8: d
in (
dom p) and
A9: (p
. d)
=
TRUE and
A10: d
in (
dom f) and
A11: (f
. d)
in (
dom i);
A12: (
dom f)
= (
dom D) by
NOMIN_2:def 7;
A13: (
dom S)
= { d where d be
TypeSCNominativeData of V, A : (
local_overlapping (V,A,d,(D
. d),a))
in (
dom i) & d
in (
dom D) } by
NOMIN_2:def 11;
A14: (
dom Da)
= { d where d be
NonatomicND of V, A : a
in (
dom d) } by
NOMIN_1:def 18;
A15: (
dom Db)
= { d where d be
NonatomicND of V, A : b
in (
dom d) } by
NOMIN_1:def 18;
A16: d
in (
dom l) by
A8,
A9,
PARTPR_1: 23;
A17: (
dom ((
less A)
*
<:Db, Da:>))
c= (
dom
<:Db, Da:>) by
RELAT_1: 25;
A18: (
dom
<:Db, Da:>)
= ((
dom Db)
/\ (
dom Da)) by
FUNCT_3:def 7;
then
A19: d
in (
dom Da) by
A16,
A17,
XBOOLE_0:def 4;
then
consider da be
NonatomicND of V, A such that
A20: d
= da and
A21: a
in (
dom da) by
A14;
A22: d
in (
dom Db) by
A16,
A17,
A18,
XBOOLE_0:def 4;
then
consider db be
NonatomicND of V, A such that
A23: d
= db and
A24: b
in (
dom db) by
A15;
reconsider L = (
local_overlapping (V,A,da,(D
. da),a)) as
Function;
(
dom i)
= (
ND (V,A)) by
Def28;
then
A25: L
in (
dom i);
A26: (
rng D)
c= (
rng (
subtraction A)) by
RELAT_1: 26;
A27: (
rng D)
c= A by
A26,
XBOOLE_1: 1;
reconsider L as
NonatomicND of V, A by
NOMIN_2: 9;
A28:
gcd_inv_pred (V,A,a,b,x0,y0,L)
proof
take L;
thus L
= L;
d
in (
dom i) & (i
. d)
=
TRUE by
A8,
A9,
PARTPR_1: 23;
then
gcd_inv_pred (V,A,a,b,x0,y0,d) by
Def28;
then
consider d1 be
NonatomicND of V, A such that
A29: d
= d1 and a
in (
dom d1) and b
in (
dom d1) and
A30: ex x,y be
Nat st x
= (d1
. a) & y
= (d1
. b) & (x
gcd y)
= (x0
gcd y0);
consider x,y be
Nat such that
A31: x
= (d1
. a) and
A32: y
= (d1
. b) and
A33: (x
gcd y)
= (x0
gcd y0) by
A30;
(D
. d)
in (
rng D) by
A10,
A12,
FUNCT_1:def 3;
then
reconsider Dd = (D
. d) as
TypeSCNominativeData of V, A by
A27,
NOMIN_1:def 6;
A34: (L
. a)
= Dd by
A1,
A20,
NOMIN_2: 10;
A35: (
<:Db, Da:>
. d)
=
[(Db
. d), (Da
. d)] by
A16,
A17,
FUNCT_3:def 7;
A36: (Da
. d)
= (
denaming (a,da)) & (Db
. d)
= (
denaming (b,db)) by
A20,
A23,
A19,
A22,
NOMIN_1:def 18;
a
is_complex_on d & b
is_complex_on d by
A5,
A6;
then
consider x1,y1 be
Complex such that
A37: x1
= (
denaming (a,da)) and
A38: y1
= (
denaming (b,db)) and
A39: (
subtraction ((
denaming (a,da)),(
denaming (b,db))))
= (x1
- y1) by
A36,
Def14;
A40: x1
= x by
A20,
A21,
A29,
A31,
A37,
NOMIN_1:def 12;
A41: y1
= y by
A23,
A24,
A29,
A32,
A38,
NOMIN_1:def 12;
A42: not da
in A by
A2,
Th3;
A43: not (
naming (V,A,a,(D
. da)))
in A by
A2,
Th3;
Dd
= (D
. d);
then
A44: (L
. b)
= (da
. b) by
A1,
A3,
A20,
A23,
A24,
A42,
A43,
NOMIN_2: 12;
A45: (
denaming (a,da))
in
COMPLEX by
A37,
XCMPLX_0:def 2;
A46: (
denaming (b,db))
in
COMPLEX by
A38,
XCMPLX_0:def 2;
A47: (
dom (
local_overlapping (V,A,da,Dd,a)))
= (
dom da) by
A1,
A20,
A21,
A42,
A43,
NOMIN_2: 14;
hence a
in (
dom L) by
A20,
A21;
thus b
in (
dom L) by
A20,
A23,
A24,
A47;
A48: (l
. d)
=
TRUE by
A8,
A9,
PARTPR_1: 23;
d
in (
dom l) by
A8,
A9,
PARTPR_1: 23;
then (l
. d)
= ((
less A)
. ((Db
. d),(Da
. d))) by
A35,
FUNCT_1: 12;
then (Db
. d)
less_pred (Da
. d) by
A4,
A36,
A45,
A46,
A48,
Def12;
then (x
- y)
in
NAT by
A36,
A37,
A38,
A40,
A41,
INT_1: 5;
then
reconsider z = (x
- y) as
Nat;
take z, y;
(
dom
<:Da, Db:>)
= ((
dom Da)
/\ (
dom Db)) by
FUNCT_3:def 7;
then
A49: d
in (
dom
<:Da, Db:>) by
A19,
A22,
XBOOLE_0:def 4;
then (
<:Da, Db:>
. d)
=
[(Da
. d), (Db
. d)] by
FUNCT_3:def 7;
then (D
. d)
= ((
subtraction A)
. ((
denaming (a,da)),(
denaming (b,db)))) by
A36,
A49,
FUNCT_1: 13
.= (
subtraction ((
denaming (a,da)),(
denaming (b,db)))) by
A4,
A45,
A46,
Def15;
hence z
= (L
. a) by
A20,
A21,
A29,
A31,
A34,
A37,
A39,
A41,
NOMIN_1:def 12;
thus y
= (L
. b) by
A20,
A23,
A24,
A38,
A41,
A44,
NOMIN_1:def 12;
((x
- (1
* y))
gcd y)
= (x
gcd y) by
NEWTON02: 5;
hence thesis by
A33;
end;
A50: d
in (
dom S) by
A10,
A12,
A13,
A20,
A25;
then (S
. d)
= (i
. L) by
A20,
NOMIN_2: 35
.=
TRUE by
A25,
A28,
Def28;
hence (i
. (f
. d))
=
TRUE by
A7,
A10,
A11,
A50,
NOMIN_3: 11;
end;
hence thesis by
NOMIN_3: 28;
end;
theorem ::
NOMIN_4:19
Th18: V is non
empty & A
is_without_nonatomicND_wrt V & a
<> b & A is
complex-containing & (for d holds a
is_complex_on d) & (for d holds b
is_complex_on d) implies
<*(
PP_and ((
less (A,a,b)),(
gcd_inv (V,A,a,b,x0,y0)))), (
SC_assignment ((
subtraction (A,b,a)),b)), (
gcd_inv (V,A,a,b,x0,y0))*> is
SFHT of (
ND (V,A))
proof
assume that
A1: V is non
empty and
A2: A
is_without_nonatomicND_wrt V and
A3: a
<> b and
A4: A is
complex-containing and
A5: for d holds a
is_complex_on d and
A6: for d holds b
is_complex_on d;
set i = (
gcd_inv (V,A,a,b,x0,y0));
set l = (
less (A,a,b));
set D = (
subtraction (A,b,a));
set Da = (
denaming (V,A,a));
set Db = (
denaming (V,A,b));
set f = (
SC_assignment (D,b));
set p = (
PP_and (l,i));
set S = (
SC_Psuperpos (i,D,b));
A7:
<*S, f, i*> is
SFHT of (
ND (V,A)) by
NOMIN_3: 29;
for d holds d
in (
dom p) & (p
. d)
=
TRUE & d
in (
dom f) & (f
. d)
in (
dom i) implies (i
. (f
. d))
=
TRUE
proof
let d such that
A8: d
in (
dom p) and
A9: (p
. d)
=
TRUE and
A10: d
in (
dom f) and
A11: (f
. d)
in (
dom i);
A12: (
dom f)
= (
dom D) by
NOMIN_2:def 7;
A13: (
dom S)
= { d where d be
TypeSCNominativeData of V, A : (
local_overlapping (V,A,d,(D
. d),b))
in (
dom i) & d
in (
dom D) } by
NOMIN_2:def 11;
A14: (
dom Da)
= { d where d be
NonatomicND of V, A : a
in (
dom d) } by
NOMIN_1:def 18;
A15: (
dom Db)
= { d where d be
NonatomicND of V, A : b
in (
dom d) } by
NOMIN_1:def 18;
A16: d
in (
dom l) by
A8,
A9,
PARTPR_1: 23;
A17: (
dom ((
less A)
*
<:Da, Db:>))
c= (
dom
<:Da, Db:>) by
RELAT_1: 25;
A18: (
dom
<:Da, Db:>)
= ((
dom Da)
/\ (
dom Db)) by
FUNCT_3:def 7;
then
A19: d
in (
dom Da) by
A16,
A17,
XBOOLE_0:def 4;
then
consider da be
NonatomicND of V, A such that
A20: d
= da and
A21: a
in (
dom da) by
A14;
A22: d
in (
dom Db) by
A16,
A17,
A18,
XBOOLE_0:def 4;
then
consider db be
NonatomicND of V, A such that
A23: d
= db and
A24: b
in (
dom db) by
A15;
reconsider L = (
local_overlapping (V,A,db,(D
. db),b)) as
Function;
(
dom i)
= (
ND (V,A)) by
Def28;
then
A25: L
in (
dom i);
A26: (
rng D)
c= (
rng (
subtraction A)) by
RELAT_1: 26;
A27: (
rng D)
c= A by
A26,
XBOOLE_1: 1;
reconsider L as
NonatomicND of V, A by
NOMIN_2: 9;
A28:
gcd_inv_pred (V,A,a,b,x0,y0,L)
proof
take L;
thus L
= L;
d
in (
dom i) & (i
. d)
=
TRUE by
A8,
A9,
PARTPR_1: 23;
then
gcd_inv_pred (V,A,a,b,x0,y0,d) by
Def28;
then
consider d1 be
NonatomicND of V, A such that
A29: d
= d1 and a
in (
dom d1) and b
in (
dom d1) and
A30: ex x,y be
Nat st x
= (d1
. a) & y
= (d1
. b) & (x
gcd y)
= (x0
gcd y0);
consider x,y be
Nat such that
A31: x
= (d1
. a) and
A32: y
= (d1
. b) and
A33: (x
gcd y)
= (x0
gcd y0) by
A30;
(D
. d)
in (
rng D) by
A10,
A12,
FUNCT_1:def 3;
then
reconsider Dd = (D
. d) as
TypeSCNominativeData of V, A by
A27,
NOMIN_1:def 6;
A34: (L
. b)
= Dd by
A1,
A23,
NOMIN_2: 10;
A35: (
<:Da, Db:>
. d)
=
[(Da
. d), (Db
. d)] by
A16,
A17,
FUNCT_3:def 7;
A36: (Da
. d)
= (
denaming (a,da)) & (Db
. d)
= (
denaming (b,db)) by
A20,
A23,
A19,
A22,
NOMIN_1:def 18;
a
is_complex_on d & b
is_complex_on d by
A5,
A6;
then
consider x1,y1 be
Complex such that
A37: x1
= (
denaming (b,db)) and
A38: y1
= (
denaming (a,da)) and
A39: (
subtraction ((
denaming (b,db)),(
denaming (a,da))))
= (x1
- y1) by
A36,
Def14;
A40: y1
= x by
A20,
A21,
A29,
A31,
A38,
NOMIN_1:def 12;
A41: x1
= y by
A23,
A24,
A29,
A32,
A37,
NOMIN_1:def 12;
A42: not db
in A by
A2,
Th3;
A43: not (
naming (V,A,b,(D
. db)))
in A by
A2,
Th3;
A44: Dd
= (D
. d);
A45: (
denaming (a,da))
in
COMPLEX by
A38,
XCMPLX_0:def 2;
A46: (
denaming (b,db))
in
COMPLEX by
A37,
XCMPLX_0:def 2;
A47: (
dom (
local_overlapping (V,A,db,Dd,b)))
= (
dom db) by
A1,
A23,
A24,
A42,
A43,
NOMIN_2: 14;
hence a
in (
dom L) by
A20,
A21,
A23;
thus b
in (
dom L) by
A23,
A24,
A47;
A48: (l
. d)
=
TRUE by
A8,
A9,
PARTPR_1: 23;
d
in (
dom l) by
A8,
A9,
PARTPR_1: 23;
then (l
. d)
= ((
less A)
. ((Da
. d),(Db
. d))) by
A35,
FUNCT_1: 12;
then (Da
. d)
less_pred (Db
. d) by
A4,
A36,
A45,
A46,
A48,
Def12;
then (y
- x)
in
NAT by
A36,
A37,
A38,
A40,
A41,
INT_1: 5;
then
reconsider z = (y
- x) as
Nat;
take x, z;
(
dom
<:Db, Da:>)
= ((
dom Da)
/\ (
dom Db)) by
FUNCT_3:def 7;
then
A49: d
in (
dom
<:Db, Da:>) by
A19,
A22,
XBOOLE_0:def 4;
then (
<:Db, Da:>
. d)
=
[(Db
. d), (Da
. d)] by
FUNCT_3:def 7;
then
A50: (D
. d)
= ((
subtraction A)
. ((
denaming (b,db)),(
denaming (a,da)))) by
A36,
A49,
FUNCT_1: 13
.= (
subtraction ((
denaming (b,db)),(
denaming (a,da)))) by
A4,
A45,
A46,
Def15;
thus x
= (L
. a) by
A1,
A3,
A20,
A21,
A23,
A29,
A31,
A42,
A43,
A44,
NOMIN_2: 12;
thus z
= (L
. b) by
A20,
A21,
A29,
A31,
A34,
A38,
A39,
A41,
A50,
NOMIN_1:def 12;
((y
- (1
* x))
gcd x)
= (y
gcd x) by
NEWTON02: 5;
hence thesis by
A33;
end;
A51: d
in (
dom S) by
A10,
A12,
A13,
A23,
A25;
then (S
. d)
= (i
. L) by
A23,
NOMIN_2: 35
.=
TRUE by
A25,
A28,
Def28;
hence (i
. (f
. d))
=
TRUE by
A7,
A10,
A11,
A51,
NOMIN_3: 11;
end;
hence thesis by
NOMIN_3: 28;
end;
theorem ::
NOMIN_4:20
Th19: V is non
empty & A
is_without_nonatomicND_wrt V & a
<> b & A is
complex-containing & (for d holds a
is_complex_on d) & (for d holds b
is_complex_on d) implies
<*(
gcd_inv (V,A,a,b,x0,y0)), (
gcd_conditional_step (V,A,a,b)), (
gcd_inv (V,A,a,b,x0,y0))*> is
SFHT of (
ND (V,A))
proof
assume that
A1: V is non
empty and
A2: A
is_without_nonatomicND_wrt V and
A3: a
<> b and
A4: A is
complex-containing and
A5: (for d holds a
is_complex_on d) & (for d holds b
is_complex_on d);
set i = (
gcd_inv (V,A,a,b,x0,y0));
set l = (
less (A,b,a));
A6:
<*(
PP_and (l,i)), (
SC_assignment ((
subtraction (A,a,b)),a)), i*> is
SFHT of (
ND (V,A)) by
A1,
A2,
A3,
A4,
A5,
Th17;
<*i, (
PPid (
ND (V,A))), i*> is
SFHT of (
ND (V,A)) by
NOMIN_3: 17;
then
<*(
PP_and ((
PP_not l),i)), (
PPid (
ND (V,A))), i*> is
SFHT of (
ND (V,A)) by
NOMIN_3: 4,
NOMIN_3: 15;
hence thesis by
A6,
NOMIN_3: 21;
end;
theorem ::
NOMIN_4:21
Th20: V is non
empty & A
is_without_nonatomicND_wrt V & a
<> b & A is
complex-containing & (for d holds a
is_complex_on d) & (for d holds b
is_complex_on d) implies
<*(
gcd_inv (V,A,a,b,x0,y0)), (
gcd_conditional_step (V,A,b,a)), (
gcd_inv (V,A,a,b,x0,y0))*> is
SFHT of (
ND (V,A))
proof
assume that
A1: V is non
empty and
A2: A
is_without_nonatomicND_wrt V and
A3: a
<> b and
A4: A is
complex-containing and
A5: (for d holds a
is_complex_on d) & (for d holds b
is_complex_on d);
set i = (
gcd_inv (V,A,a,b,x0,y0));
set l = (
less (A,a,b));
A6:
<*(
PP_and (l,i)), (
SC_assignment ((
subtraction (A,b,a)),b)), i*> is
SFHT of (
ND (V,A)) by
A1,
A2,
A3,
A4,
A5,
Th18;
<*i, (
PPid (
ND (V,A))), i*> is
SFHT of (
ND (V,A)) by
NOMIN_3: 17;
then
<*(
PP_and ((
PP_not l),i)), (
PPid (
ND (V,A))), i*> is
SFHT of (
ND (V,A)) by
NOMIN_3: 4,
NOMIN_3: 15;
hence thesis by
A6,
NOMIN_3: 21;
end;
theorem ::
NOMIN_4:22
Th21: V is non
empty & A
is_without_nonatomicND_wrt V & a
<> b & A is
complex-containing & (for d holds a
is_complex_on d) & (for d holds b
is_complex_on d) implies
<*(
gcd_inv (V,A,a,b,x0,y0)), (
gcd_loop_body (V,A,a,b)), (
gcd_inv (V,A,a,b,x0,y0))*> is
SFHT of (
ND (V,A))
proof
assume that
A1: V is non
empty and
A2: A
is_without_nonatomicND_wrt V and
A3: a
<> b and
A4: A is
complex-containing and
A5: (for d holds a
is_complex_on d) & (for d holds b
is_complex_on d);
set i = (
gcd_inv (V,A,a,b,x0,y0));
set e = (
Equality (A,a,b));
set s1 = (
gcd_conditional_step (V,A,a,b));
set s2 = (
gcd_conditional_step (V,A,b,a));
A6: (
PP_inversion i)
||= (
PP_False (
ND (V,A))) by
PARTPR_2: 10;
<*(
PP_False (
ND (V,A))), s2, i*> is
SFHT of (
ND (V,A)) by
NOMIN_3: 18;
then
A7:
<*(
PP_inversion i), s2, i*> is
SFHT of (
ND (V,A)) by
A6,
NOMIN_3: 15;
A8:
<*i, s1, i*> is
SFHT of (
ND (V,A)) by
A1,
A2,
A3,
A4,
A5,
Th19;
<*i, s2, i*> is
SFHT of (
ND (V,A)) by
A1,
A2,
A3,
A4,
A5,
Th20;
hence thesis by
A7,
A8,
NOMIN_3: 25;
end;
::$Canceled
theorem ::
NOMIN_4:24
Th23: V is non
empty & A
is_without_nonatomicND_wrt V & a
<> b & A is
complex-containing & (for d holds a
is_complex_on d) & (for d holds b
is_complex_on d) implies
<*(
gcd_inv (V,A,a,b,x0,y0)), (
gcd_main_loop (V,A,a,b)), (
PP_and ((
Equality (A,a,b)),(
gcd_inv (V,A,a,b,x0,y0))))*> is
SFHT of (
ND (V,A))
proof
set p = (
gcd_inv (V,A,a,b,x0,y0));
set r = (
PP_not (
Equality (A,a,b)));
set f = (
gcd_loop_body (V,A,a,b));
assume V is non
empty & A
is_without_nonatomicND_wrt V & a
<> b & A is
complex-containing & (for d holds a
is_complex_on d) & (for d holds b
is_complex_on d);
then
<*p, f, p*> is
SFHT of (
ND (V,A)) by
Th21;
then
A2:
<*(
PP_and (r,p)), f, p*> is
SFHT of (
ND (V,A)) by
NOMIN_3: 4,
NOMIN_3: 15;
<*(
PP_inversion p), f, p*> is
SFHT of (
ND (V,A)) by
NOMIN_3: 19;
then
<*(
PP_and (r,(
PP_inversion p))), f, p*> is
SFHT of (
ND (V,A)) by
NOMIN_3: 4,
NOMIN_3: 15;
hence thesis by
A2,
NOMIN_3: 26;
end;
theorem ::
NOMIN_4:25
Th24: V is non
empty & A
is_without_nonatomicND_wrt V & a
<> b & a
<> y & A is
complex-containing & (for d holds a
is_complex_on d) & (for d holds b
is_complex_on d) implies
<*(
valid_gcd_input (V,A,x,y,x0,y0)), (
gcd_main_part (V,A,a,b,x,y)), (
PP_and ((
Equality (A,a,b)),(
gcd_inv (V,A,a,b,x0,y0))))*> is
SFHT of (
ND (V,A))
proof
assume
A1: V is non
empty & A
is_without_nonatomicND_wrt V & a
<> b & a
<> y & A is
complex-containing & (for d holds a
is_complex_on d) & (for d holds b
is_complex_on d);
set f = (
gcd_var_init (V,A,a,b,x,y));
set g = (
gcd_main_loop (V,A,a,b));
set p = (
valid_gcd_input (V,A,x,y,x0,y0));
set q = (
gcd_inv (V,A,a,b,x0,y0));
set r = (
PP_and ((
Equality (A,a,b)),(
gcd_inv (V,A,a,b,x0,y0))));
A2:
<*p, f, q*> is
SFHT of (
ND (V,A)) by
A1,
Th16;
A3:
<*q, g, r*> is
SFHT of (
ND (V,A)) by
A1,
Th23;
<*(
PP_inversion q), g, r*> is
SFHT of (
ND (V,A)) by
NOMIN_3: 19;
hence thesis by
A2,
A3,
NOMIN_3: 25;
end;
theorem ::
NOMIN_4:26
Th25: V is non
empty & A
is_without_nonatomicND_wrt V & (for d holds a
is_a_value_on d) & (for d holds b
is_a_value_on d) implies
<*(
PP_and ((
Equality (A,a,b)),(
gcd_inv (V,A,a,b,x0,y0)))), (
SC_assignment ((
denaming (V,A,a)),z)), (
valid_gcd_output (V,A,z,x0,y0))*> is
SFHT of (
ND (V,A))
proof
assume that
A1: V is non
empty and
A2: A
is_without_nonatomicND_wrt V and
A3: (for d holds a
is_a_value_on d) & (for d holds b
is_a_value_on d);
set Da = (
denaming (V,A,a));
set Db = (
denaming (V,A,b));
set Dz = (
denaming (V,A,z));
set q = (
PP_and ((
Equality (A,a,b)),(
gcd_inv (V,A,a,b,x0,y0))));
set r = (
valid_gcd_output (V,A,z,x0,y0));
set g = (
SC_assignment (Da,z));
set E = (
Equality A);
set sp = (
SC_Psuperpos (r,Da,z));
A4:
<*sp, g, r*> is
SFHT of (
ND (V,A)) by
NOMIN_3: 29;
q
||= sp
proof
let d be
Element of (
ND (V,A));
assume
A5: d
in (
dom q) & (q
. d)
=
TRUE ;
reconsider dd = d as
TypeSCNominativeData of V, A by
NOMIN_1: 39;
set X = { d where d be
TypeSCNominativeData of V, A : d
in (
dom (
Equality (A,a,b))) & ((
Equality (A,a,b))
. d)
=
FALSE or d
in (
dom (
gcd_inv (V,A,a,b,x0,y0))) & ((
gcd_inv (V,A,a,b,x0,y0))
. d)
=
FALSE or d
in (
dom (
Equality (A,a,b))) & ((
Equality (A,a,b))
. d)
=
TRUE & d
in (
dom (
gcd_inv (V,A,a,b,x0,y0))) & ((
gcd_inv (V,A,a,b,x0,y0))
. d)
=
TRUE };
d
in X by
A5,
NOMIN_2: 17;
then
A6: ex d1 be
TypeSCNominativeData of V, A st d
= d1 & (d1
in (
dom (
Equality (A,a,b))) & ((
Equality (A,a,b))
. d1)
=
FALSE or d1
in (
dom (
gcd_inv (V,A,a,b,x0,y0))) & ((
gcd_inv (V,A,a,b,x0,y0))
. d1)
=
FALSE or d1
in (
dom (
Equality (A,a,b))) & ((
Equality (A,a,b))
. d1)
=
TRUE & d1
in (
dom (
gcd_inv (V,A,a,b,x0,y0))) & ((
gcd_inv (V,A,a,b,x0,y0))
. d1)
=
TRUE );
A7: (
dom Da)
= { d where d be
NonatomicND of V, A : a
in (
dom d) } by
NOMIN_1:def 18;
A8: d
in (
dom Da)
proof
(
dom (
Equality (A,a,b)))
= ((
dom Da)
/\ (
dom Db)) by
Th11,
A3;
hence d
in (
dom Da) by
A5,
A6,
PARTPR_1: 19,
XBOOLE_0:def 4;
end;
consider D be
NonatomicND of V, A such that
A9: d
= D and a
in (
dom D) by
A8,
A7;
A10: (
dom r)
= { d where d be
TypeSCNominativeData of V, A : d
in (
dom Dz) } by
Def26;
A11: (Da
. d) is
TypeSCNominativeData of V, A
proof
(Da
. d)
in (
ND (V,A)) by
PARTFUN1: 4,
A8;
then ex d1 be
TypeSCNominativeData of V, A st (Da
. d)
= d1;
hence thesis;
end;
A12: (
local_overlapping (V,A,d,(Da
. d),z))
in (
dom Dz)
proof
ex d2 be
NonatomicND of V, A st d2
= d & a
in (
dom d2) by
A8,
A7;
hence thesis by
A1,
A2,
Th6,
A11;
end;
then
A13: (
local_overlapping (V,A,d,(Da
. d),z))
in (
dom r) by
A10;
thus
A14: d
in (
dom sp)
proof
dd
in { d where d be
TypeSCNominativeData of V, A : (
local_overlapping (V,A,d,(Da
. d),z))
in (
dom r) & d
in (
dom Da) } by
A8,
A13;
hence thesis by
NOMIN_2:def 11;
end;
thus (sp
. d)
=
TRUE
proof
set dlo = (
local_overlapping (V,A,D,(Da
. d),z));
A15: (sp
. dd)
= (r
. dlo) & dd
in (
dom Da) by
A9,
A14,
NOMIN_2: 35;
valid_gcd_output_pred (V,A,z,x0,y0,dlo)
proof
gcd_inv_pred (V,A,a,b,x0,y0,d) by
A5,
A6,
PARTPR_1: 19,
Def28;
then
consider d2 be
NonatomicND of V, A such that
A16: d
= d2 & a
in (
dom d2) & b
in (
dom d2) & ex x,y be
Nat st x
= (d2
. a) & y
= (d2
. b) & (x
gcd y)
= (x0
gcd y0);
consider X,Y be
Nat such that
A17: X
= (d2
. a) & Y
= (d2
. b) & (X
gcd Y)
= (x0
gcd y0) by
A16;
A18: (Da
. d)
in A
proof
a
is_a_value_on dd by
A3;
hence thesis;
end;
A19: d
in (
dom Db)
proof
(
dom (
Equality (A,a,b)))
= ((
dom Da)
/\ (
dom Db)) by
Th11,
A3;
hence thesis by
A5,
A6,
PARTPR_1: 19,
XBOOLE_0:def 4;
end;
A20: (Db
. d)
in A
proof
b
is_a_value_on dd by
A3;
hence thesis;
end;
(
dom
<:Da, Db:>)
= ((
dom Da)
/\ (
dom Db)) by
FUNCT_3:def 7;
then
A21: d
in (
dom
<:Da, Db:>) by
XBOOLE_0:def 4,
A8,
A19;
A22: (Da
. d)
= (
denaming (a,d2)) by
A8,
A16,
NOMIN_1:def 18
.= (d2
. a) by
A16,
NOMIN_1:def 12;
A23: (Db
. d)
= (
denaming (b,d2)) by
A19,
A16,
NOMIN_1:def 18
.= (d2
. b) by
A16,
NOMIN_1:def 12;
TRUE
= (E
. (
<:Da, Db:>
. d)) by
A5,
A6,
A21,
FUNCT_1: 13,
PARTPR_1: 19
.= (E
. ((Da
. d),(Db
. d))) by
FUNCT_3:def 7,
A21;
then
A24: (Da
. d)
= (Db
. d) by
A18,
A20,
Def9;
A25: (X
gcd Y)
=
|.X.| by
A24,
A22,
A23,
A17,
NEWTON02: 3;
reconsider d1 = dlo as
NonatomicND of V, A by
NOMIN_2: 9;
A26: z
in (
dom d1)
proof
d1
in { d where d be
NonatomicND of V, A : z
in (
dom d) } by
A9,
A12,
NOMIN_1:def 18;
then ex dd1 be
NonatomicND of V, A st d1
= dd1 & z
in (
dom dd1);
hence z
in (
dom d1);
end;
(d1
. z)
= (x0
gcd y0) by
A1,
A11,
A22,
A17,
A25,
NOMIN_2: 10;
hence thesis by
A26;
end;
hence thesis by
A15,
A9,
Def26,
A13;
end;
end;
hence thesis by
A4,
NOMIN_3: 15;
end;
theorem ::
NOMIN_4:27
Th26: A is
complex-containing & (for d holds a
is_complex_on d) & (for d holds b
is_complex_on d) implies
<*(
PP_inversion (
PP_and ((
Equality (A,a,b)),(
gcd_inv (V,A,a,b,x0,y0))))), (
SC_assignment ((
denaming (V,A,a)),z)), (
valid_gcd_output (V,A,z,x0,y0))*> is
SFHT of (
ND (V,A))
proof
set Da = (
denaming (V,A,a));
set Db = (
denaming (V,A,b));
set Dz = (
denaming (V,A,z));
set e = (
Equality (A,a,b));
set i = (
gcd_inv (V,A,a,b,x0,y0));
set q = (
PP_and (e,i));
set r = (
valid_gcd_output (V,A,z,x0,y0));
set g = (
SC_assignment (Da,z));
set P = (
PP_inversion q);
assume that
A2: A is
complex-containing and
A3: for d holds a
is_complex_on d and
A4: for d holds b
is_complex_on d;
A5: for d holds a
is_a_value_on d by
A2,
A3,
Th7;
A6: for d holds b
is_a_value_on d by
A2,
A4,
Th7;
A9: (
dom q)
= { d where d be
TypeSCNominativeData of V, A : d
in (
dom e) & (e
. d)
=
FALSE or d
in (
dom i) & (i
. d)
=
FALSE or d
in (
dom e) & (e
. d)
=
TRUE & d
in (
dom i) & (i
. d)
=
TRUE } by
NOMIN_2: 17;
A10: (
dom e)
= ((
dom Da)
/\ (
dom Db)) by
A5,
A6,
Th11;
A11: (
dom e)
c= (
dom q) by
PARTPR_2: 3;
for d holds d
in (
dom P) & (P
. d)
=
TRUE & d
in (
dom g) & (g
. d)
in (
dom r) implies (r
. (g
. d))
=
TRUE
proof
let d such that
A12: d
in (
dom P) and (P
. d)
=
TRUE and
A13: d
in (
dom g) and (g
. d)
in (
dom r);
(
dom P)
= { d where d be
Element of (
ND (V,A)) : not d
in (
dom q) } by
PARTPR_2:def 17;
then
consider d1 be
Element of (
ND (V,A)) such that
A14: d
= d1 and
A15: not d1
in (
dom q) by
A12;
A16: (
dom g)
= (
dom Da) by
NOMIN_2:def 7;
not d1
in (
dom e) by
A11,
A15;
then
A17: not d1
in (
dom Db) by
A10,
A13,
A14,
A16,
XBOOLE_0:def 4;
A18: (
dom Db)
= { d where d be
NonatomicND of V, A : b
in (
dom d) } by
NOMIN_1:def 18;
(
dom i)
= (
ND (V,A)) by
Def28;
then
A19: d
in (
dom i);
not d
in (
dom i) or (i
. d)
<>
FALSE by
A9,
A14,
A15;
then
gcd_inv_pred (V,A,a,b,x0,y0,d) by
A19,
Def28;
hence thesis by
A14,
A17,
A18;
end;
hence
<*P, g, r*> is
SFHT of (
ND (V,A)) by
NOMIN_3: 28;
end;
::$Notion-Name
theorem ::
NOMIN_4:28
V is non
empty & A
is_without_nonatomicND_wrt V & a
<> b & a
<> y & A is
complex-containing & (for d holds a
is_complex_on d) & (for d holds b
is_complex_on d) implies
<*(
valid_gcd_input (V,A,x,y,x0,y0)), (
gcd_program (V,A,a,b,x,y,z)), (
valid_gcd_output (V,A,z,x0,y0))*> is
SFHT of (
ND (V,A))
proof
set Da = (
denaming (V,A,a));
set Db = (
denaming (V,A,b));
set Dz = (
denaming (V,A,z));
set e = (
Equality (A,a,b));
set i = (
gcd_inv (V,A,a,b,x0,y0));
set p = (
valid_gcd_input (V,A,x,y,x0,y0));
set q = (
PP_and (e,i));
set r = (
valid_gcd_output (V,A,z,x0,y0));
set f = (
gcd_main_part (V,A,a,b,x,y));
set g = (
SC_assignment (Da,z));
set P = (
PP_inversion q);
assume that
A1: V is non
empty & A
is_without_nonatomicND_wrt V & a
<> b & a
<> y and
A2: A is
complex-containing and
A3: for d holds a
is_complex_on d and
A4: for d holds b
is_complex_on d;
A5: for d holds a
is_a_value_on d by
A2,
A3,
Th7;
A6: for d holds b
is_a_value_on d by
A2,
A4,
Th7;
A7:
<*p, f, q*> is
SFHT of (
ND (V,A)) by
A1,
A2,
A3,
A4,
Th24;
A8:
<*q, g, r*> is
SFHT of (
ND (V,A)) by
A1,
A5,
A6,
Th25;
<*P, g, r*> is
SFHT of (
ND (V,A)) by
A2,
A3,
A4,
Th26;
hence thesis by
A7,
A8,
NOMIN_3: 25;
end;