defpred S₁[ Nat] means for H being LTL-formula st len H = $1 holds
P₁[H];
A4: for n being Nat st ( for k being Nat st k < n holds
S₁[k] ) holds
S₁[n]

proof

let n be Nat; :: thesis: ( ( for k being Nat st k < n holds
S₁[k] ) implies S₁[n] )
assume A5: for k being Nat st k < n holds
for H being LTL-formula st len H = k holds
P₁[H] ; :: thesis: S₁[n]
let H be LTL-formula; :: thesis: ( len H = n implies P₁[H] )
assume A6: len H = n ; :: thesis: P₁[H]

A7: now :: thesis: ( ( H is conjunctive or H is disjunctive or H is Until or H is Release ) implies P₁[H] )

assume A8: ( H is conjunctive or H is disjunctive or H is Until or H is Release ) ; :: thesis: P₁[H]
then len (the_right_argument_of H) < len H by Th11;
then A9: P₁[ the_right_argument_of H] by A5, A6;
len (the_left_argument_of H) < len H by A8, Th11;
then P₁[ the_left_argument_of H] by A5, A6;
hence P₁[H] by A3, A8, A9; :: thesis: verum

end;

now :: thesis: ( ( H is negative or H is next ) implies P₁[H] )

assume A10: ( H is negative or H is next ) ; :: thesis: P₁[H]
then len (the_argument_of H) < len H by Th10;
then P₁[ the_argument_of H] by A5, A6;
hence P₁[H] by A2, A10; :: thesis: verum

end;

hence P₁[H] by A1, A7, Th2; :: thesis: verum

end;

A11: for n being Nat holds S₁[n] from NAT_1:sch 4(A4);
let H be LTL-formula; :: thesis: P₁[H]
len H = len H ;
hence P₁[H] by A11; :: thesis: verum