let L be FinSequence; :: thesis: for F, H being LTL-formula
for W being Subset of (Subformulae H) st rng L = Subformulae H & L is one-to-one & F in W holds
len (L,(W \ {F})) = (len (L,W)) - (len F)
let F, H be LTL-formula; :: thesis: for W being Subset of (Subformulae H) st rng L = Subformulae H & L is one-to-one & F in W holds
len (L,(W \ {F})) = (len (L,W)) - (len F)
let W be Subset of (Subformulae H); :: thesis: ( rng L = Subformulae H & L is one-to-one & F in W implies len (L,(W \ {F})) = (len (L,W)) - (len F) )
assume that
A1: rng L = Subformulae H and
A2: L is one-to-one and
A3: F in W ; :: thesis: len (L,(W \ {F})) = (len (L,W)) - (len F)
consider x being object such that
A4: x in dom L and
A5: L . x = F by A1, A3, FUNCT_1:def 3;
set R2 = Partial_seq (L,(W \ {F}));
set R1 = Partial_seq (L,W);
set n = len L;
A6: F in LTL_WFF by MODELC_2:1;
x in Seg (len L) by A4, FINSEQ_1:def 3;
then x in { k where k is Nat : ( 1 <= k & k <= len L ) } by FINSEQ_1:def 1;
then consider k being Nat such that
A7: x = k and
1 <= k and
A8: k <= len L ;
reconsider k = k as Nat ;
L . k in {F} by A5, A7, TARSKI:def 1;
then not L . k in W \ {F} by XBOOLE_0:def 5;
then A9: (Partial_seq (L,(W \ {F}))) . k = 0 by Def24;
for i being Nat st i <= len L & not i = k holds
(Partial_seq (L,W)) . i = (Partial_seq (L,(W \ {F}))) . i

proof

let i be Nat; :: thesis: ( i <= len L & not i = k implies (Partial_seq (L,W)) . i = (Partial_seq (L,(W \ {F}))) . i )
assume that
i <= len L and
A10: not i = k ; :: thesis: (Partial_seq (L,W)) . i = (Partial_seq (L,(W \ {F}))) . i

now :: thesis: (Partial_seq (L,W)) . i = (Partial_seq (L,(W \ {F}))) . i

per cases ( not i in dom L or i in dom L ) ;

suppose not i in dom L ; :: thesis: (Partial_seq (L,W)) . i = (Partial_seq (L,(W \ {F}))) . i

then A11: L . i = {} by FUNCT_1:def 2;
then A12: not L . i in W by Lm24;
not L . i in W \ {F} by A11, Lm24;
then (Partial_seq (L,(W \ {F}))) . i = 0 by Def24
.= (Partial_seq (L,W)) . i by A12, Def24 ;
hence (Partial_seq (L,W)) . i = (Partial_seq (L,(W \ {F}))) . i ; :: thesis: verum

end;

suppose i in dom L ; :: thesis: (Partial_seq (L,W)) . i = (Partial_seq (L,(W \ {F}))) . i

then not L . i = F by A2, A4, A5, A7, A10, FUNCT_1:def 4;
then A13: not L . i in {F} by TARSKI:def 1;

now :: thesis: (Partial_seq (L,W)) . i = (Partial_seq (L,(W \ {F}))) . i

per cases ( L . i in W or not L . i in W ) ;

suppose A14: L . i in W ; :: thesis: (Partial_seq (L,W)) . i = (Partial_seq (L,(W \ {F}))) . i

then L . i in W \ {F} by A13, XBOOLE_0:def 5;
then (Partial_seq (L,(W \ {F}))) . i = len (CastLTL (L . i)) by Def24
.= (Partial_seq (L,W)) . i by A14, Def24 ;
hence (Partial_seq (L,W)) . i = (Partial_seq (L,(W \ {F}))) . i ; :: thesis: verum

end;

suppose A15: not L . i in W ; :: thesis: (Partial_seq (L,W)) . i = (Partial_seq (L,(W \ {F}))) . i

then not L . i in W \ {F} by XBOOLE_0:def 5;
then (Partial_seq (L,(W \ {F}))) . i = 0 by Def24
.= (Partial_seq (L,W)) . i by A15, Def24 ;
hence (Partial_seq (L,W)) . i = (Partial_seq (L,(W \ {F}))) . i ; :: thesis: verum

end;

end;

end;

hence (Partial_seq (L,W)) . i = (Partial_seq (L,(W \ {F}))) . i ; :: thesis: verum

end;

end;

end;

hence (Partial_seq (L,W)) . i = (Partial_seq (L,(W \ {F}))) . i ; :: thesis: verum

end;

then A16: (Sum ((Partial_seq (L,W)),(len L))) - ((Partial_seq (L,W)) . k) = (Sum ((Partial_seq (L,(W \ {F}))),(len L))) - ((Partial_seq (L,(W \ {F}))) . k) by A8, Lm26;
(Partial_seq (L,W)) . k = len (CastLTL (L . k)) by A3, A5, A7, Def24
.= len F by A5, A7, A6, MODELC_2:def 25 ;
hence len (L,(W \ {F})) = (len (L,W)) - (len F) by A9, A16; :: thesis: verum