let V, A be 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))
let a, b, z be 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))
let x0, y0 be Nat; ( 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 ) 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)) )
assume that
A1:
not V is empty
and
A2:
A is_without_nonatomicND_wrt V
and
A3:
( ( 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 ) )
; <*(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))
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 ((denaming (V,A,a)),z);
set E = Equality A;
set sp = SC_Psuperpos ((valid_gcd_output (V,A,z,x0,y0)),(denaming (V,A,a)),z);
A4:
<*(SC_Psuperpos ((valid_gcd_output (V,A,z,x0,y0)),(denaming (V,A,a)),z)),(SC_assignment ((denaming (V,A,a)),z)),(valid_gcd_output (V,A,z,x0,y0))*> is SFHT of (ND (V,A))
by NOMIN_3:29;
PP_and ((Equality (A,a,b)),(gcd_inv (V,A,a,b,x0,y0))) ||= SC_Psuperpos ((valid_gcd_output (V,A,z,x0,y0)),(denaming (V,A,a)),z)
proof
let d be
Element of
ND (
V,
A);
NOMIN_3:def 3 ( not d in dom (PP_and ((Equality (A,a,b)),(gcd_inv (V,A,a,b,x0,y0)))) or not (PP_and ((Equality (A,a,b)),(gcd_inv (V,A,a,b,x0,y0)))) . d = TRUE or ( d in dom (SC_Psuperpos ((valid_gcd_output (V,A,z,x0,y0)),(denaming (V,A,a)),z)) & (SC_Psuperpos ((valid_gcd_output (V,A,z,x0,y0)),(denaming (V,A,a)),z)) . d = TRUE ) )
assume A5:
(
d in dom (PP_and ((Equality (A,a,b)),(gcd_inv (V,A,a,b,x0,y0)))) &
(PP_and ((Equality (A,a,b)),(gcd_inv (V,A,a,b,x0,y0)))) . d = TRUE )
;
( d in dom (SC_Psuperpos ((valid_gcd_output (V,A,z,x0,y0)),(denaming (V,A,a)),z)) & (SC_Psuperpos ((valid_gcd_output (V,A,z,x0,y0)),(denaming (V,A,a)),z)) . 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 { 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 ) ) }
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 (denaming (V,A,a)) = { d where d is NonatomicND of V,A : a in dom d }
by NOMIN_1:def 18;
A8:
d in dom (denaming (V,A,a))
proof
dom (Equality (A,a,b)) = (dom (denaming (V,A,a))) /\ (dom (denaming (V,A,b)))
by Th11, A3;
hence
d in dom (denaming (V,A,a))
by A5, A6, PARTPR_1:19, XBOOLE_0:def 4;
verum
end;
consider D being
NonatomicND of
V,
A such that A9:
d = D
and
a in dom D
by A8, A7;
A10:
dom (valid_gcd_output (V,A,z,x0,y0)) = { d where d is TypeSCNominativeData of V,A : d in dom (denaming (V,A,z)) }
by Def26;
A11:
(denaming (V,A,a)) . d is
TypeSCNominativeData of
V,
A
proof
(denaming (V,A,a)) . d in ND (
V,
A)
by PARTFUN1:4, A8;
then
ex
d1 being
TypeSCNominativeData of
V,
A st
(denaming (V,A,a)) . d = d1
;
hence
(denaming (V,A,a)) . d is
TypeSCNominativeData of
V,
A
;
verum
end;
A12:
local_overlapping (
V,
A,
d,
((denaming (V,A,a)) . d),
z)
in dom (denaming (V,A,z))
proof
ex
d2 being
NonatomicND of
V,
A st
(
d2 = d &
a in dom d2 )
by A8, A7;
hence
local_overlapping (
V,
A,
d,
((denaming (V,A,a)) . d),
z)
in dom (denaming (V,A,z))
by A1, A2, Th6, A11;
verum
end;
then A13:
local_overlapping (
V,
A,
d,
((denaming (V,A,a)) . d),
z)
in dom (valid_gcd_output (V,A,z,x0,y0))
by A10;
thus A14:
d in dom (SC_Psuperpos ((valid_gcd_output (V,A,z,x0,y0)),(denaming (V,A,a)),z))
(SC_Psuperpos ((valid_gcd_output (V,A,z,x0,y0)),(denaming (V,A,a)),z)) . d = TRUE proof
dd in { d where d is TypeSCNominativeData of V,A : ( local_overlapping (V,A,d,((denaming (V,A,a)) . d),z) in dom (valid_gcd_output (V,A,z,x0,y0)) & d in dom (denaming (V,A,a)) ) }
by A8, A13;
hence
d in dom (SC_Psuperpos ((valid_gcd_output (V,A,z,x0,y0)),(denaming (V,A,a)),z))
by NOMIN_2:def 11;
verum
end;
thus
(SC_Psuperpos ((valid_gcd_output (V,A,z,x0,y0)),(denaming (V,A,a)),z)) . d = TRUE
verumproof
set dlo =
local_overlapping (
V,
A,
D,
((denaming (V,A,a)) . d),
z);
A15:
(
(SC_Psuperpos ((valid_gcd_output (V,A,z,x0,y0)),(denaming (V,A,a)),z)) . dd = (valid_gcd_output (V,A,z,x0,y0)) . (local_overlapping (V,A,D,((denaming (V,A,a)) . d),z)) &
dd in dom (denaming (V,A,a)) )
by A9, A14, NOMIN_2:35;
valid_gcd_output_pred V,
A,
z,
x0,
y0,
local_overlapping (
V,
A,
D,
((denaming (V,A,a)) . d),
z)
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:
(denaming (V,A,a)) . d in A
A19:
d in dom (denaming (V,A,b))
proof
dom (Equality (A,a,b)) = (dom (denaming (V,A,a))) /\ (dom (denaming (V,A,b)))
by Th11, A3;
hence
d in dom (denaming (V,A,b))
by A5, A6, PARTPR_1:19, XBOOLE_0:def 4;
verum
end;
A20:
(denaming (V,A,b)) . d in A
dom <:(denaming (V,A,a)),(denaming (V,A,b)):> = (dom (denaming (V,A,a))) /\ (dom (denaming (V,A,b)))
by FUNCT_3:def 7;
then A21:
d in dom <:(denaming (V,A,a)),(denaming (V,A,b)):>
by XBOOLE_0:def 4, A8, A19;
A22:
(denaming (V,A,a)) . d =
denaming (
a,
d2)
by A8, A16, NOMIN_1:def 18
.=
d2 . a
by A16, NOMIN_1:def 12
;
A23:
(denaming (V,A,b)) . d =
denaming (
b,
d2)
by A19, A16, NOMIN_1:def 18
.=
d2 . b
by A16, NOMIN_1:def 12
;
TRUE =
(Equality A) . (<:(denaming (V,A,a)),(denaming (V,A,b)):> . d)
by A5, A6, A21, FUNCT_1:13, PARTPR_1:19
.=
(Equality A) . (
((denaming (V,A,a)) . d),
((denaming (V,A,b)) . d))
by FUNCT_3:def 7, A21
;
then A24:
(denaming (V,A,a)) . d = (denaming (V,A,b)) . d
by A18, A20, Def9;
A25:
X gcd Y = |.X.|
by A24, A22, A23, A17, NEWTON02:3;
reconsider d1 =
local_overlapping (
V,
A,
D,
((denaming (V,A,a)) . d),
z) as
NonatomicND of
V,
A by NOMIN_2:9;
A26:
z in dom d1
d1 . z = x0 gcd y0
by A1, A11, A22, A17, A25, NOMIN_2:10;
hence
valid_gcd_output_pred V,
A,
z,
x0,
y0,
local_overlapping (
V,
A,
D,
((denaming (V,A,a)) . d),
z)
by A26;
verum
end;
hence
(SC_Psuperpos ((valid_gcd_output (V,A,z,x0,y0)),(denaming (V,A,a)),z)) . d = TRUE
by A15, A9, Def26, A13;
verum
end;
end;
hence
<*(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))
by A4, NOMIN_3:15; verum