defpred S1[ Nat] means for F being Tuple of $1,BOOLEAN st F = 0* $1 holds
Absval F = 0 ;
A1:
S1[1]
by BINARITH:41, FINSEQ_2:73;
A2:
for n being non empty Nat st S1[n] holds
S1[n + 1]
proof
let n be non
empty Nat;
:: thesis: ( S1[n] implies S1[n + 1] )
assume A3:
for
F being
Tuple of
n,
BOOLEAN st
F = 0* n holds
Absval F = 0
;
:: thesis: S1[n + 1]
let F be
Tuple of
(n + 1),
BOOLEAN ;
:: thesis: ( F = 0* (n + 1) implies Absval F = 0 )
0* n in BOOLEAN *
by Th5;
then A4:
0* n is
FinSequence of
BOOLEAN
by FINSEQ_1:def 11;
len (0* n) = n
by FINSEQ_1:def 18;
then reconsider F1 =
0* n as
Tuple of
n,
BOOLEAN by A4, FINSEQ_2:110;
assume
F = 0* (n + 1)
;
:: thesis: Absval F = 0
hence Absval F =
Absval (F1 ^ <*FALSE *>)
by FINSEQ_2:74
.=
(Absval F1) + (IFEQ FALSE ,FALSE ,0 ,(2 to_power n))
by BINARITH:46
.=
0 + (IFEQ FALSE ,FALSE ,0 ,(2 to_power n))
by A3
.=
0
by FUNCOP_1:def 8
;
:: thesis: verum
end;
thus
for n being non empty Nat holds S1[n]
from NAT_1:sch 10(A1, A2); :: thesis: verum