let V, A be set ; for loc being V -valued Function
for n0 being Nat
for val being 6 -element FinSequence st not V is empty & A is_without_nonatomicND_wrt V & Seg 6 c= dom loc & loc | (Seg 6) is one-to-one & loc,val are_different_wrt 6 holds
<*(valid_Fibonacci_input (V,A,val,n0)),(initial_assignments (A,loc,val,6)),(Fibonacci_inv (A,loc,n0))*> is SFHT of (ND (V,A))
let loc be V -valued Function; for n0 being Nat
for val being 6 -element FinSequence st not V is empty & A is_without_nonatomicND_wrt V & Seg 6 c= dom loc & loc | (Seg 6) is one-to-one & loc,val are_different_wrt 6 holds
<*(valid_Fibonacci_input (V,A,val,n0)),(initial_assignments (A,loc,val,6)),(Fibonacci_inv (A,loc,n0))*> is SFHT of (ND (V,A))
let n0 be Nat; for val being 6 -element FinSequence st not V is empty & A is_without_nonatomicND_wrt V & Seg 6 c= dom loc & loc | (Seg 6) is one-to-one & loc,val are_different_wrt 6 holds
<*(valid_Fibonacci_input (V,A,val,n0)),(initial_assignments (A,loc,val,6)),(Fibonacci_inv (A,loc,n0))*> is SFHT of (ND (V,A))
let val be 6 -element FinSequence; ( not V is empty & A is_without_nonatomicND_wrt V & Seg 6 c= dom loc & loc | (Seg 6) is one-to-one & loc,val are_different_wrt 6 implies <*(valid_Fibonacci_input (V,A,val,n0)),(initial_assignments (A,loc,val,6)),(Fibonacci_inv (A,loc,n0))*> is SFHT of (ND (V,A)) )
set size = 6;
set G = initial_assignments_Seq (A,loc,val,6);
A1:
(initial_assignments_Seq (A,loc,val,6)) . 1 = SC_assignment ((denaming (V,A,(val . 1))),(loc /. 1))
by Def8;
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 i1 = val . 1;
set j1 = val . 2;
set n1 = val . 3;
set s1 = val . 4;
set b1 = val . 5;
set c1 = val . 6;
set EN = {(val . 1),(val . 2),(val . 3),(val . 4),(val . 5),(val . 6)};
set D = ND (V,A);
set I = valid_Fibonacci_input (V,A,val,n0);
set inv = Fibonacci_inv (A,loc,n0);
set Di = denaming (V,A,(val . 1));
set Dj = denaming (V,A,(val . 2));
set Dn = denaming (V,A,(val . 3));
set Ds = denaming (V,A,(val . 4));
set Db = denaming (V,A,(val . 5));
set Dc = denaming (V,A,(val . 6));
set asi = SC_assignment ((denaming (V,A,(val . 1))),(loc /. 1));
set asj = SC_assignment ((denaming (V,A,(val . 2))),(loc /. 2));
set asn = SC_assignment ((denaming (V,A,(val . 3))),(loc /. 3));
set ass = SC_assignment ((denaming (V,A,(val . 4))),(loc /. 4));
set asb = SC_assignment ((denaming (V,A,(val . 5))),(loc /. 5));
set asc = SC_assignment ((denaming (V,A,(val . 6))),(loc /. 6));
set U1 = SC_Psuperpos ((Fibonacci_inv (A,loc,n0)),(denaming (V,A,(val . 6))),(loc /. 6));
set T1 = SC_Psuperpos ((SC_Psuperpos ((Fibonacci_inv (A,loc,n0)),(denaming (V,A,(val . 6))),(loc /. 6))),(denaming (V,A,(val . 5))),(loc /. 5));
set S1 = SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((Fibonacci_inv (A,loc,n0)),(denaming (V,A,(val . 6))),(loc /. 6))),(denaming (V,A,(val . 5))),(loc /. 5))),(denaming (V,A,(val . 4))),(loc /. 4));
set R1 = SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((Fibonacci_inv (A,loc,n0)),(denaming (V,A,(val . 6))),(loc /. 6))),(denaming (V,A,(val . 5))),(loc /. 5))),(denaming (V,A,(val . 4))),(loc /. 4))),(denaming (V,A,(val . 3))),(loc /. 3));
set Q1 = SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((Fibonacci_inv (A,loc,n0)),(denaming (V,A,(val . 6))),(loc /. 6))),(denaming (V,A,(val . 5))),(loc /. 5))),(denaming (V,A,(val . 4))),(loc /. 4))),(denaming (V,A,(val . 3))),(loc /. 3))),(denaming (V,A,(val . 2))),(loc /. 2));
set P1 = SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((Fibonacci_inv (A,loc,n0)),(denaming (V,A,(val . 6))),(loc /. 6))),(denaming (V,A,(val . 5))),(loc /. 5))),(denaming (V,A,(val . 4))),(loc /. 4))),(denaming (V,A,(val . 3))),(loc /. 3))),(denaming (V,A,(val . 2))),(loc /. 2))),(denaming (V,A,(val . 1))),(loc /. 1));
assume that
A2:
not V is empty
and
A3:
A is_without_nonatomicND_wrt V
and
A4:
Seg 6 c= dom loc
and
A5:
loc | (Seg 6) is one-to-one
and
A6:
loc,val are_different_wrt 6
; <*(valid_Fibonacci_input (V,A,val,n0)),(initial_assignments (A,loc,val,6)),(Fibonacci_inv (A,loc,n0))*> is SFHT of (ND (V,A))
A7:
Seg 6 = dom val
by FINSEQ_1:89;
A8:
<*(SC_Psuperpos ((Fibonacci_inv (A,loc,n0)),(denaming (V,A,(val . 6))),(loc /. 6))),(SC_assignment ((denaming (V,A,(val . 6))),(loc /. 6))),(Fibonacci_inv (A,loc,n0))*> is SFHT of (ND (V,A))
by NOMIN_3:29;
A9:
<*(SC_Psuperpos ((SC_Psuperpos ((Fibonacci_inv (A,loc,n0)),(denaming (V,A,(val . 6))),(loc /. 6))),(denaming (V,A,(val . 5))),(loc /. 5))),(SC_assignment ((denaming (V,A,(val . 5))),(loc /. 5))),(SC_Psuperpos ((Fibonacci_inv (A,loc,n0)),(denaming (V,A,(val . 6))),(loc /. 6)))*> is SFHT of (ND (V,A))
by NOMIN_3:29;
A10:
<*(SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((Fibonacci_inv (A,loc,n0)),(denaming (V,A,(val . 6))),(loc /. 6))),(denaming (V,A,(val . 5))),(loc /. 5))),(denaming (V,A,(val . 4))),(loc /. 4))),(SC_assignment ((denaming (V,A,(val . 4))),(loc /. 4))),(SC_Psuperpos ((SC_Psuperpos ((Fibonacci_inv (A,loc,n0)),(denaming (V,A,(val . 6))),(loc /. 6))),(denaming (V,A,(val . 5))),(loc /. 5)))*> is SFHT of (ND (V,A))
by NOMIN_3:29;
A11:
<*(SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((Fibonacci_inv (A,loc,n0)),(denaming (V,A,(val . 6))),(loc /. 6))),(denaming (V,A,(val . 5))),(loc /. 5))),(denaming (V,A,(val . 4))),(loc /. 4))),(denaming (V,A,(val . 3))),(loc /. 3))),(SC_assignment ((denaming (V,A,(val . 3))),(loc /. 3))),(SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((Fibonacci_inv (A,loc,n0)),(denaming (V,A,(val . 6))),(loc /. 6))),(denaming (V,A,(val . 5))),(loc /. 5))),(denaming (V,A,(val . 4))),(loc /. 4)))*> is SFHT of (ND (V,A))
by NOMIN_3:29;
A12:
<*(SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((Fibonacci_inv (A,loc,n0)),(denaming (V,A,(val . 6))),(loc /. 6))),(denaming (V,A,(val . 5))),(loc /. 5))),(denaming (V,A,(val . 4))),(loc /. 4))),(denaming (V,A,(val . 3))),(loc /. 3))),(denaming (V,A,(val . 2))),(loc /. 2))),(SC_assignment ((denaming (V,A,(val . 2))),(loc /. 2))),(SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((Fibonacci_inv (A,loc,n0)),(denaming (V,A,(val . 6))),(loc /. 6))),(denaming (V,A,(val . 5))),(loc /. 5))),(denaming (V,A,(val . 4))),(loc /. 4))),(denaming (V,A,(val . 3))),(loc /. 3)))*> is SFHT of (ND (V,A))
by NOMIN_3:29;
A13:
<*(SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((Fibonacci_inv (A,loc,n0)),(denaming (V,A,(val . 6))),(loc /. 6))),(denaming (V,A,(val . 5))),(loc /. 5))),(denaming (V,A,(val . 4))),(loc /. 4))),(denaming (V,A,(val . 3))),(loc /. 3))),(denaming (V,A,(val . 2))),(loc /. 2))),(denaming (V,A,(val . 1))),(loc /. 1))),(SC_assignment ((denaming (V,A,(val . 1))),(loc /. 1))),(SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((Fibonacci_inv (A,loc,n0)),(denaming (V,A,(val . 6))),(loc /. 6))),(denaming (V,A,(val . 5))),(loc /. 5))),(denaming (V,A,(val . 4))),(loc /. 4))),(denaming (V,A,(val . 3))),(loc /. 3))),(denaming (V,A,(val . 2))),(loc /. 2)))*> is SFHT of (ND (V,A))
by NOMIN_3:29;
2 = 1 + 1
;
then A14:
(initial_assignments_Seq (A,loc,val,6)) . 2 = PP_composition ((SC_assignment ((denaming (V,A,(val . 1))),(loc /. 1))),(SC_assignment ((denaming (V,A,(val . 2))),(loc /. 2))))
by A1, Def8;
3 = 2 + 1
;
then A15:
(initial_assignments_Seq (A,loc,val,6)) . 3 = PP_composition (((initial_assignments_Seq (A,loc,val,6)) . 2),(SC_assignment ((denaming (V,A,(val . 3))),(loc /. 3))))
by Def8;
4 = 3 + 1
;
then A16:
(initial_assignments_Seq (A,loc,val,6)) . 4 = PP_composition (((initial_assignments_Seq (A,loc,val,6)) . 3),(SC_assignment ((denaming (V,A,(val . 4))),(loc /. 4))))
by Def8;
5 = 4 + 1
;
then A17:
(initial_assignments_Seq (A,loc,val,6)) . 5 = PP_composition (((initial_assignments_Seq (A,loc,val,6)) . 4),(SC_assignment ((denaming (V,A,(val . 5))),(loc /. 5))))
by Def8;
6 = 5 + 1
;
then A18:
initial_assignments (A,loc,val,6) = 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))),(SC_assignment ((denaming (V,A,(val . 6))),(loc /. 6))))
by A14, A15, A16, A17, Def8;
valid_Fibonacci_input (V,A,val,n0) ||= SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((Fibonacci_inv (A,loc,n0)),(denaming (V,A,(val . 6))),(loc /. 6))),(denaming (V,A,(val . 5))),(loc /. 5))),(denaming (V,A,(val . 4))),(loc /. 4))),(denaming (V,A,(val . 3))),(loc /. 3))),(denaming (V,A,(val . 2))),(loc /. 2))),(denaming (V,A,(val . 1))),(loc /. 1))
proof
let d be
Element of
ND (
V,
A);
NOMIN_3:def 3 ( not d in dom (valid_Fibonacci_input (V,A,val,n0)) or not (valid_Fibonacci_input (V,A,val,n0)) . d = TRUE or ( d in dom (SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((Fibonacci_inv (A,loc,n0)),(denaming (V,A,(val . 6))),(loc /. 6))),(denaming (V,A,(val . 5))),(loc /. 5))),(denaming (V,A,(val . 4))),(loc /. 4))),(denaming (V,A,(val . 3))),(loc /. 3))),(denaming (V,A,(val . 2))),(loc /. 2))),(denaming (V,A,(val . 1))),(loc /. 1))) & (SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((Fibonacci_inv (A,loc,n0)),(denaming (V,A,(val . 6))),(loc /. 6))),(denaming (V,A,(val . 5))),(loc /. 5))),(denaming (V,A,(val . 4))),(loc /. 4))),(denaming (V,A,(val . 3))),(loc /. 3))),(denaming (V,A,(val . 2))),(loc /. 2))),(denaming (V,A,(val . 1))),(loc /. 1))) . d = TRUE ) )
assume
(
d in dom (valid_Fibonacci_input (V,A,val,n0)) &
(valid_Fibonacci_input (V,A,val,n0)) . d = TRUE )
;
( d in dom (SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((Fibonacci_inv (A,loc,n0)),(denaming (V,A,(val . 6))),(loc /. 6))),(denaming (V,A,(val . 5))),(loc /. 5))),(denaming (V,A,(val . 4))),(loc /. 4))),(denaming (V,A,(val . 3))),(loc /. 3))),(denaming (V,A,(val . 2))),(loc /. 2))),(denaming (V,A,(val . 1))),(loc /. 1))) & (SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((Fibonacci_inv (A,loc,n0)),(denaming (V,A,(val . 6))),(loc /. 6))),(denaming (V,A,(val . 5))),(loc /. 5))),(denaming (V,A,(val . 4))),(loc /. 4))),(denaming (V,A,(val . 3))),(loc /. 3))),(denaming (V,A,(val . 2))),(loc /. 2))),(denaming (V,A,(val . 1))),(loc /. 1))) . d = TRUE )
then
valid_Fibonacci_input_pred V,
A,
val,
n0,
d
by Def15;
then consider d1 being
NonatomicND of
V,
A such that A19:
d = d1
and A20:
{(val . 1),(val . 2),(val . 3),(val . 4),(val . 5),(val . 6)} c= dom d1
and A21:
d1 . (val . 1) = 0
and A22:
d1 . (val . 2) = 1
and A23:
d1 . (val . 3) = n0
and A24:
d1 . (val . 4) = 0
and A25:
d1 . (val . 5) = 1
and
d1 . (val . 6) = 0
;
set F =
LocalOverlapSeq (
A,
loc,
val,
d1,6);
A26:
len (LocalOverlapSeq (A,loc,val,d1,6)) = 6
by Def4;
rng val c= {(val . 1),(val . 2),(val . 3),(val . 4),(val . 5),(val . 6)}
proof
let y be
object ;
TARSKI:def 3 ( not y in rng val or y in {(val . 1),(val . 2),(val . 3),(val . 4),(val . 5),(val . 6)} )
assume
y in rng val
;
y in {(val . 1),(val . 2),(val . 3),(val . 4),(val . 5),(val . 6)}
then consider x being
object such that A27:
x in dom val
and A28:
y = val . x
by FUNCT_1:def 3;
not not
x = 1 & ... & not
x = 6
by A7, A27, FINSEQ_1:91;
hence
y in {(val . 1),(val . 2),(val . 3),(val . 4),(val . 5),(val . 6)}
by A28, ENUMSET1:def 4;
verum
end;
then
rng val c= dom d1
by A20;
then
val is_valid_wrt d1
;
then A29:
loc,
val,6
are_correct_wrt d1
by A2, A3, A7, A26, FINSEQ_1:def 3;
A30:
val . 1
in {(val . 1),(val . 2),(val . 3),(val . 4),(val . 5),(val . 6)}
by ENUMSET1:def 4;
A31:
val . 4
in {(val . 1),(val . 2),(val . 3),(val . 4),(val . 5),(val . 6)}
by ENUMSET1:def 4;
A32:
val . 5
in {(val . 1),(val . 2),(val . 3),(val . 4),(val . 5),(val . 6)}
by ENUMSET1:def 4;
A33:
dom (denaming (V,A,(val . 1))) = { d where d is NonatomicND of V,A : val . 1 in dom d }
by NOMIN_1:def 18;
A34:
dom (denaming (V,A,(val . 2))) = { d where d is NonatomicND of V,A : val . 2 in dom d }
by NOMIN_1:def 18;
A35:
dom (denaming (V,A,(val . 3))) = { d where d is NonatomicND of V,A : val . 3 in dom d }
by NOMIN_1:def 18;
A36:
dom (denaming (V,A,(val . 4))) = { d where d is NonatomicND of V,A : val . 4 in dom d }
by NOMIN_1:def 18;
A37:
dom (denaming (V,A,(val . 5))) = { d where d is NonatomicND of V,A : val . 5 in dom d }
by NOMIN_1:def 18;
A38:
dom (denaming (V,A,(val . 6))) = { d where d is NonatomicND of V,A : val . 6 in dom d }
by NOMIN_1:def 18;
A39:
dom (SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((Fibonacci_inv (A,loc,n0)),(denaming (V,A,(val . 6))),(loc /. 6))),(denaming (V,A,(val . 5))),(loc /. 5))),(denaming (V,A,(val . 4))),(loc /. 4))),(denaming (V,A,(val . 3))),(loc /. 3))),(denaming (V,A,(val . 2))),(loc /. 2))),(denaming (V,A,(val . 1))),(loc /. 1))) = { d where d is TypeSCNominativeData of V,A : ( local_overlapping (V,A,d,((denaming (V,A,(val . 1))) . d),(loc /. 1)) in dom (SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((Fibonacci_inv (A,loc,n0)),(denaming (V,A,(val . 6))),(loc /. 6))),(denaming (V,A,(val . 5))),(loc /. 5))),(denaming (V,A,(val . 4))),(loc /. 4))),(denaming (V,A,(val . 3))),(loc /. 3))),(denaming (V,A,(val . 2))),(loc /. 2))) & d in dom (denaming (V,A,(val . 1))) ) }
by NOMIN_2:def 11;
A40:
dom (SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((Fibonacci_inv (A,loc,n0)),(denaming (V,A,(val . 6))),(loc /. 6))),(denaming (V,A,(val . 5))),(loc /. 5))),(denaming (V,A,(val . 4))),(loc /. 4))),(denaming (V,A,(val . 3))),(loc /. 3))),(denaming (V,A,(val . 2))),(loc /. 2))) = { d where d is TypeSCNominativeData of V,A : ( local_overlapping (V,A,d,((denaming (V,A,(val . 2))) . d),(loc /. 2)) in dom (SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((Fibonacci_inv (A,loc,n0)),(denaming (V,A,(val . 6))),(loc /. 6))),(denaming (V,A,(val . 5))),(loc /. 5))),(denaming (V,A,(val . 4))),(loc /. 4))),(denaming (V,A,(val . 3))),(loc /. 3))) & d in dom (denaming (V,A,(val . 2))) ) }
by NOMIN_2:def 11;
A41:
dom (SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((Fibonacci_inv (A,loc,n0)),(denaming (V,A,(val . 6))),(loc /. 6))),(denaming (V,A,(val . 5))),(loc /. 5))),(denaming (V,A,(val . 4))),(loc /. 4))),(denaming (V,A,(val . 3))),(loc /. 3))) = { d where d is TypeSCNominativeData of V,A : ( local_overlapping (V,A,d,((denaming (V,A,(val . 3))) . d),(loc /. 3)) in dom (SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((Fibonacci_inv (A,loc,n0)),(denaming (V,A,(val . 6))),(loc /. 6))),(denaming (V,A,(val . 5))),(loc /. 5))),(denaming (V,A,(val . 4))),(loc /. 4))) & d in dom (denaming (V,A,(val . 3))) ) }
by NOMIN_2:def 11;
A42:
dom (SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((Fibonacci_inv (A,loc,n0)),(denaming (V,A,(val . 6))),(loc /. 6))),(denaming (V,A,(val . 5))),(loc /. 5))),(denaming (V,A,(val . 4))),(loc /. 4))) = { d where d is TypeSCNominativeData of V,A : ( local_overlapping (V,A,d,((denaming (V,A,(val . 4))) . d),(loc /. 4)) in dom (SC_Psuperpos ((SC_Psuperpos ((Fibonacci_inv (A,loc,n0)),(denaming (V,A,(val . 6))),(loc /. 6))),(denaming (V,A,(val . 5))),(loc /. 5))) & d in dom (denaming (V,A,(val . 4))) ) }
by NOMIN_2:def 11;
A43:
dom (SC_Psuperpos ((SC_Psuperpos ((Fibonacci_inv (A,loc,n0)),(denaming (V,A,(val . 6))),(loc /. 6))),(denaming (V,A,(val . 5))),(loc /. 5))) = { d where d is TypeSCNominativeData of V,A : ( local_overlapping (V,A,d,((denaming (V,A,(val . 5))) . d),(loc /. 5)) in dom (SC_Psuperpos ((Fibonacci_inv (A,loc,n0)),(denaming (V,A,(val . 6))),(loc /. 6))) & d in dom (denaming (V,A,(val . 5))) ) }
by NOMIN_2:def 11;
A44:
dom (SC_Psuperpos ((Fibonacci_inv (A,loc,n0)),(denaming (V,A,(val . 6))),(loc /. 6))) = { d where d is TypeSCNominativeData of V,A : ( local_overlapping (V,A,d,((denaming (V,A,(val . 6))) . d),(loc /. 6)) in dom (Fibonacci_inv (A,loc,n0)) & d in dom (denaming (V,A,(val . 6))) ) }
by NOMIN_2:def 11;
A45:
d1 in dom (denaming (V,A,(val . 1)))
by A20, A30, A33;
then A46:
(denaming (V,A,(val . 1))) . d1 is
TypeSCNominativeData of
V,
A
by PARTFUN1:4, NOMIN_1:39;
reconsider Li =
(LocalOverlapSeq (A,loc,val,d1,6)) . 1 as
NonatomicND of
V,
A by A26, Def6;
reconsider Lj =
(LocalOverlapSeq (A,loc,val,d1,6)) . 2 as
NonatomicND of
V,
A by A26, Def6;
reconsider Ln =
(LocalOverlapSeq (A,loc,val,d1,6)) . 3 as
NonatomicND of
V,
A by A26, Def6;
reconsider Ls =
(LocalOverlapSeq (A,loc,val,d1,6)) . 4 as
NonatomicND of
V,
A by A26, Def6;
reconsider Lb =
(LocalOverlapSeq (A,loc,val,d1,6)) . 5 as
NonatomicND of
V,
A by A26, Def6;
reconsider Lc =
(LocalOverlapSeq (A,loc,val,d1,6)) . 6 as
NonatomicND of
V,
A by A26, Def6;
A47:
(LocalOverlapSeq (A,loc,val,d1,6)) . 1
= local_overlapping (
V,
A,
d1,
((denaming (V,A,(val . 1))) . d1),
(loc /. 1))
by Def4;
A48:
(LocalOverlapSeq (A,loc,val,d1,6)) . (1 + 1) = local_overlapping (
V,
A,
Li,
((denaming (V,A,(val . 2))) . Li),
(loc /. 2))
by A26, Def4;
A49:
(LocalOverlapSeq (A,loc,val,d1,6)) . (2 + 1) = local_overlapping (
V,
A,
Lj,
((denaming (V,A,(val . 3))) . Lj),
(loc /. 3))
by A26, Def4;
A50:
(LocalOverlapSeq (A,loc,val,d1,6)) . (3 + 1) = local_overlapping (
V,
A,
Ln,
((denaming (V,A,(val . 4))) . Ln),
(loc /. 4))
by A26, Def4;
A51:
(LocalOverlapSeq (A,loc,val,d1,6)) . (4 + 1) = local_overlapping (
V,
A,
Ls,
((denaming (V,A,(val . 5))) . Ls),
(loc /. 5))
by A26, Def4;
A52:
(LocalOverlapSeq (A,loc,val,d1,6)) . (5 + 1) = local_overlapping (
V,
A,
Lb,
((denaming (V,A,(val . 6))) . Lb),
(loc /. 6))
by A26, Def4;
val . 2
in dom Li
by A29, Th10;
then A53:
Li in dom (denaming (V,A,(val . 2)))
by A34;
val . 3
in dom Lj
by A29, Th10;
then A54:
Lj in dom (denaming (V,A,(val . 3)))
by A35;
A55:
val . 4
in dom Ln
by A29, Th10;
then A56:
Ln in dom (denaming (V,A,(val . 4)))
by A36;
A57:
val . 5
in dom Ls
by A29, Th10;
then A58:
Ls in dom (denaming (V,A,(val . 5)))
by A37;
dom (Fibonacci_inv (A,loc,n0)) = ND (
V,
A)
by Def19;
then A59:
Lc in dom (Fibonacci_inv (A,loc,n0))
;
val . 6
in dom Lb
by A29, Th10;
then
Lb in dom (denaming (V,A,(val . 6)))
by A38;
then A60:
Lb in dom (SC_Psuperpos ((Fibonacci_inv (A,loc,n0)),(denaming (V,A,(val . 6))),(loc /. 6)))
by A44, A52, A59;
A61:
Ls in dom (SC_Psuperpos ((SC_Psuperpos ((Fibonacci_inv (A,loc,n0)),(denaming (V,A,(val . 6))),(loc /. 6))),(denaming (V,A,(val . 5))),(loc /. 5)))
by A43, A51, A60, A58;
then A62:
Ln in dom (SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((Fibonacci_inv (A,loc,n0)),(denaming (V,A,(val . 6))),(loc /. 6))),(denaming (V,A,(val . 5))),(loc /. 5))),(denaming (V,A,(val . 4))),(loc /. 4)))
by A42, A56, A50;
then A63:
Lj in dom (SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((Fibonacci_inv (A,loc,n0)),(denaming (V,A,(val . 6))),(loc /. 6))),(denaming (V,A,(val . 5))),(loc /. 5))),(denaming (V,A,(val . 4))),(loc /. 4))),(denaming (V,A,(val . 3))),(loc /. 3)))
by A41, A54, A49;
then A64:
Li in dom (SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((Fibonacci_inv (A,loc,n0)),(denaming (V,A,(val . 6))),(loc /. 6))),(denaming (V,A,(val . 5))),(loc /. 5))),(denaming (V,A,(val . 4))),(loc /. 4))),(denaming (V,A,(val . 3))),(loc /. 3))),(denaming (V,A,(val . 2))),(loc /. 2)))
by A40, A53, A48;
hence A65:
d in dom (SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((Fibonacci_inv (A,loc,n0)),(denaming (V,A,(val . 6))),(loc /. 6))),(denaming (V,A,(val . 5))),(loc /. 5))),(denaming (V,A,(val . 4))),(loc /. 4))),(denaming (V,A,(val . 3))),(loc /. 3))),(denaming (V,A,(val . 2))),(loc /. 2))),(denaming (V,A,(val . 1))),(loc /. 1)))
by A19, A39, A45, A47;
(SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((Fibonacci_inv (A,loc,n0)),(denaming (V,A,(val . 6))),(loc /. 6))),(denaming (V,A,(val . 5))),(loc /. 5))),(denaming (V,A,(val . 4))),(loc /. 4))),(denaming (V,A,(val . 3))),(loc /. 3))),(denaming (V,A,(val . 2))),(loc /. 2))),(denaming (V,A,(val . 1))),(loc /. 1))) . d = TRUE
A66:
Fibonacci_inv_pred A,
loc,
n0,
Lc
proof
take
Lc
;
NOMIN_7:def 18 ( Lc = Lc & {(loc /. 1),(loc /. 2),(loc /. 3),(loc /. 4),(loc /. 5),(loc /. 6)} c= dom Lc & Lc . (loc /. 2) = 1 & Lc . (loc /. 3) = n0 & ex I being Nat st
( I = Lc . (loc /. 1) & Lc . (loc /. 4) = Fib I & Lc . (loc /. 5) = Fib (I + 1) ) )
thus
Lc = Lc
;
( {(loc /. 1),(loc /. 2),(loc /. 3),(loc /. 4),(loc /. 5),(loc /. 6)} c= dom Lc & Lc . (loc /. 2) = 1 & Lc . (loc /. 3) = n0 & ex I being Nat st
( I = Lc . (loc /. 1) & Lc . (loc /. 4) = Fib I & Lc . (loc /. 5) = Fib (I + 1) ) )
A67:
loc /. 1
in dom Lc
by A29, Th9;
A68:
loc /. 2
in dom Lc
by A29, Th9;
A69:
loc /. 3
in dom Lc
by A29, Th9;
A70:
loc /. 4
in dom Lc
by A29, Th9;
A71:
loc /. 5
in dom Lc
by A29, Th9;
loc /. 6
in dom Lc
by A29, Th9;
hence
{(loc /. 1),(loc /. 2),(loc /. 3),(loc /. 4),(loc /. 5),(loc /. 6)} c= dom Lc
by A67, A68, A69, A70, A71, ENUMSET1:def 4;
( Lc . (loc /. 2) = 1 & Lc . (loc /. 3) = n0 & ex I being Nat st
( I = Lc . (loc /. 1) & Lc . (loc /. 4) = Fib I & Lc . (loc /. 5) = Fib (I + 1) ) )
A72:
loc /. 1
<> val . 4
by A6;
A73:
loc /. 1
<> val . 5
by A6;
thus
Lc . (loc /. 2) = 1
by A4, A5, A6, A22, A29, Th13;
( Lc . (loc /. 3) = n0 & ex I being Nat st
( I = Lc . (loc /. 1) & Lc . (loc /. 4) = Fib I & Lc . (loc /. 5) = Fib (I + 1) ) )
thus
Lc . (loc /. 3) = n0
by A4, A5, A6, A23, A29, Th13;
ex I being Nat st
( I = Lc . (loc /. 1) & Lc . (loc /. 4) = Fib I & Lc . (loc /. 5) = Fib (I + 1) )
A74:
Ln . (val . 4) =
Li . (val . 4)
by A6, A29, Th11
.=
0
by A2, A3, A20, A24, A31, A46, A47, A72, NOMIN_5:3
;
A75:
Ls . (val . 5) =
Li . (val . 5)
by A6, A29, Th11
.=
1
by A2, A3, A20, A25, A32, A46, A47, A73, NOMIN_5:3
;
take
0
;
( 0 = Lc . (loc /. 1) & Lc . (loc /. 4) = Fib 0 & Lc . (loc /. 5) = Fib (0 + 1) )
thus
Lc . (loc /. 1) = 0
by A4, A5, A6, A21, A29, Th13;
( Lc . (loc /. 4) = Fib 0 & Lc . (loc /. 5) = Fib (0 + 1) )
thus Lc . (loc /. 4) =
Ls . (loc /. 4)
by A4, A5, A29, Th12
.=
Fib 0
by A2, A55, A50, A74, Th2, PRE_FF:1
;
Lc . (loc /. 5) = Fib (0 + 1)
thus Lc . (loc /. 5) =
Lb . (loc /. 5)
by A4, A5, A29, Th12
.=
Fib (0 + 1)
by A2, A51, A57, A75, Th2, PRE_FF:1
;
verum
end;
thus (SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((Fibonacci_inv (A,loc,n0)),(denaming (V,A,(val . 6))),(loc /. 6))),(denaming (V,A,(val . 5))),(loc /. 5))),(denaming (V,A,(val . 4))),(loc /. 4))),(denaming (V,A,(val . 3))),(loc /. 3))),(denaming (V,A,(val . 2))),(loc /. 2))),(denaming (V,A,(val . 1))),(loc /. 1))) . d =
(SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((Fibonacci_inv (A,loc,n0)),(denaming (V,A,(val . 6))),(loc /. 6))),(denaming (V,A,(val . 5))),(loc /. 5))),(denaming (V,A,(val . 4))),(loc /. 4))),(denaming (V,A,(val . 3))),(loc /. 3))),(denaming (V,A,(val . 2))),(loc /. 2))) . ((LocalOverlapSeq (A,loc,val,d1,6)) . 1)
by A19, A47, A65, NOMIN_2:35
.=
(SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((Fibonacci_inv (A,loc,n0)),(denaming (V,A,(val . 6))),(loc /. 6))),(denaming (V,A,(val . 5))),(loc /. 5))),(denaming (V,A,(val . 4))),(loc /. 4))),(denaming (V,A,(val . 3))),(loc /. 3))) . ((LocalOverlapSeq (A,loc,val,d1,6)) . 2)
by A48, A64, NOMIN_2:35
.=
(SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((Fibonacci_inv (A,loc,n0)),(denaming (V,A,(val . 6))),(loc /. 6))),(denaming (V,A,(val . 5))),(loc /. 5))),(denaming (V,A,(val . 4))),(loc /. 4))) . ((LocalOverlapSeq (A,loc,val,d1,6)) . 3)
by A49, A63, NOMIN_2:35
.=
(SC_Psuperpos ((SC_Psuperpos ((Fibonacci_inv (A,loc,n0)),(denaming (V,A,(val . 6))),(loc /. 6))),(denaming (V,A,(val . 5))),(loc /. 5))) . ((LocalOverlapSeq (A,loc,val,d1,6)) . 4)
by A50, A62, NOMIN_2:35
.=
(SC_Psuperpos ((Fibonacci_inv (A,loc,n0)),(denaming (V,A,(val . 6))),(loc /. 6))) . ((LocalOverlapSeq (A,loc,val,d1,6)) . 5)
by A51, A61, NOMIN_2:35
.=
(Fibonacci_inv (A,loc,n0)) . ((LocalOverlapSeq (A,loc,val,d1,6)) . 6)
by A52, A60, NOMIN_2:35
.=
TRUE
by A59, A66, Def19
;
verum
end;
then A76:
<*(valid_Fibonacci_input (V,A,val,n0)),(SC_assignment ((denaming (V,A,(val . 1))),(loc /. 1))),(SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((Fibonacci_inv (A,loc,n0)),(denaming (V,A,(val . 6))),(loc /. 6))),(denaming (V,A,(val . 5))),(loc /. 5))),(denaming (V,A,(val . 4))),(loc /. 4))),(denaming (V,A,(val . 3))),(loc /. 3))),(denaming (V,A,(val . 2))),(loc /. 2)))*> is SFHT of (ND (V,A))
by A13, NOMIN_3:15;
A77:
<*(PP_inversion (SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((Fibonacci_inv (A,loc,n0)),(denaming (V,A,(val . 6))),(loc /. 6))),(denaming (V,A,(val . 5))),(loc /. 5))),(denaming (V,A,(val . 4))),(loc /. 4))),(denaming (V,A,(val . 3))),(loc /. 3))),(denaming (V,A,(val . 2))),(loc /. 2)))),(SC_assignment ((denaming (V,A,(val . 2))),(loc /. 2))),(SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((Fibonacci_inv (A,loc,n0)),(denaming (V,A,(val . 6))),(loc /. 6))),(denaming (V,A,(val . 5))),(loc /. 5))),(denaming (V,A,(val . 4))),(loc /. 4))),(denaming (V,A,(val . 3))),(loc /. 3)))*> is SFHT of (ND (V,A))
by NOMIN_4:16;
A78:
<*(PP_inversion (SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((Fibonacci_inv (A,loc,n0)),(denaming (V,A,(val . 6))),(loc /. 6))),(denaming (V,A,(val . 5))),(loc /. 5))),(denaming (V,A,(val . 4))),(loc /. 4))),(denaming (V,A,(val . 3))),(loc /. 3)))),(SC_assignment ((denaming (V,A,(val . 3))),(loc /. 3))),(SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((Fibonacci_inv (A,loc,n0)),(denaming (V,A,(val . 6))),(loc /. 6))),(denaming (V,A,(val . 5))),(loc /. 5))),(denaming (V,A,(val . 4))),(loc /. 4)))*> is SFHT of (ND (V,A))
by NOMIN_4:16;
A79:
<*(PP_inversion (SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((Fibonacci_inv (A,loc,n0)),(denaming (V,A,(val . 6))),(loc /. 6))),(denaming (V,A,(val . 5))),(loc /. 5))),(denaming (V,A,(val . 4))),(loc /. 4)))),(SC_assignment ((denaming (V,A,(val . 4))),(loc /. 4))),(SC_Psuperpos ((SC_Psuperpos ((Fibonacci_inv (A,loc,n0)),(denaming (V,A,(val . 6))),(loc /. 6))),(denaming (V,A,(val . 5))),(loc /. 5)))*> is SFHT of (ND (V,A))
by NOMIN_4:16;
A80:
<*(PP_inversion (SC_Psuperpos ((SC_Psuperpos ((Fibonacci_inv (A,loc,n0)),(denaming (V,A,(val . 6))),(loc /. 6))),(denaming (V,A,(val . 5))),(loc /. 5)))),(SC_assignment ((denaming (V,A,(val . 5))),(loc /. 5))),(SC_Psuperpos ((Fibonacci_inv (A,loc,n0)),(denaming (V,A,(val . 6))),(loc /. 6)))*> is SFHT of (ND (V,A))
by NOMIN_4:16;
<*(PP_inversion (SC_Psuperpos ((Fibonacci_inv (A,loc,n0)),(denaming (V,A,(val . 6))),(loc /. 6)))),(SC_assignment ((denaming (V,A,(val . 6))),(loc /. 6))),(Fibonacci_inv (A,loc,n0))*> is SFHT of (ND (V,A))
by NOMIN_4:16;
hence
<*(valid_Fibonacci_input (V,A,val,n0)),(initial_assignments (A,loc,val,6)),(Fibonacci_inv (A,loc,n0))*> is SFHT of (ND (V,A))
by A18, A8, A9, A10, A12, A11, A76, A77, A78, A79, A80, Th3; verum