defpred S₁[ non zero Nat] means for k being Nat st k + 1 < 2 to_power $1 holds
$1 -BinarySequence (k + 1) = ($1 -BinarySequence k) + (Bin1 $1);
A1: for n being non zero Nat st S₁[n] holds
S₁[n + 1]

proof

let n be non zero Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A2: S₁[n] ; :: thesis: S₁[n + 1]
let k be Nat; :: thesis: ( k + 1 < 2 to_power (n + 1) implies (n + 1) -BinarySequence (k + 1) = ((n + 1) -BinarySequence k) + (Bin1 (n + 1)) )
assume A3: k + 1 < 2 to_power (n + 1) ; :: thesis: (n + 1) -BinarySequence (k + 1) = ((n + 1) -BinarySequence k) + (Bin1 (n + 1))
then A4: k < 2 to_power (n + 1) by NAT_1:13;

now :: thesis: (n + 1) -BinarySequence (k + 1) = ((n + 1) -BinarySequence k) + (Bin1 (n + 1))

per cases ( k + 1 < 2 to_power n or k + 1 > 2 to_power n or k + 1 = 2 to_power n ) by XXREAL_0:1;

suppose A5: k + 1 < 2 to_power n ; :: thesis: (n + 1) -BinarySequence (k + 1) = ((n + 1) -BinarySequence k) + (Bin1 (n + 1))

then A6: k < 2 to_power n by NAT_1:13;
A7: add_ovfl ((n -BinarySequence k),(Bin1 n)) = FALSE by A5, Th32;
thus (n + 1) -BinarySequence (k + 1) = (n -BinarySequence (k + 1)) ^ <*FALSE*> by A5, Th27
.= ((n -BinarySequence k) + (Bin1 n)) ^ <*((FALSE 'xor' FALSE) 'xor' (add_ovfl ((n -BinarySequence k),(Bin1 n))))*> by A2, A5, A7
.= ((n -BinarySequence k) ^ <*FALSE*>) + ((Bin1 n) ^ <*FALSE*>) by BINARITH:19
.= ((n -BinarySequence k) ^ <*FALSE*>) + (Bin1 (n + 1)) by BINARI_2:7
.= ((n + 1) -BinarySequence k) + (Bin1 (n + 1)) by A6, Th27 ; :: thesis: verum

end;

suppose A8: k + 1 > 2 to_power n ; :: thesis: (n + 1) -BinarySequence (k + 1) = ((n + 1) -BinarySequence k) + (Bin1 (n + 1))

then A9: k >= 2 to_power n by NAT_1:13;
k + 1 < (2 to_power n) * (2 to_power 1) by A3, POWER:27;
then k + 1 < (2 to_power n) * 2 by POWER:25;
then k + 1 < (2 to_power n) + (2 to_power n) ;
then (k + 1) - (2 to_power n) < 2 to_power n by XREAL_1:19;
then (k - (2 to_power n)) + 1 < 2 to_power n ;
then A10: (k -' (2 to_power n)) + 1 < 2 to_power n by A9, XREAL_1:233;
then A11: add_ovfl ((n -BinarySequence (k -' (2 to_power n))),(Bin1 n)) = FALSE by Th32;
thus (n + 1) -BinarySequence (k + 1) = (n -BinarySequence ((k + 1) -' (2 to_power n))) ^ <*TRUE*> by A3, A8, Lm3
.= (n -BinarySequence ((k -' (2 to_power n)) + 1)) ^ <*TRUE*> by A9, NAT_D:38
.= ((n -BinarySequence (k -' (2 to_power n))) + (Bin1 n)) ^ <*((TRUE 'xor' FALSE) 'xor' (add_ovfl ((n -BinarySequence (k -' (2 to_power n))),(Bin1 n))))*> by A2, A10, A11
.= ((n -BinarySequence (k -' (2 to_power n))) ^ <*TRUE*>) + ((Bin1 n) ^ <*FALSE*>) by BINARITH:19
.= ((n -BinarySequence (k -' (2 to_power n))) ^ <*TRUE*>) + (Bin1 (n + 1)) by BINARI_2:7
.= ((n + 1) -BinarySequence k) + (Bin1 (n + 1)) by A4, A9, Lm3 ; :: thesis: verum

end;

suppose A12: k + 1 = 2 to_power n ; :: thesis: (n + 1) -BinarySequence (k + 1) = ((n + 1) -BinarySequence k) + (Bin1 (n + 1))

0* n in BOOLEAN * by Th4;
then 0* n is FinSequence of BOOLEAN by FINSEQ_1:def 11;
then reconsider z = 0* n as Tuple of n, BOOLEAN ;
A13: k < 2 to_power n by A12, NAT_1:13;
k = (2 to_power n) - 1 by A12;
then A14: n -BinarySequence k = 'not' z by A13, Lm4;
thus (n + 1) -BinarySequence (k + 1) = (0* n) ^ <*1*> by A12, Th28
.= (('not' z) + (Bin1 n)) ^ <*TRUE*> by Th24
.= ((n -BinarySequence k) + (Bin1 n)) ^ <*((FALSE 'xor' FALSE) 'xor' (add_ovfl ((n -BinarySequence k),(Bin1 n))))*> by A14, Th23
.= ((n -BinarySequence k) ^ <*FALSE*>) + ((Bin1 n) ^ <*FALSE*>) by BINARITH:19
.= ((n -BinarySequence k) ^ <*FALSE*>) + (Bin1 (n + 1)) by BINARI_2:7
.= ((n + 1) -BinarySequence k) + (Bin1 (n + 1)) by A13, Th27 ; :: thesis: verum

end;

end;

end;

hence (n + 1) -BinarySequence (k + 1) = ((n + 1) -BinarySequence k) + (Bin1 (n + 1)) ; :: thesis: verum

end;

A15: S₁[1]

proof

0* 1 in BOOLEAN * by Th4;
then 0* 1 is FinSequence of BOOLEAN by FINSEQ_1:def 11;
then reconsider x = 0* 1 as Tuple of 1, BOOLEAN ;
let k be Nat; :: thesis: ( k + 1 < 2 to_power 1 implies 1 -BinarySequence (k + 1) = (1 -BinarySequence k) + (Bin1 1) )
A16: 0* 1 = <*FALSE*> by FINSEQ_2:59;
assume A17: k + 1 < 2 to_power 1 ; :: thesis: 1 -BinarySequence (k + 1) = (1 -BinarySequence k) + (Bin1 1)
then k + 1 < 1 + 1 by POWER:25;
then k < 1 by XREAL_1:6;
then A18: k = 0 by NAT_1:14;
then k + 1 = 2 - 1
.= (2 to_power 1) - 1 by POWER:25 ;
hence 1 -BinarySequence (k + 1) = 'not' x by A17, Lm4
.= (1 -BinarySequence k) + (Bin1 1) by A18, A16, Th10, Th14, Th17, Th25 ;
:: thesis: verum

end;

thus for n being non zero Nat holds S₁[n] from NAT_1:sch 10(A15, A1); :: thesis: verum