let V, A be set ; 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; 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; ( 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 )
; 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; NOMIN_8:def 15 ( 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
; ( 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)))*>
; (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;
per cases then
( y = 1 or y = 2 or y = 3 or y = 4 or y = 5 )
;
suppose
y = 1
;
(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))hence
(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))
by A72, A34, A58;
verum end; suppose
y = 2
;
(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))hence
(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))
by A47, A71, A14, A15, A17, A72, NOMIN_8:def 14;
verum end; suppose
y = 3
;
(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))hence
(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))
by A54, A71, A14, A15, A18, A73, NOMIN_8:def 14;
verum end; suppose
y = 4
;
(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))hence
(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))
by A63, A71, A14, A15, A19, A74, NOMIN_8:def 14;
verum end; suppose
y = 5
;
(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))hence
(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))
by A70, A71, A14, A15, A20, A75, NOMIN_8:def 14;
verum end; end;