let H be CTL-formula; :: thesis: ( ( H is atomic & H . 1 <> 0 & H . 1 <> 1 & H . 1 <> 2 & H . 1 <> 3 & H . 1 <> 4 ) or ( H is negative & H . 1 = 0 ) or ( H is conjunctive & H . 1 = 1 ) or ( H is ExistNext & H . 1 = 2 ) or ( H is ExistGlobal & H . 1 = 3 ) or ( H is ExistUntill & H . 1 = 4 ) )
per cases ( H is atomic or H is negative or H is conjunctive or H is ExistNext or H is ExistGlobal or H is ExistUntill ) by Th2;
case H is atomic ; :: thesis: ( H . 1 <> 0 & H . 1 <> 1 & H . 1 <> 2 & H . 1 <> 3 & H . 1 <> 4 )
hence ( H . 1 <> 0 & H . 1 <> 1 & H . 1 <> 2 & H . 1 <> 3 & H . 1 <> 4 ) by Lm8; :: thesis: verum
end;
case H is negative ; :: thesis: H . 1 = 0
hence H . 1 = 0 by Lm3; :: thesis: verum
end;
case H is conjunctive ; :: thesis: H . 1 = 1
hence H . 1 = 1 by Lm4; :: thesis: verum
end;
case H is ExistNext ; :: thesis: H . 1 = 2
hence H . 1 = 2 by Lm5; :: thesis: verum
end;
case H is ExistGlobal ; :: thesis: H . 1 = 3
hence H . 1 = 3 by Lm6; :: thesis: verum
end;
case H is ExistUntill ; :: thesis: H . 1 = 4
hence H . 1 = 4 by Lm7; :: thesis: verum
end;
end;