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: S₁[1]

proof

let k be Nat; :: thesis: ( k + 1 < 2 to_power 1 implies 1 -BinarySequence (k + 1) = (1 -BinarySequence k) + (Bin1 1) )
assume A2: 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 A3: k = 0 by NAT_1:14;
then A4: k + 1 = 2 - 1
.= (2 to_power 1) - 1 by POWER:30 ;
0* 1 in BOOLEAN * by Th5;
then A5: 0* 1 is FinSequence of BOOLEAN by FINSEQ_1:def 11;
len (0* 1) = 1 by FINSEQ_1:def 18;
then reconsider x = 0* 1 as Tuple of 1,BOOLEAN by A5, FINSEQ_2:110;
A6: 0* 1 = <*FALSE *> by FINSEQ_2:73;
thus 1 -BinarySequence (k + 1) = 'not' x by A2, A4, Lm4
.= (1 -BinarySequence k) + (Bin1 1) by A3, A6, Th11, Th15, Th18, Th26 ; :: thesis: verum

end;

A7: 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 A8: 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 A9: k + 1 < 2 to_power (n + 1) ; :: thesis: (n + 1) -BinarySequence (k + 1) = ((n + 1) -BinarySequence k) + (Bin1 (n + 1))
then A10: 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 A11: k + 1 < 2 to_power n ; :: thesis: (n + 1) -BinarySequence (k + 1) = ((n + 1) -BinarySequence k) + (Bin1 (n + 1))

then A12: k < 2 to_power n by NAT_1:13;
A13: add_ovfl (n -BinarySequence k),(Bin1 n) = FALSE by A11, Th33;
thus (n + 1) -BinarySequence (k + 1) = (n -BinarySequence (k + 1)) ^ <*FALSE *> by A11, Th28
.= ((n -BinarySequence k) + (Bin1 n)) ^ <*((FALSE 'xor' FALSE ) 'xor' (add_ovfl (n -BinarySequence k),(Bin1 n)))*> by A8, A11, A13
.= ((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 A12, Th28 ; :: thesis: verum

end;

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

then A15: k >= 2 to_power n by NAT_1:13;
k + 1 < (2 to_power n) * (2 to_power 1) by A9, 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 A16: (k -' (2 to_power n)) + 1 < 2 to_power n by A15, XREAL_1:235;
then A17: 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 A9, A14, Lm3
.= (n -BinarySequence ((k -' (2 to_power n)) + 1)) ^ <*TRUE *> by A15, 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 A8, A16, A17
.= ((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 A10, A15, Lm3 ; :: thesis: verum

end;

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

then A19: k < 2 to_power n by NAT_1:13;
0* n in BOOLEAN * by Th5;
then A20: 0* n is FinSequence of BOOLEAN by FINSEQ_1:def 11;
len (0* n) = n by FINSEQ_1:def 18;
then reconsider z = 0* n as Tuple of n,BOOLEAN by A20, FINSEQ_2:110;
k = (2 to_power n) - 1 by A18;
then A21: n -BinarySequence k = 'not' z by A19, Lm4;
thus (n + 1) -BinarySequence (k + 1) = (0* n) ^ <*1*> by A18, 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 A21, 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 A19, Th28 ; :: thesis: verum

end;

end;

end;

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

end;

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