:: Partial Correctness of a Power Algorithm
:: by Adrian Jaszczak
::
:: Received May 27, 2019
:: Copyright (c) 2019-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, ZFMISC_1, SUBSET_1, XBOOLE_0, RELAT_1, FUNCT_1,
FINSEQ_1, NAT_1, ARYTM_3, PARTFUN1, XBOOLEAN, TARSKI, NEWTON, NOMIN_3,
NOMIN_4, XCMPLX_0, NOMIN_2, PARTPR_1, PARTPR_2, NOMIN_5, NOMIN_6, CARD_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, ENUMSET1, 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, NEWTON, NOMIN_1,
PARTPR_1, PARTPR_2, NOMIN_2, NOMIN_3, NOMIN_4, NOMIN_5;
constructors RELSET_1, INT_2, BINOP_1, FUNCOP_1, FUNCT_3, NEWTON, NOMIN_2,
NOMIN_3, NOMIN_4, NOMIN_5, ENUMSET1;
registrations ORDINAL1, RELSET_1, INT_1, NOMIN_1, XCMPLX_0;
requirements NUMERALS, BOOLE, SUBSET;
definitions TARSKI, NOMIN_3;
equalities NOMIN_1, PARTPR_1, PARTPR_2, NOMIN_2, NOMIN_4, NOMIN_5, XBOOLEAN,
BINOP_1;
expansions TARSKI, ZFMISC_1, PARTFUN1, NOMIN_4;
theorems XBOOLE_0, NOMIN_1, PARTPR_1, NOMIN_2, NOMIN_3, NOMIN_4, NOMIN_5,
FUNCT_1, ENUMSET1, FUNCT_3, PARTFUN1, TARSKI, NEWTON, PARTPR_2;
schemes PARTPR_2;
begin
definition
let D be set;
let f1,f2,f3,f4,f5 be BinominativeFunction of D;
func PP_composition(f1,f2,f3,f4,f5) -> BinominativeFunction of D equals
PP_composition(PP_composition(f1,f2,f3,f4),f5);
coherence;
end;
reserve D for non empty set;
reserve f1,f2,f3,f4,f5 for BinominativeFunction of D;
reserve p,q,r,t,w,u for PartialPredicate of D;
::$N unconditional composition rule for 5 programs
theorem Th1:
<*p,f1,q*> is SFHT of D & <*q,f2,r*> is SFHT of D &
<*r,f3,w*> is SFHT of D & <*w,f4,t*> is SFHT of D &
<*t,f5,u*> is SFHT of D &
<*PP_inversion(q),f2,r*> is SFHT of D &
<*PP_inversion(r),f3,w*> is SFHT of D &
<*PP_inversion(w),f4,t*> is SFHT of D &
<*PP_inversion(t),f5,u*> is SFHT of D
implies <*p,PP_composition(f1,f2,f3,f4,f5),u*> is SFHT of D
proof
assume that
A1: <*p,f1,q*> is SFHT of D and
A2: <*q,f2,r*> is SFHT of D and
A3: <*r,f3,w*> is SFHT of D and
A4: <*w,f4,t*> is SFHT of D and
A5: <*t,f5,u*> is SFHT of D and
A6: <*PP_inversion(q),f2,r*> is SFHT of D and
A7: <*PP_inversion(r),f3,w*> is SFHT of D and
A8: <*PP_inversion(w),f4,t*> is SFHT of D and
A9: <*PP_inversion(t),f5,u*> is SFHT of D;
<*p,PP_composition(f1,f2),r*> is SFHT of D by A1,A2,A6,NOMIN_3:25;
then <*p,PP_composition(PP_composition(f1,f2),f3),w*> is SFHT of D
by A3,A7,NOMIN_3:25;
then <*p,PP_composition(PP_composition(f1,f2,f3),f4),t*>
is SFHT of D by A4,A8,NOMIN_3:25;
hence thesis by A5,A9,NOMIN_3:25;
end;
reserve d,v,v1 for object;
reserve V,A for set;
reserve i,j,b,n,s,z for Element of V;
reserve i1,j1,b1,n1,s1 for object;
reserve d1,Li,Lj,Lb,Ln,Ls for NonatomicND of V,A;
reserve Di,Dj,Db,Dn,Ds for SCBinominativeFunction of V,A;
theorem Th2:
V is non empty & A is_without_nonatomicND_wrt V &
Di = denaming(V,A,i1) & Dj = denaming(V,A,j1) &
Db = denaming(V,A,b1) & Dn = denaming(V,A,n1) &
Ds = denaming(V,A,s1) &
Li = local_overlapping(V,A,d1,Di.d1,i) &
Lj = local_overlapping(V,A,Li,Dj.Li,j) &
Lb = local_overlapping(V,A,Lj,Db.Lj,b) &
Ln = local_overlapping(V,A,Lb,Dn.Lb,n) &
Ls = local_overlapping(V,A,Ln,Ds.Ln,s) &
j1 in dom d1 & b1 in dom d1 & n1 in dom d1 & s1 in dom d1 &
d1 in dom Di & s <> n implies Ls.n = Ln.n
proof
assume that
A1: V is non empty and
A2: A is_without_nonatomicND_wrt V and
A3: Di = denaming(V,A,i1) & Dj = denaming(V,A,j1) &
Db = denaming(V,A,b1) & Dn = denaming(V,A,n1) &
Ds = denaming(V,A,s1) &
Li = local_overlapping(V,A,d1,Di.d1,i) &
Lj = local_overlapping(V,A,Li,Dj.Li,j) &
Lb = local_overlapping(V,A,Lj,Db.Lj,b) &
Ln = local_overlapping(V,A,Lb,Dn.Lb,n) &
Ls = local_overlapping(V,A,Ln,Ds.Ln,s) and
A4: j1 in dom d1 and
A5: b1 in dom d1 and
A6: n1 in dom d1 and
A7: s1 in dom d1 and
A8: d1 in dom Di and
A9: s <> n;
A10: dom Dj = {d where d is NonatomicND of V,A: j1 in dom d}
by A3,NOMIN_1:def 18;
A11: dom Db = {d where d is NonatomicND of V,A: b1 in dom d}
by A3,NOMIN_1:def 18;
A12: dom Dn = {d where d is NonatomicND of V,A: n1 in dom d}
by A3,NOMIN_1:def 18;
A13: dom Ds = {d where d is NonatomicND of V,A: s1 in dom d}
by A3,NOMIN_1:def 18;
Di.d1 is TypeSCNominativeData of V,A by A8,PARTFUN1:4,NOMIN_1:39;
then
A14: dom Li = {i} \/ dom d1 by A1,A2,A3,NOMIN_4:4;
j1 in dom Li by A4,A14,XBOOLE_0:def 3;
then Li in dom Dj by A10;
then Dj.Li is TypeSCNominativeData of V,A by PARTFUN1:4,NOMIN_1:39;
then
A15: dom Lj = {j} \/ dom Li by A1,A2,A3,NOMIN_4:4;
b1 in dom Li by A5,A14,XBOOLE_0:def 3;
then b1 in dom Lj by A15,XBOOLE_0:def 3;
then Lj in dom Db by A11;
then Db.Lj is TypeSCNominativeData of V,A by PARTFUN1:4,NOMIN_1:39;
then
A16: dom Lb = {b} \/ dom Lj by A1,A2,A3,NOMIN_4:4;
n1 in dom Li by A6,A14,XBOOLE_0:def 3;
then n1 in dom Lj by A15,XBOOLE_0:def 3;
then n1 in dom Lb by A16,XBOOLE_0:def 3;
then Lb in dom Dn by A12;
then Dn.Lb is TypeSCNominativeData of V,A by PARTFUN1:4, NOMIN_1:39;
then
A17: dom Ln = {n} \/ dom Lb by A1,A2,A3,NOMIN_4:4;
s1 in dom Li by A7,A14,XBOOLE_0:def 3;
then s1 in dom Lj by A15,XBOOLE_0:def 3;
then s1 in dom Lb by A16,XBOOLE_0:def 3;
then s1 in dom Ln by A17,XBOOLE_0:def 3;
then
A18: Ln in dom Ds by A13;
n in {n} by TARSKI:def 1;
then
A19: n in dom Ln by A17,XBOOLE_0:def 3;
Ds.Ln is TypeSCNominativeData of V,A by A18,PARTFUN1:4,NOMIN_1:39;
hence Ls.n = Ln.n by A1,A2,A9,A19,A3,NOMIN_5:3;
end;
theorem Th3:
V is non empty & A is_without_nonatomicND_wrt V &
Di = denaming(V,A,i1) & Dj = denaming(V,A,j1) &
Db = denaming(V,A,b1) & Dn = denaming(V,A,n1) &
Ds = denaming(V,A,s1) &
Li = local_overlapping(V,A,d1,Di.d1,i) &
Lj = local_overlapping(V,A,Li,Dj.Li,j) &
Lb = local_overlapping(V,A,Lj,Db.Lj,b) &
Ln = local_overlapping(V,A,Lb,Dn.Lb,n) &
Ls = local_overlapping(V,A,Ln,Ds.Ln,s) &
j1 in dom d1 & b1 in dom d1 & n1 in dom d1 & s1 in dom d1 &
d1 in dom Di & s <> i implies Ls.i = Ln.i
proof
assume that
A1: V is non empty and
A2: A is_without_nonatomicND_wrt V and
A3: Di = denaming(V,A,i1) & Dj = denaming(V,A,j1) &
Db = denaming(V,A,b1) & Dn = denaming(V,A,n1) &
Ds = denaming(V,A,s1) &
Li = local_overlapping(V,A,d1,Di.d1,i) &
Lj = local_overlapping(V,A,Li,Dj.Li,j) &
Lb = local_overlapping(V,A,Lj,Db.Lj,b) &
Ln = local_overlapping(V,A,Lb,Dn.Lb,n) &
Ls = local_overlapping(V,A,Ln,Ds.Ln,s) and
A4: j1 in dom d1 and
A5: b1 in dom d1 and
A6: n1 in dom d1 and
A7: s1 in dom d1 and
A8: d1 in dom Di and
A9: s <> i;
A10: dom Dj = {d where d is NonatomicND of V,A: j1 in dom d}
by A3,NOMIN_1:def 18;
A11: dom Db = {d where d is NonatomicND of V,A: b1 in dom d}
by A3,NOMIN_1:def 18;
A12: dom Dn = {d where d is NonatomicND of V,A: n1 in dom d}
by A3,NOMIN_1:def 18;
A13: dom Ds = {d where d is NonatomicND of V,A: s1 in dom d}
by A3,NOMIN_1:def 18;
Di.d1 is TypeSCNominativeData of V,A by A8,PARTFUN1:4,NOMIN_1:39;
then
A14: dom Li = {i} \/ dom d1 by A1,A2,A3,NOMIN_4:4;
j1 in dom Li by A4,A14,XBOOLE_0:def 3;
then Li in dom Dj by A10;
then Dj.Li is TypeSCNominativeData of V,A by PARTFUN1:4,NOMIN_1:39;
then
A15: dom Lj = {j} \/ dom Li by A1,A2,A3,NOMIN_4:4;
b1 in dom Li by A5,A14,XBOOLE_0:def 3;
then b1 in dom Lj by A15,XBOOLE_0:def 3;
then Lj in dom Db by A11;
then Db.Lj is TypeSCNominativeData of V,A by PARTFUN1:4,NOMIN_1:39;
then
A16: dom Lb = {b} \/ dom Lj by A1,A2,A3,NOMIN_4:4;
n1 in dom Li by A6,A14,XBOOLE_0:def 3;
then n1 in dom Lj by A15,XBOOLE_0:def 3;
then n1 in dom Lb by A16,XBOOLE_0:def 3;
then Lb in dom Dn by A12;
then Dn.Lb is TypeSCNominativeData of V,A by PARTFUN1:4, NOMIN_1:39;
then
A17: dom Ln = {n} \/ dom Lb by A1,A2,A3,NOMIN_4:4;
s1 in dom Li by A7,A14,XBOOLE_0:def 3;
then s1 in dom Lj by A15,XBOOLE_0:def 3;
then s1 in dom Lb by A16,XBOOLE_0:def 3;
then s1 in dom Ln by A17,XBOOLE_0:def 3;
then
A18: Ln in dom Ds by A13;
i in {i} by TARSKI:def 1;
then i in dom Li by A14,XBOOLE_0:def 3;
then i in dom Lj by A15,XBOOLE_0:def 3;
then i in dom Lb by A16,XBOOLE_0:def 3;
then
A19: i in dom Ln by A17,XBOOLE_0:def 3;
Ds.Ln is TypeSCNominativeData of V,A by A18,PARTFUN1:4,NOMIN_1:39;
hence Ls.i = Ln.i by A1,A2,A9,A19,A3,NOMIN_5:3;
end;
reserve f for SCBinominativeFunction of V,A;
reserve T for TypeSCNominativeData of V,A;
:: Pseudocode of b|^n
::
:: i := val.1
:: j := val.2
:: b := val.3
:: n := val.4
:: s := val.5
:: { s == b|^i }
:: while ( i <> n )
:: i := i + j
:: s := s * b
:: return s
:: { n == i && s == b|^i }
::
:: where
:: val.1 = 0,
:: val.2 = 1,
:: val.3, val.4 - the input base and exponent, respectively,
:: val.5 = 1
:: are input data from the environment,
:: and loc/.1 = i, loc/.2 = j, loc/.3 = b, loc/.4 = n, loc/.5 = s.
reserve loc for V-valued Function;
reserve val for Function;
definition
let V,A,loc;
func power_loop_body(A,loc) -> SCBinominativeFunction of V,A equals
PP_composition(
SC_assignment(addition(A,loc/.1,loc/.2),loc/.1),
SC_assignment(multiplication(A,loc/.5,loc/.3),loc/.5)
);
coherence;
end;
definition
let V,A,loc;
func power_main_loop(A,loc) -> SCBinominativeFunction of V,A equals
PP_while(PP_not(Equality(A,loc/.1,loc/.4)),power_loop_body(A,loc));
coherence;
end;
definition
let V,A,loc,val;
func power_var_init(A,loc,val)
-> SCBinominativeFunction of V,A equals
PP_composition(
SC_assignment(denaming(V,A,val.1), loc/.1),
SC_assignment(denaming(V,A,val.2), loc/.2),
SC_assignment(denaming(V,A,val.3), loc/.3),
SC_assignment(denaming(V,A,val.4), loc/.4),
SC_assignment(denaming(V,A,val.5), loc/.5)
);
coherence;
end;
definition
let V,A,loc,val;
func power_main_part(A,loc,val)
-> SCBinominativeFunction of V,A equals
PP_composition(
power_var_init(A,loc,val),
power_main_loop(A,loc)
);
coherence;
end;
definition
let V,A,loc,val,z;
func power_program(A,loc,val,z)
-> SCBinominativeFunction of V,A equals
PP_composition(
power_main_part(A,loc,val),
SC_assignment(denaming(V,A,loc/.5),z)
);
coherence;
end;
reserve n0 for Nat;
reserve b0 for Complex;
definition
let V,A,val,b0,n0,d;
pred valid_power_input_pred V,A,val,b0,n0,d means
ex d1 being NonatomicND of V,A st d = d1 &
{ val.1, val.2, val.3, val.4, val.5 } c= dom d1 &
d1.(val.1) = 0 & d1.(val.2) = 1 &
d1.(val.3) = b0 & d1.(val.4) = n0 & d1.(val.5) = 1;
end;
definition
let V,A,val,b0,n0;
defpred P[object] means valid_power_input_pred V,A,val,b0,n0,$1;
func valid_power_input(V,A,val,b0,n0)
-> SCPartialNominativePredicate of V,A
means :Def8:
dom it = ND(V,A) &
for d being object st d in dom it holds
(valid_power_input_pred V,A,val,b0,n0,d implies it.d = TRUE) &
(not valid_power_input_pred V,A,val,b0,n0,d implies it.d = FALSE);
existence
proof
A1: ND(V,A) c= ND(V,A);
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
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,val,b0,n0;
cluster valid_power_input(V,A,val,b0,n0) -> total;
coherence by Def8;
end;
definition
let V,A,z,b0,n0,d;
pred valid_power_output_pred A,z,b0,n0,d means
ex d1 being NonatomicND of V,A st d = d1 & z in dom d1 & d1.z = b0|^n0;
end;
definition
let V,A,z,b0,n0;
set D = {d where d is TypeSCNominativeData of V,A: d in dom denaming(V,A,z)};
defpred P[object] means valid_power_output_pred A,z,b0,n0,$1;
func valid_power_output(A,z,b0,n0) -> SCPartialNominativePredicate of V,A
means :Def10:
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_power_output_pred A,z,b0,n0,d implies it.d = TRUE) &
(not valid_power_output_pred A,z,b0,n0,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;
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
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,loc,b0,n0,d;
pred power_inv_pred A,loc,b0,n0,d means
ex d1 being NonatomicND of V,A st
d = d1 & { loc/.1, loc/.2, loc/.3, loc/.4, loc/.5 } c= dom d1 &
d1.(loc/.2) = 1 & d1.(loc/.3) = b0 & d1.(loc/.4) = n0 &
ex S being Complex, I being Nat st
I = d1.(loc/.1) & S = d1.(loc/.5) & S = b0|^I;
end;
definition
let V,A,loc,b0,n0;
defpred P[object] means power_inv_pred A,loc,b0,n0,$1;
func power_inv(A,loc,b0,n0) ->
SCPartialNominativePredicate of V,A means
:Def12:
dom it = ND(V,A) &
for d being object st d in dom it holds
(power_inv_pred A,loc,b0,n0,d implies it.d = TRUE) &
(not power_inv_pred A,loc,b0,n0,d implies it.d = FALSE);
existence
proof
A1: ND(V,A) c= ND(V,A);
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
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,loc,b0,n0;
cluster power_inv(A,loc,b0,n0) -> total;
coherence by Def12;
end;
definition
let V,loc,val;
pred loc,val are_compatible_wrt_5_locs means
val.5 <> loc/.4 & val.5 <> loc/.3 & val.5 <> loc/.2 & val.5 <> loc/.1 &
val.4 <> loc/.3 & val.4 <> loc/.2 & val.4 <> loc/.1 &
val.3 <> loc/.2 & val.3 <> loc/.1 & val.2 <> loc/.1;
end;
theorem Th4:
V is non empty & A is_without_nonatomicND_wrt V &
loc/.1, loc/.2, loc/.3, loc/.4, loc/.5 are_mutually_distinct &
loc,val are_compatible_wrt_5_locs
implies
<* valid_power_input(V,A,val,b0,n0),
power_var_init(A,loc,val),
power_inv(A,loc,b0,n0) *> is SFHT of ND(V,A)
proof
set i = loc/.1, j = loc/.2, b = loc/.3, n = loc/.4, s = loc/.5;
set i1 = val.1, j1 = val.2, b1 = val.3, n1 = val.4, s1 = val.5;
set D = ND(V,A);
set I = valid_power_input(V,A,val,b0,n0);
set F = power_var_init(A,loc,val);
set inv = power_inv(A,loc,b0,n0);
set Di = denaming(V,A,i1);
set Dj = denaming(V,A,j1);
set Db = denaming(V,A,b1);
set Dn = denaming(V,A,n1);
set Ds = denaming(V,A,s1);
set asi = SC_assignment(Di,i);
set asj = SC_assignment(Dj,j);
set asb = SC_assignment(Db,b);
set asn = SC_assignment(Dn,n);
set ass = SC_assignment(Ds,s);
set T1 = SC_Psuperpos(inv,Ds,s);
set S1 = SC_Psuperpos(T1,Dn,n);
set R1 = SC_Psuperpos(S1,Db,b);
set Q1 = SC_Psuperpos(R1,Dj,j);
set P1 = SC_Psuperpos(Q1,Di,i);
assume that
A1: V is non empty and
A2: A is_without_nonatomicND_wrt V and
A3: i,j,b,n,s are_mutually_distinct and
A4: loc,val are_compatible_wrt_5_locs;
A5: <*P1,asi,Q1*> is SFHT of D by NOMIN_3:29;
A6: <*Q1,asj,R1*> is SFHT of D by NOMIN_3:29;
A7: <*R1,asb,S1*> is SFHT of D by NOMIN_3:29;
A8: <*S1,asn,T1*> is SFHT of D by NOMIN_3:29;
A9: <*T1,ass,inv*> is SFHT of D by NOMIN_3:29;
I ||= P1
proof
let d be Element of D;
assume d in dom I & I.d = TRUE;
then valid_power_input_pred V,A,val,b0,n0,d by Def8;
then consider d1 being NonatomicND of V,A such that
A10: d = d1 and
A11: {i1,j1,b1,n1,s1} c= dom d1 and
A12: d1.i1 = 0 and
A13: d1.j1 = 1 and
A14: d1.b1 = b0 and
A15: d1.n1 = n0 and
A16: d1.s1 = 1;
A17: i1 in {i1,j1,b1,n1,s1} by ENUMSET1:def 3;
A18: j1 in {i1,j1,b1,n1,s1} by ENUMSET1:def 3;
A19: b1 in {i1,j1,b1,n1,s1} by ENUMSET1:def 3;
A20: n1 in {i1,j1,b1,n1,s1} by ENUMSET1:def 3;
A21: s1 in {i1,j1,b1,n1,s1} by ENUMSET1:def 3;
A23: dom Di = {d where d is NonatomicND of V,A: i1 in dom d}
by NOMIN_1:def 18;
A24: dom Dj = {d where d is NonatomicND of V,A: j1 in dom d}
by NOMIN_1:def 18;
A25: dom Db = {d where d is NonatomicND of V,A: b1 in dom d}
by NOMIN_1:def 18;
A26: dom Dn = {d where d is NonatomicND of V,A: n1 in dom d}
by NOMIN_1:def 18;
A27: dom Ds = {d where d is NonatomicND of V,A: s1 in dom d}
by NOMIN_1:def 18;
A28: dom P1 = {d where d is TypeSCNominativeData of V,A:
local_overlapping(V,A,d,Di.d,i) in dom Q1 & d in dom Di}
by NOMIN_2:def 11;
A29: dom Q1 = {d where d is TypeSCNominativeData of V,A:
local_overlapping(V,A,d,Dj.d,j) in dom R1 & d in dom Dj}
by NOMIN_2:def 11;
A30: dom R1 = {d where d is TypeSCNominativeData of V,A:
local_overlapping(V,A,d,Db.d,b) in dom S1 & d in dom Db}
by NOMIN_2:def 11;
A31: dom S1 = {d where d is TypeSCNominativeData of V,A:
local_overlapping(V,A,d,Dn.d,n) in dom T1 & d in dom Dn}
by NOMIN_2:def 11;
A32: dom T1 = {d where d is TypeSCNominativeData of V,A:
local_overlapping(V,A,d,Ds.d,s) in dom inv & d in dom Ds}
by NOMIN_2:def 11;
reconsider Li = local_overlapping(V,A,d1,Di.d1,i) as NonatomicND of V,A
by NOMIN_2:9;
reconsider Lj = local_overlapping(V,A,Li,Dj.Li,j) as NonatomicND of V,A
by NOMIN_2:9;
reconsider Lb = local_overlapping(V,A,Lj,Db.Lj,b) as NonatomicND of V,A
by NOMIN_2:9;
reconsider Ln = local_overlapping(V,A,Lb,Dn.Lb,n) as NonatomicND of V,A
by NOMIN_2:9;
reconsider Ls = local_overlapping(V,A,Ln,Ds.Ln,s) as NonatomicND of V,A
by NOMIN_2:9;
A33: d1 in dom Di by A11,A17,A23;
then
A34: Di.d1 is TypeSCNominativeData of V,A by PARTFUN1:4,NOMIN_1:39;
then
A35: dom Li = {i} \/ dom d1 by A1,A2,NOMIN_4:4;
dom inv = D by Def12;
then
A36: Ls in dom inv;
A37: j1 in dom Li by A11,A18,A35,XBOOLE_0:def 3;
then
A38: Li in dom Dj by A24;
then
A39: Dj.Li is TypeSCNominativeData of V,A by PARTFUN1:4,NOMIN_1:39;
then
A40: dom Lj = {j} \/ dom Li by A1,A2,NOMIN_4:4;
A41: b1 in dom Li by A11,A19,A35,XBOOLE_0:def 3;
then
A42: b1 in dom Lj by A40,XBOOLE_0:def 3;
then
A43: Lj in dom Db by A25;
then
A44: Db.Lj is TypeSCNominativeData of V,A by PARTFUN1:4,NOMIN_1:39;
then
A45: dom Lb = {b} \/ dom Lj by A1,A2,NOMIN_4:4;
A46: n1 in dom Li by A11,A20,A35,XBOOLE_0:def 3;
then
A47: n1 in dom Lj by A40,XBOOLE_0:def 3;
then
A48: n1 in dom Lb by A45,XBOOLE_0:def 3;
then
A49: Lb in dom Dn by A26;
then
A50: Dn.Lb is TypeSCNominativeData of V,A by PARTFUN1:4,NOMIN_1:39;
then
A51: dom Ln = {n} \/ dom Lb by A1,A2,NOMIN_4:4;
A52: s1 in dom Li by A11,A21,A35,XBOOLE_0:def 3;
then
A53: s1 in dom Lj by A40,XBOOLE_0:def 3;
then
A54: s1 in dom Lb by A45,XBOOLE_0:def 3;
then
A55: s1 in dom Ln by A51,XBOOLE_0:def 3;
then
A56: Ln in dom Ds by A27;
then
A57: Ln in dom T1 by A32,A36;
then
A58: Lb in dom S1 by A31,A49;
then
A59: Lj in dom R1 by A30,A43;
then
A60: Li in dom Q1 by A29,A38;
hence
A61: d in dom P1 by A10,A28,A33;
A62: power_inv_pred A,loc,b0,n0,Ls
proof
take Ls;
thus Ls = Ls;
A63: Ds.Ln is TypeSCNominativeData of V,A by A56,PARTFUN1:4,NOMIN_1:39;
then
A64: dom Ls = {s} \/ dom Ln by A1,A2,NOMIN_4:4;
i in {i} by TARSKI:def 1;
then
A65: i in dom Li by A35,XBOOLE_0:def 3;
then
A66: i in dom Lj by A40,XBOOLE_0:def 3;
then
A67: i in dom Lb by A45,XBOOLE_0:def 3;
then i in dom Ln by A51,XBOOLE_0:def 3;
then
A68: i in dom Ls by A64,XBOOLE_0:def 3;
j in {j} by TARSKI:def 1;
then
A69: j in dom Lj by A40,XBOOLE_0:def 3;
then
A70: j in dom Lb by A45,XBOOLE_0:def 3;
then
A71: j in dom Ln by A51,XBOOLE_0:def 3;
then
A72: j in dom Ls by A64,XBOOLE_0:def 3;
b in {b} by TARSKI:def 1;
then
A73: b in dom Lb by A45,XBOOLE_0:def 3;
then
A74: b in dom Ln by A51,XBOOLE_0:def 3;
then
A75: b in dom Ls by A64, XBOOLE_0:def 3;
n in {n} by TARSKI:def 1;
then n in dom Ln by A51,XBOOLE_0:def 3;
then
A76: n in dom Ls by A64,XBOOLE_0:def 3;
s in {s} by TARSKI:def 1;
then s in dom Ls by A64,XBOOLE_0:def 3;
hence {i,j,b,n,s} c= dom Ls by A68,A72,A75,A76,ENUMSET1:def 3;
thus Ls.j = Ln.j by A1,A2,A3,A63,A71,NOMIN_5:3
.= Lb.j by A1,A2,A3,A50,A70,NOMIN_5:3
.= Lj.j by A1,A2,A3,A44,A69,NOMIN_5:3
.= Dj.Li by A1,A39,NOMIN_2:10
.= denaming(j1,Li) by A38,NOMIN_1:def 18
.= Li.j1 by A37,NOMIN_1:def 12
.= 1 by A1,A2,A11,A4,A18,A13,A34,NOMIN_5:3;
thus Ls.b = Ln.b by A1,A2,A3,A63,A74,NOMIN_5:3
.= Lb.b by A1,A2,A3,A50,A73,NOMIN_5:3
.= Db.Lj by A1,A44,NOMIN_2:10
.= denaming(b1,Lj) by A43,NOMIN_1:def 18
.= Lj.b1 by A42,NOMIN_1:def 12
.= Li.b1 by A1,A2,A4,A39,A41,NOMIN_5:3
.= b0 by A1,A2,A11,A19,A14,A34,A4,NOMIN_5:3;
thus Ls.n = Ln.n by A1,A2,A3,A11,A18,A19,A20,A21,A33,Th2
.= Dn.Lb by A1,A50,NOMIN_2:10
.= denaming(n1,Lb) by A49,NOMIN_1:def 18
.= Lb.n1 by A48,NOMIN_1:def 12
.= Lj.n1 by A1,A2,A4,A44,A47,NOMIN_5:3
.= Li.n1 by A1,A2,A4,A39,A46,NOMIN_5:3
.= n0 by A1,A2,A11,A20,A15,A4,A34,NOMIN_5:3;
A78: Ln.s1 = Lb.s1 by A1,A2,A4,A50,A54,NOMIN_5:3
.= Lj.s1 by A1,A2,A4,A44,A53,NOMIN_5:3
.= Li.s1 by A1,A2,A39,A4,A52,NOMIN_5:3
.= 1 by A1,A2,A11,A21,A16,A34,A4,NOMIN_5:3;
take 1,0;
thus Ls.i = Ln.i by A1,A2,A11,A3,A18,A19,A20,A21,A33,Th3
.= Lb.i by A1,A2,A50,A3,A67,NOMIN_5:3
.= Lj.i by A1,A2,A66,A3,A44,NOMIN_5:3
.= Li.i by A1,A2,A39,A3,A65,NOMIN_5:3
.= Di.d1 by A1,A34,NOMIN_2:10
.= denaming(i1,d1) by A33,NOMIN_1:def 18
.= 0 by A11,A12,A17,NOMIN_1:def 12;
thus Ls.s = Ds.Ln by A1,A63,NOMIN_2:10
.= denaming(s1,Ln) by A56,NOMIN_1:def 18
.= 1 by A78,A55,NOMIN_1:def 12;
thus 1 = b0|^0 by NEWTON:4;
end;
thus P1.d = Q1.Li by A10,A61,NOMIN_2:35
.= R1.Lj by A60,NOMIN_2:35
.= S1.Lb by A59,NOMIN_2:35
.= T1.Ln by A58,NOMIN_2:35
.= inv.Ls by A57,NOMIN_2:35
.= TRUE by A36,A62,Def12;
end;
then
A79: <*I,asi,Q1*> is SFHT of D by A5,NOMIN_3:15;
A80: <*PP_inversion(Q1),asj,R1*> is SFHT of D by NOMIN_4:16;
A81: <*PP_inversion(R1),asb,S1*> is SFHT of D by NOMIN_4:16;
A82: <*PP_inversion(S1),asn,T1*> is SFHT of D by NOMIN_4:16;
<*PP_inversion(T1),ass,inv*> is SFHT of D by NOMIN_4:16;
hence thesis by A79,A6,A7,A8,A9,A80,A81,A82,Th1;
end;
theorem Th5:
V is non empty & A is complex-containing & A is_without_nonatomicND_wrt V &
loc/.1, loc/.2, loc/.3, loc/.4, loc/.5 are_mutually_distinct
implies
<* power_inv(A,loc,b0,n0),
power_loop_body(A,loc),
power_inv(A,loc,b0,n0) *> is SFHT of ND(V,A)
proof
set i = loc/.1, j = loc/.2, b = loc/.3, n = loc/.4, s = loc/.5;
assume that
A1: V is non empty and
A2: A is complex-containing and
A3: A is_without_nonatomicND_wrt V and
A4: i,j,b,n,s are_mutually_distinct;
set D = ND(V,A);
set inv = power_inv(A,loc,b0,n0);
set L = power_loop_body(A,loc);
set add = addition(A,i,j);
set mlt = multiplication(A,s,b);
set f = SC_assignment(add,i);
set g = SC_assignment(mlt,s);
set Di = denaming(V,A,i);
set Dj = denaming(V,A,j);
set Db = denaming(V,A,b);
set Dn = denaming(V,A,n);
set Ds = denaming(V,A,s);
now
let d be TypeSCNominativeData of V,A such that
A5: d in dom inv and
A6: inv.d = TRUE and
A7: d in dom L and
A8: L.d in dom inv;
power_inv_pred A,loc,b0,n0,d by A5,A6,Def12;
then consider d1 being NonatomicND of V,A such that
A9: d = d1 and
A10: {i,j,b,n,s} c= dom d1 and
A11: d1.j = 1 and
A12: d1.b = b0 and
A13: d1.n = n0 and
A14: ex S being Complex, I being Nat st I = d1.i & S = d1.s & S = b0|^I;
A15: i in {i,j,b,n,s} by ENUMSET1:def 3;
A16: j in {i,j,b,n,s} by ENUMSET1:def 3;
A17: b in {i,j,b,n,s} by ENUMSET1:def 3;
A18: n in {i,j,b,n,s} by ENUMSET1:def 3;
A19: s in {i,j,b,n,s} by ENUMSET1:def 3;
consider S being Complex, I being Nat such that
A20: I = d1.i and
A22: S = d1.s and
A23: S = b0|^I by A14;
A24: dom f = dom add by NOMIN_2:def 7;
A25: dom g = dom mlt by NOMIN_2:def 7;
A26: PP_composition(f,g) = g*f by PARTPR_2:def 1;
then
A27: d in dom f by A7,FUNCT_1:11;
then reconsider Ad = add.d1 as TypeSCNominativeData of V,A
by A24,A9,PARTFUN1:4,NOMIN_1:39;
reconsider La = local_overlapping(V,A,d1,Ad,i)
as NonatomicND of V,A by NOMIN_2:9;
reconsider Lm = local_overlapping(V,A,La,mlt.La,s)
as NonatomicND of V,A by NOMIN_2:9;
L = g*f by PARTPR_2:def 1;
then
A28: L.d = g.(f.d) by A7,FUNCT_1:12;
A29: f.d = La by A9,A27,NOMIN_2:def 7;
then
A30: La in dom g by A7,A26,FUNCT_1:11;
A31: g.La = Lm by A30,NOMIN_2:def 7;
power_inv_pred A,loc,b0,n0,Lm
proof
take Lm;
thus Lm = Lm;
A32: mlt.La is TypeSCNominativeData of V,A by A25,A30,PARTFUN1:4,NOMIN_1:39;
A33: dom Lm = dom La \/ {s} by A3,A1,A25,A30,A31,NOMIN_4:5;
A34: dom La = {i} \/ dom d1 by A3,A1,NOMIN_4:4;
i in {i} by TARSKI:def 1;
then
A35: i in dom La by A34,XBOOLE_0:def 3;
then
A36: i in dom Lm by A33,XBOOLE_0:def 3;
A37: j in dom La by A10,A16,A34,XBOOLE_0:def 3;
then
A38: j in dom Lm by A33,XBOOLE_0:def 3;
A39: b in dom La by A17,A10,A34,XBOOLE_0:def 3;
then
A40: b in dom Lm by A33,XBOOLE_0:def 3;
A41: n in dom La by A10,A18,A34,XBOOLE_0:def 3;
then
A42: n in dom Lm by A33,XBOOLE_0:def 3;
s in {s} by TARSKI:def 1;
then s in dom Lm by A33,XBOOLE_0:def 3;
hence {i,j,b,n,s} c= dom Lm by A36,A38,A40,A42,ENUMSET1:def 3;
thus Lm.j = La.j by A1,A32,A3,A4,A37,NOMIN_5:3
.= 1 by A3,A1,A10,A16,A11,A4,NOMIN_5:3;
thus Lm.b = La.b by A1,A4,A32,A39,A3,NOMIN_5:3
.= b0 by A3,A1,A10,A4,A17,A12,NOMIN_5:3;
thus Lm.n = La.n by A4,A1,A32,A41,A3,NOMIN_5:3
.= n0 by A10,A3,A1,A4,A18,A13,NOMIN_5:3;
take S1 = S*b0, I1 = I+1;
La.i = Ad by A1,NOMIN_2:10
.= I1 by A15,A2,A10,A20,A11,A16,A9,A27,A24,NOMIN_5:4;
hence Lm.i = I1 by A1,A32,A3,A4,A35,NOMIN_5:3;
A43: s in dom La by A10,A19,A34,XBOOLE_0:def 3;
A44: La.s = d1.s by A3,A1,A10,A4,A19,NOMIN_5:3;
A45: La.b = d1.b by A3,A1,A10,A4,A17,NOMIN_5:3;
thus Lm.s = mlt.La by A1,A32,NOMIN_2:10
.= S1 by A39,A12,A45,A2,A22,A43,A25,A30,A44,NOMIN_5:5;
thus S1 = b0|^I1 by A23,NEWTON:6;
end;
hence inv.(L.d) = TRUE by A8,A28,A29,A31,Def12;
end;
hence thesis by NOMIN_3:28;
end;
::$CT
theorem Th7:
V is non empty & A is complex-containing & A is_without_nonatomicND_wrt V &
loc/.1, loc/.2, loc/.3, loc/.4, loc/.5 are_mutually_distinct
implies
<* power_inv(A,loc,b0,n0),
power_main_loop(A,loc),
PP_and(Equality(A,loc/.1,loc/.4),power_inv(A,loc,b0,n0)) *>
is SFHT of ND(V,A)
proof
set i = loc/.1, j = loc/.2, b = loc/.3, n = loc/.4, s = loc/.5;
set D = ND(V,A);
set inv = power_inv(A,loc,b0,n0);
set B = power_loop_body(A,loc);
set E = Equality(A,i,n);
assume V is non empty & A is complex-containing &
A is_without_nonatomicND_wrt V & i,j,b,n,s are_mutually_distinct;
then
A1: <*inv,B,inv*> is SFHT of D by Th5;
PP_and(PP_not(E),inv) ||= inv by NOMIN_3:3;
then
A2: <*PP_and(PP_not(E),inv),B,inv*> is SFHT of D by A1,NOMIN_3:15;
A3: <*PP_inversion(inv),B,inv*> is SFHT of D by NOMIN_3:19;
PP_and(PP_not(E),PP_inversion(inv)) ||= PP_inversion(inv) by NOMIN_3:3;
then <*PP_and(PP_not(E),PP_inversion(inv)),B,inv*> is SFHT of D
by A3,NOMIN_3:15;
hence thesis by A2,NOMIN_3:26;
end;
theorem Th8:
V is non empty & A is complex-containing & A is_without_nonatomicND_wrt V &
loc/.1, loc/.2, loc/.3, loc/.4, loc/.5 are_mutually_distinct &
loc,val are_compatible_wrt_5_locs
implies
<* valid_power_input(V,A,val,b0,n0),
power_main_part(A,loc,val),
PP_and(Equality(A,loc/.1,loc/.4),power_inv(A,loc,b0,n0)) *>
is SFHT of ND(V,A)
proof
set i = loc/.1, j = loc/.2, b = loc/.3, n = loc/.4, s = loc/.5;
set i1 = val.1, j1 = val.2, b1 = val.3, n1 = val.4, s1 = val.5;
set D = ND(V,A);
set p = valid_power_input(V,A,val,b0,n0);
set f = power_var_init(A,loc,val);
set g = power_main_loop(A,loc);
set q = power_inv(A,loc,b0,n0);
set r = PP_and(Equality(A,i,n),power_inv(A,loc,b0,n0));
assume
A1: V is non empty & A is complex-containing & A is_without_nonatomicND_wrt V &
i,j,b,n,s are_mutually_distinct & loc,val are_compatible_wrt_5_locs;
then
A2: <*p,f,q*> is SFHT of D by Th4;
A3: <*q,g,r*> is SFHT of D by A1,Th7;
<*PP_inversion(q),g,r*> is SFHT of D by NOMIN_3:19;
hence thesis by A2,A3,NOMIN_3:25;
end;
theorem Th9:
V is non empty & A is_without_nonatomicND_wrt V &
(for T holds loc/.1 is_a_value_on T) & (for T holds loc/.4 is_a_value_on T)
implies
PP_and(Equality(A,loc/.1,loc/.4),power_inv(A,loc,b0,n0))
||=
SC_Psuperpos(valid_power_output(A,z,b0,n0),denaming(V,A,loc/.5),z)
proof
set i = loc/.1, j = loc/.2, b = loc/.3, n = loc/.4, s = loc/.5;
set D = ND(V,A);
set inv = power_inv(A,loc,b0,n0);
set Di = denaming(V,A,i);
set Db = denaming(V,A,b);
set Dn = denaming(V,A,n);
set Ds = denaming(V,A,s);
set Dz = denaming(V,A,z);
set ass = SC_assignment(Ds,z);
set out = valid_power_output(A,z,b0,n0);
set p = SC_Psuperpos(out,Ds,z);
set E = Equality(A,i,n);
assume that
A1: V is non empty & A is_without_nonatomicND_wrt V and
A2: for T holds i is_a_value_on T and
A3: for T holds n is_a_value_on T;
let d be Element of D such that
A4: d in dom PP_and(E,inv) and
A5: (PP_and(E,inv)).d = TRUE;
A6: dom p = {d where d is TypeSCNominativeData of V,A:
local_overlapping(V,A,d,Ds.d,z) in dom out & d in dom Ds}
by NOMIN_2:def 11;
A7: dom out = {d where d is TypeSCNominativeData of V,A: d in dom Dz}
by Def10;
A8: dom Ds = {d where d is NonatomicND of V,A: s in dom d} by NOMIN_1:def 18;
A9: dom Dz = {d where d is NonatomicND of V,A: z in dom d} by NOMIN_1:def 18;
A10: d in dom E by A4,A5,PARTPR_1:23;
A11: d in dom inv by A4,A5,PARTPR_1:23;
A12: dom E = dom Di /\ dom Dn by A2,A3,NOMIN_4:11;
then
A13: d in dom Di by A10,XBOOLE_0:def 4;
inv.d = TRUE by A4,A5,PARTPR_1:23;
then power_inv_pred A,loc,b0,n0,d by A11,Def12;
then consider d1 being NonatomicND of V,A such that
A14: d = d1 and
A15: {i,j,b,n,s} c= dom d1 and
A16: d1.n = n0 and d1.b = b0 and
A18: ex S being Complex, I being Nat st I = d1.i & S = d1.s & S = b0|^I;
A19: i in {i,j,b,n,s} by ENUMSET1:def 3;
A20: n in {i,j,b,n,s} by ENUMSET1:def 3;
A21: s in {i,j,b,n,s} by ENUMSET1:def 3;
reconsider dd = d as TypeSCNominativeData of V,A by NOMIN_1:39;
set L = local_overlapping(V,A,dd,Ds.dd,z);
A22: dd in dom Ds by A15,A8,A14,A21;
then Ds.d1 in D by A14,PARTFUN1:4;
then
A23: ex d2 being TypeSCNominativeData of V,A st Ds.d1 = d2;
then
A24: L in dom Dz by A1,A14,NOMIN_4:6;
then
A25: L in dom out by A7;
hence
A26: d in dom p by A6,A22;
valid_power_output_pred A,z,b0,n0,L
proof
consider S being Complex, I being Nat such that
A27: I = d1.i and
A29: S = d1.s and
A30: S = b0|^I by A18;
A31: ex d being NonatomicND of V,A st L = d & z in dom d by A9,A24;
then reconsider dlo = L as NonatomicND of V,A;
take dlo;
thus L = dlo;
thus z in dom dlo by A31;
A32: i is_a_value_on dd by A2;
A33: n is_a_value_on dd by A3;
A34: dom <:Di,Dn:> = dom Di /\ dom Dn by FUNCT_3:def 7;
d in dom <:Di,Dn:> by A10,A12,FUNCT_3:def 7;
then
A35: E.d = (Equality(A)).(<:Di,Dn:>.d) by FUNCT_1:13;
A36: d in dom Dn by A10,A12,XBOOLE_0:def 4;
A37: <:Di,Dn:>.d = [Di.d,Dn.d] by A10,A12,A34,FUNCT_3:def 7;
A38: Di.d = denaming(i,d1) by A14,A13,NOMIN_1:def 18
.= d1.i by A15,A19,NOMIN_1:def 12;
A39: Dn.d = denaming(n,d1) by A14,A36,NOMIN_1:def 18
.= d1.n by A15,A20,NOMIN_1:def 12;
A40: Ds.d = denaming(s,d1) by A22,A14,NOMIN_1:def 18
.= d1.s by A15,A21,NOMIN_1:def 12;
(Equality(A)).(Di.d,Dn.d) <> FALSE by A4,A5,A35,A37,PARTPR_1:23;
then Di.d = Dn.d by A32,A33,NOMIN_4:def 9;
hence dlo.z = b0|^n0
by A1,A14,A16,A23,A27,A29,A30,A38,A39,A40,NOMIN_2:10;
end;
hence TRUE = out.L by A25,Def10
.= p.d by A26,NOMIN_2:35;
end;
theorem Th10:
V is non empty & A is_without_nonatomicND_wrt V &
(for T holds loc/.1 is_a_value_on T) & (for T holds loc/.4 is_a_value_on T)
implies
<* PP_and(Equality(A,loc/.1,loc/.4),power_inv(A,loc,b0,n0)),
SC_assignment(denaming(V,A,loc/.5),z),
valid_power_output(A,z,b0,n0) *> is SFHT of ND(V,A)
proof
set s = loc/.5;
<*SC_Psuperpos(valid_power_output(A,z,b0,n0),denaming(V,A,s),z),
SC_assignment(denaming(V,A,s),z),
valid_power_output(A,z,b0,n0)*> is SFHT of ND(V,A) by NOMIN_3:29;
hence thesis by Th9,NOMIN_3:15;
end;
theorem Th11:
(for T holds loc/.1 is_a_value_on T) & (for T holds loc/.4 is_a_value_on T)
implies
<* PP_inversion(PP_and(Equality(A,loc/.1,loc/.4),power_inv(A,loc,b0,n0))),
SC_assignment(denaming(V,A,loc/.5),z),
valid_power_output(A,z,b0,n0) *> is SFHT of ND(V,A)
proof
set i = loc/.1, j = loc/.2, b = loc/.3, n = loc/.4, s = loc/.5;
set D = ND(V,A);
set inv = power_inv(A,loc,b0,n0);
set O = valid_power_output(A,z,b0,n0);
set Di = denaming(V,A,i);
set Dn = denaming(V,A,n);
set Ds = denaming(V,A,s);
set g = SC_assignment(Ds,z);
set E = Equality(A,i,n);
set q = PP_and(E,inv);
set P = PP_inversion(q);
assume
A1: (for T holds i is_a_value_on T) & (for T holds n is_a_value_on T);
now
let d be TypeSCNominativeData of V,A such that
A2: d in dom P and
P.d = TRUE and
d in dom g and
g.d in dom O;
A3: dom q = {d where d is Element of D:
d in dom E & E.d = FALSE or d in dom inv & inv.d = FALSE
or d in dom E & E.d = TRUE & d in dom inv & inv.d = TRUE} by PARTPR_1:16;
A4: dom Di = {d where d is NonatomicND of V,A: i in dom d} by NOMIN_1:def 18;
A5: dom Dn = {d where d is NonatomicND of V,A: n in dom d} by NOMIN_1:def 18;
A6: dom E = dom Di /\ dom Dn by A1,NOMIN_4:11;
A7: not d in dom q by A2,PARTPR_2:9;
dom E c= dom q by PARTPR_2:3;
then not d in dom E by A2,PARTPR_2:9;
then
A8: not d in dom Di or not d in dom Dn by A6,XBOOLE_0:def 4;
dom inv = D by Def12;
then
A9: d in dom inv;
then inv.d <> FALSE by A3,A7;
then power_inv_pred A,loc,b0,n0,d by A9,Def12;
then consider d1 being NonatomicND of V,A such that
A10: d = d1 & {i,j,b,n,s} c= dom d1 and
d1.(loc/.2) = 1 & d1.(loc/.3) = b0 & d1.(loc/.4) = n0 &
ex S being Complex, I being Nat st I = d1.(loc/.1)
& S = d1.(loc/.5) & S = b0|^I;
i in {i,j,b,n,s} & n in {i,j,b,n,s} by ENUMSET1:def 3;
hence O.(g.d) = TRUE by A4,A5,A8,A10;
end;
hence thesis by NOMIN_3:28;
end;
::$N Partial correctness of a POWER algorithm
theorem
V is non empty & A is complex-containing & A is_without_nonatomicND_wrt V &
loc/.1, loc/.2, loc/.3, loc/.4, loc/.5 are_mutually_distinct &
loc,val are_compatible_wrt_5_locs &
(for T holds loc/.1 is_a_value_on T) & (for T holds loc/.4 is_a_value_on T)
implies
<* valid_power_input(V,A,val,b0,n0),
power_program(A,loc,val,z),
valid_power_output(A,z,b0,n0) *>
is SFHT of ND(V,A)
proof
set i = loc/.1, j = loc/.2, b = loc/.3, n = loc/.4, s = loc/.5;
set D = ND(V,A);
set p = valid_power_input(V,A,val,b0,n0);
set f = power_main_part(A,loc,val);
set g = SC_assignment(denaming(V,A,s),z);
set q = valid_power_output(A,z,b0,n0);
set inv = power_inv(A,loc,b0,n0);
set E = Equality(A,i,n);
assume that
A1: V is non empty & A is complex-containing & A is_without_nonatomicND_wrt V
& i,j,b,n,s are_mutually_distinct and
A2: loc,val are_compatible_wrt_5_locs and
A3: (for T holds i is_a_value_on T) & (for T holds n is_a_value_on T);
A4: <*p,f,PP_and(E,inv)*> is SFHT of D by A1,A2,Th8;
A5: <*PP_and(E,inv),g,q*> is SFHT of D by A1,A3,Th10;
<*PP_inversion(PP_and(E,inv)),g,q*> is SFHT of D by A3,Th11;
hence thesis by A4,A5,NOMIN_3:25;
end;