let V, A be set ; for loc being V -valued Function
for n0 being Nat st not V is empty & A is complex-containing & A is_without_nonatomicND_wrt V & ( 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 ) ) & Seg 6 c= dom loc & loc | (Seg 6) is one-to-one holds
<*(Fibonacci_inv (A,loc,n0)),(Fibonacci_loop_body (A,loc)),(Fibonacci_inv (A,loc,n0))*> is SFHT of (ND (V,A))
let loc be V -valued Function; for n0 being Nat st not V is empty & A is complex-containing & A is_without_nonatomicND_wrt V & ( 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 ) ) & Seg 6 c= dom loc & loc | (Seg 6) is one-to-one holds
<*(Fibonacci_inv (A,loc,n0)),(Fibonacci_loop_body (A,loc)),(Fibonacci_inv (A,loc,n0))*> is SFHT of (ND (V,A))
let n0 be Nat; ( not V is empty & A is complex-containing & A is_without_nonatomicND_wrt V & ( 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 ) ) & Seg 6 c= dom loc & loc | (Seg 6) is one-to-one implies <*(Fibonacci_inv (A,loc,n0)),(Fibonacci_loop_body (A,loc)),(Fibonacci_inv (A,loc,n0))*> is SFHT of (ND (V,A)) )
set i = loc /. 1;
set j = loc /. 2;
set n = loc /. 3;
set s = loc /. 4;
set b = loc /. 5;
set c = loc /. 6;
assume that
A1:
not V is empty
and
A2:
A is complex-containing
and
A3:
A is_without_nonatomicND_wrt V
and
A4:
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 )
; ( not Seg 6 c= dom loc or not loc | (Seg 6) is one-to-one or <*(Fibonacci_inv (A,loc,n0)),(Fibonacci_loop_body (A,loc)),(Fibonacci_inv (A,loc,n0))*> is SFHT of (ND (V,A)) )
assume that
A5:
Seg 6 c= dom loc
and
A6:
loc | (Seg 6) is one-to-one
; <*(Fibonacci_inv (A,loc,n0)),(Fibonacci_loop_body (A,loc)),(Fibonacci_inv (A,loc,n0))*> is SFHT of (ND (V,A))
set D = ND (V,A);
set EN = {(loc /. 1),(loc /. 2),(loc /. 3),(loc /. 4),(loc /. 5),(loc /. 6)};
set inv = Fibonacci_inv (A,loc,n0);
set B = Fibonacci_loop_body (A,loc);
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 Acs = addition (A,(loc /. 6),(loc /. 4));
set Aij = addition (A,(loc /. 1),(loc /. 2));
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 ((addition (A,(loc /. 6),(loc /. 4))),(loc /. 5));
set AS4 = SC_assignment ((addition (A,(loc /. 1),(loc /. 2))),(loc /. 1));
now for d being TypeSCNominativeData of V,A st d in dom (Fibonacci_inv (A,loc,n0)) & (Fibonacci_inv (A,loc,n0)) . d = TRUE & d in dom (Fibonacci_loop_body (A,loc)) & (Fibonacci_loop_body (A,loc)) . d in dom (Fibonacci_inv (A,loc,n0)) holds
(Fibonacci_inv (A,loc,n0)) . ((Fibonacci_loop_body (A,loc)) . d) = TRUE let d be
TypeSCNominativeData of
V,
A;
( d in dom (Fibonacci_inv (A,loc,n0)) & (Fibonacci_inv (A,loc,n0)) . d = TRUE & d in dom (Fibonacci_loop_body (A,loc)) & (Fibonacci_loop_body (A,loc)) . d in dom (Fibonacci_inv (A,loc,n0)) implies (Fibonacci_inv (A,loc,n0)) . ((Fibonacci_loop_body (A,loc)) . d) = TRUE )assume that A7:
d in dom (Fibonacci_inv (A,loc,n0))
and A8:
(Fibonacci_inv (A,loc,n0)) . d = TRUE
and A9:
d in dom (Fibonacci_loop_body (A,loc))
and A10:
(Fibonacci_loop_body (A,loc)) . d in dom (Fibonacci_inv (A,loc,n0))
;
(Fibonacci_inv (A,loc,n0)) . ((Fibonacci_loop_body (A,loc)) . d) = TRUE
Fibonacci_inv_pred A,
loc,
n0,
d
by A7, A8, Def19;
then consider d1 being
NonatomicND of
V,
A such that A11:
d = d1
and A12:
{(loc /. 1),(loc /. 2),(loc /. 3),(loc /. 4),(loc /. 5),(loc /. 6)} c= dom d1
and A13:
d1 . (loc /. 2) = 1
and A14:
d1 . (loc /. 3) = n0
and A15:
ex
I being
Nat st
(
I = d1 . (loc /. 1) &
d1 . (loc /. 4) = Fib I &
d1 . (loc /. 5) = Fib (I + 1) )
;
A16:
loc /. 1
in {(loc /. 1),(loc /. 2),(loc /. 3),(loc /. 4),(loc /. 5),(loc /. 6)}
by ENUMSET1:def 4;
A17:
loc /. 2
in {(loc /. 1),(loc /. 2),(loc /. 3),(loc /. 4),(loc /. 5),(loc /. 6)}
by ENUMSET1:def 4;
A18:
loc /. 3
in {(loc /. 1),(loc /. 2),(loc /. 3),(loc /. 4),(loc /. 5),(loc /. 6)}
by ENUMSET1:def 4;
A19:
loc /. 4
in {(loc /. 1),(loc /. 2),(loc /. 3),(loc /. 4),(loc /. 5),(loc /. 6)}
by ENUMSET1:def 4;
A20:
loc /. 5
in {(loc /. 1),(loc /. 2),(loc /. 3),(loc /. 4),(loc /. 5),(loc /. 6)}
by ENUMSET1:def 4;
consider I being
Nat such that A21:
I = d1 . (loc /. 1)
and A22:
d1 . (loc /. 4) = Fib I
and A23:
d1 . (loc /. 5) = Fib (I + 1)
by A15;
A24:
dom (SC_assignment ((denaming (V,A,(loc /. 4))),(loc /. 6))) = dom (denaming (V,A,(loc /. 4)))
by NOMIN_2:def 7;
A25:
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 ((SC_assignment ((denaming (V,A,(loc /. 4))),(loc /. 6))),(SC_assignment ((denaming (V,A,(loc /. 5))),(loc /. 4))))),
(SC_assignment ((addition (A,(loc /. 6),(loc /. 4))),(loc /. 5)))) =
PP_composition (
((SC_assignment ((denaming (V,A,(loc /. 5))),(loc /. 4))) * (SC_assignment ((denaming (V,A,(loc /. 4))),(loc /. 6)))),
(SC_assignment ((addition (A,(loc /. 6),(loc /. 4))),(loc /. 5))))
by PARTPR_2:def 1
.=
(SC_assignment ((addition (A,(loc /. 6),(loc /. 4))),(loc /. 5))) * ((SC_assignment ((denaming (V,A,(loc /. 5))),(loc /. 4))) * (SC_assignment ((denaming (V,A,(loc /. 4))),(loc /. 6))))
by PARTPR_2:def 1
;
then A26:
Fibonacci_loop_body (
A,
loc)
= (SC_assignment ((addition (A,(loc /. 1),(loc /. 2))),(loc /. 1))) * ((SC_assignment ((addition (A,(loc /. 6),(loc /. 4))),(loc /. 5))) * ((SC_assignment ((denaming (V,A,(loc /. 5))),(loc /. 4))) * (SC_assignment ((denaming (V,A,(loc /. 4))),(loc /. 6)))))
by PARTPR_2:def 1;
A27:
((SC_assignment ((addition (A,(loc /. 6),(loc /. 4))),(loc /. 5))) * (SC_assignment ((denaming (V,A,(loc /. 5))),(loc /. 4)))) * (SC_assignment ((denaming (V,A,(loc /. 4))),(loc /. 6))) = (SC_assignment ((addition (A,(loc /. 6),(loc /. 4))),(loc /. 5))) * ((SC_assignment ((denaming (V,A,(loc /. 5))),(loc /. 4))) * (SC_assignment ((denaming (V,A,(loc /. 4))),(loc /. 6))))
by RELAT_1:36;
A28:
Fibonacci_loop_body (
A,
loc)
= (SC_assignment ((addition (A,(loc /. 1),(loc /. 2))),(loc /. 1))) * (((SC_assignment ((addition (A,(loc /. 6),(loc /. 4))),(loc /. 5))) * (SC_assignment ((denaming (V,A,(loc /. 5))),(loc /. 4)))) * (SC_assignment ((denaming (V,A,(loc /. 4))),(loc /. 6))))
by A26, RELAT_1:36;
then A29:
d in dom (((SC_assignment ((addition (A,(loc /. 6),(loc /. 4))),(loc /. 5))) * (SC_assignment ((denaming (V,A,(loc /. 5))),(loc /. 4)))) * (SC_assignment ((denaming (V,A,(loc /. 4))),(loc /. 6))))
by A9, FUNCT_1:11;
then A30:
d in dom ((SC_assignment ((denaming (V,A,(loc /. 5))),(loc /. 4))) * (SC_assignment ((denaming (V,A,(loc /. 4))),(loc /. 6))))
by A27, FUNCT_1:11;
then A31:
((SC_assignment ((denaming (V,A,(loc /. 5))),(loc /. 4))) * (SC_assignment ((denaming (V,A,(loc /. 4))),(loc /. 6)))) . d = (SC_assignment ((denaming (V,A,(loc /. 5))),(loc /. 4))) . ((SC_assignment ((denaming (V,A,(loc /. 4))),(loc /. 6))) . d)
by FUNCT_1:12;
A32:
dom (denaming (V,A,(loc /. 1))) = { d where d is NonatomicND of V,A : loc /. 1 in dom d }
by NOMIN_1:def 18;
A33:
dom (denaming (V,A,(loc /. 2))) = { d where d is NonatomicND of V,A : loc /. 2 in dom d }
by NOMIN_1:def 18;
A34:
dom (denaming (V,A,(loc /. 4))) = { d where d is NonatomicND of V,A : loc /. 4 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:
d in dom (SC_assignment ((denaming (V,A,(loc /. 4))),(loc /. 6)))
by A29, FUNCT_1:11;
then reconsider Ad =
(denaming (V,A,(loc /. 4))) . d1 as
TypeSCNominativeData of
V,
A by A24, A11, PARTFUN1:4, NOMIN_1:39;
reconsider L1 =
local_overlapping (
V,
A,
d1,
Ad,
(loc /. 6)) as
NonatomicND of
V,
A by NOMIN_2:9;
A37:
(SC_assignment ((denaming (V,A,(loc /. 4))),(loc /. 6))) . d = L1
by A11, A36, NOMIN_2:def 7;
then A38:
L1 in dom (SC_assignment ((denaming (V,A,(loc /. 5))),(loc /. 4)))
by A30, FUNCT_1:11;
reconsider DbL1 =
(denaming (V,A,(loc /. 5))) . L1 as
TypeSCNominativeData of
V,
A by A25, A38, PARTFUN1:4, NOMIN_1:39;
reconsider L2 =
local_overlapping (
V,
A,
L1,
DbL1,
(loc /. 4)) as
NonatomicND of
V,
A by NOMIN_2:9;
A39:
(SC_assignment ((denaming (V,A,(loc /. 5))),(loc /. 4))) . L1 = L2
by A38, NOMIN_2:def 7;
A40:
dom L1 = {(loc /. 6)} \/ (dom d1)
by A3, A1, NOMIN_4:4;
A41:
dom L2 = (dom L1) \/ {(loc /. 4)}
by A3, A1, A25, A38, A39, NOMIN_4:5;
loc /. 6
in {(loc /. 6)}
by TARSKI:def 1;
then A42:
loc /. 6
in dom L1
by A40, XBOOLE_0:def 3;
then A43:
loc /. 6
in dom L2
by A41, XBOOLE_0:def 3;
then A44:
L2 in dom (denaming (V,A,(loc /. 6)))
by A35;
A45:
dom (addition A) = [:A,A:]
by A2, FUNCT_2:def 1;
loc /. 4
in {(loc /. 4)}
by TARSKI:def 1;
then A46:
loc /. 4
in dom L2
by A41, XBOOLE_0:def 3;
then
L2 in dom (denaming (V,A,(loc /. 4)))
by A34;
then
L2 in (dom (denaming (V,A,(loc /. 6)))) /\ (dom (denaming (V,A,(loc /. 4))))
by A44, XBOOLE_0:def 4;
then A47:
L2 in dom <:(denaming (V,A,(loc /. 6))),(denaming (V,A,(loc /. 4))):>
by FUNCT_3:def 7;
then A48:
<:(denaming (V,A,(loc /. 6))),(denaming (V,A,(loc /. 4))):> . L2 = [((denaming (V,A,(loc /. 6))) . L2),((denaming (V,A,(loc /. 4))) . L2)]
by FUNCT_3:def 7;
(
loc /. 6
is_a_value_on L2 &
loc /. 4
is_a_value_on L2 )
by A4;
then
[((denaming (V,A,(loc /. 6))) . L2),((denaming (V,A,(loc /. 4))) . L2)] in [:A,A:]
by ZFMISC_1:87;
then A49:
L2 in dom (addition (A,(loc /. 6),(loc /. 4)))
by A47, A45, A48, FUNCT_1:11;
then reconsider AcsL2 =
(addition (A,(loc /. 6),(loc /. 4))) . L2 as
TypeSCNominativeData of
V,
A by PARTFUN1:4, NOMIN_1:39;
reconsider L3 =
local_overlapping (
V,
A,
L2,
AcsL2,
(loc /. 5)) as
NonatomicND of
V,
A by NOMIN_2:9;
A50:
dom L3 = {(loc /. 5)} \/ (dom L2)
by A1, A3, NOMIN_4:4;
A51:
dom L2 = {(loc /. 4)} \/ (dom L1)
by A1, A3, NOMIN_4:4;
A52:
loc /. 1
in dom L1
by A12, A16, A40, XBOOLE_0:def 3;
then A53:
loc /. 1
in dom L2
by A51, XBOOLE_0:def 3;
then A54:
loc /. 1
in dom L3
by A50, XBOOLE_0:def 3;
then A55:
L3 in dom (denaming (V,A,(loc /. 1)))
by A32;
A56:
loc /. 2
in dom L1
by A12, A17, A40, XBOOLE_0:def 3;
then A57:
loc /. 2
in dom L2
by A51, XBOOLE_0:def 3;
then A58:
loc /. 2
in dom L3
by A50, XBOOLE_0:def 3;
then A59:
L3 in dom (denaming (V,A,(loc /. 2)))
by A33;
L3 in (dom (denaming (V,A,(loc /. 1)))) /\ (dom (denaming (V,A,(loc /. 2))))
by A55, A59, XBOOLE_0:def 4;
then A60:
L3 in dom <:(denaming (V,A,(loc /. 1))),(denaming (V,A,(loc /. 2))):>
by FUNCT_3:def 7;
then A61:
<:(denaming (V,A,(loc /. 1))),(denaming (V,A,(loc /. 2))):> . L3 = [((denaming (V,A,(loc /. 1))) . L3),((denaming (V,A,(loc /. 2))) . L3)]
by FUNCT_3:def 7;
(
loc /. 1
is_a_value_on L3 &
loc /. 2
is_a_value_on L3 )
by A4;
then
[((denaming (V,A,(loc /. 1))) . L3),((denaming (V,A,(loc /. 2))) . L3)] in [:A,A:]
by ZFMISC_1:87;
then A62:
L3 in dom (addition (A,(loc /. 1),(loc /. 2)))
by A45, A60, A61, FUNCT_1:11;
then reconsider AijL3 =
(addition (A,(loc /. 1),(loc /. 2))) . L3 as
TypeSCNominativeData of
V,
A by PARTFUN1:4, NOMIN_1:39;
reconsider L4 =
local_overlapping (
V,
A,
L3,
AijL3,
(loc /. 1)) as
NonatomicND of
V,
A by NOMIN_2:9;
A63:
dom L4 = {(loc /. 1)} \/ (dom L3)
by A1, A3, NOMIN_4:4;
A64:
d in dom ((SC_assignment ((addition (A,(loc /. 6),(loc /. 4))),(loc /. 5))) * ((SC_assignment ((denaming (V,A,(loc /. 5))),(loc /. 4))) * (SC_assignment ((denaming (V,A,(loc /. 4))),(loc /. 6)))))
by A9, A26, FUNCT_1:11;
then
L2 in dom (SC_assignment ((addition (A,(loc /. 6),(loc /. 4))),(loc /. 5)))
by A31, A37, A39, FUNCT_1:11;
then A65:
(SC_assignment ((addition (A,(loc /. 6),(loc /. 4))),(loc /. 5))) . L2 = L3
by NOMIN_2:def 7;
A66:
((SC_assignment ((addition (A,(loc /. 6),(loc /. 4))),(loc /. 5))) * ((SC_assignment ((denaming (V,A,(loc /. 5))),(loc /. 4))) * (SC_assignment ((denaming (V,A,(loc /. 4))),(loc /. 6))))) . d = (SC_assignment ((addition (A,(loc /. 6),(loc /. 4))),(loc /. 5))) . (((SC_assignment ((denaming (V,A,(loc /. 5))),(loc /. 4))) * (SC_assignment ((denaming (V,A,(loc /. 4))),(loc /. 6)))) . d)
by A64, FUNCT_1:12;
Fibonacci_loop_body (
A,
loc) =
((SC_assignment ((addition (A,(loc /. 1),(loc /. 2))),(loc /. 1))) * ((SC_assignment ((addition (A,(loc /. 6),(loc /. 4))),(loc /. 5))) * (SC_assignment ((denaming (V,A,(loc /. 5))),(loc /. 4))))) * (SC_assignment ((denaming (V,A,(loc /. 4))),(loc /. 6)))
by A28, RELAT_1:36
.=
(((SC_assignment ((addition (A,(loc /. 1),(loc /. 2))),(loc /. 1))) * (SC_assignment ((addition (A,(loc /. 6),(loc /. 4))),(loc /. 5)))) * (SC_assignment ((denaming (V,A,(loc /. 5))),(loc /. 4)))) * (SC_assignment ((denaming (V,A,(loc /. 4))),(loc /. 6)))
by RELAT_1:36
;
then
(SC_assignment ((denaming (V,A,(loc /. 4))),(loc /. 6))) . d in dom (((SC_assignment ((addition (A,(loc /. 1),(loc /. 2))),(loc /. 1))) * (SC_assignment ((addition (A,(loc /. 6),(loc /. 4))),(loc /. 5)))) * (SC_assignment ((denaming (V,A,(loc /. 5))),(loc /. 4))))
by A9, FUNCT_1:11;
then
(SC_assignment ((denaming (V,A,(loc /. 5))),(loc /. 4))) . L1 in dom ((SC_assignment ((addition (A,(loc /. 1),(loc /. 2))),(loc /. 1))) * (SC_assignment ((addition (A,(loc /. 6),(loc /. 4))),(loc /. 5))))
by A37, FUNCT_1:11;
then
(SC_assignment ((addition (A,(loc /. 6),(loc /. 4))),(loc /. 5))) . L2 in dom (SC_assignment ((addition (A,(loc /. 1),(loc /. 2))),(loc /. 1)))
by A39, FUNCT_1:11;
then A67:
L4 =
(SC_assignment ((addition (A,(loc /. 1),(loc /. 2))),(loc /. 1))) . L3
by A65, NOMIN_2:def 7
.=
(Fibonacci_loop_body (A,loc)) . d
by A65, A39, A37, A31, A66, A9, A26, FUNCT_1:12
;
Fibonacci_inv_pred A,
loc,
n0,
L4
proof
take
L4
;
NOMIN_7:def 18 ( L4 = L4 & {(loc /. 1),(loc /. 2),(loc /. 3),(loc /. 4),(loc /. 5),(loc /. 6)} c= dom L4 & L4 . (loc /. 2) = 1 & L4 . (loc /. 3) = n0 & ex I being Nat st
( I = L4 . (loc /. 1) & L4 . (loc /. 4) = Fib I & L4 . (loc /. 5) = Fib (I + 1) ) )
thus
L4 = L4
;
( {(loc /. 1),(loc /. 2),(loc /. 3),(loc /. 4),(loc /. 5),(loc /. 6)} c= dom L4 & L4 . (loc /. 2) = 1 & L4 . (loc /. 3) = n0 & ex I being Nat st
( I = L4 . (loc /. 1) & L4 . (loc /. 4) = Fib I & L4 . (loc /. 5) = Fib (I + 1) ) )
loc /. 1
in {(loc /. 1)}
by TARSKI:def 1;
then A68:
loc /. 1
in dom L4
by A63, XBOOLE_0:def 3;
A69:
loc /. 2
in dom L4
by A58, A63, XBOOLE_0:def 3;
A70:
loc /. 3
in dom L1
by A12, A18, A40, XBOOLE_0:def 3;
then A71:
loc /. 3
in dom L2
by A51, XBOOLE_0:def 3;
then A72:
loc /. 3
in dom L3
by A50, XBOOLE_0:def 3;
then A73:
loc /. 3
in dom L4
by A63, XBOOLE_0:def 3;
A74:
loc /. 4
in dom L3
by A46, A50, XBOOLE_0:def 3;
then A75:
loc /. 4
in dom L4
by A63, XBOOLE_0:def 3;
A76:
loc /. 5
in dom L1
by A12, A20, A40, XBOOLE_0:def 3;
then
loc /. 5
in dom L2
by A51, XBOOLE_0:def 3;
then A77:
loc /. 5
in dom L3
by A50, XBOOLE_0:def 3;
then A78:
loc /. 5
in dom L4
by A63, XBOOLE_0:def 3;
loc /. 6
in dom L3
by A43, A50, XBOOLE_0:def 3;
then
loc /. 6
in dom L4
by A63, XBOOLE_0:def 3;
hence
{(loc /. 1),(loc /. 2),(loc /. 3),(loc /. 4),(loc /. 5),(loc /. 6)} c= dom L4
by A68, A69, A73, A75, A78, ENUMSET1:def 4;
( L4 . (loc /. 2) = 1 & L4 . (loc /. 3) = n0 & ex I being Nat st
( I = L4 . (loc /. 1) & L4 . (loc /. 4) = Fib I & L4 . (loc /. 5) = Fib (I + 1) ) )
A79:
L3 . (loc /. 2) =
L2 . (loc /. 2)
by A1, A3, A6, A57, A5, Th1, NOMIN_5:3
.=
L1 . (loc /. 2)
by A1, A3, A56, A5, A6, Th1, NOMIN_5:3
.=
1
by A1, A3, A12, A13, A17, A5, A6, Th1, NOMIN_5:3
;
hence
L4 . (loc /. 2) = 1
by A1, A3, A58, A5, A6, Th1, NOMIN_5:3;
( L4 . (loc /. 3) = n0 & ex I being Nat st
( I = L4 . (loc /. 1) & L4 . (loc /. 4) = Fib I & L4 . (loc /. 5) = Fib (I + 1) ) )
thus L4 . (loc /. 3) =
L3 . (loc /. 3)
by A1, A3, A72, A5, A6, Th1, NOMIN_5:3
.=
L2 . (loc /. 3)
by A1, A3, A71, A5, A6, Th1, NOMIN_5:3
.=
L1 . (loc /. 3)
by A1, A3, A70, A5, A6, Th1, NOMIN_5:3
.=
n0
by A1, A3, A12, A14, A18, A5, A6, Th1, NOMIN_5:3
;
ex I being Nat st
( I = L4 . (loc /. 1) & L4 . (loc /. 4) = Fib I & L4 . (loc /. 5) = Fib (I + 1) )
take I1 =
I + 1;
( I1 = L4 . (loc /. 1) & L4 . (loc /. 4) = Fib I1 & L4 . (loc /. 5) = Fib (I1 + 1) )
A80:
L3 . (loc /. 1) =
L2 . (loc /. 1)
by A1, A3, A53, A5, A6, Th1, NOMIN_5:3
.=
L1 . (loc /. 1)
by A1, A3, A52, A5, A6, Th1, NOMIN_5:3
.=
I
by A1, A3, A12, A16, A21, A5, A6, Th1, NOMIN_5:3
;
thus L4 . (loc /. 1) =
(addition (A,(loc /. 1),(loc /. 2))) . L3
by A1, NOMIN_2:10
.=
I1
by A2, A62, A54, A58, A79, A80, NOMIN_5:4
;
( L4 . (loc /. 4) = Fib I1 & L4 . (loc /. 5) = Fib (I1 + 1) )
A81:
L2 . (loc /. 4) =
L1 . (loc /. 5)
by A1, A76, Th2
.=
Fib I1
by A1, A3, A23, A12, A20, A5, A6, Th1, NOMIN_5:3
;
thus L4 . (loc /. 4) =
L3 . (loc /. 4)
by A1, A3, A74, A5, A6, Th1, NOMIN_5:3
.=
Fib I1
by A1, A3, A46, A81, A5, A6, Th1, NOMIN_5:3
;
L4 . (loc /. 5) = Fib (I1 + 1)
A82:
L2 . (loc /. 6) =
L1 . (loc /. 6)
by A1, A3, A42, A5, A6, Th1, NOMIN_5:3
.=
Fib I
by A1, A12, A19, A22, Th2
;
thus L4 . (loc /. 5) =
L3 . (loc /. 5)
by A1, A3, A77, A5, A6, Th1, NOMIN_5:3
.=
(addition (A,(loc /. 6),(loc /. 4))) . L2
by A1, NOMIN_2:10
.=
(Fib I) + (Fib I1)
by A2, A49, A46, A81, A43, A82, NOMIN_5:4
.=
Fib (I1 + 1)
by PRE_FF:1
;
verum
end; hence
(Fibonacci_inv (A,loc,n0)) . ((Fibonacci_loop_body (A,loc)) . d) = TRUE
by A10, A67, Def19;
verum end;
hence
<*(Fibonacci_inv (A,loc,n0)),(Fibonacci_loop_body (A,loc)),(Fibonacci_inv (A,loc,n0))*> is SFHT of (ND (V,A))
by NOMIN_3:28; verum