defpred S1[ non zero Nat] means for z1, z2 being Tuple of $1, BOOLEAN holds (Absval (z1 + z2)) + (IFEQ ((add_ovfl (z1,z2)),FALSE,0,(2 to_power $1))) = (Absval z1) + (Absval z2);
set f = FALSE ;
set t = TRUE ;
A1:
for n being non zero Nat st S1[n] holds
S1[n + 1]
proof
let n be non
zero Nat;
( S1[n] implies S1[n + 1] )
assume A2:
S1[
n]
;
S1[n + 1]
let z1,
z2 be
Tuple of
n + 1,
BOOLEAN ;
(Absval (z1 + z2)) + (IFEQ ((add_ovfl (z1,z2)),FALSE,0,(2 to_power (n + 1)))) = (Absval z1) + (Absval z2)
consider t1 being
Element of
n -tuples_on BOOLEAN,
d1 being
Element of
BOOLEAN such that A3:
z1 = t1 ^ <*d1*>
by FINSEQ_2:117;
consider t2 being
Element of
n -tuples_on BOOLEAN,
d2 being
Element of
BOOLEAN such that A4:
z2 = t2 ^ <*d2*>
by FINSEQ_2:117;
reconsider C1 =
IFEQ (
(add_ovfl (z1,z2)),
FALSE,
0,
(2 to_power (n + 1))),
C2 =
IFEQ (
((d1 'xor' d2) 'xor' (add_ovfl (t1,t2))),
FALSE,
0,
(2 to_power n)),
C3 =
IFEQ (
d1,
FALSE,
0,
(2 to_power n)),
C4 =
IFEQ (
d2,
FALSE,
0,
(2 to_power n)),
C5 =
IFEQ (
(add_ovfl (t1,t2)),
FALSE,
0,
(2 to_power n)) as
Real ;
A5:
add_ovfl (
z1,
z2) =
((d1 '&' ((t2 ^ <*d2*>) /. (n + 1))) 'or' (((t1 ^ <*d1*>) /. (n + 1)) '&' ((carry ((t1 ^ <*d1*>),(t2 ^ <*d2*>))) /. (n + 1)))) 'or' (((t2 ^ <*d2*>) /. (n + 1)) '&' ((carry ((t1 ^ <*d1*>),(t2 ^ <*d2*>))) /. (n + 1)))
by A3, A4, Th2
.=
((d1 '&' d2) 'or' (((t1 ^ <*d1*>) /. (n + 1)) '&' ((carry ((t1 ^ <*d1*>),(t2 ^ <*d2*>))) /. (n + 1)))) 'or' (((t2 ^ <*d2*>) /. (n + 1)) '&' ((carry ((t1 ^ <*d1*>),(t2 ^ <*d2*>))) /. (n + 1)))
by Th2
.=
((d1 '&' d2) 'or' (d1 '&' ((carry ((t1 ^ <*d1*>),(t2 ^ <*d2*>))) /. (n + 1)))) 'or' (((t2 ^ <*d2*>) /. (n + 1)) '&' ((carry ((t1 ^ <*d1*>),(t2 ^ <*d2*>))) /. (n + 1)))
by Th2
.=
((d1 '&' d2) 'or' (d1 '&' ((carry ((t1 ^ <*d1*>),(t2 ^ <*d2*>))) /. (n + 1)))) 'or' (d2 '&' ((carry ((t1 ^ <*d1*>),(t2 ^ <*d2*>))) /. (n + 1)))
by Th2
.=
((d1 '&' d2) 'or' (d1 '&' (add_ovfl (t1,t2)))) 'or' (d2 '&' ((carry ((t1 ^ <*d1*>),(t2 ^ <*d2*>))) /. (n + 1)))
by Th18
.=
((d1 '&' d2) 'or' (d1 '&' (add_ovfl (t1,t2)))) 'or' (d2 '&' (add_ovfl (t1,t2)))
by Th18
;
A6:
C2 + C1 = (C5 + C3) + C4
proof
now C2 + C1 = (C5 + C3) + C4per cases
( d1 = FALSE or d1 <> FALSE )
;
suppose A7:
d1 = FALSE
;
C2 + C1 = (C5 + C3) + C4then A8:
C3 = 0
by FUNCOP_1:def 8;
now C2 + C1 = (C5 + C3) + C4per cases
( d2 = FALSE or d2 <> FALSE )
;
suppose A10:
d2 <> FALSE
;
C2 + C1 = (C5 + C3) + C4then A11:
C4 = 2
to_power n
by FUNCOP_1:def 8;
now C2 + C1 = (C5 + C3) + C4per cases
( add_ovfl (t1,t2) = FALSE or add_ovfl (t1,t2) <> FALSE )
;
suppose A13:
add_ovfl (
t1,
t2)
<> FALSE
;
C2 + C1 = (C5 + C3) + C4(d1 'xor' d2) 'xor' (add_ovfl (t1,t2)) =
TRUE 'xor' (add_ovfl (t1,t2))
by A7, A10, XBOOLEAN:def 3
.=
FALSE
by A13, XBOOLEAN:def 3
;
then A14:
C2 = 0
by FUNCOP_1:def 8;
A15:
C5 = 2
to_power n
by A13, FUNCOP_1:def 8;
((d1 '&' d2) 'or' (d1 '&' (add_ovfl (t1,t2)))) 'or' (d2 '&' (add_ovfl (t1,t2))) =
(FALSE 'or' FALSE) 'or' (TRUE '&' (add_ovfl (t1,t2)))
by A7, A10, XBOOLEAN:def 3
.=
TRUE
by A13, XBOOLEAN:def 3
;
then
C1 = 2
to_power (n + 1)
by A5, FUNCOP_1:def 8;
hence C2 + C1 =
(2 to_power n) * (2 to_power 1)
by A14, POWER:27
.=
2
* (2 to_power n)
by POWER:25
.=
(C5 + C3) + C4
by A8, A11, A15
;
verum end; end; end; hence
C2 + C1 = (C5 + C3) + C4
;
verum end; end; end; hence
C2 + C1 = (C5 + C3) + C4
;
verum end; suppose A16:
d1 <> FALSE
;
C2 + C1 = (C5 + C3) + C4then A17:
C3 = 2
to_power n
by FUNCOP_1:def 8;
now C2 + C1 = (C5 + C3) + C4per cases
( d2 = FALSE or d2 <> FALSE )
;
suppose A18:
d2 = FALSE
;
C2 + C1 = (C5 + C3) + C4then A19:
C4 = 0
by FUNCOP_1:def 8;
now C2 + C1 = (C5 + C3) + C4per cases
( add_ovfl (t1,t2) = FALSE or add_ovfl (t1,t2) <> FALSE )
;
suppose A20:
add_ovfl (
t1,
t2)
<> FALSE
;
C2 + C1 = (C5 + C3) + C4(d1 'xor' d2) 'xor' (add_ovfl (t1,t2)) =
TRUE 'xor' (add_ovfl (t1,t2))
by A16, A18, XBOOLEAN:def 3
.=
FALSE
by A20, XBOOLEAN:def 3
;
then A21:
C2 = 0
by FUNCOP_1:def 8;
A22:
C5 = 2
to_power n
by A20, FUNCOP_1:def 8;
((d1 '&' d2) 'or' (d1 '&' (add_ovfl (t1,t2)))) 'or' (d2 '&' (add_ovfl (t1,t2))) =
(FALSE 'or' (TRUE '&' (add_ovfl (t1,t2)))) 'or' (d2 '&' (add_ovfl (t1,t2)))
by A16, A18, XBOOLEAN:def 3
.=
(FALSE 'or' (TRUE '&' TRUE)) 'or' (d2 '&' (add_ovfl (t1,t2)))
by A20, XBOOLEAN:def 3
.=
TRUE
;
then
C1 = 2
to_power (n + 1)
by A5, FUNCOP_1:def 8;
hence C2 + C1 =
(2 to_power n) * (2 to_power 1)
by A21, POWER:27
.=
2
* (2 to_power n)
by POWER:25
.=
(C5 + C3) + C4
by A17, A19, A22
;
verum end; end; end; hence
C2 + C1 = (C5 + C3) + C4
;
verum end; suppose A23:
d2 <> FALSE
;
C2 + C1 = (C5 + C3) + C4then A24:
C4 = 2
to_power n
by FUNCOP_1:def 8;
now C2 + C1 = (C5 + C3) + C4per cases
( add_ovfl (t1,t2) = FALSE or add_ovfl (t1,t2) <> FALSE )
;
suppose A25:
add_ovfl (
t1,
t2)
= FALSE
;
C2 + C1 = (C5 + C3) + C4(d1 'xor' d2) 'xor' (add_ovfl (t1,t2)) =
(TRUE 'xor' d2) 'xor' (add_ovfl (t1,t2))
by A16, XBOOLEAN:def 3
.=
FALSE
by A23, A25, XBOOLEAN:def 3
;
then A26:
C2 = 0
by FUNCOP_1:def 8;
A27:
C5 = 0
by A25, FUNCOP_1:def 8;
((d1 '&' d2) 'or' (d1 '&' (add_ovfl (t1,t2)))) 'or' (d2 '&' (add_ovfl (t1,t2))) =
((TRUE '&' d2) 'or' (d1 '&' (add_ovfl (t1,t2)))) 'or' (d2 '&' (add_ovfl (t1,t2)))
by A16, XBOOLEAN:def 3
.=
((TRUE '&' TRUE) 'or' (d1 '&' (add_ovfl (t1,t2)))) 'or' (d2 '&' (add_ovfl (t1,t2)))
by A23, XBOOLEAN:def 3
.=
TRUE
;
then
C1 = 2
to_power (n + 1)
by A5, FUNCOP_1:def 8;
hence C2 + C1 =
(2 to_power n) * (2 to_power 1)
by A26, POWER:27
.=
2
* (2 to_power n)
by POWER:25
.=
(C5 + C3) + C4
by A17, A24, A27
;
verum end; suppose A28:
add_ovfl (
t1,
t2)
<> FALSE
;
C2 + C1 = (C5 + C3) + C4(d1 'xor' d2) 'xor' (add_ovfl (t1,t2)) =
(TRUE 'xor' d2) 'xor' (add_ovfl (t1,t2))
by A16, XBOOLEAN:def 3
.=
FALSE 'xor' (add_ovfl (t1,t2))
by A23, XBOOLEAN:def 3
.=
TRUE
by A28, XBOOLEAN:def 3
;
then A29:
C2 = 2
to_power n
by FUNCOP_1:def 8;
((d1 '&' d2) 'or' (d1 '&' (add_ovfl (t1,t2)))) 'or' (d2 '&' (add_ovfl (t1,t2))) =
((TRUE '&' d2) 'or' (d1 '&' (add_ovfl (t1,t2)))) 'or' (d2 '&' (add_ovfl (t1,t2)))
by A16, XBOOLEAN:def 3
.=
((TRUE '&' TRUE) 'or' (d1 '&' (add_ovfl (t1,t2)))) 'or' (d2 '&' (add_ovfl (t1,t2)))
by A23, XBOOLEAN:def 3
.=
TRUE
;
then
C1 = 2
to_power (n + 1)
by A5, FUNCOP_1:def 8;
hence C2 + C1 =
(2 to_power n) + ((2 to_power n) * (2 to_power 1))
by A29, POWER:27
.=
(2 to_power n) + (2 * (2 to_power n))
by POWER:25
.=
((2 to_power n) + (2 to_power n)) + (2 to_power n)
.=
(C5 + C3) + C4
by A17, A24, A28, FUNCOP_1:def 8
;
verum end; end; end; hence
C2 + C1 = (C5 + C3) + C4
;
verum end; end; end; hence
C2 + C1 = (C5 + C3) + C4
;
verum end; end; end;
hence
C2 + C1 = (C5 + C3) + C4
;
verum
end;
thus (Absval (z1 + z2)) + (IFEQ ((add_ovfl (z1,z2)),FALSE,0,(2 to_power (n + 1)))) =
(Absval ((t1 + t2) ^ <*((d1 'xor' d2) 'xor' (add_ovfl (t1,t2)))*>)) + (IFEQ ((add_ovfl (z1,z2)),FALSE,0,(2 to_power (n + 1))))
by A3, A4, Th19
.=
((Absval (t1 + t2)) + C2) + C1
by Th20
.=
(((Absval (t1 + t2)) + C5) + C3) + C4
by A6
.=
(((Absval t1) + (Absval t2)) + C3) + C4
by A2
.=
((Absval t1) + C3) + ((Absval t2) + C4)
.=
((Absval t1) + (IFEQ (d1,FALSE,0,(2 to_power n)))) + (Absval (t2 ^ <*d2*>))
by Th20
.=
(Absval z1) + (Absval z2)
by A3, A4, Th20
;
verum
end;
A30:
S1[1]
proof
reconsider T =
<*TRUE*>,
F =
<*FALSE*> as
Tuple of 1,
BOOLEAN ;
let z1,
z2 be
Tuple of 1,
BOOLEAN ;
(Absval (z1 + z2)) + (IFEQ ((add_ovfl (z1,z2)),FALSE,0,(2 to_power 1))) = (Absval z1) + (Absval z2)
A31:
(carry (z1,z2)) /. 1
= FALSE
by Def2;
A32:
Absval T = 1
by Th16;
A33:
Absval F = 0
by Th15;
per cases
( ( z1 = <*FALSE*> & z2 = <*FALSE*> ) or ( z1 = <*TRUE*> & z2 = <*FALSE*> ) or ( z1 = <*FALSE*> & z2 = <*TRUE*> ) or ( z1 = <*TRUE*> & z2 = <*TRUE*> ) )
by Th14;
suppose A34:
(
z1 = <*FALSE*> &
z2 = <*FALSE*> )
;
(Absval (z1 + z2)) + (IFEQ ((add_ovfl (z1,z2)),FALSE,0,(2 to_power 1))) = (Absval z1) + (Absval z2)
add_ovfl (
z1,
z2)
= FALSE
by A31, A34, FINSEQ_4:16;
then
IFEQ (
(add_ovfl (z1,z2)),
FALSE,
0,
(2 to_power 1))
= 0
by FUNCOP_1:def 8;
hence
(Absval (z1 + z2)) + (IFEQ ((add_ovfl (z1,z2)),FALSE,0,(2 to_power 1))) = (Absval z1) + (Absval z2)
by A33, A34, A35, Def5;
verum end; suppose A38:
(
z1 = <*TRUE*> &
z2 = <*FALSE*> )
;
(Absval (z1 + z2)) + (IFEQ ((add_ovfl (z1,z2)),FALSE,0,(2 to_power 1))) = (Absval z1) + (Absval z2)
add_ovfl (
z1,
z2)
= FALSE
by A31, A38, FINSEQ_4:16;
then
IFEQ (
(add_ovfl (z1,z2)),
FALSE,
0,
(2 to_power 1))
= 0
by FUNCOP_1:def 8;
hence
(Absval (z1 + z2)) + (IFEQ ((add_ovfl (z1,z2)),FALSE,0,(2 to_power 1))) = (Absval z1) + (Absval z2)
by A33, A38, A39, Def5;
verum end; suppose A42:
(
z1 = <*FALSE*> &
z2 = <*TRUE*> )
;
(Absval (z1 + z2)) + (IFEQ ((add_ovfl (z1,z2)),FALSE,0,(2 to_power 1))) = (Absval z1) + (Absval z2)
add_ovfl (
z1,
z2)
= FALSE
by A31, A42, FINSEQ_4:16;
then
IFEQ (
(add_ovfl (z1,z2)),
FALSE,
0,
(2 to_power 1))
= 0
by FUNCOP_1:def 8;
hence
(Absval (z1 + z2)) + (IFEQ ((add_ovfl (z1,z2)),FALSE,0,(2 to_power 1))) = (Absval z1) + (Absval z2)
by A33, A42, A43, Def5;
verum end; suppose A45:
(
z1 = <*TRUE*> &
z2 = <*TRUE*> )
;
(Absval (z1 + z2)) + (IFEQ ((add_ovfl (z1,z2)),FALSE,0,(2 to_power 1))) = (Absval z1) + (Absval z2)then A47:
z1 + z2 = <*FALSE*>
by Def5;
add_ovfl (
z1,
z2)
= TRUE
by A31, A45, FINSEQ_4:16;
then IFEQ (
(add_ovfl (z1,z2)),
FALSE,
0,
(2 to_power 1)) =
2
to_power 1
by FUNCOP_1:def 8
.=
2
by POWER:25
;
hence
(Absval (z1 + z2)) + (IFEQ ((add_ovfl (z1,z2)),FALSE,0,(2 to_power 1))) = (Absval z1) + (Absval z2)
by A32, A33, A45, A47;
verum end; end;
end;
thus
for n being non zero Nat holds S1[n]
from NAT_1:sch 10(A30, A1); verum