set A = F1();
A6:
ex n being Nat st F2() in (ElementaryInstructions F1()) |^ n
by Th79;
defpred S1[ Nat] means for I being Element of F1() st I in (ElementaryInstructions F1()) |^ $1 holds
P1[I];
(ElementaryInstructions F1()) |^ 0 = ElementaryInstructions F1()
by Th18;
then A7:
S1[ 0 ]
by A1;
A8:
now for n being Nat st S1[n] holds
S1[n + 1]let n be
Nat;
( S1[n] implies S1[n + 1] )assume A9:
S1[
n]
;
S1[n + 1]thus
S1[
n + 1]
verumproof
let I be
Element of
F1();
( I in (ElementaryInstructions F1()) |^ (n + 1) implies P1[I] )
assume A10:
I in (ElementaryInstructions F1()) |^ (n + 1)
;
P1[I]
per cases
( I in (ElementaryInstructions F1()) |^ n or I = EmptyIns F1() or ex I1, I2 being Element of F1() st
( I = I1 \; I2 & I1 in (ElementaryInstructions F1()) |^ n & I2 in (ElementaryInstructions F1()) |^ n ) or ex C, I1, I2 being Element of F1() st
( I = if-then-else (C,I1,I2) & C in (ElementaryInstructions F1()) |^ n & I1 in (ElementaryInstructions F1()) |^ n & I2 in (ElementaryInstructions F1()) |^ n ) or ex C, J being Element of F1() st
( I = while (C,J) & C in (ElementaryInstructions F1()) |^ n & J in (ElementaryInstructions F1()) |^ n ) )
by A10, Th77;
suppose
ex
C,
I1,
I2 being
Element of
F1() st
(
I = if-then-else (
C,
I1,
I2) &
C in (ElementaryInstructions F1()) |^ n &
I1 in (ElementaryInstructions F1()) |^ n &
I2 in (ElementaryInstructions F1()) |^ n )
;
P1[I]then consider C,
I1,
I2 being
Element of
F1()
such that A15:
I = if-then-else (
C,
I1,
I2)
and A16:
C in (ElementaryInstructions F1()) |^ n
and A17:
I1 in (ElementaryInstructions F1()) |^ n
and A18:
I2 in (ElementaryInstructions F1()) |^ n
;
A19:
P1[
C]
by A9, A16;
A20:
P1[
I1]
by A9, A17;
P1[
I2]
by A9, A18;
hence
P1[
I]
by A4, A15, A19, A20;
verum end; end;
end; end;
for n being Nat holds S1[n]
from NAT_1:sch 2(A7, A8);
hence
P1[F2()]
by A6; verum