let V, A be 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))
let a, b be 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))
let x, y be 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))
let x0, y0 be Nat; ( not V is 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)) )
assume that
A1:
not V is empty
and
A2:
A is_without_nonatomicND_wrt V
and
A3:
a <> b
and
A4:
a <> y
; <*(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))
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 ((gcd_inv (V,A,a,b,x0,y0)),(denaming (V,A,y)),b);
set P = SC_Psuperpos ((SC_Psuperpos ((gcd_inv (V,A,a,b,x0,y0)),(denaming (V,A,y)),b)),(denaming (V,A,x)),a);
set F = SC_assignment ((denaming (V,A,x)),a);
set G = SC_assignment ((denaming (V,A,y)),b);
set H = gcd_var_init (V,A,a,b,x,y);
set I = valid_gcd_input (V,A,x,y,x0,y0);
A5:
<*(SC_Psuperpos ((SC_Psuperpos ((gcd_inv (V,A,a,b,x0,y0)),(denaming (V,A,y)),b)),(denaming (V,A,x)),a)),(SC_assignment ((denaming (V,A,x)),a)),(SC_Psuperpos ((gcd_inv (V,A,a,b,x0,y0)),(denaming (V,A,y)),b))*> is SFHT of (ND (V,A))
by NOMIN_3:29;
A6:
<*(SC_Psuperpos ((gcd_inv (V,A,a,b,x0,y0)),(denaming (V,A,y)),b)),(SC_assignment ((denaming (V,A,y)),b)),(gcd_inv (V,A,a,b,x0,y0))*> is SFHT of (ND (V,A))
by NOMIN_3:29;
A7:
dom (SC_Psuperpos ((gcd_inv (V,A,a,b,x0,y0)),(denaming (V,A,y)),b)) = { d where d is TypeSCNominativeData of V,A : ( local_overlapping (V,A,d,((denaming (V,A,y)) . d),b) in dom (gcd_inv (V,A,a,b,x0,y0)) & d in dom (denaming (V,A,y)) ) }
by NOMIN_2:def 11;
A8:
dom (denaming (V,A,y)) = { d where d is NonatomicND of V,A : y in dom d }
by NOMIN_1:def 18;
A9:
dom (gcd_inv (V,A,a,b,x0,y0)) = ND (V,A)
by Def28;
<*(PP_inversion (SC_Psuperpos ((gcd_inv (V,A,a,b,x0,y0)),(denaming (V,A,y)),b))),(SC_assignment ((denaming (V,A,y)),b)),(gcd_inv (V,A,a,b,x0,y0))*> is SFHT of (ND (V,A))
by Th15;
then A10:
<*(SC_Psuperpos ((SC_Psuperpos ((gcd_inv (V,A,a,b,x0,y0)),(denaming (V,A,y)),b)),(denaming (V,A,x)),a)),(gcd_var_init (V,A,a,b,x,y)),(gcd_inv (V,A,a,b,x0,y0))*> is SFHT of (ND (V,A))
by A5, A6, NOMIN_3:25;
valid_gcd_input (V,A,x,y,x0,y0) ||= SC_Psuperpos ((SC_Psuperpos ((gcd_inv (V,A,a,b,x0,y0)),(denaming (V,A,y)),b)),(denaming (V,A,x)),a)
proof
let d be
Element of
ND (
V,
A);
NOMIN_3:def 3 ( not d in dom (valid_gcd_input (V,A,x,y,x0,y0)) or not (valid_gcd_input (V,A,x,y,x0,y0)) . d = TRUE or ( d in dom (SC_Psuperpos ((SC_Psuperpos ((gcd_inv (V,A,a,b,x0,y0)),(denaming (V,A,y)),b)),(denaming (V,A,x)),a)) & (SC_Psuperpos ((SC_Psuperpos ((gcd_inv (V,A,a,b,x0,y0)),(denaming (V,A,y)),b)),(denaming (V,A,x)),a)) . d = TRUE ) )
assume that A11:
d in dom (valid_gcd_input (V,A,x,y,x0,y0))
and A12:
(valid_gcd_input (V,A,x,y,x0,y0)) . d = TRUE
;
( d in dom (SC_Psuperpos ((SC_Psuperpos ((gcd_inv (V,A,a,b,x0,y0)),(denaming (V,A,y)),b)),(denaming (V,A,x)),a)) & (SC_Psuperpos ((SC_Psuperpos ((gcd_inv (V,A,a,b,x0,y0)),(denaming (V,A,y)),b)),(denaming (V,A,x)),a)) . d = TRUE )
A13:
valid_gcd_input_pred V,
A,
x,
y,
x0,
y0,
d
by A11, A12, Def24;
then reconsider d =
d as
NonatomicND of
V,
A ;
A14:
dom (denaming (V,A,x)) = { d where d is NonatomicND of V,A : x in dom d }
by NOMIN_1:def 18;
A15:
dom (SC_Psuperpos ((SC_Psuperpos ((gcd_inv (V,A,a,b,x0,y0)),(denaming (V,A,y)),b)),(denaming (V,A,x)),a)) = { d where d is TypeSCNominativeData of V,A : ( local_overlapping (V,A,d,((denaming (V,A,x)) . d),a) in dom (SC_Psuperpos ((gcd_inv (V,A,a,b,x0,y0)),(denaming (V,A,y)),b)) & d in dom (denaming (V,A,x)) ) }
by NOMIN_2:def 11;
reconsider Lx =
local_overlapping (
V,
A,
d,
((denaming (V,A,x)) . d),
a) as
NonatomicND of
V,
A by NOMIN_2:9;
reconsider Ly =
local_overlapping (
V,
A,
Lx,
((denaming (V,A,y)) . Lx),
b) as
NonatomicND of
V,
A by NOMIN_2:9;
A16:
Ly in dom (gcd_inv (V,A,a,b,x0,y0))
by A9;
reconsider GO =
global_overlapping (
V,
A,
Lx,
(naming (V,A,b,((denaming (V,A,y)) . Lx)))) as
Function ;
set d1 =
naming (
V,
A,
a,
((denaming (V,A,x)) . d));
set d2 =
b .--> ((denaming (V,A,y)) . Lx);
A17:
not
Lx in A
by A2, Th3;
A18:
not
d in A
by A2, Th3;
A19:
not
naming (
V,
A,
a,
((denaming (V,A,x)) . d))
in A
by A2, Th3;
A20:
Lx = (naming (V,A,a,((denaming (V,A,x)) . d))) \/ (d | ((dom d) \ (dom (naming (V,A,a,((denaming (V,A,x)) . d))))))
by A18, A19, NOMIN_1:64;
then
naming (
V,
A,
a,
((denaming (V,A,x)) . d))
c= Lx
by XBOOLE_1:7;
then A21:
dom (naming (V,A,a,((denaming (V,A,x)) . d))) c= dom Lx
by GRFUNC_1:2;
A22:
d in dom (denaming (V,A,x))
by A13, A14;
then A23:
(denaming (V,A,x)) . d is
TypeSCNominativeData of
V,
A
by PARTFUN1:4, NOMIN_1:39;
then A24:
naming (
V,
A,
a,
((denaming (V,A,x)) . d))
= a .--> ((denaming (V,A,x)) . d)
by A1, NOMIN_1:def 13;
not
y in dom (naming (V,A,a,((denaming (V,A,x)) . d)))
by A4, A24, TARSKI:def 1;
then
y in (dom d) \ (dom (naming (V,A,a,((denaming (V,A,x)) . d))))
by A13, XBOOLE_0:def 5;
then A25:
y in dom (d | ((dom d) \ (dom (naming (V,A,a,((denaming (V,A,x)) . d))))))
by RELAT_1:57;
d | ((dom d) \ (dom (naming (V,A,a,((denaming (V,A,x)) . d))))) c= Lx
by A20, XBOOLE_1:7;
then A26:
dom (d | ((dom d) \ (dom (naming (V,A,a,((denaming (V,A,x)) . d)))))) c= dom Lx
by GRFUNC_1:2;
then A27:
Lx in dom (denaming (V,A,y))
by A8, A25;
A28:
(denaming (V,A,y)) . Lx is
TypeSCNominativeData of
V,
A
by A27, PARTFUN1:4, NOMIN_1:39;
then A29:
naming (
V,
A,
b,
((denaming (V,A,y)) . Lx))
= b .--> ((denaming (V,A,y)) . Lx)
by A1, NOMIN_1:def 13;
then A30:
not
b .--> ((denaming (V,A,y)) . Lx) in A
by A2, Th3;
then A31:
Ly = (b .--> ((denaming (V,A,y)) . Lx)) \/ (Lx | ((dom Lx) \ (dom (b .--> ((denaming (V,A,y)) . Lx)))))
by A29, A17, NOMIN_1:64;
then
b .--> ((denaming (V,A,y)) . Lx) c= Ly
by XBOOLE_1:7;
then A32:
dom (b .--> ((denaming (V,A,y)) . Lx)) c= dom Ly
by GRFUNC_1:2;
A34:
not
a in dom (b .--> ((denaming (V,A,y)) . Lx))
by A3, TARSKI:def 1;
a in {a}
by TARSKI:def 1;
then A35:
a in (dom Lx) \ (dom (b .--> ((denaming (V,A,y)) . Lx)))
by A21, A24, A34, XBOOLE_0:def 5;
reconsider G1 =
global_overlapping (
V,
A,
Lx,
(b .--> ((denaming (V,A,y)) . Lx))) as
Function by A29;
A36:
G1 = (b .--> ((denaming (V,A,y)) . Lx)) \/ (Lx | ((dom Lx) \ (dom (b .--> ((denaming (V,A,y)) . Lx)))))
by A29, A17, A30, NOMIN_1:64;
A37:
a in dom (Lx | ((dom Lx) \ (dom (b .--> ((denaming (V,A,y)) . Lx)))))
by A35, RELAT_1:57;
Lx | ((dom Lx) \ (dom (b .--> ((denaming (V,A,y)) . Lx)))) c= Ly
by A31, XBOOLE_1:7;
then A38:
dom (Lx | ((dom Lx) \ (dom (b .--> ((denaming (V,A,y)) . Lx))))) 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 (b .--> ((denaming (V,A,y)) . Lx))))) . a
by A36, A37, GRFUNC_1:15
.=
Lx . a
by A37, FUNCT_1:47
.=
(denaming (V,A,x)) . 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 =
(denaming (V,A,y)) . 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 (SC_Psuperpos ((gcd_inv (V,A,a,b,x0,y0)),(denaming (V,A,y)),b))
by A7, A16, A27;
then
d in dom (SC_Psuperpos ((SC_Psuperpos ((gcd_inv (V,A,a,b,x0,y0)),(denaming (V,A,y)),b)),(denaming (V,A,x)),a))
by A15, A22;
then (SC_Psuperpos ((SC_Psuperpos ((gcd_inv (V,A,a,b,x0,y0)),(denaming (V,A,y)),b)),(denaming (V,A,x)),a)) . d =
(SC_Psuperpos ((gcd_inv (V,A,a,b,x0,y0)),(denaming (V,A,y)),b)) . Lx
by NOMIN_2:35
.=
(gcd_inv (V,A,a,b,x0,y0)) . Ly
by A43, NOMIN_2:35
.=
TRUE
by A16, A42, Def28
;
hence
(
d in dom (SC_Psuperpos ((SC_Psuperpos ((gcd_inv (V,A,a,b,x0,y0)),(denaming (V,A,y)),b)),(denaming (V,A,x)),a)) &
(SC_Psuperpos ((SC_Psuperpos ((gcd_inv (V,A,a,b,x0,y0)),(denaming (V,A,y)),b)),(denaming (V,A,x)),a)) . d = TRUE )
by A15, A43, A22;
verum
end;
hence
<*(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))
by A10, NOMIN_3:15; verum