defpred S₁[ non empty 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 empty Nat st S₁[n] holds
S₁[n + 1]

proof

let n be non empty 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

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, Th33;
thus (n + 1) -BinarySequence (k + 1) = (n -BinarySequence (k + 1)) ^ <*FALSE *> by A5, Th28
.= ((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:45
.= ((n -BinarySequence k) ^ <*FALSE *>) + (Bin1 (n + 1)) by BINARI_2:9
.= ((n + 1) -BinarySequence k) + (Bin1 (n + 1)) by A6, Th28 ; :: 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:32;
then k + 1 < (2 to_power n) * 2 by POWER:30;
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:21;
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:235;
then A11: add_ovfl (n -BinarySequence (k -' (2 to_power n))),(Bin1 n) = FALSE by Th33;
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:45
.= ((n -BinarySequence (k -' (2 to_power n))) ^ <*TRUE *>) + (Bin1 (n + 1)) by BINARI_2:9
.= ((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 Th5;
then 0* n is FinSequence of BOOLEAN by FINSEQ_1:def 11;
then reconsider z = 0* n as Tuple of n, BOOLEAN ;
A14: k < 2 to_power n by A12, NAT_1:13;
k = (2 to_power n) - 1 by A12;
then A15: n -BinarySequence k = 'not' z by A14, Lm4;
thus (n + 1) -BinarySequence (k + 1) = (0* n) ^ <*1*> by A12, Th29
.= (('not' z) + (Bin1 n)) ^ <*TRUE *> by Th25
.= ((n -BinarySequence k) + (Bin1 n)) ^ <*((FALSE 'xor' FALSE ) 'xor' (add_ovfl (n -BinarySequence k),(Bin1 n)))*> by A15, Th24
.= ((n -BinarySequence k) ^ <*FALSE *>) + ((Bin1 n) ^ <*FALSE *>) by BINARITH:45
.= ((n -BinarySequence k) ^ <*FALSE *>) + (Bin1 (n + 1)) by BINARI_2:9
.= ((n + 1) -BinarySequence k) + (Bin1 (n + 1)) by A14, Th28 ; :: thesis: verum

end;

end;

end;

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

end;

A16: S₁[1]

proof

0* 1 in BOOLEAN * by Th5;
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) )
A18: 0* 1 = <*FALSE *> by FINSEQ_2:73;
assume A19: k + 1 < 2 to_power 1 ; :: thesis: 1 -BinarySequence (k + 1) = (1 -BinarySequence k) + (Bin1 1)
then k + 1 < 1 + 1 by POWER:30;
then k < 1 by XREAL_1:8;
then A20: k = 0 by NAT_1:14;
then k + 1 = 2 - 1
.= (2 to_power 1) - 1 by POWER:30 ;
hence 1 -BinarySequence (k + 1) = 'not' x by A19, Lm4
.= (1 -BinarySequence k) + (Bin1 1) by A20, A18, Th11, Th15, Th18, Th26 ;
:: thesis: verum

end;

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