let V, A be 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))
let a, b, z be 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))
let x0, y0 be Nat; ( 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 ) 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)) )
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 ((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 P = PP_inversion (PP_and ((Equality (A,a,b)),(gcd_inv (V,A,a,b,x0,y0))));
assume that
A2:
A is complex-containing
and
A3:
for d being TypeSCNominativeData of V,A holds a is_complex_on d
and
A4:
for d being TypeSCNominativeData of V,A holds b is_complex_on d
; <*(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))
A5:
for d being TypeSCNominativeData of V,A holds a is_a_value_on d
by A2, A3, Th7;
A6:
for d being TypeSCNominativeData of V,A holds b is_a_value_on d
by A2, A4, Th7;
A9:
dom (PP_and ((Equality (A,a,b)),(gcd_inv (V,A,a,b,x0,y0)))) = { 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 NOMIN_2:17;
A10:
dom (Equality (A,a,b)) = (dom (denaming (V,A,a))) /\ (dom (denaming (V,A,b)))
by A5, A6, Th11;
A11:
dom (Equality (A,a,b)) c= dom (PP_and ((Equality (A,a,b)),(gcd_inv (V,A,a,b,x0,y0))))
by PARTPR_2:3;
for d being TypeSCNominativeData of V,A st d in dom (PP_inversion (PP_and ((Equality (A,a,b)),(gcd_inv (V,A,a,b,x0,y0))))) & (PP_inversion (PP_and ((Equality (A,a,b)),(gcd_inv (V,A,a,b,x0,y0))))) . d = TRUE & d in dom (SC_assignment ((denaming (V,A,a)),z)) & (SC_assignment ((denaming (V,A,a)),z)) . d in dom (valid_gcd_output (V,A,z,x0,y0)) holds
(valid_gcd_output (V,A,z,x0,y0)) . ((SC_assignment ((denaming (V,A,a)),z)) . d) = TRUE
proof
let d be
TypeSCNominativeData of
V,
A;
( d in dom (PP_inversion (PP_and ((Equality (A,a,b)),(gcd_inv (V,A,a,b,x0,y0))))) & (PP_inversion (PP_and ((Equality (A,a,b)),(gcd_inv (V,A,a,b,x0,y0))))) . d = TRUE & d in dom (SC_assignment ((denaming (V,A,a)),z)) & (SC_assignment ((denaming (V,A,a)),z)) . d in dom (valid_gcd_output (V,A,z,x0,y0)) implies (valid_gcd_output (V,A,z,x0,y0)) . ((SC_assignment ((denaming (V,A,a)),z)) . d) = TRUE )
assume that A12:
d in dom (PP_inversion (PP_and ((Equality (A,a,b)),(gcd_inv (V,A,a,b,x0,y0)))))
and
(PP_inversion (PP_and ((Equality (A,a,b)),(gcd_inv (V,A,a,b,x0,y0))))) . d = TRUE
and A13:
d in dom (SC_assignment ((denaming (V,A,a)),z))
and
(SC_assignment ((denaming (V,A,a)),z)) . d in dom (valid_gcd_output (V,A,z,x0,y0))
;
(valid_gcd_output (V,A,z,x0,y0)) . ((SC_assignment ((denaming (V,A,a)),z)) . d) = TRUE
dom (PP_inversion (PP_and ((Equality (A,a,b)),(gcd_inv (V,A,a,b,x0,y0))))) = { d where d is Element of ND (V,A) : not d in dom (PP_and ((Equality (A,a,b)),(gcd_inv (V,A,a,b,x0,y0)))) }
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 (PP_and ((Equality (A,a,b)),(gcd_inv (V,A,a,b,x0,y0))))
by A12;
A16:
dom (SC_assignment ((denaming (V,A,a)),z)) = dom (denaming (V,A,a))
by NOMIN_2:def 7;
not
d1 in dom (Equality (A,a,b))
by A11, A15;
then A17:
not
d1 in dom (denaming (V,A,b))
by A10, A13, A14, A16, XBOOLE_0:def 4;
A18:
dom (denaming (V,A,b)) = { d where d is NonatomicND of V,A : b in dom d }
by NOMIN_1:def 18;
dom (gcd_inv (V,A,a,b,x0,y0)) = ND (
V,
A)
by Def28;
then A19:
d in dom (gcd_inv (V,A,a,b,x0,y0))
;
( not
d in dom (gcd_inv (V,A,a,b,x0,y0)) or
(gcd_inv (V,A,a,b,x0,y0)) . d <> FALSE )
by A9, A14, A15;
then
gcd_inv_pred V,
A,
a,
b,
x0,
y0,
d
by A19, Def28;
hence
(valid_gcd_output (V,A,z,x0,y0)) . ((SC_assignment ((denaming (V,A,a)),z)) . d) = TRUE
by A14, A17, A18;
verum
end;
hence
<*(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))
by NOMIN_3:28; verum