:: Partial correctness of GCD algorithm
:: by Ievgen Ivanov , Artur Korni{\l}owicz and Mykola Nikitchenko
::
:: Copyright (c) 2018-2021 Association of Mizar Users

definition
let A be set ;
end;

:: deftheorem defines complex-containing NOMIN_4:def 1 :
for A being set holds
( A is complex-containing iff COMPLEX c= A );

registration
existence
ex b1 being set st b1 is complex-containing
proof end;
cluster complex-containing -> non empty for set ;
coherence
for b1 being set st b1 is complex-containing holds
not b1 is empty
by XBOOLE_1:3;
end;

scheme :: NOMIN_4:sch 1
BinPredToFunEx{ F1() -> set , F2() -> set , P1[ object , object ] } :
ex f being Function of [:F1(),F2():],BOOLEAN st
for x, y being object st x in F1() & y in F2() holds
( ( P1[x,y] implies f . (x,y) = TRUE ) & ( P1[x,y] implies f . (x,y) = FALSE ) )
proof end;

scheme :: NOMIN_4:sch 2
BinPredToFunUnique{ F1() -> set , F2() -> set , P1[ object , object ] } :
for f, g being Function of [:F1(),F2():],BOOLEAN st ( for x, y being object st x in F1() & y in F2() holds
( ( P1[x,y] implies f . (x,y) = TRUE ) & ( P1[x,y] implies f . (x,y) = FALSE ) ) ) & ( for x, y being object st x in F1() & y in F2() holds
( ( P1[x,y] implies g . (x,y) = TRUE ) & ( P1[x,y] implies g . (x,y) = FALSE ) ) ) holds
f = g
proof end;

scheme :: NOMIN_4:sch 3
Lambda2Unique{ F1() -> set , F2() -> set , F3() -> set , F4( object , object ) -> object } :
for f, g being Function of [:F1(),F2():],F3() st ( for x, y being object st x in F1() & y in F2() holds
f . (x,y) = F4(x,y) ) & ( for x, y being object st x in F1() & y in F2() holds
g . (x,y) = F4(x,y) ) holds
f = g
proof end;

definition
let V, A be set ;
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 } is set
;
end;

:: 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 } ;

theorem Th1: :: NOMIN_4:1
for V, A being set
for d being object st d in nonatomicsND (V,A) holds
d is NonatomicND of V,A
proof end;

theorem Th2: :: NOMIN_4:2
for V, A being set holds {} in nonatomicsND (V,A)
proof end;

registration
let V, A be set ;
cluster nonatomicsND (V,A) -> non empty functional ;
coherence
( not nonatomicsND (V,A) is empty & nonatomicsND (V,A) is functional )
proof end;
end;

definition
let V, A be set ;
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) );

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
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)
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}
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))
proof end;

definition
let V, A be set ;
let d be TypeSCNominativeData of V,A;
let a be Element of V;
pred a is_ext_real_on d means :: NOMIN_4:def 4
(denaming (V,A,a)) . d is ext-real ;
pred a is_complex_on d means :: NOMIN_4:def 5
(denaming (V,A,a)) . d is complex ;
pred a is_a_value_on d means :: NOMIN_4:def 6
(denaming (V,A,a)) . d in A;
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 );

:: 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 );

:: 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 );

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
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
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:]
proof end;

definition
let V, A be set ;
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)):> is SCPartialNominativePredicate of V,A
proof end;
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)):>;

definition
let V, A be set ;
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)):> is SCBinominativeFunction of V,A
proof end;
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)):>;

definition
let A be set ;
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
ex b1 being Function of [:A,A:],BOOLEAN st
for a, b being object st a in A & b in A holds
( ( a = b implies b1 . (a,b) = TRUE ) & ( a <> b implies b1 . (a,b) = FALSE ) )
proof end;
uniqueness
for b1, b2 being Function of [:A,A:],BOOLEAN st ( for a, b being object st a in A & b in A holds
( ( a = b implies b1 . (a,b) = TRUE ) & ( a <> b implies b1 . (a,b) = FALSE ) ) ) & ( for a, b being object st a in A & b in A holds
( ( a = b implies b2 . (a,b) = TRUE ) & ( a <> b implies b2 . (a,b) = FALSE ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def9 defines Equality NOMIN_4:def 9 :
for A being set
for b2 being Function of [:A,A:],BOOLEAN holds
( b2 = Equality A iff for a, b being object st a in A & b in A holds
( ( a = b implies b2 . (a,b) = TRUE ) & ( a <> b implies b2 . (a,b) = FALSE ) ) );

definition
let V, A be set ;
let x, y be Element of V;
func Equality (A,x,y) -> SCPartialNominativePredicate of V,A equals :: NOMIN_4:def 10
lift_binary_pred ((),x,y);
coherence
lift_binary_pred ((),x,y) is SCPartialNominativePredicate of V,A
;
end;

:: 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 ((),x,y);

definition
let x, y be object ;
pred x less_pred y means :: NOMIN_4:def 11
ex x1, y1 being ExtReal st
( x1 = x & y1 = y & x1 < y1 );
irreflexivity
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;

:: 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 ) );

theorem Th10: :: NOMIN_4:10
for x, y being ExtReal holds
( x less_pred y or y less_pred x or x = y )
proof end;

definition
let A be set ;
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
ex b1 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 b1 . (x,y) = TRUE ) & ( not x less_pred y implies b1 . (x,y) = FALSE ) )
proof end;
uniqueness
for b1, b2 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 b1 . (x,y) = TRUE ) & ( not x less_pred y implies b1 . (x,y) = FALSE ) ) ) & ( for x, y being object st x in A & y in A holds
( ( x less_pred y implies b2 . (x,y) = TRUE ) & ( not x less_pred y implies b2 . (x,y) = FALSE ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def12 defines less NOMIN_4:def 12 :
for A being set
for b2 being Function of [:A,A:],BOOLEAN holds
( b2 = less A iff for x, y being object st x in A & y in A holds
( ( x less_pred y implies b2 . (x,y) = TRUE ) & ( not x less_pred y implies b2 . (x,y) = FALSE ) ) );

definition
let V, A be set ;
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) is SCPartialNominativePredicate of V,A
;
end;

:: 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);

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)))
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)))
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)))
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 )
proof end;

