:: Partial correctness of GCD algorithm
:: by Ievgen Ivanov , Artur Korni{\l}owicz and Mykola Nikitchenko
::
:: Received June 29, 2018
:: Copyright (c) 2018-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NOMIN_1, NUMBERS, SUBSET_1, XBOOLE_0, RELAT_1, FUNCT_1, FINSEQ_1,
XXREAL_0, NAT_1, ARYTM_3, PARTFUN1, MARGREL1, XBOOLEAN, TARSKI, FUNCOP_1,
ZFMISC_1, ARYTM_1, NOMIN_3, NOMIN_4, XCMPLX_0, INT_2, NOMIN_2, ORDERS_5,
PARTPR_1, COMPLEX1, PARTPR_2;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, MARGREL1,
RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, FINSEQ_1, FUNCOP_1,
BINOP_1, XXREAL_0, XCMPLX_0, FUNCT_3, INT_2, NOMIN_1, PARTPR_1, PARTPR_2,
NOMIN_2, NOMIN_3;
constructors RELSET_1, NOMIN_3, INT_2, NOMIN_2;
registrations XBOOLE_0, RELAT_1, FUNCT_1, ORDINAL1, FUNCOP_1, RELSET_1, INT_1,
NOMIN_3, NOMIN_1, MARGREL1, XCMPLX_0, NEWTON02, NUMBERS, NOMIN_2;
requirements NUMERALS, BOOLE, SUBSET, ARITHM;
definitions TARSKI, XBOOLE_0, FUNCT_1, NOMIN_3;
equalities XBOOLEAN, NOMIN_1, NOMIN_2, FUNCOP_1, BINOP_1, PARTPR_1, PARTPR_2;
expansions NOMIN_1, NOMIN_3, PARTFUN1;
theorems TARSKI, RELAT_1, RELSET_1, BINOP_1, PARTFUN1, FUNCT_1, FUNCT_2,
XXREAL_0, INT_1, NOMIN_1, NOMIN_3, FUNCT_3, XBOOLE_1, XCMPLX_0, ZFMISC_1,
NOMIN_2, XBOOLE_0, GRFUNC_1, NEWTON02, PARTPR_1, PARTPR_2;
schemes BINOP_1, PARTPR_2;
begin
reserve v for object;
reserve V,A for set;
reserve f for SCBinominativeFunction of V,A;
definition
let A;
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
BinPredToFunEx{ X, Y() -> set, P[object,object] }:
ex f being Function of [:X(),Y():],BOOLEAN st
for x,y being 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)
proof
defpred Q[object,object,object] means
(P[$1,$2] & $3 = TRUE) or (not P[$1,$2] & $3 = FALSE);
A1: for x,y being object st x in X() & y in Y()
ex z being 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 being Function of [:X(),Y():],BOOLEAN such that
A4: for x, y being 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
BinPredToFunUnique{ X, Y() -> set, P[object,object] }:
for f,g being Function of [:X(),Y():],BOOLEAN st
(for x,y being 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 being 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
proof
let f,g be Function of [:X(),Y():],BOOLEAN such that
A1: (for x,y being 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 being 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 being 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
Lambda2Unique{X, Y, Z() -> set, F(object,object)->object}:
for f,g being Function of [:X(),Y():],Z() st
(for x,y being object st x in X() & y in Y() holds f.(x,y) = F(x,y)) &
(for x,y being object st x in X() & y in Y() holds g.(x,y) = F(x,y))
holds f = g
proof
let f,g be Function of [:X(),Y():],Z() such that
A1: for x,y being object st x in X() & y in Y() holds f.(x,y) = F(x,y) and
A2: for x,y being object st x in X() & y in Y() holds g.(x,y) = F(x,y);
for a,b being 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;
func nonatomicsND(V,A) -> set equals
the set of all d where d is NonatomicND of V,A;
coherence;
end;
theorem Th1:
for d being 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 being NonatomicND of V,A st d = d1;
hence thesis;
end;
theorem 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;
pred A is_without_nonatomicND_wrt V means
A misses nonatomicsND(V,A);
end;
theorem Th3:
A is_without_nonatomicND_wrt V implies
for d being 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 Th4:
A is_without_nonatomicND_wrt V & v in V implies
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
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
A is_without_nonatomicND_wrt V implies
for d being 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 Th6:
for d1 being 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 being 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 is 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;
pred a is_ext_real_on d means
denaming(V,A,a).d is ext-real;
pred a is_complex_on d means
denaming(V,A,a).d is complex;
pred a is_a_value_on d means
denaming(V,A,a).d in A;
end;
theorem 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 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 being object such that
A2: x in dom f and
A3: f.x = y by FUNCT_1:def 3;
dom f = {d where d is NonatomicND of V,A: a in dom d} by NOMIN_1:def 18;
then consider d being 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 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;
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 being 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;
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 being 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 being 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;
func Equality(A) -> Function of [:A,A:],BOOLEAN means :Def9:
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
proof
defpred P[object,object] means $1 = $2;
consider f being Function of [:A,A:],BOOLEAN such that
A1: for x, y being 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 being Function of [:A,A:],BOOLEAN st
(for x,y being 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 being 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;
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;
pred x less_pred y means
ex x1,y1 being ExtReal st x1 = x & y1 = y & x1 < y1;
irreflexivity;
asymmetry;
end;
theorem Th10:
for x,y being 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;
func less(A) -> Function of [:A,A:],BOOLEAN means :Def12:
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
proof
defpred P[object,object] means $1 less_pred $2;
consider f being Function of [:A,A:],BOOLEAN such that
A1: for x, y being 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 being Function of [:A,A:],BOOLEAN st
(for x,y being 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 being 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;
func less(A,x,y) -> SCPartialNominativePredicate of V,A equals
lift_binary_pred(less(A),x,y);
coherence;
end;
theorem 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 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
(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 is 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 is 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 being 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 being 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 being 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
(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;
func subtraction(x,y) -> Complex means :Def14:
ex x1,y1 being 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;
func subtraction(A) -> Function of [:A,A:],A means :Def15:
for x,y being 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 being 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 being Function of [:A,A:],A such that
A3: for x, y being 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 being Function of [:A,A:],A st
(for x,y being object st x in A & y in A holds f.(x,y) = F(x,y)) &
(for x,y being 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;
func subtraction(A,x,y) -> SCBinominativeFunction of V,A equals
lift_binary_op(subtraction(A),x,y);
coherence;
end;
theorem
A is complex-containing & a in dom d1 & b in dom d1 &
d1 in dom subtraction(A,a,b) implies
for x,y being 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 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,a,b;
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;
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;
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;
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;
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;
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;
pred valid_gcd_input_pred V,A,x,y,x0,y0,d means
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;
definition
let V,A,x,y,x0,y0;
func valid_gcd_input(V,A,x,y,x0,y0) -> SCPartialNominativePredicate of V,A
means :Def24:
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
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 being SCPartialNominativePredicate of V,A such that
A2: dom p = ND(V,A) & (for d being 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 being SCPartialNominativePredicate of V,A st
(dom p = ND(V,A) & (for d being 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 being 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;
pred valid_gcd_output_pred V,A,z,x0,y0,d means
ex d1 being 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 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:
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
proof
A1: D c= ND(V,A)
proof
let v;
assume v in D;
then ex d being 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 being SCPartialNominativePredicate of V,A such that
A2: dom p = D & (for d being 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 being SCPartialNominativePredicate of V,A st
(dom p = D & (for d being 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 being 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;
pred gcd_inv_pred V,A,a,b,x0,y0,d means
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;
definition
let V,A,a,b,x0,y0;
func gcd_inv(V,A,a,b,x0,y0) -> SCPartialNominativePredicate of V,A means
:Def28:
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
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 being SCPartialNominativePredicate of V,A such that
A2: dom p = ND(V,A) & (for d being 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 being SCPartialNominativePredicate of V,A st
(dom p = ND(V,A) & (for d being 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 being 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 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 is Element of ND(V,A): not d in dom P}
by PARTPR_2:def 17;
then
A4: ex d1 being 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 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 is 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 is 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 is NonatomicND of V,A: x in dom d} by NOMIN_1:def 18;
A15: dom P = {d where d is 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 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 is 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 is NonatomicND of V,A: a in dom d} by NOMIN_1:def 18;
A15: dom Db = {d where d is 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 being 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 being 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 being NonatomicND of V,A such that
A29: d = d1 and
a in dom d1 and
b in dom d1 and
A30: ex x,y being Nat st x = d1.a & y = d1.b & x gcd y = x0 gcd y0;
consider x,y being 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 being 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 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 is 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 is NonatomicND of V,A: a in dom d} by NOMIN_1:def 18;
A15: dom Db = {d where d is 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 being 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 being 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 being NonatomicND of V,A such that
A29: d = d1 and
a in dom d1 and
b in dom d1 and
A30: ex x,y being Nat st x = d1.a & y = d1.b & x gcd y = x0 gcd y0;
consider x,y being 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 being 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 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,15;
hence thesis by A6,NOMIN_3:21;
end;
theorem 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,15;
hence thesis by A6,NOMIN_3:21;
end;
theorem 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;
::$CT
theorem 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,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,15;
hence thesis by A2,NOMIN_3:26;
end;
theorem 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 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 is 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 being 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 is 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 being NonatomicND of V,A such that
A9: d = D and a in dom D by A8,A7;
A10: dom r = {d where d is 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 being TypeSCNominativeData of V,A st Da.d = d1;
hence thesis;
end;
A12: local_overlapping(V,A,d,Da.d,z) in dom Dz ::lemma
proof
ex d2 being 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 is 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 being NonatomicND of V,A such that
A16: d = d2 & a in dom d2 &
b in dom d2 & ex x,y being Nat st x = d2.a & y = d2.b &
x gcd y = x0 gcd y0;
consider X,Y being 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 is NonatomicND of V,A: z in dom d}
by A9,A12,NOMIN_1:def 18;
then ex dd1 being 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 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 is 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 is Element of ND(V,A): not d in dom q}
by PARTPR_2:def 17;
then consider d1 being 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 is 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;
::$N Partial correctness of GCD algorithm
theorem
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;