let V, A be set ; :: thesis:
let loc be V -valued Function; :: thesis:
let n0 be Nat; :: thesis:
let val be 6 -element FinSequence; :: thesis:
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 ; :: thesis:
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); :: according to NOMIN_3:def 3 :: thesis:
assume ( d in dom (valid_Fibonacci_input (V,A,val,n0)) & (valid_Fibonacci_input (V,A,val,n0)) . d = TRUE ) ; :: thesis:
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 ; :: according to TARSKI:def 3 :: thesis:
assume y in rng val ; :: thesis:
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; :: thesis:

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; :: thesis:
A66: Fibonacci_inv_pred A,loc,n0,Lc

proof

take Lc ; :: according to NOMIN_7:def 18 :: thesis:
thus Lc = Lc ; :: thesis:
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; :: thesis:
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; :: thesis:
thus Lc . (loc /. 3) = n0 by A4, A5, A6, A23, A29, Th13; :: thesis:
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 ; :: thesis:
thus Lc . (loc /. 1) = 0 by A4, A5, A6, A21, A29, Th13; :: thesis:
thus Lc . (loc /. 4) = Ls . (loc /. 4) by A4, A5, A29, Th12
.= Fib 0 by A2, A55, A50, A74, Th2, PRE_FF:1 ; :: thesis:
thus Lc . (loc /. 5) = Lb . (loc /. 5) by A4, A5, A29, Th12
.= Fib (0 + 1) by A2, A51, A57, A75, Th2, PRE_FF:1 ; :: thesis:

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 ; :: thesis:

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; :: thesis: