NOMIN_4: Partial correctness of GCD algorithm

proof end;

cluster complex-containing -> non empty for set ;

coherence by XBOOLE_1:3;

end;

scheme :: NOMIN_4:sch 1
BinPredToFunEx{ F₁() -> set , F₂() -> set , P₁[ object , object ] } :

ex f being Function of [:F₁(),F₂():],BOOLEAN st
for x, y being object st x in F₁() & y in F₂() holds
( ( P₁[x,y] implies f . (x,y) = TRUE ) & ( P₁[x,y] implies f . (x,y) = FALSE ) )

proof end;

scheme :: NOMIN_4:sch 2
BinPredToFunUnique{ F₁() -> set , F₂() -> set , P₁[ object , object ] } :

for f, g being Function of [:F₁(),F₂():],BOOLEAN st ( for x, y being object st x in F₁() & y in F₂() holds
( ( P₁[x,y] implies f . (x,y) = TRUE ) & ( P₁[x,y] implies f . (x,y) = FALSE ) ) ) & ( for x, y being object st x in F₁() & y in F₂() holds
( ( P₁[x,y] implies g . (x,y) = TRUE ) & ( P₁[x,y] implies g . (x,y) = FALSE ) ) ) holds
f = g

proof end;

scheme :: NOMIN_4:sch 3
Lambda2Unique{ F₁() -> set , F₂() -> set , F₃() -> set , F₄( object , object ) -> object } :

for f, g being Function of [:F₁(),F₂():],F₃() st ( for x, y being object st x in F₁() & y in F₂() holds
f . (x,y) = F₄(x,y) ) & ( for x, y being object st x in F₁() & y in F₂() holds
g . (x,y) = F₄(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 } ;

end;

:: deftheorem defines nonatomicsND NOMIN_4:def 2 :

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

proof end;

end;

definition

let V, A be set ;

pred A is_without_nonatomicND_wrt V means :: NOMIN_4:def 3
A misses nonatomicsND (V,A);

end;

:: deftheorem defines is_without_nonatomicND_wrt NOMIN_4:def 3 :

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 :

:: deftheorem defines is_complex_on NOMIN_4:def 5 :

:: deftheorem defines is_a_value_on NOMIN_4:def 6 :

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

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

proof end;

end;

:: deftheorem defines lift_binary_pred NOMIN_4:def 7 :

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

proof end;

end;

:: deftheorem defines lift_binary_op NOMIN_4:def 8 :

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

proof end;

proof end;

end;

:: deftheorem Def9 defines Equality NOMIN_4:def 9 :

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

end;

:: deftheorem defines Equality NOMIN_4:def 10 :

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 ;
asymmetry ;

end;

:: deftheorem defines less_pred NOMIN_4:def 11 :

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

proof end;

proof end;

end;

:: deftheorem Def12 defines less NOMIN_4:def 12 :

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

end;

:: deftheorem defines less NOMIN_4:def 13 :

theorem Th11: :: NOMIN_4:11

proof end;

theorem Th12: :: NOMIN_4:12

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

proof end;

uniqueness ;

end;

:: deftheorem Def14 defines subtraction NOMIN_4:def 14 :

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

proof end;

proof end;

end;

:: deftheorem Def15 defines subtraction NOMIN_4:def 15 :

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

end;

:: deftheorem defines subtraction NOMIN_4:def 16 :

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

end;

:: deftheorem defines gcd_conditional_step NOMIN_4:def 17 :

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

end;

:: deftheorem defines gcd_loop_body NOMIN_4:def 18 :

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

end;

:: deftheorem defines gcd_main_loop NOMIN_4:def 19 :

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

end;

:: deftheorem defines gcd_var_init NOMIN_4:def 20 :

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

end;

:: deftheorem defines gcd_main_part NOMIN_4:def 21 :

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

end;

:: deftheorem defines gcd_program NOMIN_4:def 22 :

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 :

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

proof end;

proof end;

end;

:: deftheorem Def24 defines valid_gcd_input NOMIN_4:def 24 :

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

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

proof end;

proof end;

end;

:: deftheorem Def26 defines valid_gcd_output NOMIN_4:def 26 :

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 :

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

proof end;