let V, A be set ; :: thesis:
let loc be V -valued Function; :: thesis:
let d1 be NonatomicND of V,A; :: thesis:
let size be non zero Nat; :: thesis:
let val be size -element FinSequence; :: thesis:
let p be SCPartialNominativePredicate of V,A; :: thesis:
set SE = SC_Psuperpos_Seq (loc,val,p);
set F = LocalOverlapSeq (A,loc,val,d1,size);
set dd = (LocalOverlapSeq (A,loc,val,d1,size)) . (size - 1);
set D1 = denaming (V,A,(val . 1));
set D2 = denaming (V,A,(val . 2));
set P = (SC_Psuperpos_Seq (loc,val,p)) . (size - 2);
assume that
A1: 3 <= size and
A2: loc,val,size are_correct_wrt d1 and
A3: local_overlapping (V,A,((LocalOverlapSeq (A,loc,val,d1,size)) . (size - 1)),((denaming (V,A,(val . (len val)))) . ((LocalOverlapSeq (A,loc,val,d1,size)) . (size - 1))),(loc /. (len val))) in dom p and
A4: local_overlapping (V,A,d1,((denaming (V,A,(val . 1))) . d1),(loc /. 1)) in dom ((SC_Psuperpos_Seq (loc,val,p)) . (size - 1)) ; :: thesis:
A5: len val = size by CARD_1:def 7;
A6: len (SC_Psuperpos_Seq (loc,val,p)) = len val by Def9;
A7: len (LocalOverlapSeq (A,loc,val,d1,size)) = size by NOMIN_7:def 4;
A8: 2 < size by A1, XXREAL_0:2;
reconsider nn = size - 2 as Element of NAT by A1, XXREAL_0:2, INT_1:5;
set N = nn + 1;
A9: 3 - 2 <= nn by A1, XREAL_1:9;
then A10: 1 + 1 <= nn + 1 by XREAL_1:6;
A12: size - 1 < size by XREAL_1:44;
A13: nn < size by XREAL_1:44;
A15: (len val) - (nn + 1) = 1 by A5;
A16: (LocalOverlapSeq (A,loc,val,d1,size)) . 1 = local_overlapping (V,A,d1,((denaming (V,A,(val . 1))) . d1),(loc /. 1)) by NOMIN_7:def 4;
A11: 1 <= nn + 1 by A9, XREAL_1:29;
then A14: 1 < len (LocalOverlapSeq (A,loc,val,d1,size)) by A7, A12, XXREAL_0:2;
then A17: (LocalOverlapSeq (A,loc,val,d1,size)) . 1 is NonatomicND of V,A by NOMIN_7:def 6;
A18: (SC_Psuperpos_Seq (loc,val,p)) . ((nn + 1) + 1) = SC_Psuperpos (((SC_Psuperpos_Seq (loc,val,p)) . (nn + 1)),(denaming (V,A,(val . 1))),(loc /. 1)) by A6, A11, A12, A15, Def9;
A19: (LocalOverlapSeq (A,loc,val,d1,size)) . (1 + 1) = local_overlapping (V,A,((LocalOverlapSeq (A,loc,val,d1,size)) . 1),((denaming (V,A,(val . (1 + 1)))) . ((LocalOverlapSeq (A,loc,val,d1,size)) . 1)),(loc /. (1 + 1))) by A14, NOMIN_7:def 4;
A20: dom (SC_Psuperpos (((SC_Psuperpos_Seq (loc,val,p)) . (size - 2)),(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_Seq (loc,val,p)) . (size - 2)) & d in dom (denaming (V,A,(val . 2))) ) } by NOMIN_2:def 11;
A21: local_overlapping (V,A,((LocalOverlapSeq (A,loc,val,d1,size)) . ((size - nn) - 1)),((denaming (V,A,(val . ((len val) - nn)))) . ((LocalOverlapSeq (A,loc,val,d1,size)) . ((size - nn) - 1))),(loc /. ((len val) - nn))) in dom ((SC_Psuperpos_Seq (loc,val,p)) . (size - 2)) by A2, A10, A3, XREAL_1:44, Th16;
A22: dom (denaming (V,A,(val . 2))) = { d where d is NonatomicND of V,A : val . 2 in dom d } by NOMIN_1:def 18;
val . 2 in dom ((LocalOverlapSeq (A,loc,val,d1,size)) . 1) by A7, A2, A8, A14, NOMIN_7:10;
then (LocalOverlapSeq (A,loc,val,d1,size)) . 1 in dom (denaming (V,A,(val . 2))) by A17, A22;
then A23: (LocalOverlapSeq (A,loc,val,d1,size)) . 1 in dom (SC_Psuperpos (((SC_Psuperpos_Seq (loc,val,p)) . (size - 2)),(denaming (V,A,(val . 2))),(loc /. 2))) by A5, A17, A20, A21;
A24: dom (SC_Psuperpos (((SC_Psuperpos_Seq (loc,val,p)) . (nn + 1)),(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_Seq (loc,val,p)) . (nn + 1)) & d in dom (denaming (V,A,(val . 1))) ) } by NOMIN_2:def 11;
A25: dom (denaming (V,A,(val . 1))) = { d where d is NonatomicND of V,A : val . 1 in dom d } by NOMIN_1:def 18;
A26: val is_valid_wrt d1 by A2;
1 in dom val by A5, A7, A14, FINSEQ_3:25;
then val . 1 in rng val by FUNCT_1:def 3;
then d1 in dom (denaming (V,A,(val . 1))) by A25, A26;
then d1 in dom (SC_Psuperpos (((SC_Psuperpos_Seq (loc,val,p)) . (nn + 1)),(denaming (V,A,(val . 1))),(loc /. 1))) by A24, A4;
hence ((SC_Psuperpos_Seq (loc,val,p)) . (len (SC_Psuperpos_Seq (loc,val,p)))) . d1 = ((SC_Psuperpos_Seq (loc,val,p)) . (nn + 1)) . ((LocalOverlapSeq (A,loc,val,d1,size)) . (size - (nn + 1))) by A5, A6, A18, A16, NOMIN_2:35
.= ((SC_Psuperpos_Seq (loc,val,p)) . nn) . ((LocalOverlapSeq (A,loc,val,d1,size)) . (size - nn)) by A2, A3, A11, A12, A9, A13, Th17
.= (SC_Psuperpos (((SC_Psuperpos_Seq (loc,val,p)) . (size - 2)),(denaming (V,A,(val . 2))),(loc /. 2))) . ((LocalOverlapSeq (A,loc,val,d1,size)) . 1) by A17, A23, A19, NOMIN_2:35 ;
:: thesis: