:: by Ievgen Ivanov , Artur Korni{\l}owicz and Mykola Nikitchenko

::

:: Received June 29, 2018

:: Copyright (c) 2018-2019 Association of Mizar Users

:: deftheorem defines complex-containing NOMIN_4:def 1 :

for A being set holds

( A is complex-containing iff COMPLEX c= A );

for A being set holds

( A is complex-containing iff COMPLEX c= A );

registration

existence

ex b_{1} being set st b_{1} is complex-containing

for b_{1} being set st b_{1} is complex-containing holds

not b_{1} is empty
by XBOOLE_1:3;

end;
ex b

proof end;

coherence for b

not b

scheme :: NOMIN_4:sch 1

BinPredToFunEx{ F_{1}() -> set , F_{2}() -> set , P_{1}[ object , object ] } :

BinPredToFunEx{ F

ex f being Function of [:F_{1}(),F_{2}():],BOOLEAN st

for x, y being object st x in F_{1}() & y in F_{2}() holds

( ( P_{1}[x,y] implies f . (x,y) = TRUE ) & ( P_{1}[x,y] implies f . (x,y) = FALSE ) )

for x, y being object st x in F

( ( P

proof end;

scheme :: NOMIN_4:sch 2

BinPredToFunUnique{ F_{1}() -> set , F_{2}() -> set , P_{1}[ object , object ] } :

BinPredToFunUnique{ F

for f, g being Function of [:F_{1}(),F_{2}():],BOOLEAN st ( for x, y being object st x in F_{1}() & y in F_{2}() holds

( ( P_{1}[x,y] implies f . (x,y) = TRUE ) & ( P_{1}[x,y] implies f . (x,y) = FALSE ) ) ) & ( for x, y being object st x in F_{1}() & y in F_{2}() holds

( ( P_{1}[x,y] implies g . (x,y) = TRUE ) & ( P_{1}[x,y] implies g . (x,y) = FALSE ) ) ) holds

f = g

( ( P

( ( P

f = g

proof end;

scheme :: NOMIN_4:sch 3

Lambda2Unique{ F_{1}() -> set , F_{2}() -> set , F_{3}() -> set , F_{4}( object , object ) -> object } :

Lambda2Unique{ F

for f, g being Function of [:F_{1}(),F_{2}():],F_{3}() st ( for x, y being object st x in F_{1}() & y in F_{2}() holds

f . (x,y) = F_{4}(x,y) ) & ( for x, y being object st x in F_{1}() & y in F_{2}() holds

g . (x,y) = F_{4}(x,y) ) holds

f = g

f . (x,y) = F

g . (x,y) = F

f = g

proof end;

definition

let V, A be set ;

{ d where d is NonatomicND of V,A : verum } is set ;

end;
func nonatomicsND (V,A) -> set equals :: NOMIN_4:def 2

{ d where d is NonatomicND of V,A : verum } ;

coherence { d where d is NonatomicND of V,A : verum } ;

{ d where d is NonatomicND of V,A : verum } is set ;

:: deftheorem defines nonatomicsND NOMIN_4:def 2 :

for V, A being set holds nonatomicsND (V,A) = { d where d is NonatomicND of V,A : verum } ;

for V, A being set holds nonatomicsND (V,A) = { d where d is NonatomicND of V,A : verum } ;

registration

let V, A be set ;

coherence

( not nonatomicsND (V,A) is empty & nonatomicsND (V,A) is functional )

end;
coherence

( not nonatomicsND (V,A) is empty & nonatomicsND (V,A) is functional )

proof end;

:: deftheorem defines is_without_nonatomicND_wrt NOMIN_4:def 3 :

for V, A being set holds

( A is_without_nonatomicND_wrt V iff A misses nonatomicsND (V,A) );

for V, A being set holds

( A is_without_nonatomicND_wrt V iff A misses nonatomicsND (V,A) );

theorem Th3: :: NOMIN_4:3

for V, A being set st A is_without_nonatomicND_wrt V holds

for d being NonatomicND of V,A holds not d in A

for d being NonatomicND of V,A holds not d in A

proof end;

theorem Th4: :: NOMIN_4:4

for v being object

for V, A being set st A is_without_nonatomicND_wrt V & v in V holds

for d1 being NonatomicND of V,A

for d2 being TypeSCNominativeData of V,A holds dom (local_overlapping (V,A,d1,d2,v)) = {v} \/ (dom d1)

for V, A being set st A is_without_nonatomicND_wrt V & v in V holds

for d1 being NonatomicND of V,A

for d2 being TypeSCNominativeData of V,A holds dom (local_overlapping (V,A,d1,d2,v)) = {v} \/ (dom d1)

proof end;

theorem :: NOMIN_4:5

for v being object

for V, A being set

for f being SCBinominativeFunction of V,A st A is_without_nonatomicND_wrt V holds

for d being NonatomicND of V,A st v in V & d in dom f holds

dom ((SC_assignment (f,v)) . d) = (dom d) \/ {v}

for V, A being set

for f being SCBinominativeFunction of V,A st A is_without_nonatomicND_wrt V holds

for d being NonatomicND of V,A st v in V & d in dom f holds

dom ((SC_assignment (f,v)) . d) = (dom d) \/ {v}

proof end;

theorem Th6: :: NOMIN_4:6

for v being object

for V, A being set

for d being TypeSCNominativeData of V,A

for d1 being NonatomicND of V,A st v in V & A is_without_nonatomicND_wrt V holds

local_overlapping (V,A,d1,d,v) in dom (denaming (V,A,v))

for V, A being set

for d being TypeSCNominativeData of V,A

for d1 being NonatomicND of V,A st v in V & A is_without_nonatomicND_wrt V holds

local_overlapping (V,A,d1,d,v) in dom (denaming (V,A,v))

proof end;

:: deftheorem defines is_ext_real_on NOMIN_4:def 4 :

for V, A being set

for d being TypeSCNominativeData of V,A

for a being Element of V holds

( a is_ext_real_on d iff (denaming (V,A,a)) . d is ext-real );

for V, A being set

for d being TypeSCNominativeData of V,A

for a being Element of V holds

( a is_ext_real_on d iff (denaming (V,A,a)) . d is ext-real );

:: deftheorem defines is_complex_on NOMIN_4:def 5 :

for V, A being set

for d being TypeSCNominativeData of V,A

for a being Element of V holds

( a is_complex_on d iff (denaming (V,A,a)) . d is complex );

for V, A being set

for d being TypeSCNominativeData of V,A

for a being Element of V holds

( a is_complex_on d iff (denaming (V,A,a)) . d is complex );

:: deftheorem defines is_a_value_on NOMIN_4:def 6 :

for V, A being set

for d being TypeSCNominativeData of V,A

for a being Element of V holds

( a is_a_value_on d iff (denaming (V,A,a)) . d in A );

for V, A being set

for d being TypeSCNominativeData of V,A

for a being Element of V holds

( a is_a_value_on d iff (denaming (V,A,a)) . d in A );

theorem Th7: :: NOMIN_4:7

for V, A being set

for a being Element of V st A is complex-containing & ( for d being TypeSCNominativeData of V,A holds a is_complex_on d ) holds

for d being TypeSCNominativeData of V,A holds a is_a_value_on d

for a being Element of V st A is complex-containing & ( for d being TypeSCNominativeData of V,A holds a is_complex_on d ) holds

for d being TypeSCNominativeData of V,A holds a is_a_value_on d

proof end;

theorem Th8: :: NOMIN_4:8

for V, A being set

for a being Element of V st ( for d being TypeSCNominativeData of V,A holds a is_a_value_on d ) holds

rng (denaming (V,A,a)) c= A

for a being Element of V st ( for d being TypeSCNominativeData of V,A holds a is_a_value_on d ) holds

rng (denaming (V,A,a)) c= A

proof end;

theorem Th9: :: NOMIN_4:9

for V, A being set

for a, b being Element of V st ( for d being TypeSCNominativeData of V,A holds a is_a_value_on d ) & ( for d being TypeSCNominativeData of V,A holds b is_a_value_on d ) holds

rng <:(denaming (V,A,a)),(denaming (V,A,b)):> c= [:A,A:]

for a, b being Element of V st ( for d being TypeSCNominativeData of V,A holds a is_a_value_on d ) & ( for d being TypeSCNominativeData of V,A holds b is_a_value_on d ) holds

rng <:(denaming (V,A,a)),(denaming (V,A,b)):> c= [:A,A:]

proof end;

definition

let V, A be set ;

let a, b be Element of V;

let p be Function of [:A,A:],BOOLEAN;

p * <:(denaming (V,A,a)),(denaming (V,A,b)):> is SCPartialNominativePredicate of V,A

end;
let a, b be Element of V;

let p be Function of [:A,A:],BOOLEAN;

func lift_binary_pred (p,a,b) -> SCPartialNominativePredicate of V,A equals :: NOMIN_4:def 7

p * <:(denaming (V,A,a)),(denaming (V,A,b)):>;

coherence p * <:(denaming (V,A,a)),(denaming (V,A,b)):>;

p * <:(denaming (V,A,a)),(denaming (V,A,b)):> is SCPartialNominativePredicate of V,A

proof end;

:: deftheorem defines lift_binary_pred NOMIN_4:def 7 :

for V, A being set

for a, b being Element of V

for p being Function of [:A,A:],BOOLEAN holds lift_binary_pred (p,a,b) = p * <:(denaming (V,A,a)),(denaming (V,A,b)):>;

for V, A being set

for a, b being Element of V

for p being Function of [:A,A:],BOOLEAN holds lift_binary_pred (p,a,b) = p * <:(denaming (V,A,a)),(denaming (V,A,b)):>;

definition

let V, A be set ;

let a, b be Element of V;

let op be Function of [:A,A:],A;

op * <:(denaming (V,A,a)),(denaming (V,A,b)):> is SCBinominativeFunction of V,A

end;
let a, b be Element of V;

let op be Function of [:A,A:],A;

func lift_binary_op (op,a,b) -> SCBinominativeFunction of V,A equals :: NOMIN_4:def 8

op * <:(denaming (V,A,a)),(denaming (V,A,b)):>;

coherence op * <:(denaming (V,A,a)),(denaming (V,A,b)):>;

op * <:(denaming (V,A,a)),(denaming (V,A,b)):> is SCBinominativeFunction of V,A

proof end;

:: deftheorem defines lift_binary_op NOMIN_4:def 8 :

for V, A being set

for a, b being Element of V

for op being Function of [:A,A:],A holds lift_binary_op (op,a,b) = op * <:(denaming (V,A,a)),(denaming (V,A,b)):>;

for V, A being set

for a, b being Element of V

for op being Function of [:A,A:],A holds lift_binary_op (op,a,b) = op * <:(denaming (V,A,a)),(denaming (V,A,b)):>;

definition

let A be set ;

ex b_{1} being Function of [:A,A:],BOOLEAN st

for a, b being object st a in A & b in A holds

( ( a = b implies b_{1} . (a,b) = TRUE ) & ( a <> b implies b_{1} . (a,b) = FALSE ) )

for b_{1}, b_{2} being Function of [:A,A:],BOOLEAN st ( for a, b being object st a in A & b in A holds

( ( a = b implies b_{1} . (a,b) = TRUE ) & ( a <> b implies b_{1} . (a,b) = FALSE ) ) ) & ( for a, b being object st a in A & b in A holds

( ( a = b implies b_{2} . (a,b) = TRUE ) & ( a <> b implies b_{2} . (a,b) = FALSE ) ) ) holds

b_{1} = b_{2}

end;
func Equality A -> Function of [:A,A:],BOOLEAN means :Def9: :: NOMIN_4:def 9

for a, b being object st a in A & b in A holds

( ( a = b implies it . (a,b) = TRUE ) & ( a <> b implies it . (a,b) = FALSE ) );

existence for a, b being object st a in A & b in A holds

( ( a = b implies it . (a,b) = TRUE ) & ( a <> b implies it . (a,b) = FALSE ) );

ex b

for a, b being object st a in A & b in A holds

( ( a = b implies b

proof end;

uniqueness for b

( ( a = b implies b

( ( a = b implies b

b

proof end;

:: deftheorem Def9 defines Equality NOMIN_4:def 9 :

for A being set

for b_{2} being Function of [:A,A:],BOOLEAN holds

( b_{2} = Equality A iff for a, b being object st a in A & b in A holds

( ( a = b implies b_{2} . (a,b) = TRUE ) & ( a <> b implies b_{2} . (a,b) = FALSE ) ) );

for A being set

for b

( b

( ( a = b implies b

definition

let V, A be set ;

let x, y be Element of V;

lift_binary_pred ((Equality A),x,y) is SCPartialNominativePredicate of V,A ;

end;
let x, y be Element of V;

func Equality (A,x,y) -> SCPartialNominativePredicate of V,A equals :: NOMIN_4:def 10

lift_binary_pred ((Equality A),x,y);

coherence lift_binary_pred ((Equality A),x,y);

lift_binary_pred ((Equality A),x,y) is SCPartialNominativePredicate of V,A ;

:: deftheorem defines Equality NOMIN_4:def 10 :

for V, A being set

for x, y being Element of V holds Equality (A,x,y) = lift_binary_pred ((Equality A),x,y);

for V, A being set

for x, y being Element of V holds Equality (A,x,y) = lift_binary_pred ((Equality A),x,y);

definition

let x, y be object ;

for x being object

for x1, y1 being ExtReal holds

( not x1 = x or not y1 = x or not x1 < y1 ) ;

asymmetry

for x, y being object st ex x1, y1 being ExtReal st

( x1 = x & y1 = y & x1 < y1 ) holds

for x1, y1 being ExtReal holds

( not x1 = y or not y1 = x or not x1 < y1 ) ;

end;
pred x less_pred y means :: NOMIN_4:def 11

ex x1, y1 being ExtReal st

( x1 = x & y1 = y & x1 < y1 );

irreflexivity ex x1, y1 being ExtReal st

( x1 = x & y1 = y & x1 < y1 );

for x being object

for x1, y1 being ExtReal holds

( not x1 = x or not y1 = x or not x1 < y1 ) ;

asymmetry

for x, y being object st ex x1, y1 being ExtReal st

( x1 = x & y1 = y & x1 < y1 ) holds

for x1, y1 being ExtReal holds

( not x1 = y or not y1 = x or not x1 < y1 ) ;

:: deftheorem defines less_pred NOMIN_4:def 11 :

for x, y being object holds

( x less_pred y iff ex x1, y1 being ExtReal st

( x1 = x & y1 = y & x1 < y1 ) );

for x, y being object holds

( x less_pred y iff ex x1, y1 being ExtReal st

( x1 = x & y1 = y & x1 < y1 ) );

definition

let A be set ;

ex b_{1} being Function of [:A,A:],BOOLEAN st

for x, y being object st x in A & y in A holds

( ( x less_pred y implies b_{1} . (x,y) = TRUE ) & ( not x less_pred y implies b_{1} . (x,y) = FALSE ) )

for b_{1}, b_{2} being Function of [:A,A:],BOOLEAN st ( for x, y being object st x in A & y in A holds

( ( x less_pred y implies b_{1} . (x,y) = TRUE ) & ( not x less_pred y implies b_{1} . (x,y) = FALSE ) ) ) & ( for x, y being object st x in A & y in A holds

( ( x less_pred y implies b_{2} . (x,y) = TRUE ) & ( not x less_pred y implies b_{2} . (x,y) = FALSE ) ) ) holds

b_{1} = b_{2}

end;
func less A -> Function of [:A,A:],BOOLEAN means :Def12: :: NOMIN_4:def 12

for x, y being 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 for x, y being 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 ) );

ex b

for x, y being object st x in A & y in A holds

( ( x less_pred y implies b

proof end;

uniqueness for b

( ( x less_pred y implies b

( ( x less_pred y implies b

b

proof end;

:: deftheorem Def12 defines less NOMIN_4:def 12 :

for A being set

for b_{2} being Function of [:A,A:],BOOLEAN holds

( b_{2} = less A iff for x, y being object st x in A & y in A holds

( ( x less_pred y implies b_{2} . (x,y) = TRUE ) & ( not x less_pred y implies b_{2} . (x,y) = FALSE ) ) );

for A being set

for b

( b

( ( x less_pred y implies b

definition

let V, A be set ;

let x, y be Element of V;

lift_binary_pred ((less A),x,y) is SCPartialNominativePredicate of V,A ;

end;
let x, y be Element of V;

func less (A,x,y) -> SCPartialNominativePredicate of V,A equals :: NOMIN_4:def 13

lift_binary_pred ((less A),x,y);

coherence lift_binary_pred ((less A),x,y);

lift_binary_pred ((less A),x,y) is SCPartialNominativePredicate of V,A ;

:: deftheorem defines less NOMIN_4:def 13 :

for V, A being set

for x, y being Element of V holds less (A,x,y) = lift_binary_pred ((less A),x,y);

for V, A being set

for x, y being Element of V holds less (A,x,y) = lift_binary_pred ((less A),x,y);

theorem Th11: :: NOMIN_4:11

for V, A being set

for a, b being Element of V st ( for d being TypeSCNominativeData of V,A holds a is_a_value_on d ) & ( for d being TypeSCNominativeData of V,A holds b is_a_value_on d ) holds

dom (Equality (A,a,b)) = (dom (denaming (V,A,a))) /\ (dom (denaming (V,A,b)))

for a, b being Element of V st ( for d being TypeSCNominativeData of V,A holds a is_a_value_on d ) & ( for d being TypeSCNominativeData of V,A holds b is_a_value_on d ) holds

dom (Equality (A,a,b)) = (dom (denaming (V,A,a))) /\ (dom (denaming (V,A,b)))

proof end;

theorem Th12: :: NOMIN_4:12

for V, A being set

for a, b being Element of V st ( for d being TypeSCNominativeData of V,A holds a is_a_value_on d ) & ( for d being TypeSCNominativeData of V,A holds b is_a_value_on d ) holds

dom (less (A,a,b)) = (dom (denaming (V,A,a))) /\ (dom (denaming (V,A,b)))

for a, b being Element of V st ( for d being TypeSCNominativeData of V,A holds a is_a_value_on d ) & ( for d being TypeSCNominativeData of V,A holds b is_a_value_on d ) holds

dom (less (A,a,b)) = (dom (denaming (V,A,a))) /\ (dom (denaming (V,A,b)))

proof end;

theorem :: NOMIN_4:13

for V, A being set

for a, b being Element of V st ( for d being TypeSCNominativeData of V,A holds a is_a_value_on d ) & ( for d being TypeSCNominativeData of V,A holds b is_a_value_on d ) & ( for d being TypeSCNominativeData of V,A holds a is_ext_real_on d ) & ( for d being TypeSCNominativeData of V,A holds b is_ext_real_on d ) holds

PP_not (Equality (A,a,b)) = PP_or ((less (A,a,b)),(less (A,b,a)))

for a, b being Element of V st ( for d being TypeSCNominativeData of V,A holds a is_a_value_on d ) & ( for d being TypeSCNominativeData of V,A holds b is_a_value_on d ) & ( for d being TypeSCNominativeData of V,A holds a is_ext_real_on d ) & ( for d being TypeSCNominativeData of V,A holds b is_ext_real_on d ) holds

PP_not (Equality (A,a,b)) = PP_or ((less (A,a,b)),(less (A,b,a)))

proof end;

theorem :: NOMIN_4:14

for V, A being set

for d being TypeSCNominativeData of V,A

for a, b being Element of V st ( for d being TypeSCNominativeData of V,A holds a is_a_value_on d ) & ( for d being TypeSCNominativeData of V,A 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 & not ( d in dom (less (A,a,b)) & (less (A,a,b)) . d = TRUE ) holds

( d in dom (less (A,b,a)) & (less (A,b,a)) . d = TRUE )

for d being TypeSCNominativeData of V,A

for a, b being Element of V st ( for d being TypeSCNominativeData of V,A holds a is_a_value_on d ) & ( for d being TypeSCNominativeData of V,A 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 & not ( d in dom (less (A,a,b)) & (less (A,a,b)) . d = TRUE ) holds

( d in dom (less (A,b,a)) & (less (A,b,a)) . d = TRUE )

proof end;

definition

let x, y be object ;

assume A1: ( x is Complex & y is Complex ) ;

ex b_{1}, x1, y1 being Complex st

( x1 = x & y1 = y & b_{1} = x1 - y1 )

for b_{1}, b_{2} being Complex st ex x1, y1 being Complex st

( x1 = x & y1 = y & b_{1} = x1 - y1 ) & ex x1, y1 being Complex st

( x1 = x & y1 = y & b_{2} = x1 - y1 ) holds

b_{1} = b_{2}
;

end;
assume A1: ( x is Complex & y is Complex ) ;

func subtraction (x,y) -> Complex means :Def14: :: NOMIN_4:def 14

ex x1, y1 being Complex st

( x1 = x & y1 = y & it = x1 - y1 );

existence ex x1, y1 being Complex st

( x1 = x & y1 = y & it = x1 - y1 );

ex b

( x1 = x & y1 = y & b

proof end;

uniqueness for b

( x1 = x & y1 = y & b

( x1 = x & y1 = y & b

b

:: deftheorem Def14 defines subtraction NOMIN_4:def 14 :

for x, y being object st x is Complex & y is Complex holds

for b_{3} being Complex holds

( b_{3} = subtraction (x,y) iff ex x1, y1 being Complex st

( x1 = x & y1 = y & b_{3} = x1 - y1 ) );

for x, y being object st x is Complex & y is Complex holds

for b

( b

( x1 = x & y1 = y & b

definition

let A be set ;

assume A1: A is complex-containing ;

ex b_{1} being Function of [:A,A:],A st

for x, y being object st x in A & y in A holds

b_{1} . (x,y) = subtraction (x,y)

for b_{1}, b_{2} being Function of [:A,A:],A st ( for x, y being object st x in A & y in A holds

b_{1} . (x,y) = subtraction (x,y) ) & ( for x, y being object st x in A & y in A holds

b_{2} . (x,y) = subtraction (x,y) ) holds

b_{1} = b_{2}

end;
assume A1: A is complex-containing ;

func subtraction A -> Function of [:A,A:],A means :Def15: :: NOMIN_4:def 15

for x, y being object st x in A & y in A holds

it . (x,y) = subtraction (x,y);

existence for x, y being object st x in A & y in A holds

it . (x,y) = subtraction (x,y);

ex b

for x, y being object st x in A & y in A holds

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def15 defines subtraction NOMIN_4:def 15 :

for A being set st A is complex-containing holds

for b_{2} being Function of [:A,A:],A holds

( b_{2} = subtraction A iff for x, y being object st x in A & y in A holds

b_{2} . (x,y) = subtraction (x,y) );

for A being set st A is complex-containing holds

for b

( b

b

definition

let V, A be set ;

let x, y be Element of V;

lift_binary_op ((subtraction A),x,y) is SCBinominativeFunction of V,A ;

end;
let x, y be Element of V;

func subtraction (A,x,y) -> SCBinominativeFunction of V,A equals :: NOMIN_4:def 16

lift_binary_op ((subtraction A),x,y);

coherence lift_binary_op ((subtraction A),x,y);

lift_binary_op ((subtraction A),x,y) is SCBinominativeFunction of V,A ;

:: deftheorem defines subtraction NOMIN_4:def 16 :

for V, A being set

for x, y being Element of V holds subtraction (A,x,y) = lift_binary_op ((subtraction A),x,y);

for V, A being set

for x, y being Element of V holds subtraction (A,x,y) = lift_binary_op ((subtraction A),x,y);

theorem :: NOMIN_4:15

for V, A being set

for d1 being NonatomicND of V,A

for a, b being Element of V st A is complex-containing & a in dom d1 & b in dom d1 & d1 in dom (subtraction (A,a,b)) holds

for x, y being Complex st x = d1 . a & y = d1 . b holds

(subtraction (A,a,b)) . d1 = x - y

for d1 being NonatomicND of V,A

for a, b being Element of V st A is complex-containing & a in dom d1 & b in dom d1 & d1 in dom (subtraction (A,a,b)) holds

for x, y being Complex st x = d1 . a & y = d1 . b holds

(subtraction (A,a,b)) . d1 = x - y

proof end;

definition

let V, A be set ;

let a, b be Element of V;

PP_IF ((less (A,b,a)),(SC_assignment ((subtraction (A,a,b)),a)),(PPid (ND (V,A)))) is SCBinominativeFunction of V,A ;

end;
let a, b be Element of V;

func gcd_conditional_step (V,A,a,b) -> SCBinominativeFunction of V,A equals :: NOMIN_4:def 17

PP_IF ((less (A,b,a)),(SC_assignment ((subtraction (A,a,b)),a)),(PPid (ND (V,A))));

coherence PP_IF ((less (A,b,a)),(SC_assignment ((subtraction (A,a,b)),a)),(PPid (ND (V,A))));

PP_IF ((less (A,b,a)),(SC_assignment ((subtraction (A,a,b)),a)),(PPid (ND (V,A)))) is SCBinominativeFunction of V,A ;

:: deftheorem defines gcd_conditional_step NOMIN_4:def 17 :

for V, A being set

for a, b being Element of V holds gcd_conditional_step (V,A,a,b) = PP_IF ((less (A,b,a)),(SC_assignment ((subtraction (A,a,b)),a)),(PPid (ND (V,A))));

for V, A being set

for a, b being Element of V holds gcd_conditional_step (V,A,a,b) = PP_IF ((less (A,b,a)),(SC_assignment ((subtraction (A,a,b)),a)),(PPid (ND (V,A))));

definition

let V, A be set ;

let a, b be Element of V;

PP_composition ((gcd_conditional_step (V,A,a,b)),(gcd_conditional_step (V,A,b,a))) is SCBinominativeFunction of V,A ;

end;
let a, b be Element of V;

func gcd_loop_body (V,A,a,b) -> SCBinominativeFunction of V,A equals :: NOMIN_4:def 18

PP_composition ((gcd_conditional_step (V,A,a,b)),(gcd_conditional_step (V,A,b,a)));

coherence PP_composition ((gcd_conditional_step (V,A,a,b)),(gcd_conditional_step (V,A,b,a)));

PP_composition ((gcd_conditional_step (V,A,a,b)),(gcd_conditional_step (V,A,b,a))) is SCBinominativeFunction of V,A ;

:: deftheorem defines gcd_loop_body NOMIN_4:def 18 :

for V, A being set

for a, b being Element of V holds gcd_loop_body (V,A,a,b) = PP_composition ((gcd_conditional_step (V,A,a,b)),(gcd_conditional_step (V,A,b,a)));

for V, A being set

for a, b being Element of V holds gcd_loop_body (V,A,a,b) = PP_composition ((gcd_conditional_step (V,A,a,b)),(gcd_conditional_step (V,A,b,a)));

definition

let V, A be set ;

let a, b be Element of V;

PP_while ((PP_not (Equality (A,a,b))),(gcd_loop_body (V,A,a,b))) is SCBinominativeFunction of V,A ;

end;
let a, b be Element of V;

func gcd_main_loop (V,A,a,b) -> SCBinominativeFunction of V,A equals :: NOMIN_4:def 19

PP_while ((PP_not (Equality (A,a,b))),(gcd_loop_body (V,A,a,b)));

coherence PP_while ((PP_not (Equality (A,a,b))),(gcd_loop_body (V,A,a,b)));

PP_while ((PP_not (Equality (A,a,b))),(gcd_loop_body (V,A,a,b))) is SCBinominativeFunction of V,A ;

:: deftheorem defines gcd_main_loop NOMIN_4:def 19 :

for V, A being set

for a, b being Element of V holds gcd_main_loop (V,A,a,b) = PP_while ((PP_not (Equality (A,a,b))),(gcd_loop_body (V,A,a,b)));

for V, A being set

for a, b being Element of V holds gcd_main_loop (V,A,a,b) = PP_while ((PP_not (Equality (A,a,b))),(gcd_loop_body (V,A,a,b)));

definition

let V, A be set ;

let a, b be Element of V;

let x, y be object ;

PP_composition ((SC_assignment ((denaming (V,A,x)),a)),(SC_assignment ((denaming (V,A,y)),b))) is SCBinominativeFunction of V,A ;

end;
let a, b be Element of V;

let x, y be object ;

func gcd_var_init (V,A,a,b,x,y) -> SCBinominativeFunction of V,A equals :: NOMIN_4:def 20

PP_composition ((SC_assignment ((denaming (V,A,x)),a)),(SC_assignment ((denaming (V,A,y)),b)));

coherence PP_composition ((SC_assignment ((denaming (V,A,x)),a)),(SC_assignment ((denaming (V,A,y)),b)));

PP_composition ((SC_assignment ((denaming (V,A,x)),a)),(SC_assignment ((denaming (V,A,y)),b))) is SCBinominativeFunction of V,A ;

:: deftheorem defines gcd_var_init NOMIN_4:def 20 :

for V, A being set

for a, b being Element of V

for x, y being object holds gcd_var_init (V,A,a,b,x,y) = PP_composition ((SC_assignment ((denaming (V,A,x)),a)),(SC_assignment ((denaming (V,A,y)),b)));

for V, A being set

for a, b being Element of V

for x, y being object holds gcd_var_init (V,A,a,b,x,y) = PP_composition ((SC_assignment ((denaming (V,A,x)),a)),(SC_assignment ((denaming (V,A,y)),b)));

definition

let V, A be set ;

let a, b be Element of V;

let x, y be object ;

PP_composition ((gcd_var_init (V,A,a,b,x,y)),(gcd_main_loop (V,A,a,b))) is SCBinominativeFunction of V,A ;

end;
let a, b be Element of V;

let x, y be object ;

func gcd_main_part (V,A,a,b,x,y) -> SCBinominativeFunction of V,A equals :: NOMIN_4:def 21

PP_composition ((gcd_var_init (V,A,a,b,x,y)),(gcd_main_loop (V,A,a,b)));

coherence PP_composition ((gcd_var_init (V,A,a,b,x,y)),(gcd_main_loop (V,A,a,b)));

PP_composition ((gcd_var_init (V,A,a,b,x,y)),(gcd_main_loop (V,A,a,b))) is SCBinominativeFunction of V,A ;

:: deftheorem defines gcd_main_part NOMIN_4:def 21 :

for V, A being set

for a, b being Element of V

for x, y being object holds gcd_main_part (V,A,a,b,x,y) = PP_composition ((gcd_var_init (V,A,a,b,x,y)),(gcd_main_loop (V,A,a,b)));

for V, A being set

for a, b being Element of V

for x, y being object holds gcd_main_part (V,A,a,b,x,y) = PP_composition ((gcd_var_init (V,A,a,b,x,y)),(gcd_main_loop (V,A,a,b)));

definition

let V, A be set ;

let a, b be Element of V;

let x, y be object ;

let z be Element of V;

PP_composition ((gcd_main_part (V,A,a,b,x,y)),(SC_assignment ((denaming (V,A,a)),z))) is SCBinominativeFunction of V,A ;

end;
let a, b be Element of V;

let x, y be object ;

let z be Element of V;

func gcd_program (V,A,a,b,x,y,z) -> SCBinominativeFunction of V,A equals :: NOMIN_4:def 22

PP_composition ((gcd_main_part (V,A,a,b,x,y)),(SC_assignment ((denaming (V,A,a)),z)));

coherence PP_composition ((gcd_main_part (V,A,a,b,x,y)),(SC_assignment ((denaming (V,A,a)),z)));

PP_composition ((gcd_main_part (V,A,a,b,x,y)),(SC_assignment ((denaming (V,A,a)),z))) is SCBinominativeFunction of V,A ;

:: deftheorem defines gcd_program NOMIN_4:def 22 :

for V, A being set

for a, b being Element of V

for x, y being object

for z being Element of V holds gcd_program (V,A,a,b,x,y,z) = PP_composition ((gcd_main_part (V,A,a,b,x,y)),(SC_assignment ((denaming (V,A,a)),z)));

for V, A being set

for a, b being Element of V

for x, y being object

for z being Element of V holds gcd_program (V,A,a,b,x,y,z) = PP_composition ((gcd_main_part (V,A,a,b,x,y)),(SC_assignment ((denaming (V,A,a)),z)));

definition

let V, A be set ;

let x, y be object ;

let x0, y0 be Nat;

let d be object ;

end;
let x, y be object ;

let x0, y0 be Nat;

let d be object ;

pred valid_gcd_input_pred V,A,x,y,x0,y0,d means :: NOMIN_4:def 23

ex d1 being NonatomicND of V,A st

( d = d1 & x in dom d1 & y in dom d1 & d1 . x = x0 & d1 . y = y0 );

ex d1 being NonatomicND of V,A st

( d = d1 & x in dom d1 & y in dom d1 & d1 . x = x0 & d1 . y = y0 );

:: deftheorem defines valid_gcd_input_pred NOMIN_4:def 23 :

for V, A being set

for x, y being object

for x0, y0 being Nat

for d being object holds

( valid_gcd_input_pred V,A,x,y,x0,y0,d iff ex d1 being NonatomicND of V,A st

( d = d1 & x in dom d1 & y in dom d1 & d1 . x = x0 & d1 . y = y0 ) );

for V, A being set

for x, y being object

for x0, y0 being Nat

for d being object holds

( valid_gcd_input_pred V,A,x,y,x0,y0,d iff ex d1 being NonatomicND of V,A st

( d = d1 & x in dom d1 & y in dom d1 & d1 . x = x0 & d1 . y = y0 ) );

definition

let V, A be set ;

let x, y be object ;

let x0, y0 be Nat;

ex b_{1} being SCPartialNominativePredicate of V,A st

( dom b_{1} = ND (V,A) & ( for d being object st d in dom b_{1} holds

( ( valid_gcd_input_pred V,A,x,y,x0,y0,d implies b_{1} . d = TRUE ) & ( not valid_gcd_input_pred V,A,x,y,x0,y0,d implies b_{1} . d = FALSE ) ) ) )

for b_{1}, b_{2} being SCPartialNominativePredicate of V,A st dom b_{1} = ND (V,A) & ( for d being object st d in dom b_{1} holds

( ( valid_gcd_input_pred V,A,x,y,x0,y0,d implies b_{1} . d = TRUE ) & ( not valid_gcd_input_pred V,A,x,y,x0,y0,d implies b_{1} . d = FALSE ) ) ) & dom b_{2} = ND (V,A) & ( for d being object st d in dom b_{2} holds

( ( valid_gcd_input_pred V,A,x,y,x0,y0,d implies b_{2} . d = TRUE ) & ( not valid_gcd_input_pred V,A,x,y,x0,y0,d implies b_{2} . d = FALSE ) ) ) holds

b_{1} = b_{2}

end;
let x, y be object ;

let x0, y0 be Nat;

func valid_gcd_input (V,A,x,y,x0,y0) -> SCPartialNominativePredicate of V,A means :Def24: :: NOMIN_4:def 24

( dom it = ND (V,A) & ( for d being 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 ( dom it = ND (V,A) & ( for d being 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 ) ) ) );

ex b

( dom b

( ( valid_gcd_input_pred V,A,x,y,x0,y0,d implies b

proof end;

uniqueness for b

( ( valid_gcd_input_pred V,A,x,y,x0,y0,d implies b

( ( valid_gcd_input_pred V,A,x,y,x0,y0,d implies b

b

proof end;

:: deftheorem Def24 defines valid_gcd_input NOMIN_4:def 24 :

for V, A being set

for x, y being object

for x0, y0 being Nat

for b_{7} being SCPartialNominativePredicate of V,A holds

( b_{7} = valid_gcd_input (V,A,x,y,x0,y0) iff ( dom b_{7} = ND (V,A) & ( for d being object st d in dom b_{7} holds

( ( valid_gcd_input_pred V,A,x,y,x0,y0,d implies b_{7} . d = TRUE ) & ( not valid_gcd_input_pred V,A,x,y,x0,y0,d implies b_{7} . d = FALSE ) ) ) ) );

for V, A being set

for x, y being object

for x0, y0 being Nat

for b

( b

( ( valid_gcd_input_pred V,A,x,y,x0,y0,d implies b

registration

let V, A be set ;

let x, y be object ;

let x0, y0 be Nat;

coherence

valid_gcd_input (V,A,x,y,x0,y0) is total by Def24;

end;
let x, y be object ;

let x0, y0 be Nat;

coherence

valid_gcd_input (V,A,x,y,x0,y0) is total by Def24;

definition

let V, A be set ;

let z be Element of V;

let x0, y0 be Nat;

let d be object ;

end;
let z be Element of V;

let x0, y0 be Nat;

let d be object ;

pred valid_gcd_output_pred V,A,z,x0,y0,d means :: NOMIN_4:def 25

ex d1 being NonatomicND of V,A st

( d = d1 & z in dom d1 & d1 . z = x0 gcd y0 );

ex d1 being NonatomicND of V,A st

( d = d1 & z in dom d1 & d1 . z = x0 gcd y0 );

:: deftheorem defines valid_gcd_output_pred NOMIN_4:def 25 :

for V, A being set

for z being Element of V

for x0, y0 being Nat

for d being object holds

( valid_gcd_output_pred V,A,z,x0,y0,d iff ex d1 being NonatomicND of V,A st

( d = d1 & z in dom d1 & d1 . z = x0 gcd y0 ) );

for V, A being set

for z being Element of V

for x0, y0 being Nat

for d being object holds

( valid_gcd_output_pred V,A,z,x0,y0,d iff ex d1 being NonatomicND of V,A st

( d = d1 & z in dom d1 & d1 . z = x0 gcd y0 ) );

definition

let V, A be set ;

let z be Element of V;

let x0, y0 be Nat;

set D = { d where d is TypeSCNominativeData of V,A : d in dom (denaming (V,A,z)) } ;

ex b_{1} being SCPartialNominativePredicate of V,A st

( dom b_{1} = { d where d is TypeSCNominativeData of V,A : d in dom (denaming (V,A,z)) } & ( for d being object st d in dom b_{1} holds

( ( valid_gcd_output_pred V,A,z,x0,y0,d implies b_{1} . d = TRUE ) & ( not valid_gcd_output_pred V,A,z,x0,y0,d implies b_{1} . d = FALSE ) ) ) )

for b_{1}, b_{2} being SCPartialNominativePredicate of V,A st dom b_{1} = { d where d is TypeSCNominativeData of V,A : d in dom (denaming (V,A,z)) } & ( for d being object st d in dom b_{1} holds

( ( valid_gcd_output_pred V,A,z,x0,y0,d implies b_{1} . d = TRUE ) & ( not valid_gcd_output_pred V,A,z,x0,y0,d implies b_{1} . d = FALSE ) ) ) & dom b_{2} = { d where d is TypeSCNominativeData of V,A : d in dom (denaming (V,A,z)) } & ( for d being object st d in dom b_{2} holds

( ( valid_gcd_output_pred V,A,z,x0,y0,d implies b_{2} . d = TRUE ) & ( not valid_gcd_output_pred V,A,z,x0,y0,d implies b_{2} . d = FALSE ) ) ) holds

b_{1} = b_{2}

end;
let z be Element of V;

let x0, y0 be Nat;

set D = { d where d is TypeSCNominativeData of V,A : d in dom (denaming (V,A,z)) } ;

func valid_gcd_output (V,A,z,x0,y0) -> SCPartialNominativePredicate of V,A means :Def26: :: NOMIN_4:def 26

( dom it = { d where d is TypeSCNominativeData of V,A : d in dom (denaming (V,A,z)) } & ( for d being 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 ( dom it = { d where d is TypeSCNominativeData of V,A : d in dom (denaming (V,A,z)) } & ( for d being 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 ) ) ) );

ex b

( dom b

( ( valid_gcd_output_pred V,A,z,x0,y0,d implies b

proof end;

uniqueness for b

( ( valid_gcd_output_pred V,A,z,x0,y0,d implies b

( ( valid_gcd_output_pred V,A,z,x0,y0,d implies b

b

proof end;

:: deftheorem Def26 defines valid_gcd_output NOMIN_4:def 26 :

for V, A being set

for z being Element of V

for x0, y0 being Nat

for b_{6} being SCPartialNominativePredicate of V,A holds

( b_{6} = valid_gcd_output (V,A,z,x0,y0) iff ( dom b_{6} = { d where d is TypeSCNominativeData of V,A : d in dom (denaming (V,A,z)) } & ( for d being object st d in dom b_{6} holds

( ( valid_gcd_output_pred V,A,z,x0,y0,d implies b_{6} . d = TRUE ) & ( not valid_gcd_output_pred V,A,z,x0,y0,d implies b_{6} . d = FALSE ) ) ) ) );

for V, A being set

for z being Element of V

for x0, y0 being Nat

for b

( b

( ( valid_gcd_output_pred V,A,z,x0,y0,d implies b

:: deftheorem defines gcd_inv_pred NOMIN_4:def 27 :

for V, A being set

for a, b being Element of V

for x0, y0 being Nat

for d being object holds

( gcd_inv_pred V,A,a,b,x0,y0,d iff ex d1 being NonatomicND of V,A st

( d = d1 & a in dom d1 & b in dom d1 & ex x, y being Nat st

( x = d1 . a & y = d1 . b & x gcd y = x0 gcd y0 ) ) );

for V, A being set

for a, b being Element of V

for x0, y0 being Nat

for d being object holds

( gcd_inv_pred V,A,a,b,x0,y0,d iff ex d1 being NonatomicND of V,A st

( d = d1 & a in dom d1 & b in dom d1 & ex x, y being Nat st

( x = d1 . a & y = d1 . b & x gcd y = x0 gcd y0 ) ) );

definition

let V, A be set ;

let a, b be Element of V;

let x0, y0 be Nat;

ex b_{1} being SCPartialNominativePredicate of V,A st

( dom b_{1} = ND (V,A) & ( for d being object st d in dom b_{1} holds

( ( gcd_inv_pred V,A,a,b,x0,y0,d implies b_{1} . d = TRUE ) & ( not gcd_inv_pred V,A,a,b,x0,y0,d implies b_{1} . d = FALSE ) ) ) )

for b_{1}, b_{2} being SCPartialNominativePredicate of V,A st dom b_{1} = ND (V,A) & ( for d being object st d in dom b_{1} holds

( ( gcd_inv_pred V,A,a,b,x0,y0,d implies b_{1} . d = TRUE ) & ( not gcd_inv_pred V,A,a,b,x0,y0,d implies b_{1} . d = FALSE ) ) ) & dom b_{2} = ND (V,A) & ( for d being object st d in dom b_{2} holds

( ( gcd_inv_pred V,A,a,b,x0,y0,d implies b_{2} . d = TRUE ) & ( not gcd_inv_pred V,A,a,b,x0,y0,d implies b_{2} . d = FALSE ) ) ) holds

b_{1} = b_{2}

end;
let a, b be Element of V;

let x0, y0 be Nat;

func gcd_inv (V,A,a,b,x0,y0) -> SCPartialNominativePredicate of V,A means :Def28: :: NOMIN_4:def 28

( dom it = ND (V,A) & ( for d being 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 ( dom it = ND (V,A) & ( for d being 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 ) ) ) );

ex b

( dom b

( ( gcd_inv_pred V,A,a,b,x0,y0,d implies b

proof end;

uniqueness for b

( ( gcd_inv_pred V,A,a,b,x0,y0,d implies b

( ( gcd_inv_pred V,A,a,b,x0,y0,d implies b

b

proof end;

:: deftheorem Def28 defines gcd_inv NOMIN_4:def 28 :

for V, A being set

for a, b being Element of V

for x0, y0 being Nat

for b_{7} being SCPartialNominativePredicate of V,A holds

( b_{7} = gcd_inv (V,A,a,b,x0,y0) iff ( dom b_{7} = ND (V,A) & ( for d being object st d in dom b_{7} holds

( ( gcd_inv_pred V,A,a,b,x0,y0,d implies b_{7} . d = TRUE ) & ( not gcd_inv_pred V,A,a,b,x0,y0,d implies b_{7} . d = FALSE ) ) ) ) );

for V, A being set

for a, b being Element of V

for x0, y0 being Nat

for b

( b

( ( gcd_inv_pred V,A,a,b,x0,y0,d implies b

registration

let V, A be set ;

let a, b be Element of V;

let x0, y0 be Nat;

coherence

gcd_inv (V,A,a,b,x0,y0) is total by Def28;

end;
let a, b be Element of V;

let x0, y0 be Nat;

coherence

gcd_inv (V,A,a,b,x0,y0) is total by Def28;

theorem Th15: :: NOMIN_4:16

for V, A being set

for a being Element of V

for x being object

for p being SCPartialNominativePredicate of V,A holds <*(PP_inversion (SC_Psuperpos (p,(denaming (V,A,x)),a))),(SC_assignment ((denaming (V,A,x)),a)),p*> is SFHT of (ND (V,A))

for a being Element of V

for x being object

for p being SCPartialNominativePredicate of V,A holds <*(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 end;

theorem Th16: :: NOMIN_4:17

for V, A being set

for a, b being Element of V

for x, y being object

for x0, y0 being Nat st not V is empty & A is_without_nonatomicND_wrt V & a <> b & a <> y holds

<*(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))

for a, b being Element of V

for x, y being object

for x0, y0 being Nat st not V is empty & A is_without_nonatomicND_wrt V & a <> b & a <> y holds

<*(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 end;

theorem Th17: :: NOMIN_4:18

for V, A being set

for a, b being Element of V

for x0, y0 being Nat st not V is empty & A is_without_nonatomicND_wrt V & a <> b & A is complex-containing & ( for d being TypeSCNominativeData of V,A holds a is_complex_on d ) & ( for d being TypeSCNominativeData of V,A holds b is_complex_on d ) holds

<*(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))

for a, b being Element of V

for x0, y0 being Nat st not V is empty & A is_without_nonatomicND_wrt V & a <> b & A is complex-containing & ( for d being TypeSCNominativeData of V,A holds a is_complex_on d ) & ( for d being TypeSCNominativeData of V,A holds b is_complex_on d ) holds

<*(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 end;

theorem Th18: :: NOMIN_4:19

for V, A being set

for a, b being Element of V

for x0, y0 being Nat st not V is empty & A is_without_nonatomicND_wrt V & a <> b & A is complex-containing & ( for d being TypeSCNominativeData of V,A holds a is_complex_on d ) & ( for d being TypeSCNominativeData of V,A holds b is_complex_on d ) holds

<*(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))

for a, b being Element of V

for x0, y0 being Nat st not V is empty & A is_without_nonatomicND_wrt V & a <> b & A is complex-containing & ( for d being TypeSCNominativeData of V,A holds a is_complex_on d ) & ( for d being TypeSCNominativeData of V,A holds b is_complex_on d ) holds

<*(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 end;

theorem Th19: :: NOMIN_4:20

for V, A being set

for a, b being Element of V

for x0, y0 being Nat st not V is empty & A is_without_nonatomicND_wrt V & a <> b & A is complex-containing & ( for d being TypeSCNominativeData of V,A holds a is_complex_on d ) & ( for d being TypeSCNominativeData of V,A holds b is_complex_on d ) holds

<*(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))

for a, b being Element of V

for x0, y0 being Nat st not V is empty & A is_without_nonatomicND_wrt V & a <> b & A is complex-containing & ( for d being TypeSCNominativeData of V,A holds a is_complex_on d ) & ( for d being TypeSCNominativeData of V,A holds b is_complex_on d ) holds

<*(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 end;

theorem Th20: :: NOMIN_4:21

for V, A being set

for a, b being Element of V

for x0, y0 being Nat st not V is empty & A is_without_nonatomicND_wrt V & a <> b & A is complex-containing & ( for d being TypeSCNominativeData of V,A holds a is_complex_on d ) & ( for d being TypeSCNominativeData of V,A holds b is_complex_on d ) holds

<*(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))

for a, b being Element of V

for x0, y0 being Nat st not V is empty & A is_without_nonatomicND_wrt V & a <> b & A is complex-containing & ( for d being TypeSCNominativeData of V,A holds a is_complex_on d ) & ( for d being TypeSCNominativeData of V,A holds b is_complex_on d ) holds

<*(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 end;

theorem Th21: :: NOMIN_4:22

for V, A being set

for a, b being Element of V

for x0, y0 being Nat st not V is empty & A is_without_nonatomicND_wrt V & a <> b & A is complex-containing & ( for d being TypeSCNominativeData of V,A holds a is_complex_on d ) & ( for d being TypeSCNominativeData of V,A holds b is_complex_on d ) holds

<*(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))

for a, b being Element of V

for x0, y0 being Nat st not V is empty & A is_without_nonatomicND_wrt V & a <> b & A is complex-containing & ( for d being TypeSCNominativeData of V,A holds a is_complex_on d ) & ( for d being TypeSCNominativeData of V,A holds b is_complex_on d ) holds

<*(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 end;

theorem Th22: :: NOMIN_4:23

for V, A being set

for a, b being Element of V

for x0, y0 being Nat st not V is empty & A is_without_nonatomicND_wrt V & a <> b & A is complex-containing & ( for d being TypeSCNominativeData of V,A holds a is_complex_on d ) & ( for d being TypeSCNominativeData of V,A holds b is_complex_on d ) holds

<*(PP_inversion (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))

for a, b being Element of V

for x0, y0 being Nat st not V is empty & A is_without_nonatomicND_wrt V & a <> b & A is complex-containing & ( for d being TypeSCNominativeData of V,A holds a is_complex_on d ) & ( for d being TypeSCNominativeData of V,A holds b is_complex_on d ) holds

<*(PP_inversion (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 end;

theorem Th23: :: NOMIN_4:24

for V, A being set

for a, b being Element of V

for x0, y0 being Nat st not V is empty & A is_without_nonatomicND_wrt V & a <> b & A is complex-containing & ( for d being TypeSCNominativeData of V,A holds a is_complex_on d ) & ( for d being TypeSCNominativeData of V,A holds b is_complex_on d ) holds

<*(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))

for a, b being Element of V

for x0, y0 being Nat st not V is empty & A is_without_nonatomicND_wrt V & a <> b & A is complex-containing & ( for d being TypeSCNominativeData of V,A holds a is_complex_on d ) & ( for d being TypeSCNominativeData of V,A holds b is_complex_on d ) holds

<*(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 end;

theorem Th24: :: NOMIN_4:25

for V, A being set

for a, b being Element of V

for x, y being object

for x0, y0 being Nat st not V is empty & A is_without_nonatomicND_wrt V & a <> b & a <> y & A is complex-containing & ( for d being TypeSCNominativeData of V,A holds a is_complex_on d ) & ( for d being TypeSCNominativeData of V,A holds b is_complex_on d ) holds

<*(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))

for a, b being Element of V

for x, y being object

for x0, y0 being Nat st not V is empty & A is_without_nonatomicND_wrt V & a <> b & a <> y & A is complex-containing & ( for d being TypeSCNominativeData of V,A holds a is_complex_on d ) & ( for d being TypeSCNominativeData of V,A holds b is_complex_on d ) holds

<*(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 end;

theorem Th25: :: NOMIN_4:26

for V, A being set

for a, b, z being Element of V

for x0, y0 being Nat st not V is empty & A is_without_nonatomicND_wrt V & ( for d being TypeSCNominativeData of V,A holds a is_a_value_on d ) & ( for d being TypeSCNominativeData of V,A holds b is_a_value_on d ) holds

<*(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))

for a, b, z being Element of V

for x0, y0 being Nat st not V is empty & A is_without_nonatomicND_wrt V & ( for d being TypeSCNominativeData of V,A holds a is_a_value_on d ) & ( for d being TypeSCNominativeData of V,A holds b is_a_value_on d ) holds

<*(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 end;

theorem Th26: :: NOMIN_4:27

for V, A being set

for a, b, z being Element of V

for x0, y0 being Nat st A is complex-containing & ( for d being TypeSCNominativeData of V,A holds a is_complex_on d ) & ( for d being TypeSCNominativeData of V,A holds b is_complex_on d ) holds

<*(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))

for a, b, z being Element of V

for x0, y0 being Nat st A is complex-containing & ( for d being TypeSCNominativeData of V,A holds a is_complex_on d ) & ( for d being TypeSCNominativeData of V,A holds b is_complex_on d ) holds

<*(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 end;

theorem :: NOMIN_4:28

for V, A being set

for a, b, z being Element of V

for x, y being object

for x0, y0 being Nat st not V is empty & A is_without_nonatomicND_wrt V & a <> b & a <> y & A is complex-containing & ( for d being TypeSCNominativeData of V,A holds a is_complex_on d ) & ( for d being TypeSCNominativeData of V,A holds b is_complex_on d ) holds

<*(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))

for a, b, z being Element of V

for x, y being object

for x0, y0 being Nat st not V is empty & A is_without_nonatomicND_wrt V & a <> b & a <> y & A is complex-containing & ( for d being TypeSCNominativeData of V,A holds a is_complex_on d ) & ( for d being TypeSCNominativeData of V,A holds b is_complex_on d ) holds

<*(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 end;

:: Atomic data are assumed to be natural numbers

:: Basic operations and relations on atomic data include difference operation (subtraction) and comparisons (less, Equality)

:: Pseudo code of the algorithm

:: Input: nonnegative integers x and y

:: Output: nonnegative integer z = gcd(x,y)

:: a := x;

:: b := y;

:: while not (a=b) do

:: if b<a then a := a-b;

:: if a<b then b := b-a;

:: end;

:: z := a;