definition
let x, y be object ;
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 b1, x1, y1 being Complex st
( x1 = x & y1 = y & b1 = x1 - y1 )
proof end;
uniqueness
for b1, b2 being Complex st ex x1, y1 being Complex st
( x1 = x & y1 = y & b1 = x1 - y1 ) & ex x1, y1 being Complex st
( x1 = x & y1 = y & b2 = x1 - y1 ) holds
b1 = b2
;
end;

:: deftheorem Def14 defines subtraction NOMIN_4:def 14 :
for x, y being object st x is Complex & y is Complex holds
for b3 being Complex holds
( b3 = subtraction (x,y) iff ex x1, y1 being Complex st
( x1 = x & y1 = y & b3 = x1 - y1 ) );

definition
let A be set ;
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
ex b1 being Function of [:A,A:],A st
for x, y being object st x in A & y in A holds
b1 . (x,y) = subtraction (x,y)
proof end;
uniqueness
for b1, b2 being Function of [:A,A:],A st ( for x, y being object st x in A & y in A holds
b1 . (x,y) = subtraction (x,y) ) & ( for x, y being object st x in A & y in A holds
b2 . (x,y) = subtraction (x,y) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def15 defines subtraction NOMIN_4:def 15 :
for A being set st A is complex-containing holds
for b2 being Function of [:A,A:],A holds
( b2 = subtraction A iff for x, y being object st x in A & y in A holds
b2 . (x,y) = subtraction (x,y) );

definition
let V, A be set ;
let x, y be Element of V;
func subtraction (A,x,y) -> SCBinominativeFunction of V,A equals :: NOMIN_4:def 16
lift_binary_op ((),x,y);
coherence
lift_binary_op ((),x,y) is SCBinominativeFunction of V,A
;
end;

:: 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 ((),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
proof end;

:: Definition of a program over type SC nominative data which implements the GCD computation algorithm
:: 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;
definition
let V, A be set ;
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)))) is SCBinominativeFunction of V,A
;
end;

:: 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))));

definition
let V, A be set ;
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))) is SCBinominativeFunction of V,A
;
end;

:: 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)));

definition
let V, A be set ;
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))) is SCBinominativeFunction of V,A
;
end;

:: 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)));

definition
let V, A be set ;
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))) is SCBinominativeFunction of V,A
;
end;

:: 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)));

definition
let V, A be set ;
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))) is SCBinominativeFunction of V,A
;
end;

:: 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)));

definition
let V, A be set ;
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))) is SCBinominativeFunction of V,A
;
end;

:: 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)));

definition
let V, A be set ;
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 );
end;

:: 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 ) );

definition
let V, A be set ;
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
ex b1 being SCPartialNominativePredicate of V,A st
( dom b1 = ND (V,A) & ( for d being object st d in dom b1 holds
( ( valid_gcd_input_pred V,A,x,y,x0,y0,d implies b1 . d = TRUE ) & ( not valid_gcd_input_pred V,A,x,y,x0,y0,d implies b1 . d = FALSE ) ) ) )
proof end;
uniqueness
for b1, b2 being SCPartialNominativePredicate of V,A st dom b1 = ND (V,A) & ( for d being object st d in dom b1 holds
( ( valid_gcd_input_pred V,A,x,y,x0,y0,d implies b1 . d = TRUE ) & ( not valid_gcd_input_pred V,A,x,y,x0,y0,d implies b1 . d = FALSE ) ) ) & dom b2 = ND (V,A) & ( for d being object st d in dom b2 holds
( ( valid_gcd_input_pred V,A,x,y,x0,y0,d implies b2 . d = TRUE ) & ( not valid_gcd_input_pred V,A,x,y,x0,y0,d implies b2 . d = FALSE ) ) ) holds
b1 = b2
proof end;
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 b7 being SCPartialNominativePredicate of V,A holds
( b7 = valid_gcd_input (V,A,x,y,x0,y0) iff ( dom b7 = ND (V,A) & ( for d being object st d in dom b7 holds
( ( valid_gcd_input_pred V,A,x,y,x0,y0,d implies b7 . d = TRUE ) & ( not valid_gcd_input_pred V,A,x,y,x0,y0,d implies b7 . d = FALSE ) ) ) ) );

