let n be Nat; for s1, s2 being State of SCMPDS
for P1, P2 being Instruction-Sequence of SCMPDS st GCD-Algorithm c= P1 & GCD-Algorithm c= P2 & IC s1 = 5 & n = s1 . SBP & s1 . GBP = 0 & s1 . (DataLoc ((s1 . SBP),3)) > 0 & IC s2 = IC s1 & s2 . SBP = s1 . SBP & s2 . GBP = 0 & s2 . (DataLoc ((s1 . SBP),2)) = s1 . (DataLoc ((s1 . SBP),2)) & s2 . (DataLoc ((s1 . SBP),3)) = s1 . (DataLoc ((s1 . SBP),3)) holds
for k being Nat
for a being Int_position st k <= 7 & s1 . a = s2 . a holds
( IC (Comput (P1,s1,k)) = IC (Comput (P2,s2,k)) & (Comput (P1,s1,k)) . a = (Comput (P2,s2,k)) . a )
let s1, s2 be State of SCMPDS; for P1, P2 being Instruction-Sequence of SCMPDS st GCD-Algorithm c= P1 & GCD-Algorithm c= P2 & IC s1 = 5 & n = s1 . SBP & s1 . GBP = 0 & s1 . (DataLoc ((s1 . SBP),3)) > 0 & IC s2 = IC s1 & s2 . SBP = s1 . SBP & s2 . GBP = 0 & s2 . (DataLoc ((s1 . SBP),2)) = s1 . (DataLoc ((s1 . SBP),2)) & s2 . (DataLoc ((s1 . SBP),3)) = s1 . (DataLoc ((s1 . SBP),3)) holds
for k being Nat
for a being Int_position st k <= 7 & s1 . a = s2 . a holds
( IC (Comput (P1,s1,k)) = IC (Comput (P2,s2,k)) & (Comput (P1,s1,k)) . a = (Comput (P2,s2,k)) . a )
let P1, P2 be Instruction-Sequence of SCMPDS; ( GCD-Algorithm c= P1 & GCD-Algorithm c= P2 & IC s1 = 5 & n = s1 . SBP & s1 . GBP = 0 & s1 . (DataLoc ((s1 . SBP),3)) > 0 & IC s2 = IC s1 & s2 . SBP = s1 . SBP & s2 . GBP = 0 & s2 . (DataLoc ((s1 . SBP),2)) = s1 . (DataLoc ((s1 . SBP),2)) & s2 . (DataLoc ((s1 . SBP),3)) = s1 . (DataLoc ((s1 . SBP),3)) implies for k being Nat
for a being Int_position st k <= 7 & s1 . a = s2 . a holds
( IC (Comput (P1,s1,k)) = IC (Comput (P2,s2,k)) & (Comput (P1,s1,k)) . a = (Comput (P2,s2,k)) . a ) )
set GA = GCD-Algorithm ;
assume that
A1:
GCD-Algorithm c= P1
and
A2:
GCD-Algorithm c= P2
; ( not IC s1 = 5 or not n = s1 . SBP or not s1 . GBP = 0 or not s1 . (DataLoc ((s1 . SBP),3)) > 0 or not IC s2 = IC s1 or not s2 . SBP = s1 . SBP or not s2 . GBP = 0 or not s2 . (DataLoc ((s1 . SBP),2)) = s1 . (DataLoc ((s1 . SBP),2)) or not s2 . (DataLoc ((s1 . SBP),3)) = s1 . (DataLoc ((s1 . SBP),3)) or for k being Nat
for a being Int_position st k <= 7 & s1 . a = s2 . a holds
( IC (Comput (P1,s1,k)) = IC (Comput (P2,s2,k)) & (Comput (P1,s1,k)) . a = (Comput (P2,s2,k)) . a ) )
assume A3:
IC s1 = 5
; ( not n = s1 . SBP or not s1 . GBP = 0 or not s1 . (DataLoc ((s1 . SBP),3)) > 0 or not IC s2 = IC s1 or not s2 . SBP = s1 . SBP or not s2 . GBP = 0 or not s2 . (DataLoc ((s1 . SBP),2)) = s1 . (DataLoc ((s1 . SBP),2)) or not s2 . (DataLoc ((s1 . SBP),3)) = s1 . (DataLoc ((s1 . SBP),3)) or for k being Nat
for a being Int_position st k <= 7 & s1 . a = s2 . a holds
( IC (Comput (P1,s1,k)) = IC (Comput (P2,s2,k)) & (Comput (P1,s1,k)) . a = (Comput (P2,s2,k)) . a ) )
assume A4:
n = s1 . SBP
; ( not s1 . GBP = 0 or not s1 . (DataLoc ((s1 . SBP),3)) > 0 or not IC s2 = IC s1 or not s2 . SBP = s1 . SBP or not s2 . GBP = 0 or not s2 . (DataLoc ((s1 . SBP),2)) = s1 . (DataLoc ((s1 . SBP),2)) or not s2 . (DataLoc ((s1 . SBP),3)) = s1 . (DataLoc ((s1 . SBP),3)) or for k being Nat
for a being Int_position st k <= 7 & s1 . a = s2 . a holds
( IC (Comput (P1,s1,k)) = IC (Comput (P2,s2,k)) & (Comput (P1,s1,k)) . a = (Comput (P2,s2,k)) . a ) )
assume A5:
s1 . GBP = 0
; ( not s1 . (DataLoc ((s1 . SBP),3)) > 0 or not IC s2 = IC s1 or not s2 . SBP = s1 . SBP or not s2 . GBP = 0 or not s2 . (DataLoc ((s1 . SBP),2)) = s1 . (DataLoc ((s1 . SBP),2)) or not s2 . (DataLoc ((s1 . SBP),3)) = s1 . (DataLoc ((s1 . SBP),3)) or for k being Nat
for a being Int_position st k <= 7 & s1 . a = s2 . a holds
( IC (Comput (P1,s1,k)) = IC (Comput (P2,s2,k)) & (Comput (P1,s1,k)) . a = (Comput (P2,s2,k)) . a ) )
assume A6:
s1 . (DataLoc ((s1 . SBP),3)) > 0
; ( not IC s2 = IC s1 or not s2 . SBP = s1 . SBP or not s2 . GBP = 0 or not s2 . (DataLoc ((s1 . SBP),2)) = s1 . (DataLoc ((s1 . SBP),2)) or not s2 . (DataLoc ((s1 . SBP),3)) = s1 . (DataLoc ((s1 . SBP),3)) or for k being Nat
for a being Int_position st k <= 7 & s1 . a = s2 . a holds
( IC (Comput (P1,s1,k)) = IC (Comput (P2,s2,k)) & (Comput (P1,s1,k)) . a = (Comput (P2,s2,k)) . a ) )
assume that
A7:
IC s2 = IC s1
and
A8:
s2 . SBP = s1 . SBP
and
A9:
s2 . GBP = 0
; ( not s2 . (DataLoc ((s1 . SBP),2)) = s1 . (DataLoc ((s1 . SBP),2)) or not s2 . (DataLoc ((s1 . SBP),3)) = s1 . (DataLoc ((s1 . SBP),3)) or for k being Nat
for a being Int_position st k <= 7 & s1 . a = s2 . a holds
( IC (Comput (P1,s1,k)) = IC (Comput (P2,s2,k)) & (Comput (P1,s1,k)) . a = (Comput (P2,s2,k)) . a ) )
assume that
A10:
s2 . (DataLoc ((s1 . SBP),2)) = s1 . (DataLoc ((s1 . SBP),2))
and
A11:
s2 . (DataLoc ((s1 . SBP),3)) = s1 . (DataLoc ((s1 . SBP),3))
; for k being Nat
for a being Int_position st k <= 7 & s1 . a = s2 . a holds
( IC (Comput (P1,s1,k)) = IC (Comput (P2,s2,k)) & (Comput (P1,s1,k)) . a = (Comput (P2,s2,k)) . a )
A12:
P1 /. (IC s1) = P1 . (IC s1)
by PBOOLE:143;
A13: Comput (P1,s1,(1 + 0)) =
Following (P1,(Comput (P1,s1,0)))
by EXTPRO_1:3
.=
Following (P1,s1)
by EXTPRO_1:2
.=
Exec (((SBP,3) <=0_goto 9),s1)
by A12, A3, Lm1, A1
;
A14:
P2 /. (IC s2) = P2 . (IC s2)
by PBOOLE:143;
A15: Comput (P2,s2,(1 + 0)) =
Following (P2,(Comput (P2,s2,0)))
by EXTPRO_1:3
.=
Following (P2,s2)
by EXTPRO_1:2
.=
Exec (((SBP,3) <=0_goto 9),s2)
by A3, A7, Lm1, A14, A2
;
A16:
P1 /. (IC (Comput (P1,s1,1))) = P1 . (IC (Comput (P1,s1,1)))
by PBOOLE:143;
A17: IC (Comput (P1,s1,1)) =
(IC s1) + 1
by A6, A13, SCMPDS_2:56
.=
5 + 1
by A3
;
then A18: CurInstr (P1,(Comput (P1,s1,1))) =
P1 . 6
by A16
.=
(SBP,6) := (SBP,3)
by Lm1, A1
;
A19: Comput (P1,s1,(1 + 1)) =
Following (P1,(Comput (P1,s1,1)))
by EXTPRO_1:3
.=
Exec (((SBP,6) := (SBP,3)),(Comput (P1,s1,1)))
by A18
;
A20:
(Comput (P1,s1,1)) . SBP = n
by A4, A13, SCMPDS_2:56;
A21:
(Comput (P1,s1,1)) . GBP = 0
by A5, A13, SCMPDS_2:56;
A22:
P2 /. (IC (Comput (P2,s2,1))) = P2 . (IC (Comput (P2,s2,1)))
by PBOOLE:143;
A23: IC (Comput (P2,s2,1)) =
(IC s2) + 1
by A6, A8, A11, A15, SCMPDS_2:56
.=
5 + 1
by A3, A7
;
then A24: CurInstr (P2,(Comput (P2,s2,1))) =
P2 . 6
by A22
.=
(SBP,6) := (SBP,3)
by Lm1, A2
;
A25: Comput (P2,s2,(1 + 1)) =
Following (P2,(Comput (P2,s2,1)))
by EXTPRO_1:3
.=
Exec (((SBP,6) := (SBP,3)),(Comput (P2,s2,1)))
by A24
;
A26:
P1 /. (IC (Comput (P1,s1,2))) = P1 . (IC (Comput (P1,s1,2)))
by PBOOLE:143;
A27: IC (Comput (P1,s1,2)) =
(IC (Comput (P1,s1,1))) + 1
by A19, SCMPDS_2:47
.=
6 + 1
by A17
;
then A28: CurInstr (P1,(Comput (P1,s1,2))) =
P1 . 7
by A26
.=
Divide (SBP,2,SBP,3)
by Lm1, A1
;
A29: Comput (P1,s1,(2 + 1)) =
Following (P1,(Comput (P1,s1,2)))
by EXTPRO_1:3
.=
Exec ((Divide (SBP,2,SBP,3)),(Comput (P1,s1,2)))
by A28
;
A30:
DataLoc (((Comput (P1,s1,1)) . SBP),6) = intpos (n + 6)
by A20, Th1;
then A31:
(Comput (P1,s1,2)) . SBP = n
by A19, A20, Lm3, SCMPDS_2:47;
A32:
(Comput (P1,s1,2)) . GBP = 0
by A19, A21, A30, Lm2, SCMPDS_2:47;
A33:
P2 /. (IC (Comput (P2,s2,2))) = P2 . (IC (Comput (P2,s2,2)))
by PBOOLE:143;
A34: IC (Comput (P2,s2,2)) =
(IC (Comput (P2,s2,1))) + 1
by A25, SCMPDS_2:47
.=
6 + 1
by A23
;
then A35: CurInstr (P2,(Comput (P2,s2,2))) =
P2 . 7
by A33
.=
Divide (SBP,2,SBP,3)
by Lm1, A2
;
A36: Comput (P2,s2,(2 + 1)) =
Following (P2,(Comput (P2,s2,2)))
by EXTPRO_1:3
.=
Exec ((Divide (SBP,2,SBP,3)),(Comput (P2,s2,2)))
by A35
;
A37:
P1 /. (IC (Comput (P1,s1,3))) = P1 . (IC (Comput (P1,s1,3)))
by PBOOLE:143;
A38: IC (Comput (P1,s1,3)) =
(IC (Comput (P1,s1,2))) + 1
by A29, SCMPDS_2:52
.=
7 + 1
by A27
;
then A39: CurInstr (P1,(Comput (P1,s1,3))) =
P1 . 8
by A37
.=
(SBP,7) := (SBP,3)
by Lm1, A1
;
A40: Comput (P1,s1,(3 + 1)) =
Following (P1,(Comput (P1,s1,3)))
by EXTPRO_1:3
.=
Exec (((SBP,7) := (SBP,3)),(Comput (P1,s1,3)))
by A39
;
A41:
DataLoc (((Comput (P1,s1,2)) . SBP),2) = intpos (n + 2)
by A31, Th1;
then A42:
SBP <> DataLoc (((Comput (P1,s1,2)) . SBP),2)
by Lm3;
A43:
DataLoc (((Comput (P1,s1,2)) . SBP),3) = intpos (n + 3)
by A31, Th1;
then
SBP <> DataLoc (((Comput (P1,s1,2)) . SBP),3)
by Lm3;
then A44:
(Comput (P1,s1,3)) . SBP = n
by A29, A31, A42, SCMPDS_2:52;
A45:
GBP <> DataLoc (((Comput (P1,s1,2)) . SBP),2)
by A41, Lm2;
GBP <> DataLoc (((Comput (P1,s1,2)) . SBP),3)
by A43, Lm2;
then A46:
(Comput (P1,s1,3)) . GBP = 0
by A29, A32, A45, SCMPDS_2:52;
A47:
P2 /. (IC (Comput (P2,s2,3))) = P2 . (IC (Comput (P2,s2,3)))
by PBOOLE:143;
A48: IC (Comput (P2,s2,3)) =
(IC (Comput (P2,s2,2))) + 1
by A36, SCMPDS_2:52
.=
7 + 1
by A34
;
then A49: CurInstr (P2,(Comput (P2,s2,3))) =
P2 . 8
by A47
.=
(SBP,7) := (SBP,3)
by Lm1, A2
;
A50: Comput (P2,s2,(3 + 1)) =
Following (P2,(Comput (P2,s2,3)))
by EXTPRO_1:3
.=
Exec (((SBP,7) := (SBP,3)),(Comput (P2,s2,3)))
by A49
;
A51:
P1 /. (IC (Comput (P1,s1,4))) = P1 . (IC (Comput (P1,s1,4)))
by PBOOLE:143;
A52: IC (Comput (P1,s1,4)) =
(IC (Comput (P1,s1,3))) + 1
by A40, SCMPDS_2:47
.=
8 + 1
by A38
;
then A53: CurInstr (P1,(Comput (P1,s1,4))) =
P1 . 9
by A51
.=
(SBP,(4 + RetSP)) := (GBP,1)
by Lm1, A1
;
A54: Comput (P1,s1,(4 + 1)) =
Following (P1,(Comput (P1,s1,4)))
by EXTPRO_1:3
.=
Exec (((SBP,(4 + RetSP)) := (GBP,1)),(Comput (P1,s1,4)))
by A53
;
A55:
DataLoc (((Comput (P1,s1,3)) . SBP),7) = intpos (n + 7)
by A44, Th1;
then A56:
(Comput (P1,s1,4)) . SBP = n
by A40, A44, Lm3, SCMPDS_2:47;
A57:
(Comput (P1,s1,4)) . GBP = 0
by A40, A46, A55, Lm2, SCMPDS_2:47;
A58:
P2 /. (IC (Comput (P2,s2,4))) = P2 . (IC (Comput (P2,s2,4)))
by PBOOLE:143;
A59: IC (Comput (P2,s2,4)) =
(IC (Comput (P2,s2,3))) + 1
by A50, SCMPDS_2:47
.=
8 + 1
by A48
;
then A60: CurInstr (P2,(Comput (P2,s2,4))) =
P2 . 9
by A58
.=
(SBP,(4 + RetSP)) := (GBP,1)
by Lm1, A2
;
A61: Comput (P2,s2,(4 + 1)) =
Following (P2,(Comput (P2,s2,4)))
by EXTPRO_1:3
.=
Exec (((SBP,(4 + RetSP)) := (GBP,1)),(Comput (P2,s2,4)))
by A60
;
A62:
P1 /. (IC (Comput (P1,s1,5))) = P1 . (IC (Comput (P1,s1,5)))
by PBOOLE:143;
A63: IC (Comput (P1,s1,5)) =
(IC (Comput (P1,s1,4))) + 1
by A54, SCMPDS_2:47
.=
9 + 1
by A52
;
then A64: CurInstr (P1,(Comput (P1,s1,5))) =
P1 . 10
by A62
.=
AddTo (GBP,1,4)
by Lm1, A1
;
A65: Comput (P1,s1,(5 + 1)) =
Following (P1,(Comput (P1,s1,5)))
by EXTPRO_1:3
.=
Exec ((AddTo (GBP,1,4)),(Comput (P1,s1,5)))
by A64
;
DataLoc (((Comput (P1,s1,4)) . SBP),(4 + RetSP)) = intpos (n + (4 + 0))
by A56, Th1, SCMPDS_I:def 13;
then A66:
(Comput (P1,s1,5)) . GBP = 0
by A54, A57, Lm2, SCMPDS_2:47;
A67:
P2 /. (IC (Comput (P2,s2,5))) = P2 . (IC (Comput (P2,s2,5)))
by PBOOLE:143;
A68: IC (Comput (P2,s2,5)) =
(IC (Comput (P2,s2,4))) + 1
by A61, SCMPDS_2:47
.=
9 + 1
by A59
;
then A69: CurInstr (P2,(Comput (P2,s2,5))) =
P2 . 10
by A67
.=
AddTo (GBP,1,4)
by Lm1, A2
;
A70: Comput (P2,s2,(5 + 1)) =
Following (P2,(Comput (P2,s2,5)))
by EXTPRO_1:3
.=
Exec ((AddTo (GBP,1,4)),(Comput (P2,s2,5)))
by A69
;
A71:
P1 /. (IC (Comput (P1,s1,6))) = P1 . (IC (Comput (P1,s1,6)))
by PBOOLE:143;
A72: IC (Comput (P1,s1,6)) =
(IC (Comput (P1,s1,5))) + 1
by A65, SCMPDS_2:48
.=
10 + 1
by A63
;
then A73: CurInstr (P1,(Comput (P1,s1,6))) =
P1 . 11
by A71
.=
saveIC (SBP,RetIC)
by Lm1, A1
;
A74: Comput (P1,s1,(6 + 1)) =
Following (P1,(Comput (P1,s1,6)))
by EXTPRO_1:3
.=
Exec ((saveIC (SBP,RetIC)),(Comput (P1,s1,6)))
by A73
;
A75:
P2 /. (IC (Comput (P2,s2,6))) = P2 . (IC (Comput (P2,s2,6)))
by PBOOLE:143;
A76: IC (Comput (P2,s2,6)) =
(IC (Comput (P2,s2,5))) + 1
by A70, SCMPDS_2:48
.=
10 + 1
by A68
;
then A77: CurInstr (P2,(Comput (P2,s2,6))) =
P2 . 11
by A75
.=
saveIC (SBP,RetIC)
by Lm1, A2
;
A78: Comput (P2,s2,(6 + 1)) =
Following (P2,(Comput (P2,s2,6)))
by EXTPRO_1:3
.=
Exec ((saveIC (SBP,RetIC)),(Comput (P2,s2,6)))
by A77
;
A79:
now for b being Int_position st s1 . b = s2 . b holds
(Comput (P1,s1,1)) . b = (Comput (P2,s2,1)) . blet b be
Int_position;
( s1 . b = s2 . b implies (Comput (P1,s1,1)) . b = (Comput (P2,s2,1)) . b )assume
s1 . b = s2 . b
;
(Comput (P1,s1,1)) . b = (Comput (P2,s2,1)) . bhence (Comput (P1,s1,1)) . b =
s2 . b
by A13, SCMPDS_2:56
.=
(Comput (P2,s2,1)) . b
by A15, SCMPDS_2:56
;
verum end;
A80:
for b being Int_position st s1 . b = s2 . b holds
(Comput (P1,s1,2)) . b = (Comput (P2,s2,2)) . b
proof
let b be
Int_position;
( s1 . b = s2 . b implies (Comput (P1,s1,2)) . b = (Comput (P2,s2,2)) . b )
assume A81:
s1 . b = s2 . b
;
(Comput (P1,s1,2)) . b = (Comput (P2,s2,2)) . b
per cases
( b = DataLoc (((Comput (P1,s1,1)) . SBP),6) or b <> DataLoc (((Comput (P1,s1,1)) . SBP),6) )
;
suppose A82:
b = DataLoc (
((Comput (P1,s1,1)) . SBP),6)
;
(Comput (P1,s1,2)) . b = (Comput (P2,s2,2)) . bthen A83:
b = DataLoc (
((Comput (P2,s2,1)) . SBP),6)
by A8, A79;
thus (Comput (P1,s1,2)) . b =
(Comput (P1,s1,1)) . (DataLoc ((s1 . SBP),3))
by A4, A19, A20, A82, SCMPDS_2:47
.=
(Comput (P2,s2,1)) . (DataLoc (((Comput (P1,s1,1)) . SBP),3))
by A4, A11, A20, A79
.=
(Comput (P2,s2,1)) . (DataLoc (((Comput (P2,s2,1)) . SBP),3))
by A8, A79
.=
(Comput (P2,s2,2)) . b
by A25, A83, SCMPDS_2:47
;
verum end; suppose A84:
b <> DataLoc (
((Comput (P1,s1,1)) . SBP),6)
;
(Comput (P1,s1,2)) . b = (Comput (P2,s2,2)) . bthen A85:
b <> DataLoc (
((Comput (P2,s2,1)) . SBP),6)
by A8, A79;
thus (Comput (P1,s1,2)) . b =
(Comput (P1,s1,1)) . b
by A19, A84, SCMPDS_2:47
.=
(Comput (P2,s2,1)) . b
by A79, A81
.=
(Comput (P2,s2,2)) . b
by A25, A85, SCMPDS_2:47
;
verum end; end;
end;
A86:
now for b being Int_position st s1 . b = s2 . b holds
(Comput (P1,s1,3)) . b = (Comput (P2,s2,3)) . blet b be
Int_position;
( s1 . b = s2 . b implies (Comput (P1,s1,3)) . b1 = (Comput (P2,s2,3)) . b1 )assume A87:
s1 . b = s2 . b
;
(Comput (P1,s1,3)) . b1 = (Comput (P2,s2,3)) . b1set x1 =
DataLoc (
((Comput (P1,s1,2)) . SBP),2);
set x2 =
DataLoc (
((Comput (P1,s1,2)) . SBP),3);
set y1 =
DataLoc (
((Comput (P2,s2,2)) . SBP),2);
set y2 =
DataLoc (
((Comput (P2,s2,2)) . SBP),3);
A88:
DataLoc (
((Comput (P1,s1,2)) . SBP),2)
= DataLoc (
((Comput (P2,s2,2)) . SBP),2)
by A8, A80;
A89:
DataLoc (
((Comput (P1,s1,2)) . SBP),3)
= DataLoc (
((Comput (P2,s2,2)) . SBP),3)
by A8, A80;
per cases
( ( b <> DataLoc (((Comput (P1,s1,2)) . SBP),2) & b <> DataLoc (((Comput (P1,s1,2)) . SBP),3) ) or b = DataLoc (((Comput (P1,s1,2)) . SBP),2) or b = DataLoc (((Comput (P1,s1,2)) . SBP),3) )
;
suppose A90:
(
b <> DataLoc (
((Comput (P1,s1,2)) . SBP),2) &
b <> DataLoc (
((Comput (P1,s1,2)) . SBP),3) )
;
(Comput (P1,s1,3)) . b1 = (Comput (P2,s2,3)) . b1hence (Comput (P1,s1,3)) . b =
(Comput (P1,s1,2)) . b
by A29, SCMPDS_2:52
.=
(Comput (P2,s2,2)) . b
by A80, A87
.=
(Comput (P2,s2,3)) . b
by A36, A88, A89, A90, SCMPDS_2:52
;
verum end; suppose A91:
b = DataLoc (
((Comput (P1,s1,2)) . SBP),2)
;
(Comput (P1,s1,3)) . b1 = (Comput (P2,s2,3)) . b1A92:
n + 2
<> n + 3
;
then A93:
DataLoc (
((Comput (P1,s1,2)) . SBP),2)
<> DataLoc (
((Comput (P1,s1,2)) . SBP),3)
by A41, A43, AMI_3:10;
A94:
DataLoc (
((Comput (P2,s2,2)) . SBP),2)
<> DataLoc (
((Comput (P2,s2,2)) . SBP),3)
by A41, A43, A88, A89, A92, AMI_3:10;
thus (Comput (P1,s1,3)) . b =
((Comput (P1,s1,2)) . (DataLoc (((Comput (P1,s1,2)) . SBP),2))) div ((Comput (P1,s1,2)) . (DataLoc (((Comput (P1,s1,2)) . SBP),3)))
by A29, A91, A93, SCMPDS_2:52
.=
((Comput (P2,s2,2)) . (DataLoc (((Comput (P1,s1,2)) . SBP),2))) div ((Comput (P1,s1,2)) . (DataLoc (((Comput (P1,s1,2)) . SBP),3)))
by A4, A10, A31, A80
.=
((Comput (P2,s2,2)) . (DataLoc (((Comput (P1,s1,2)) . SBP),2))) div ((Comput (P2,s2,2)) . (DataLoc (((Comput (P1,s1,2)) . SBP),3)))
by A4, A11, A31, A80
.=
(Comput (P2,s2,3)) . b
by A36, A88, A89, A91, A94, SCMPDS_2:52
;
verum end; suppose A95:
b = DataLoc (
((Comput (P1,s1,2)) . SBP),3)
;
(Comput (P1,s1,3)) . b1 = (Comput (P2,s2,3)) . b1hence (Comput (P1,s1,3)) . b =
((Comput (P1,s1,2)) . (DataLoc (((Comput (P1,s1,2)) . SBP),2))) mod ((Comput (P1,s1,2)) . (DataLoc (((Comput (P1,s1,2)) . SBP),3)))
by A29, SCMPDS_2:52
.=
((Comput (P2,s2,2)) . (DataLoc (((Comput (P1,s1,2)) . SBP),2))) mod ((Comput (P1,s1,2)) . (DataLoc (((Comput (P1,s1,2)) . SBP),3)))
by A4, A10, A31, A80
.=
((Comput (P2,s2,2)) . (DataLoc (((Comput (P1,s1,2)) . SBP),2))) mod ((Comput (P2,s2,2)) . (DataLoc (((Comput (P1,s1,2)) . SBP),3)))
by A4, A11, A31, A80
.=
(Comput (P2,s2,3)) . b
by A36, A88, A89, A95, SCMPDS_2:52
;
verum end; end; end;
A96:
now for b being Int_position st s1 . b = s2 . b holds
(Comput (P1,s1,4)) . b = (Comput (P2,s2,4)) . blet b be
Int_position;
( s1 . b = s2 . b implies (Comput (P1,s1,4)) . b1 = (Comput (P2,s2,4)) . b1 )assume A97:
s1 . b = s2 . b
;
(Comput (P1,s1,4)) . b1 = (Comput (P2,s2,4)) . b1per cases
( b = DataLoc (((Comput (P1,s1,3)) . SBP),7) or b <> DataLoc (((Comput (P1,s1,3)) . SBP),7) )
;
suppose A98:
b = DataLoc (
((Comput (P1,s1,3)) . SBP),7)
;
(Comput (P1,s1,4)) . b1 = (Comput (P2,s2,4)) . b1then A99:
b = DataLoc (
((Comput (P2,s2,3)) . SBP),7)
by A8, A86;
thus (Comput (P1,s1,4)) . b =
(Comput (P1,s1,3)) . (DataLoc (((Comput (P1,s1,3)) . SBP),3))
by A40, A98, SCMPDS_2:47
.=
(Comput (P2,s2,3)) . (DataLoc (((Comput (P1,s1,3)) . SBP),3))
by A4, A11, A44, A86
.=
(Comput (P2,s2,3)) . (DataLoc (((Comput (P2,s2,3)) . SBP),3))
by A8, A86
.=
(Comput (P2,s2,4)) . b
by A50, A99, SCMPDS_2:47
;
verum end; suppose A100:
b <> DataLoc (
((Comput (P1,s1,3)) . SBP),7)
;
(Comput (P1,s1,4)) . b1 = (Comput (P2,s2,4)) . b1then A101:
b <> DataLoc (
((Comput (P2,s2,3)) . SBP),7)
by A8, A86;
thus (Comput (P1,s1,4)) . b =
(Comput (P1,s1,3)) . b
by A40, A100, SCMPDS_2:47
.=
(Comput (P2,s2,3)) . b
by A86, A97
.=
(Comput (P2,s2,4)) . b
by A50, A101, SCMPDS_2:47
;
verum end; end; end;
A102:
now for b being Int_position st s1 . b = s2 . b holds
(Comput (P1,s1,5)) . b = (Comput (P2,s2,5)) . blet b be
Int_position;
( s1 . b = s2 . b implies (Comput (P1,s1,5)) . b1 = (Comput (P2,s2,5)) . b1 )assume A103:
s1 . b = s2 . b
;
(Comput (P1,s1,5)) . b1 = (Comput (P2,s2,5)) . b1A104:
s1 . (DataLoc (((Comput (P1,s1,4)) . GBP),1)) =
s2 . (intpos (0 + 1))
by A8, A57, Th1
.=
s2 . (DataLoc (((Comput (P1,s1,4)) . GBP),1))
by A57, Th1
;
per cases
( b = DataLoc (((Comput (P1,s1,4)) . SBP),(4 + RetSP)) or b <> DataLoc (((Comput (P1,s1,4)) . SBP),(4 + RetSP)) )
;
suppose A105:
b = DataLoc (
((Comput (P1,s1,4)) . SBP),
(4 + RetSP))
;
(Comput (P1,s1,5)) . b1 = (Comput (P2,s2,5)) . b1then A106:
b = DataLoc (
((Comput (P2,s2,4)) . SBP),
(4 + RetSP))
by A8, A96;
thus (Comput (P1,s1,5)) . b =
(Comput (P1,s1,4)) . (DataLoc (((Comput (P1,s1,4)) . GBP),1))
by A54, A105, SCMPDS_2:47
.=
(Comput (P2,s2,4)) . (DataLoc (((Comput (P1,s1,4)) . GBP),1))
by A96, A104
.=
(Comput (P2,s2,4)) . (DataLoc (((Comput (P2,s2,4)) . GBP),1))
by A5, A9, A96
.=
(Comput (P2,s2,5)) . b
by A61, A106, SCMPDS_2:47
;
verum end; suppose A107:
b <> DataLoc (
((Comput (P1,s1,4)) . SBP),
(4 + RetSP))
;
(Comput (P1,s1,5)) . b1 = (Comput (P2,s2,5)) . b1then A108:
b <> DataLoc (
((Comput (P2,s2,4)) . SBP),
(4 + RetSP))
by A8, A96;
thus (Comput (P1,s1,5)) . b =
(Comput (P1,s1,4)) . b
by A54, A107, SCMPDS_2:47
.=
(Comput (P2,s2,4)) . b
by A96, A103
.=
(Comput (P2,s2,5)) . b
by A61, A108, SCMPDS_2:47
;
verum end; end; end;
A109:
now for b being Int_position st s1 . b = s2 . b holds
(Comput (P1,s1,6)) . b = (Comput (P2,s2,6)) . blet b be
Int_position;
( s1 . b = s2 . b implies (Comput (P1,s1,6)) . b1 = (Comput (P2,s2,6)) . b1 )assume A110:
s1 . b = s2 . b
;
(Comput (P1,s1,6)) . b1 = (Comput (P2,s2,6)) . b1A111:
s1 . (DataLoc (((Comput (P1,s1,5)) . GBP),1)) =
s2 . (intpos (0 + 1))
by A8, A66, Th1
.=
s2 . (DataLoc (((Comput (P1,s1,5)) . GBP),1))
by A66, Th1
;
per cases
( b = DataLoc (((Comput (P1,s1,5)) . GBP),1) or b <> DataLoc (((Comput (P1,s1,5)) . GBP),1) )
;
suppose A112:
b = DataLoc (
((Comput (P1,s1,5)) . GBP),1)
;
(Comput (P1,s1,6)) . b1 = (Comput (P2,s2,6)) . b1then A113:
b = DataLoc (
((Comput (P2,s2,5)) . GBP),1)
by A5, A9, A102;
thus (Comput (P1,s1,6)) . b =
((Comput (P1,s1,5)) . (DataLoc (((Comput (P1,s1,5)) . GBP),1))) + 4
by A65, A112, SCMPDS_2:48
.=
((Comput (P2,s2,5)) . (DataLoc (((Comput (P1,s1,5)) . GBP),1))) + 4
by A102, A111
.=
((Comput (P2,s2,5)) . (DataLoc (((Comput (P2,s2,5)) . GBP),1))) + 4
by A5, A9, A102
.=
(Comput (P2,s2,6)) . b
by A70, A113, SCMPDS_2:48
;
verum end; suppose A114:
b <> DataLoc (
((Comput (P1,s1,5)) . GBP),1)
;
(Comput (P1,s1,6)) . b1 = (Comput (P2,s2,6)) . b1then A115:
b <> DataLoc (
((Comput (P2,s2,5)) . GBP),1)
by A5, A9, A102;
thus (Comput (P1,s1,6)) . b =
(Comput (P1,s1,5)) . b
by A65, A114, SCMPDS_2:48
.=
(Comput (P2,s2,5)) . b
by A102, A110
.=
(Comput (P2,s2,6)) . b
by A70, A115, SCMPDS_2:48
;
verum end; end; end;
A116:
now for b being Int_position st s1 . b = s2 . b holds
(Comput (P1,s1,7)) . b = (Comput (P2,s2,7)) . blet b be
Int_position;
( s1 . b = s2 . b implies (Comput (P1,s1,7)) . b1 = (Comput (P2,s2,7)) . b1 )assume A117:
s1 . b = s2 . b
;
(Comput (P1,s1,7)) . b1 = (Comput (P2,s2,7)) . b1per cases
( b = DataLoc (((Comput (P1,s1,6)) . SBP),RetIC) or b <> DataLoc (((Comput (P1,s1,6)) . SBP),RetIC) )
;
suppose A118:
b = DataLoc (
((Comput (P1,s1,6)) . SBP),
RetIC)
;
(Comput (P1,s1,7)) . b1 = (Comput (P2,s2,7)) . b1then A119:
b = DataLoc (
((Comput (P2,s2,6)) . SBP),
RetIC)
by A8, A109;
thus (Comput (P1,s1,7)) . b =
IC (Comput (P1,s1,6))
by A74, A118, SCMPDS_2:59
.=
(Comput (P2,s2,7)) . b
by A72, A76, A78, A119, SCMPDS_2:59
;
verum end; suppose A120:
b <> DataLoc (
((Comput (P1,s1,6)) . SBP),
RetIC)
;
(Comput (P1,s1,7)) . b1 = (Comput (P2,s2,7)) . b1then A121:
b <> DataLoc (
((Comput (P2,s2,6)) . SBP),
RetIC)
by A8, A109;
thus (Comput (P1,s1,7)) . b =
(Comput (P1,s1,6)) . b
by A74, A120, SCMPDS_2:59
.=
(Comput (P2,s2,6)) . b
by A109, A117
.=
(Comput (P2,s2,7)) . b
by A78, A121, SCMPDS_2:59
;
verum end; end; end;
hereby verum
let k be
Nat;
for a being Int_position st k <= 7 & s1 . a = s2 . a holds
( IC (Comput (P1,s1,b2)) = IC (Comput (P2,s2,b2)) & (Comput (P1,s1,b2)) . b3 = (Comput (P2,s2,b2)) . b3 )let a be
Int_position;
( k <= 7 & s1 . a = s2 . a implies ( IC (Comput (P1,s1,b1)) = IC (Comput (P2,s2,b1)) & (Comput (P1,s1,b1)) . b2 = (Comput (P2,s2,b1)) . b2 ) )assume that A122:
k <= 7
and A123:
s1 . a = s2 . a
;
( IC (Comput (P1,s1,b1)) = IC (Comput (P2,s2,b1)) & (Comput (P1,s1,b1)) . b2 = (Comput (P2,s2,b1)) . b2 )
not not
k = 0 & ... & not
k = 7
by A122;
per cases then
( k = 0 or k = 1 or k = 2 or k = 3 or k = 4 or k = 5 or k = 6 or k = 7 )
;
suppose A124:
k = 0
;
( IC (Comput (P1,s1,b1)) = IC (Comput (P2,s2,b1)) & (Comput (P1,s1,b1)) . b2 = (Comput (P2,s2,b1)) . b2 )hence IC (Comput (P1,s1,k)) =
IC s1
by EXTPRO_1:2
.=
IC (Comput (P2,s2,k))
by A7, A124, EXTPRO_1:2
;
(Comput (P1,s1,k)) . a = (Comput (P2,s2,k)) . athus (Comput (P1,s1,k)) . a =
s1 . a
by A124, EXTPRO_1:2
.=
(Comput (P2,s2,k)) . a
by A123, A124, EXTPRO_1:2
;
verum end; suppose A125:
k = 1
;
( IC (Comput (P1,s1,b1)) = IC (Comput (P2,s2,b1)) & (Comput (P1,s1,b1)) . b2 = (Comput (P2,s2,b1)) . b2 )hence
IC (Comput (P1,s1,k)) = IC (Comput (P2,s2,k))
by A17, A23;
(Comput (P1,s1,k)) . a = (Comput (P2,s2,k)) . athus
(Comput (P1,s1,k)) . a = (Comput (P2,s2,k)) . a
by A79, A123, A125;
verum end; suppose A126:
k = 2
;
( IC (Comput (P1,s1,b1)) = IC (Comput (P2,s2,b1)) & (Comput (P1,s1,b1)) . b2 = (Comput (P2,s2,b1)) . b2 )hence
IC (Comput (P1,s1,k)) = IC (Comput (P2,s2,k))
by A27, A34;
(Comput (P1,s1,k)) . a = (Comput (P2,s2,k)) . athus
(Comput (P1,s1,k)) . a = (Comput (P2,s2,k)) . a
by A80, A123, A126;
verum end; suppose A127:
k = 3
;
( IC (Comput (P1,s1,b1)) = IC (Comput (P2,s2,b1)) & (Comput (P1,s1,b1)) . b2 = (Comput (P2,s2,b1)) . b2 )hence
IC (Comput (P1,s1,k)) = IC (Comput (P2,s2,k))
by A38, A48;
(Comput (P1,s1,k)) . a = (Comput (P2,s2,k)) . athus
(Comput (P1,s1,k)) . a = (Comput (P2,s2,k)) . a
by A86, A123, A127;
verum end; suppose A128:
k = 4
;
( IC (Comput (P1,s1,b1)) = IC (Comput (P2,s2,b1)) & (Comput (P1,s1,b1)) . b2 = (Comput (P2,s2,b1)) . b2 )hence
IC (Comput (P1,s1,k)) = IC (Comput (P2,s2,k))
by A52, A59;
(Comput (P1,s1,k)) . a = (Comput (P2,s2,k)) . athus
(Comput (P1,s1,k)) . a = (Comput (P2,s2,k)) . a
by A96, A123, A128;
verum end; suppose A129:
k = 5
;
( IC (Comput (P1,s1,b1)) = IC (Comput (P2,s2,b1)) & (Comput (P1,s1,b1)) . b2 = (Comput (P2,s2,b1)) . b2 )hence
IC (Comput (P1,s1,k)) = IC (Comput (P2,s2,k))
by A63, A68;
(Comput (P1,s1,k)) . a = (Comput (P2,s2,k)) . athus
(Comput (P1,s1,k)) . a = (Comput (P2,s2,k)) . a
by A102, A123, A129;
verum end; suppose A130:
k = 6
;
( IC (Comput (P1,s1,b1)) = IC (Comput (P2,s2,b1)) & (Comput (P1,s1,b1)) . b2 = (Comput (P2,s2,b1)) . b2 )hence
IC (Comput (P1,s1,k)) = IC (Comput (P2,s2,k))
by A72, A76;
(Comput (P1,s1,k)) . a = (Comput (P2,s2,k)) . athus
(Comput (P1,s1,k)) . a = (Comput (P2,s2,k)) . a
by A109, A123, A130;
verum end; suppose A131:
k = 7
;
( IC (Comput (P1,s1,b1)) = IC (Comput (P2,s2,b1)) & (Comput (P1,s1,b1)) . b2 = (Comput (P2,s2,b1)) . b2 )hence IC (Comput (P1,s1,k)) =
(IC (Comput (P2,s2,6))) + 1
by A72, A74, A76, SCMPDS_2:59
.=
IC (Comput (P2,s2,k))
by A78, A131, SCMPDS_2:59
;
(Comput (P1,s1,k)) . a = (Comput (P2,s2,k)) . athus
(Comput (P1,s1,k)) . a = (Comput (P2,s2,k)) . a
by A116, A123, A131;
verum end; end;
end;