let V, A be set ; :: thesis: for loc being V -valued Function
for d1 being NonatomicND of V,A st not V is empty & A is complex-containing & A is_without_nonatomicND_wrt V & d1 in dom (Lucas_loop_body (A,loc)) & loc is_valid_wrt d1 & Seg 10 c= dom loc & ( for T being TypeSCNominativeData of V,A holds
( loc /. 1 is_a_value_on T & loc /. 2 is_a_value_on T & loc /. 4 is_a_value_on T & loc /. 6 is_a_value_on T & loc /. 7 is_a_value_on T & loc /. 8 is_a_value_on T & loc /. 9 is_a_value_on T & loc /. 10 is_a_value_on T ) ) holds
prg_doms_of loc,d1,<*(denaming (V,A,(loc /. 4))),(denaming (V,A,(loc /. 5))),(multiplication (A,(loc /. 7),(loc /. 4))),(multiplication (A,(loc /. 8),(loc /. 6))),(subtraction (A,(loc /. 9),(loc /. 10))),(addition (A,(loc /. 1),(loc /. 2)))*>,<*6,4,9,10,5,1*>
let loc be V -valued Function; :: thesis: for d1 being NonatomicND of V,A st not V is empty & A is complex-containing & A is_without_nonatomicND_wrt V & d1 in dom (Lucas_loop_body (A,loc)) & loc is_valid_wrt d1 & Seg 10 c= dom loc & ( for T being TypeSCNominativeData of V,A holds
( loc /. 1 is_a_value_on T & loc /. 2 is_a_value_on T & loc /. 4 is_a_value_on T & loc /. 6 is_a_value_on T & loc /. 7 is_a_value_on T & loc /. 8 is_a_value_on T & loc /. 9 is_a_value_on T & loc /. 10 is_a_value_on T ) ) holds
prg_doms_of loc,d1,<*(denaming (V,A,(loc /. 4))),(denaming (V,A,(loc /. 5))),(multiplication (A,(loc /. 7),(loc /. 4))),(multiplication (A,(loc /. 8),(loc /. 6))),(subtraction (A,(loc /. 9),(loc /. 10))),(addition (A,(loc /. 1),(loc /. 2)))*>,<*6,4,9,10,5,1*>
let d1 be NonatomicND of V,A; :: thesis: ( not V is empty & A is complex-containing & A is_without_nonatomicND_wrt V & d1 in dom (Lucas_loop_body (A,loc)) & loc is_valid_wrt d1 & Seg 10 c= dom loc & ( for T being TypeSCNominativeData of V,A holds
( loc /. 1 is_a_value_on T & loc /. 2 is_a_value_on T & loc /. 4 is_a_value_on T & loc /. 6 is_a_value_on T & loc /. 7 is_a_value_on T & loc /. 8 is_a_value_on T & loc /. 9 is_a_value_on T & loc /. 10 is_a_value_on T ) ) implies prg_doms_of loc,d1,<*(denaming (V,A,(loc /. 4))),(denaming (V,A,(loc /. 5))),(multiplication (A,(loc /. 7),(loc /. 4))),(multiplication (A,(loc /. 8),(loc /. 6))),(subtraction (A,(loc /. 9),(loc /. 10))),(addition (A,(loc /. 1),(loc /. 2)))*>,<*6,4,9,10,5,1*> )
set i = loc /. 1;
set j = loc /. 2;
set n = loc /. 3;
set s = loc /. 4;
set b = loc /. 5;
set c = loc /. 6;
set p = loc /. 7;
set q = loc /. 8;
set ps = loc /. 9;
set qc = loc /. 10;
set B = Lucas_loop_body (A,loc);
assume that
A1: not V is empty and
A2: A is complex-containing and
A3: A is_without_nonatomicND_wrt V and
A4: d1 in dom (Lucas_loop_body (A,loc)) and
A5: loc is_valid_wrt d1 and
A6: Seg 10 c= dom loc and
A7: for T being TypeSCNominativeData of V,A holds
( loc /. 1 is_a_value_on T & loc /. 2 is_a_value_on T & loc /. 4 is_a_value_on T & loc /. 6 is_a_value_on T & loc /. 7 is_a_value_on T & loc /. 8 is_a_value_on T & loc /. 9 is_a_value_on T & loc /. 10 is_a_value_on T ) ; :: thesis: prg_doms_of loc,d1,<*(denaming (V,A,(loc /. 4))),(denaming (V,A,(loc /. 5))),(multiplication (A,(loc /. 7),(loc /. 4))),(multiplication (A,(loc /. 8),(loc /. 6))),(subtraction (A,(loc /. 9),(loc /. 10))),(addition (A,(loc /. 1),(loc /. 2)))*>,<*6,4,9,10,5,1*>
set D = ND (V,A);
set EN = {(loc /. 1),(loc /. 2),(loc /. 3),(loc /. 4),(loc /. 5),(loc /. 6),(loc /. 7),(loc /. 8),(loc /. 9),(loc /. 10)};
set Di = denaming (V,A,(loc /. 1));
set Dj = denaming (V,A,(loc /. 2));
set Dn = denaming (V,A,(loc /. 3));
set Ds = denaming (V,A,(loc /. 4));
set Db = denaming (V,A,(loc /. 5));
set Dc = denaming (V,A,(loc /. 6));
set Dp = denaming (V,A,(loc /. 7));
set Dq = denaming (V,A,(loc /. 8));
set Dps = denaming (V,A,(loc /. 9));
set Dqc = denaming (V,A,(loc /. 10));
set Aij = addition (A,(loc /. 1),(loc /. 2));
set Mps = multiplication (A,(loc /. 7),(loc /. 4));
set Mqc = multiplication (A,(loc /. 8),(loc /. 6));
set Scs = subtraction (A,(loc /. 9),(loc /. 10));
set AS1 = SC_assignment ((denaming (V,A,(loc /. 4))),(loc /. 6));
set AS2 = SC_assignment ((denaming (V,A,(loc /. 5))),(loc /. 4));
set AS3 = SC_assignment ((multiplication (A,(loc /. 7),(loc /. 4))),(loc /. 9));
set AS4 = SC_assignment ((multiplication (A,(loc /. 8),(loc /. 6))),(loc /. 10));
set AS5 = SC_assignment ((subtraction (A,(loc /. 9),(loc /. 10))),(loc /. 5));
set AS6 = SC_assignment ((addition (A,(loc /. 1),(loc /. 2))),(loc /. 1));
set prg = <*(denaming (V,A,(loc /. 4))),(denaming (V,A,(loc /. 5))),(multiplication (A,(loc /. 7),(loc /. 4))),(multiplication (A,(loc /. 8),(loc /. 6))),(subtraction (A,(loc /. 9),(loc /. 10))),(addition (A,(loc /. 1),(loc /. 2)))*>;
set pos = <*6,4,9,10,5,1*>;
set PS = PrgLocalOverlapSeq (A,loc,d1,<*(denaming (V,A,(loc /. 4))),(denaming (V,A,(loc /. 5))),(multiplication (A,(loc /. 7),(loc /. 4))),(multiplication (A,(loc /. 8),(loc /. 6))),(subtraction (A,(loc /. 9),(loc /. 10))),(addition (A,(loc /. 1),(loc /. 2)))*>,<*6,4,9,10,5,1*>);
A8: {(loc /. 1),(loc /. 2),(loc /. 3),(loc /. 4),(loc /. 5),(loc /. 6),(loc /. 7),(loc /. 8),(loc /. 9),(loc /. 10)} c= dom d1 by A5, A6, Th12;
A9: loc /. 1 in {(loc /. 1),(loc /. 2),(loc /. 3),(loc /. 4),(loc /. 5),(loc /. 6),(loc /. 7),(loc /. 8),(loc /. 9),(loc /. 10)} by ENUMSET1:def 8;
A10: loc /. 2 in {(loc /. 1),(loc /. 2),(loc /. 3),(loc /. 4),(loc /. 5),(loc /. 6),(loc /. 7),(loc /. 8),(loc /. 9),(loc /. 10)} by ENUMSET1:def 8;
A11: loc /. 5 in {(loc /. 1),(loc /. 2),(loc /. 3),(loc /. 4),(loc /. 5),(loc /. 6),(loc /. 7),(loc /. 8),(loc /. 9),(loc /. 10)} by ENUMSET1:def 8;
A12: loc /. 7 in {(loc /. 1),(loc /. 2),(loc /. 3),(loc /. 4),(loc /. 5),(loc /. 6),(loc /. 7),(loc /. 8),(loc /. 9),(loc /. 10)} by ENUMSET1:def 8;
A13: loc /. 8 in {(loc /. 1),(loc /. 2),(loc /. 3),(loc /. 4),(loc /. 5),(loc /. 6),(loc /. 7),(loc /. 8),(loc /. 9),(loc /. 10)} by ENUMSET1:def 8;
A14: len <*(denaming (V,A,(loc /. 4))),(denaming (V,A,(loc /. 5))),(multiplication (A,(loc /. 7),(loc /. 4))),(multiplication (A,(loc /. 8),(loc /. 6))),(subtraction (A,(loc /. 9),(loc /. 10))),(addition (A,(loc /. 1),(loc /. 2)))*> = 6 by AOFA_A00:20;
A15: len (PrgLocalOverlapSeq (A,loc,d1,<*(denaming (V,A,(loc /. 4))),(denaming (V,A,(loc /. 5))),(multiplication (A,(loc /. 7),(loc /. 4))),(multiplication (A,(loc /. 8),(loc /. 6))),(subtraction (A,(loc /. 9),(loc /. 10))),(addition (A,(loc /. 1),(loc /. 2)))*>,<*6,4,9,10,5,1*>)) = len <*(denaming (V,A,(loc /. 4))),(denaming (V,A,(loc /. 5))),(multiplication (A,(loc /. 7),(loc /. 4))),(multiplication (A,(loc /. 8),(loc /. 6))),(subtraction (A,(loc /. 9),(loc /. 10))),(addition (A,(loc /. 1),(loc /. 2)))*> by NOMIN_8:def 14;
A16: ( <*(denaming (V,A,(loc /. 4))),(denaming (V,A,(loc /. 5))),(multiplication (A,(loc /. 7),(loc /. 4))),(multiplication (A,(loc /. 8),(loc /. 6))),(subtraction (A,(loc /. 9),(loc /. 10))),(addition (A,(loc /. 1),(loc /. 2)))*> . 1 = denaming (V,A,(loc /. 4)) & <*6,4,9,10,5,1*> . 1 = 6 ) ;
A17: ( <*(denaming (V,A,(loc /. 4))),(denaming (V,A,(loc /. 5))),(multiplication (A,(loc /. 7),(loc /. 4))),(multiplication (A,(loc /. 8),(loc /. 6))),(subtraction (A,(loc /. 9),(loc /. 10))),(addition (A,(loc /. 1),(loc /. 2)))*> . 2 = denaming (V,A,(loc /. 5)) & <*6,4,9,10,5,1*> . 2 = 4 ) ;
A18: ( <*(denaming (V,A,(loc /. 4))),(denaming (V,A,(loc /. 5))),(multiplication (A,(loc /. 7),(loc /. 4))),(multiplication (A,(loc /. 8),(loc /. 6))),(subtraction (A,(loc /. 9),(loc /. 10))),(addition (A,(loc /. 1),(loc /. 2)))*> . 3 = multiplication (A,(loc /. 7),(loc /. 4)) & <*6,4,9,10,5,1*> . 3 = 9 ) ;
A19: ( <*(denaming (V,A,(loc /. 4))),(denaming (V,A,(loc /. 5))),(multiplication (A,(loc /. 7),(loc /. 4))),(multiplication (A,(loc /. 8),(loc /. 6))),(subtraction (A,(loc /. 9),(loc /. 10))),(addition (A,(loc /. 1),(loc /. 2)))*> . 4 = multiplication (A,(loc /. 8),(loc /. 6)) & <*6,4,9,10,5,1*> . 4 = 10 ) ;
A20: ( <*(denaming (V,A,(loc /. 4))),(denaming (V,A,(loc /. 5))),(multiplication (A,(loc /. 7),(loc /. 4))),(multiplication (A,(loc /. 8),(loc /. 6))),(subtraction (A,(loc /. 9),(loc /. 10))),(addition (A,(loc /. 1),(loc /. 2)))*> . 5 = subtraction (A,(loc /. 9),(loc /. 10)) & <*6,4,9,10,5,1*> . 5 = 5 ) ;
A21: dom (SC_assignment ((denaming (V,A,(loc /. 4))),(loc /. 6))) = dom (denaming (V,A,(loc /. 4))) by NOMIN_2:def 7;
A22: dom (SC_assignment ((denaming (V,A,(loc /. 5))),(loc /. 4))) = dom (denaming (V,A,(loc /. 5))) by NOMIN_2:def 7;
PP_composition ((PP_composition ((PP_composition ((PP_composition ((SC_assignment ((denaming (V,A,(loc /. 4))),(loc /. 6))),(SC_assignment ((denaming (V,A,(loc /. 5))),(loc /. 4))))),(SC_assignment ((multiplication (A,(loc /. 7),(loc /. 4))),(loc /. 9))))),(SC_assignment ((multiplication (A,(loc /. 8),(loc /. 6))),(loc /. 10))))),(SC_assignment ((subtraction (A,(loc /. 9),(loc /. 10))),(loc /. 5)))) = PP_composition ((PP_composition ((PP_composition (((SC_assignment ((denaming (V,A,(loc /. 5))),(loc /. 4))) * (SC_assignment ((denaming (V,A,(loc /. 4))),(loc /. 6)))),(SC_assignment ((multiplication (A,(loc /. 7),(loc /. 4))),(loc /. 9))))),(SC_assignment ((multiplication (A,(loc /. 8),(loc /. 6))),(loc /. 10))))),(SC_assignment ((subtraction (A,(loc /. 9),(loc /. 10))),(loc /. 5)))) by PARTPR_2:def 1
.= PP_composition ((PP_composition (((SC_assignment ((multiplication (A,(loc /. 7),(loc /. 4))),(loc /. 9))) * ((SC_assignment ((denaming (V,A,(loc /. 5))),(loc /. 4))) * (SC_assignment ((denaming (V,A,(loc /. 4))),(loc /. 6))))),(SC_assignment ((multiplication (A,(loc /. 8),(loc /. 6))),(loc /. 10))))),(SC_assignment ((subtraction (A,(loc /. 9),(loc /. 10))),(loc /. 5)))) by PARTPR_2:def 1
.= PP_composition (((SC_assignment ((multiplication (A,(loc /. 8),(loc /. 6))),(loc /. 10))) * ((SC_assignment ((multiplication (A,(loc /. 7),(loc /. 4))),(loc /. 9))) * ((SC_assignment ((denaming (V,A,(loc /. 5))),(loc /. 4))) * (SC_assignment ((denaming (V,A,(loc /. 4))),(loc /. 6)))))),(SC_assignment ((subtraction (A,(loc /. 9),(loc /. 10))),(loc /. 5)))) by PARTPR_2:def 1
.= (SC_assignment ((subtraction (A,(loc /. 9),(loc /. 10))),(loc /. 5))) * ((SC_assignment ((multiplication (A,(loc /. 8),(loc /. 6))),(loc /. 10))) * ((SC_assignment ((multiplication (A,(loc /. 7),(loc /. 4))),(loc /. 9))) * ((SC_assignment ((denaming (V,A,(loc /. 5))),(loc /. 4))) * (SC_assignment ((denaming (V,A,(loc /. 4))),(loc /. 6)))))) by PARTPR_2:def 1 ;
then A23: Lucas_loop_body (A,loc) = (SC_assignment ((addition (A,(loc /. 1),(loc /. 2))),(loc /. 1))) * ((SC_assignment ((subtraction (A,(loc /. 9),(loc /. 10))),(loc /. 5))) * ((SC_assignment ((multiplication (A,(loc /. 8),(loc /. 6))),(loc /. 10))) * ((SC_assignment ((multiplication (A,(loc /. 7),(loc /. 4))),(loc /. 9))) * ((SC_assignment ((denaming (V,A,(loc /. 5))),(loc /. 4))) * (SC_assignment ((denaming (V,A,(loc /. 4))),(loc /. 6))))))) by PARTPR_2:def 1;
A24: ((((SC_assignment ((subtraction (A,(loc /. 9),(loc /. 10))),(loc /. 5))) * (SC_assignment ((multiplication (A,(loc /. 8),(loc /. 6))),(loc /. 10)))) * (SC_assignment ((multiplication (A,(loc /. 7),(loc /. 4))),(loc /. 9)))) * (SC_assignment ((denaming (V,A,(loc /. 5))),(loc /. 4)))) * (SC_assignment ((denaming (V,A,(loc /. 4))),(loc /. 6))) = (((SC_assignment ((subtraction (A,(loc /. 9),(loc /. 10))),(loc /. 5))) * (SC_assignment ((multiplication (A,(loc /. 8),(loc /. 6))),(loc /. 10)))) * (SC_assignment ((multiplication (A,(loc /. 7),(loc /. 4))),(loc /. 9)))) * ((SC_assignment ((denaming (V,A,(loc /. 5))),(loc /. 4))) * (SC_assignment ((denaming (V,A,(loc /. 4))),(loc /. 6)))) by RELAT_1:36
.= ((SC_assignment ((subtraction (A,(loc /. 9),(loc /. 10))),(loc /. 5))) * (SC_assignment ((multiplication (A,(loc /. 8),(loc /. 6))),(loc /. 10)))) * ((SC_assignment ((multiplication (A,(loc /. 7),(loc /. 4))),(loc /. 9))) * ((SC_assignment ((denaming (V,A,(loc /. 5))),(loc /. 4))) * (SC_assignment ((denaming (V,A,(loc /. 4))),(loc /. 6))))) by RELAT_1:36
.= (SC_assignment ((subtraction (A,(loc /. 9),(loc /. 10))),(loc /. 5))) * ((SC_assignment ((multiplication (A,(loc /. 8),(loc /. 6))),(loc /. 10))) * ((SC_assignment ((multiplication (A,(loc /. 7),(loc /. 4))),(loc /. 9))) * ((SC_assignment ((denaming (V,A,(loc /. 5))),(loc /. 4))) * (SC_assignment ((denaming (V,A,(loc /. 4))),(loc /. 6)))))) by RELAT_1:36 ;
A25: (SC_assignment ((subtraction (A,(loc /. 9),(loc /. 10))),(loc /. 5))) * ((SC_assignment ((multiplication (A,(loc /. 8),(loc /. 6))),(loc /. 10))) * ((SC_assignment ((multiplication (A,(loc /. 7),(loc /. 4))),(loc /. 9))) * ((SC_assignment ((denaming (V,A,(loc /. 5))),(loc /. 4))) * (SC_assignment ((denaming (V,A,(loc /. 4))),(loc /. 6)))))) = (SC_assignment ((subtraction (A,(loc /. 9),(loc /. 10))),(loc /. 5))) * (((SC_assignment ((multiplication (A,(loc /. 8),(loc /. 6))),(loc /. 10))) * (SC_assignment ((multiplication (A,(loc /. 7),(loc /. 4))),(loc /. 9)))) * ((SC_assignment ((denaming (V,A,(loc /. 5))),(loc /. 4))) * (SC_assignment ((denaming (V,A,(loc /. 4))),(loc /. 6))))) by RELAT_1:36
.= (SC_assignment ((subtraction (A,(loc /. 9),(loc /. 10))),(loc /. 5))) * ((((SC_assignment ((multiplication (A,(loc /. 8),(loc /. 6))),(loc /. 10))) * (SC_assignment ((multiplication (A,(loc /. 7),(loc /. 4))),(loc /. 9)))) * (SC_assignment ((denaming (V,A,(loc /. 5))),(loc /. 4)))) * (SC_assignment ((denaming (V,A,(loc /. 4))),(loc /. 6)))) by RELAT_1:36 ;
A26: (((SC_assignment ((multiplication (A,(loc /. 8),(loc /. 6))),(loc /. 10))) * (SC_assignment ((multiplication (A,(loc /. 7),(loc /. 4))),(loc /. 9)))) * (SC_assignment ((denaming (V,A,(loc /. 5))),(loc /. 4)))) * (SC_assignment ((denaming (V,A,(loc /. 4))),(loc /. 6))) = ((SC_assignment ((multiplication (A,(loc /. 8),(loc /. 6))),(loc /. 10))) * (SC_assignment ((multiplication (A,(loc /. 7),(loc /. 4))),(loc /. 9)))) * ((SC_assignment ((denaming (V,A,(loc /. 5))),(loc /. 4))) * (SC_assignment ((denaming (V,A,(loc /. 4))),(loc /. 6)))) by RELAT_1:36
.= (SC_assignment ((multiplication (A,(loc /. 8),(loc /. 6))),(loc /. 10))) * ((SC_assignment ((multiplication (A,(loc /. 7),(loc /. 4))),(loc /. 9))) * ((SC_assignment ((denaming (V,A,(loc /. 5))),(loc /. 4))) * (SC_assignment ((denaming (V,A,(loc /. 4))),(loc /. 6))))) by RELAT_1:36 ;
A27: (SC_assignment ((multiplication (A,(loc /. 8),(loc /. 6))),(loc /. 10))) * ((SC_assignment ((multiplication (A,(loc /. 7),(loc /. 4))),(loc /. 9))) * ((SC_assignment ((denaming (V,A,(loc /. 5))),(loc /. 4))) * (SC_assignment ((denaming (V,A,(loc /. 4))),(loc /. 6))))) = (SC_assignment ((multiplication (A,(loc /. 8),(loc /. 6))),(loc /. 10))) * (((SC_assignment ((multiplication (A,(loc /. 7),(loc /. 4))),(loc /. 9))) * (SC_assignment ((denaming (V,A,(loc /. 5))),(loc /. 4)))) * (SC_assignment ((denaming (V,A,(loc /. 4))),(loc /. 6)))) by RELAT_1:36;
A28: ((SC_assignment ((multiplication (A,(loc /. 7),(loc /. 4))),(loc /. 9))) * (SC_assignment ((denaming (V,A,(loc /. 5))),(loc /. 4)))) * (SC_assignment ((denaming (V,A,(loc /. 4))),(loc /. 6))) = (SC_assignment ((multiplication (A,(loc /. 7),(loc /. 4))),(loc /. 9))) * ((SC_assignment ((denaming (V,A,(loc /. 5))),(loc /. 4))) * (SC_assignment ((denaming (V,A,(loc /. 4))),(loc /. 6)))) by RELAT_1:36;
Lucas_loop_body (A,loc) = (SC_assignment ((addition (A,(loc /. 1),(loc /. 2))),(loc /. 1))) * (((SC_assignment ((subtraction (A,(loc /. 9),(loc /. 10))),(loc /. 5))) * (SC_assignment ((multiplication (A,(loc /. 8),(loc /. 6))),(loc /. 10)))) * ((SC_assignment ((multiplication (A,(loc /. 7),(loc /. 4))),(loc /. 9))) * ((SC_assignment ((denaming (V,A,(loc /. 5))),(loc /. 4))) * (SC_assignment ((denaming (V,A,(loc /. 4))),(loc /. 6)))))) by A23, RELAT_1:36
.= (SC_assignment ((addition (A,(loc /. 1),(loc /. 2))),(loc /. 1))) * ((((SC_assignment ((subtraction (A,(loc /. 9),(loc /. 10))),(loc /. 5))) * (SC_assignment ((multiplication (A,(loc /. 8),(loc /. 6))),(loc /. 10)))) * (SC_assignment ((multiplication (A,(loc /. 7),(loc /. 4))),(loc /. 9)))) * ((SC_assignment ((denaming (V,A,(loc /. 5))),(loc /. 4))) * (SC_assignment ((denaming (V,A,(loc /. 4))),(loc /. 6))))) by RELAT_1:36
.= (SC_assignment ((addition (A,(loc /. 1),(loc /. 2))),(loc /. 1))) * (((((SC_assignment ((subtraction (A,(loc /. 9),(loc /. 10))),(loc /. 5))) * (SC_assignment ((multiplication (A,(loc /. 8),(loc /. 6))),(loc /. 10)))) * (SC_assignment ((multiplication (A,(loc /. 7),(loc /. 4))),(loc /. 9)))) * (SC_assignment ((denaming (V,A,(loc /. 5))),(loc /. 4)))) * (SC_assignment ((denaming (V,A,(loc /. 4))),(loc /. 6)))) by RELAT_1:36 ;
then A29: d1 in dom (((((SC_assignment ((subtraction (A,(loc /. 9),(loc /. 10))),(loc /. 5))) * (SC_assignment ((multiplication (A,(loc /. 8),(loc /. 6))),(loc /. 10)))) * (SC_assignment ((multiplication (A,(loc /. 7),(loc /. 4))),(loc /. 9)))) * (SC_assignment ((denaming (V,A,(loc /. 5))),(loc /. 4)))) * (SC_assignment ((denaming (V,A,(loc /. 4))),(loc /. 6)))) by A4, FUNCT_1:11;
then d1 in dom ((((SC_assignment ((multiplication (A,(loc /. 8),(loc /. 6))),(loc /. 10))) * (SC_assignment ((multiplication (A,(loc /. 7),(loc /. 4))),(loc /. 9)))) * (SC_assignment ((denaming (V,A,(loc /. 5))),(loc /. 4)))) * (SC_assignment ((denaming (V,A,(loc /. 4))),(loc /. 6)))) by A24, A25, FUNCT_1:11;
then d1 in dom (((SC_assignment ((multiplication (A,(loc /. 7),(loc /. 4))),(loc /. 9))) * (SC_assignment ((denaming (V,A,(loc /. 5))),(loc /. 4)))) * (SC_assignment ((denaming (V,A,(loc /. 4))),(loc /. 6)))) by A26, A27, FUNCT_1:11;
then A30: d1 in dom ((SC_assignment ((denaming (V,A,(loc /. 5))),(loc /. 4))) * (SC_assignment ((denaming (V,A,(loc /. 4))),(loc /. 6)))) by A28, FUNCT_1:11;
A31: dom (denaming (V,A,(loc /. 1))) = { d where d is NonatomicND of V,A : loc /. 1 in dom d } by NOMIN_1:def 18;
A32: dom (denaming (V,A,(loc /. 2))) = { d where d is NonatomicND of V,A : loc /. 2 in dom d } by NOMIN_1:def 18;
A33: dom (denaming (V,A,(loc /. 4))) = { d where d is NonatomicND of V,A : loc /. 4 in dom d } by NOMIN_1:def 18;
A34: dom (denaming (V,A,(loc /. 5))) = { d where d is NonatomicND of V,A : loc /. 5 in dom d } by NOMIN_1:def 18;
A35: dom (denaming (V,A,(loc /. 6))) = { d where d is NonatomicND of V,A : loc /. 6 in dom d } by NOMIN_1:def 18;
A36: dom (denaming (V,A,(loc /. 7))) = { d where d is NonatomicND of V,A : loc /. 7 in dom d } by NOMIN_1:def 18;
A37: dom (denaming (V,A,(loc /. 8))) = { d where d is NonatomicND of V,A : loc /. 8 in dom d } by NOMIN_1:def 18;
A38: dom (denaming (V,A,(loc /. 9))) = { d where d is NonatomicND of V,A : loc /. 9 in dom d } by NOMIN_1:def 18;
A39: dom (denaming (V,A,(loc /. 10))) = { d where d is NonatomicND of V,A : loc /. 10 in dom d } by NOMIN_1:def 18;
A40: d1 in dom (denaming (V,A,(loc /. 4))) by A21, A29, FUNCT_1:11;
then reconsider Ad = (denaming (V,A,(loc /. 4))) . d1 as TypeSCNominativeData of V,A by PARTFUN1:4, NOMIN_1:39;
reconsider L1 = local_overlapping (V,A,d1,Ad,(loc /. 6)) as NonatomicND of V,A by NOMIN_2:9;
(SC_assignment ((denaming (V,A,(loc /. 4))),(loc /. 6))) . d1 = L1 by A21, A40, NOMIN_2:def 7;
then L1 in dom (SC_assignment ((denaming (V,A,(loc /. 5))),(loc /. 4))) by A30, FUNCT_1:11;
then reconsider DbL1 = (denaming (V,A,(loc /. 5))) . L1 as TypeSCNominativeData of V,A by A22, PARTFUN1:4, NOMIN_1:39;
reconsider L2 = local_overlapping (V,A,L1,DbL1,(loc /. 4)) as NonatomicND of V,A by NOMIN_2:9;
A41: dom L1 = {(loc /. 6)} \/ (dom d1) by A3, A1, NOMIN_4:4;
A42: dom L2 = {(loc /. 4)} \/ (dom L1) by A3, A1, NOMIN_4:4;
loc /. 4 in {(loc /. 4)} by TARSKI:def 1;
then loc /. 4 in dom L2 by A42, XBOOLE_0:def 3;
then A43: L2 in dom (denaming (V,A,(loc /. 4))) by A33;
loc /. 7 in dom L1 by A8, A12, A41, XBOOLE_0:def 3;
then loc /. 7 in dom L2 by A42, XBOOLE_0:def 3;
then L2 in dom (denaming (V,A,(loc /. 7))) by A36;
then L2 in (dom (denaming (V,A,(loc /. 4)))) /\ (dom (denaming (V,A,(loc /. 7)))) by A43, XBOOLE_0:def 4;
then A44: L2 in dom <:(denaming (V,A,(loc /. 7))),(denaming (V,A,(loc /. 4))):> by FUNCT_3:def 7;
then A45: <:(denaming (V,A,(loc /. 7))),(denaming (V,A,(loc /. 4))):> . L2 = [((denaming (V,A,(loc /. 7))) . L2),((denaming (V,A,(loc /. 4))) . L2)] by FUNCT_3:def 7;
A46: dom (multiplication A) = [:A,A:] by A2, FUNCT_2:def 1;
( loc /. 7 is_a_value_on L2 & loc /. 4 is_a_value_on L2 ) by A7;
then [((denaming (V,A,(loc /. 7))) . L2),((denaming (V,A,(loc /. 4))) . L2)] in [:A,A:] by ZFMISC_1:87;
then A47: L2 in dom (multiplication (A,(loc /. 7),(loc /. 4))) by A44, A46, A45, FUNCT_1:11;
then reconsider MpsL2 = (multiplication (A,(loc /. 7),(loc /. 4))) . L2 as TypeSCNominativeData of V,A by PARTFUN1:4, NOMIN_1:39;
reconsider L3 = local_overlapping (V,A,L2,MpsL2,(loc /. 9)) as NonatomicND of V,A by NOMIN_2:9;
A48: dom L3 = {(loc /. 9)} \/ (dom L2) by A1, A3, NOMIN_4:4;
loc /. 8 in dom L1 by A8, A13, A41, XBOOLE_0:def 3;
then loc /. 8 in dom L2 by A42, XBOOLE_0:def 3;
then A49: loc /. 8 in dom L3 by A48, XBOOLE_0:def 3;
loc /. 6 in {(loc /. 6)} by TARSKI:def 1;
then loc /. 6 in dom L1 by A41, XBOOLE_0:def 3;
then loc /. 6 in dom L2 by A42, XBOOLE_0:def 3;
then A50: loc /. 6 in dom L3 by A48, XBOOLE_0:def 3;
A51: L3 in dom (denaming (V,A,(loc /. 8))) by A49, A37;
L3 in dom (denaming (V,A,(loc /. 6))) by A50, A35;
then L3 in (dom (denaming (V,A,(loc /. 8)))) /\ (dom (denaming (V,A,(loc /. 6)))) by A51, XBOOLE_0:def 4;
then A52: L3 in dom <:(denaming (V,A,(loc /. 8))),(denaming (V,A,(loc /. 6))):> by FUNCT_3:def 7;
then A53: <:(denaming (V,A,(loc /. 8))),(denaming (V,A,(loc /. 6))):> . L3 = [((denaming (V,A,(loc /. 8))) . L3),((denaming (V,A,(loc /. 6))) . L3)] by FUNCT_3:def 7;
( loc /. 8 is_a_value_on L3 & loc /. 6 is_a_value_on L3 ) by A7;
then [((denaming (V,A,(loc /. 8))) . L3),((denaming (V,A,(loc /. 6))) . L3)] in [:A,A:] by ZFMISC_1:87;
then A54: L3 in dom (multiplication (A,(loc /. 8),(loc /. 6))) by A52, A46, A53, FUNCT_1:11;
then reconsider MqcL3 = (multiplication (A,(loc /. 8),(loc /. 6))) . L3 as TypeSCNominativeData of V,A by PARTFUN1:4, NOMIN_1:39;
reconsider L4 = local_overlapping (V,A,L3,MqcL3,(loc /. 10)) as NonatomicND of V,A by NOMIN_2:9;
A55: dom L4 = {(loc /. 10)} \/ (dom L3) by A1, A3, NOMIN_4:4;
loc /. 10 in {(loc /. 10)} by TARSKI:def 1;
then A56: loc /. 10 in dom L4 by A55, XBOOLE_0:def 3;
loc /. 9 in {(loc /. 9)} by TARSKI:def 1;
then loc /. 9 in dom L3 by A48, XBOOLE_0:def 3;
then A57: loc /. 9 in dom L4 by A55, XBOOLE_0:def 3;
A58: loc /. 5 in dom L1 by A8, A11, A41, XBOOLE_0:def 3;
A59: L4 in dom (denaming (V,A,(loc /. 9))) by A57, A38;
L4 in dom (denaming (V,A,(loc /. 10))) by A56, A39;
then L4 in (dom (denaming (V,A,(loc /. 9)))) /\ (dom (denaming (V,A,(loc /. 10)))) by A59, XBOOLE_0:def 4;
then A60: L4 in dom <:(denaming (V,A,(loc /. 9))),(denaming (V,A,(loc /. 10))):> by FUNCT_3:def 7;
then A61: <:(denaming (V,A,(loc /. 9))),(denaming (V,A,(loc /. 10))):> . L4 = [((denaming (V,A,(loc /. 9))) . L4),((denaming (V,A,(loc /. 10))) . L4)] by FUNCT_3:def 7;
A62: dom (subtraction A) = [:A,A:] by A2, FUNCT_2:def 1;
( loc /. 9 is_a_value_on L4 & loc /. 10 is_a_value_on L4 ) by A7;
then [((denaming (V,A,(loc /. 9))) . L4),((denaming (V,A,(loc /. 10))) . L4)] in [:A,A:] by ZFMISC_1:87;
then A63: L4 in dom (subtraction (A,(loc /. 9),(loc /. 10))) by A60, A62, A61, FUNCT_1:11;
then reconsider ScsL4 = (subtraction (A,(loc /. 9),(loc /. 10))) . L4 as TypeSCNominativeData of V,A by PARTFUN1:4, NOMIN_1:39;
reconsider L5 = local_overlapping (V,A,L4,ScsL4,(loc /. 5)) as NonatomicND of V,A by NOMIN_2:9;
A64: dom L5 = {(loc /. 5)} \/ (dom L4) by A1, A3, NOMIN_4:4;
loc /. 1 in dom L1 by A8, A9, A41, XBOOLE_0:def 3;
then loc /. 1 in dom L2 by A42, XBOOLE_0:def 3;
then loc /. 1 in dom L3 by A48, XBOOLE_0:def 3;
then loc /. 1 in dom L4 by A55, XBOOLE_0:def 3;
then loc /. 1 in dom L5 by A64, XBOOLE_0:def 3;
then A65: L5 in dom (denaming (V,A,(loc /. 1))) by A31;
loc /. 2 in dom L1 by A8, A10, A41, XBOOLE_0:def 3;
then loc /. 2 in dom L2 by A42, XBOOLE_0:def 3;
then loc /. 2 in dom L3 by A48, XBOOLE_0:def 3;
then loc /. 2 in dom L4 by A55, XBOOLE_0:def 3;
then loc /. 2 in dom L5 by A64, XBOOLE_0:def 3;
then A66: L5 in dom (denaming (V,A,(loc /. 2))) by A32;
L5 in (dom (denaming (V,A,(loc /. 1)))) /\ (dom (denaming (V,A,(loc /. 2)))) by A65, A66, XBOOLE_0:def 4;
then A67: L5 in dom <:(denaming (V,A,(loc /. 1))),(denaming (V,A,(loc /. 2))):> by FUNCT_3:def 7;
then A68: <:(denaming (V,A,(loc /. 1))),(denaming (V,A,(loc /. 2))):> . L5 = [((denaming (V,A,(loc /. 1))) . L5),((denaming (V,A,(loc /. 2))) . L5)] by FUNCT_3:def 7;
A69: dom (addition A) = [:A,A:] by A2, FUNCT_2:def 1;
( loc /. 1 is_a_value_on L5 & loc /. 2 is_a_value_on L5 ) by A7;
then [((denaming (V,A,(loc /. 1))) . L5),((denaming (V,A,(loc /. 2))) . L5)] in [:A,A:] by ZFMISC_1:87;
then A70: L5 in dom (addition (A,(loc /. 1),(loc /. 2))) by A69, A67, A68, FUNCT_1:11;
A71: ( 2 = 1 + 1 & 3 = 2 + 1 & 4 = 3 + 1 & 5 = 4 + 1 & 6 = 5 + 1 ) ;
A72: (PrgLocalOverlapSeq (A,loc,d1,<*(denaming (V,A,(loc /. 4))),(denaming (V,A,(loc /. 5))),(multiplication (A,(loc /. 7),(loc /. 4))),(multiplication (A,(loc /. 8),(loc /. 6))),(subtraction (A,(loc /. 9),(loc /. 10))),(addition (A,(loc /. 1),(loc /. 2)))*>,<*6,4,9,10,5,1*>)) . 1 = L1 by A14, A16, NOMIN_8:def 14;
A73: (PrgLocalOverlapSeq (A,loc,d1,<*(denaming (V,A,(loc /. 4))),(denaming (V,A,(loc /. 5))),(multiplication (A,(loc /. 7),(loc /. 4))),(multiplication (A,(loc /. 8),(loc /. 6))),(subtraction (A,(loc /. 9),(loc /. 10))),(addition (A,(loc /. 1),(loc /. 2)))*>,<*6,4,9,10,5,1*>)) . 2 = L2 by A71, A14, A15, A17, A72, NOMIN_8:def 14;
A74: (PrgLocalOverlapSeq (A,loc,d1,<*(denaming (V,A,(loc /. 4))),(denaming (V,A,(loc /. 5))),(multiplication (A,(loc /. 7),(loc /. 4))),(multiplication (A,(loc /. 8),(loc /. 6))),(subtraction (A,(loc /. 9),(loc /. 10))),(addition (A,(loc /. 1),(loc /. 2)))*>,<*6,4,9,10,5,1*>)) . 3 = L3 by A71, A14, A15, A18, A73, NOMIN_8:def 14;
A75: (PrgLocalOverlapSeq (A,loc,d1,<*(denaming (V,A,(loc /. 4))),(denaming (V,A,(loc /. 5))),(multiplication (A,(loc /. 7),(loc /. 4))),(multiplication (A,(loc /. 8),(loc /. 6))),(subtraction (A,(loc /. 9),(loc /. 10))),(addition (A,(loc /. 1),(loc /. 2)))*>,<*6,4,9,10,5,1*>)) . 4 = L4 by A71, A14, A15, A19, A74, NOMIN_8:def 14;
let y be Nat; :: according to NOMIN_8:def 15 :: thesis: ( not 1 <= y or len <*(denaming (V,A,(loc /. 4))),(denaming (V,A,(loc /. 5))),(multiplication (A,(loc /. 7),(loc /. 4))),(multiplication (A,(loc /. 8),(loc /. 6))),(subtraction (A,(loc /. 9),(loc /. 10))),(addition (A,(loc /. 1),(loc /. 2)))*> <= y or (PrgLocalOverlapSeq (A,loc,d1,<*(denaming (V,A,(loc /. 4))),(denaming (V,A,(loc /. 5))),(multiplication (A,(loc /. 7),(loc /. 4))),(multiplication (A,(loc /. 8),(loc /. 6))),(subtraction (A,(loc /. 9),(loc /. 10))),(addition (A,(loc /. 1),(loc /. 2)))*>,<*6,4,9,10,5,1*>)) . y in dom (<*(denaming (V,A,(loc /. 4))),(denaming (V,A,(loc /. 5))),(multiplication (A,(loc /. 7),(loc /. 4))),(multiplication (A,(loc /. 8),(loc /. 6))),(subtraction (A,(loc /. 9),(loc /. 10))),(addition (A,(loc /. 1),(loc /. 2)))*> . (y + 1)) )
assume A76: 1 <= y ; :: thesis: ( len <*(denaming (V,A,(loc /. 4))),(denaming (V,A,(loc /. 5))),(multiplication (A,(loc /. 7),(loc /. 4))),(multiplication (A,(loc /. 8),(loc /. 6))),(subtraction (A,(loc /. 9),(loc /. 10))),(addition (A,(loc /. 1),(loc /. 2)))*> <= y or (PrgLocalOverlapSeq (A,loc,d1,<*(denaming (V,A,(loc /. 4))),(denaming (V,A,(loc /. 5))),(multiplication (A,(loc /. 7),(loc /. 4))),(multiplication (A,(loc /. 8),(loc /. 6))),(subtraction (A,(loc /. 9),(loc /. 10))),(addition (A,(loc /. 1),(loc /. 2)))*>,<*6,4,9,10,5,1*>)) . y in dom (<*(denaming (V,A,(loc /. 4))),(denaming (V,A,(loc /. 5))),(multiplication (A,(loc /. 7),(loc /. 4))),(multiplication (A,(loc /. 8),(loc /. 6))),(subtraction (A,(loc /. 9),(loc /. 10))),(addition (A,(loc /. 1),(loc /. 2)))*> . (y + 1)) )
assume y < len <*(denaming (V,A,(loc /. 4))),(denaming (V,A,(loc /. 5))),(multiplication (A,(loc /. 7),(loc /. 4))),(multiplication (A,(loc /. 8),(loc /. 6))),(subtraction (A,(loc /. 9),(loc /. 10))),(addition (A,(loc /. 1),(loc /. 2)))*> ; :: thesis: (PrgLocalOverlapSeq (A,loc,d1,<*(denaming (V,A,(loc /. 4))),(denaming (V,A,(loc /. 5))),(multiplication (A,(loc /. 7),(loc /. 4))),(multiplication (A,(loc /. 8),(loc /. 6))),(subtraction (A,(loc /. 9),(loc /. 10))),(addition (A,(loc /. 1),(loc /. 2)))*>,<*6,4,9,10,5,1*>)) . y in dom (<*(denaming (V,A,(loc /. 4))),(denaming (V,A,(loc /. 5))),(multiplication (A,(loc /. 7),(loc /. 4))),(multiplication (A,(loc /. 8),(loc /. 6))),(subtraction (A,(loc /. 9),(loc /. 10))),(addition (A,(loc /. 1),(loc /. 2)))*> . (y + 1))
then (y + 1) - 1 <= 6 - 1 by A14, NAT_1:13;
then not not y = 1 + 0 & ... & not y = 1 + 4 by A76, NAT_1:62;