let H, v be LTL-formula; ( H in Subformulae v implies len (LTLNew2 (H,v)) <= (len H) - 1 )
set New = LTLNew2 (H,v);
set Left = {(the_left_argument_of H)};
set Right = {(the_right_argument_of H)};
assume A1:
H in Subformulae v
; len (LTLNew2 (H,v)) <= (len H) - 1
then A2:
LTLNew2 (H,v) = LTLNew2 H
by Def28;
ex F being LTL-formula st
( H = F & F is_subformula_of v )
by A1, MODELC_2:def 24;
then A3:
Subformulae H c= Subformulae v
by MODELC_2:46;
now len (LTLNew2 (H,v)) <= (len H) - 1per cases
( H is Release or H is disjunctive or H is Until or H is conjunctive or H is next or ( not H is conjunctive & not H is disjunctive & not H is next & not H is Until & not H is Release ) )
;
suppose A4:
H is
Release
;
len (LTLNew2 (H,v)) <= (len H) - 1then
{(the_right_argument_of H)} is
Subset of
(Subformulae H)
by Lm12;
then reconsider Right =
{(the_right_argument_of H)} as
Subset of
(Subformulae v) by A3, XBOOLE_1:1;
{(the_left_argument_of H)} is
Subset of
(Subformulae H)
by A4, Lm12;
then reconsider Left =
{(the_left_argument_of H)} as
Subset of
(Subformulae v) by A3, XBOOLE_1:1;
LTLNew2 (
H,
v)
= {(the_left_argument_of H),(the_right_argument_of H)}
by A2, A4, Def2;
then
LTLNew2 (
H,
v)
= Left \/ Right
by ENUMSET1:1;
then A5:
len (LTLNew2 (H,v)) <= (len Left) + (len Right)
by Th18;
A6:
len H = (1 + (len (the_left_argument_of H))) + (len (the_right_argument_of H))
by A4, MODELC_2:11;
(
len Left = len (the_left_argument_of H) &
len Right = len (the_right_argument_of H) )
by Th14;
hence
len (LTLNew2 (H,v)) <= (len H) - 1
by A6, A5;
verum end; end; end;
hence
len (LTLNew2 (H,v)) <= (len H) - 1
; verum