registration
let V, A be set ;
let x, y be object ;
let x0, y0 be Nat;
cluster valid_gcd_input (V,A,x,y,x0,y0) -> total ;
coherence
valid_gcd_input (V,A,x,y,x0,y0) is total
by Def24;
end;

definition
let V, A be set ;
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 );
end;

:: 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 ) );

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)) } ;
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
ex b1 being SCPartialNominativePredicate of V,A st
( dom b1 = { d where d is TypeSCNominativeData of V,A : d in dom (denaming (V,A,z)) } & ( for d being object st d in dom b1 holds
( ( valid_gcd_output_pred V,A,z,x0,y0,d implies b1 . d = TRUE ) & ( not valid_gcd_output_pred V,A,z,x0,y0,d implies b1 . d = FALSE ) ) ) )
proof end;
uniqueness
for b1, b2 being SCPartialNominativePredicate of V,A st dom b1 = { d where d is TypeSCNominativeData of V,A : d in dom (denaming (V,A,z)) } & ( for d being object st d in dom b1 holds
( ( valid_gcd_output_pred V,A,z,x0,y0,d implies b1 . d = TRUE ) & ( not valid_gcd_output_pred V,A,z,x0,y0,d implies b1 . d = FALSE ) ) ) & dom b2 = { d where d is TypeSCNominativeData of V,A : d in dom (denaming (V,A,z)) } & ( for d being object st d in dom b2 holds
( ( valid_gcd_output_pred V,A,z,x0,y0,d implies b2 . d = TRUE ) & ( not valid_gcd_output_pred V,A,z,x0,y0,d implies b2 . d = FALSE ) ) ) holds
b1 = b2
proof end;
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 b6 being SCPartialNominativePredicate of V,A holds
( b6 = valid_gcd_output (V,A,z,x0,y0) iff ( dom b6 = { d where d is TypeSCNominativeData of V,A : d in dom (denaming (V,A,z)) } & ( for d being object st d in dom b6 holds
( ( valid_gcd_output_pred V,A,z,x0,y0,d implies b6 . d = TRUE ) & ( not valid_gcd_output_pred V,A,z,x0,y0,d implies b6 . d = FALSE ) ) ) ) );

definition
let V, A be set ;
let a, b be Element of V;
let x0, y0 be Nat;
let d be object ;
pred gcd_inv_pred V,A,a,b,x0,y0,d means :: NOMIN_4:def 27
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 ) );
end;

:: 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 ) ) );

definition
let V, A be set ;
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
ex b1 being SCPartialNominativePredicate of V,A st
( dom b1 = ND (V,A) & ( for d being object st d in dom b1 holds
( ( gcd_inv_pred V,A,a,b,x0,y0,d implies b1 . d = TRUE ) & ( not gcd_inv_pred V,A,a,b,x0,y0,d implies b1 . d = FALSE ) ) ) )
proof end;
uniqueness
for b1, b2 being SCPartialNominativePredicate of V,A st dom b1 = ND (V,A) & ( for d being object st d in dom b1 holds
( ( gcd_inv_pred V,A,a,b,x0,y0,d implies b1 . d = TRUE ) & ( not gcd_inv_pred V,A,a,b,x0,y0,d implies b1 . d = FALSE ) ) ) & dom b2 = ND (V,A) & ( for d being object st d in dom b2 holds
( ( gcd_inv_pred V,A,a,b,x0,y0,d implies b2 . d = TRUE ) & ( not gcd_inv_pred V,A,a,b,x0,y0,d implies b2 . d = FALSE ) ) ) holds
b1 = b2
proof end;
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 b7 being SCPartialNominativePredicate of V,A holds
( b7 = gcd_inv (V,A,a,b,x0,y0) iff ( dom b7 = ND (V,A) & ( for d being object st d in dom b7 holds
( ( gcd_inv_pred V,A,a,b,x0,y0,d implies b7 . d = TRUE ) & ( not gcd_inv_pred V,A,a,b,x0,y0,d implies b7 . d = FALSE ) ) ) ) );

registration
let V, A be set ;
let a, b be Element of V;
let x0, y0 be Nat;
cluster gcd_inv (V,A,a,b,x0,y0) -> total ;
coherence
gcd_inv (V,A,a,b,x0,y0) is total
by Def28;
end;

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))
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))
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))
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))
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))
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))
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))
proof end;

theorem :: NOMIN_4:23
canceled;

::\$CT
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))
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))
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))
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))
proof end;

:: Partial correctness of GCD algorithm
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))
proof end;