set a = GBP ;
let s be State of SCMPDS ; ( s . GBP = 0 implies ( (IExec ((((GBP ,5 := GBP ,4) ';' (SubFrom GBP ,5,GBP ,2)) ';' (GBP ,3 := GBP ,2)) ';' (AddTo GBP ,3,1)),s) . GBP = 0 & (IExec ((((GBP ,5 := GBP ,4) ';' (SubFrom GBP ,5,GBP ,2)) ';' (GBP ,3 := GBP ,2)) ';' (AddTo GBP ,3,1)),s) . (intpos 1) = s . (intpos 1) & (IExec ((((GBP ,5 := GBP ,4) ';' (SubFrom GBP ,5,GBP ,2)) ';' (GBP ,3 := GBP ,2)) ';' (AddTo GBP ,3,1)),s) . (intpos 2) = s . (intpos 2) & (IExec ((((GBP ,5 := GBP ,4) ';' (SubFrom GBP ,5,GBP ,2)) ';' (GBP ,3 := GBP ,2)) ';' (AddTo GBP ,3,1)),s) . (intpos 3) = (s . (intpos 2)) + 1 & (IExec ((((GBP ,5 := GBP ,4) ';' (SubFrom GBP ,5,GBP ,2)) ';' (GBP ,3 := GBP ,2)) ';' (AddTo GBP ,3,1)),s) . (intpos 4) = s . (intpos 4) & (IExec ((((GBP ,5 := GBP ,4) ';' (SubFrom GBP ,5,GBP ,2)) ';' (GBP ,3 := GBP ,2)) ';' (AddTo GBP ,3,1)),s) . (intpos 5) = (s . (intpos 4)) - (s . (intpos 2)) & ( for i being Element of NAT st i >= 8 holds
(IExec ((((GBP ,5 := GBP ,4) ';' (SubFrom GBP ,5,GBP ,2)) ';' (GBP ,3 := GBP ,2)) ';' (AddTo GBP ,3,1)),s) . (intpos i) = s . (intpos i) ) ) )
set t0 = Initialize s;
set t1 = IExec ((((GBP ,5 := GBP ,4) ';' (SubFrom GBP ,5,GBP ,2)) ';' (GBP ,3 := GBP ,2)) ';' (AddTo GBP ,3,1)),s;
set t2 = IExec (((GBP ,5 := GBP ,4) ';' (SubFrom GBP ,5,GBP ,2)) ';' (GBP ,3 := GBP ,2)),s;
set t3 = IExec ((GBP ,5 := GBP ,4) ';' (SubFrom GBP ,5,GBP ,2)),s;
set t4 = Exec (GBP ,5 := GBP ,4),(Initialize s);
assume
s . GBP = 0
; ( (IExec ((((GBP ,5 := GBP ,4) ';' (SubFrom GBP ,5,GBP ,2)) ';' (GBP ,3 := GBP ,2)) ';' (AddTo GBP ,3,1)),s) . GBP = 0 & (IExec ((((GBP ,5 := GBP ,4) ';' (SubFrom GBP ,5,GBP ,2)) ';' (GBP ,3 := GBP ,2)) ';' (AddTo GBP ,3,1)),s) . (intpos 1) = s . (intpos 1) & (IExec ((((GBP ,5 := GBP ,4) ';' (SubFrom GBP ,5,GBP ,2)) ';' (GBP ,3 := GBP ,2)) ';' (AddTo GBP ,3,1)),s) . (intpos 2) = s . (intpos 2) & (IExec ((((GBP ,5 := GBP ,4) ';' (SubFrom GBP ,5,GBP ,2)) ';' (GBP ,3 := GBP ,2)) ';' (AddTo GBP ,3,1)),s) . (intpos 3) = (s . (intpos 2)) + 1 & (IExec ((((GBP ,5 := GBP ,4) ';' (SubFrom GBP ,5,GBP ,2)) ';' (GBP ,3 := GBP ,2)) ';' (AddTo GBP ,3,1)),s) . (intpos 4) = s . (intpos 4) & (IExec ((((GBP ,5 := GBP ,4) ';' (SubFrom GBP ,5,GBP ,2)) ';' (GBP ,3 := GBP ,2)) ';' (AddTo GBP ,3,1)),s) . (intpos 5) = (s . (intpos 4)) - (s . (intpos 2)) & ( for i being Element of NAT st i >= 8 holds
(IExec ((((GBP ,5 := GBP ,4) ';' (SubFrom GBP ,5,GBP ,2)) ';' (GBP ,3 := GBP ,2)) ';' (AddTo GBP ,3,1)),s) . (intpos i) = s . (intpos i) ) )
then A1:
(Initialize s) . GBP = 0
by SCMPDS_5:40;
then A2:
DataLoc ((Initialize s) . GBP ),5 = intpos (0 + 5)
by SCMP_GCD:5;
then A3: (Exec (GBP ,5 := GBP ,4),(Initialize s)) . (intpos 5) =
(Initialize s) . (DataLoc ((Initialize s) . GBP ),4)
by SCMPDS_2:59
.=
(Initialize s) . (intpos (0 + 4))
by A1, SCMP_GCD:5
.=
s . (intpos 4)
by SCMPDS_5:40
;
(Initialize s) . (intpos 4) = s . (intpos 4)
by SCMPDS_5:40;
then A4:
(Exec (GBP ,5 := GBP ,4),(Initialize s)) . (intpos 4) = s . (intpos 4)
by A2, AMI_3:52, SCMPDS_2:59;
(Initialize s) . (intpos 1) = s . (intpos 1)
by SCMPDS_5:40;
then A5:
(Exec (GBP ,5 := GBP ,4),(Initialize s)) . (intpos 1) = s . (intpos 1)
by A2, AMI_3:52, SCMPDS_2:59;
A6:
(Exec (GBP ,5 := GBP ,4),(Initialize s)) . GBP = 0
by A1, A2, AMI_3:52, SCMPDS_2:59;
then A7:
DataLoc ((Exec (GBP ,5 := GBP ,4),(Initialize s)) . GBP ),5 = intpos (0 + 5)
by SCMP_GCD:5;
A8: (IExec ((GBP ,5 := GBP ,4) ';' (SubFrom GBP ,5,GBP ,2)),s) . GBP =
(Exec (SubFrom GBP ,5,GBP ,2),(Exec (GBP ,5 := GBP ,4),(Initialize s))) . GBP
by SCMPDS_5:47
.=
0
by A6, A7, AMI_3:52, SCMPDS_2:62
;
then A9:
DataLoc ((IExec ((GBP ,5 := GBP ,4) ';' (SubFrom GBP ,5,GBP ,2)),s) . GBP ),3 = intpos (0 + 3)
by SCMP_GCD:5;
A10: (IExec ((GBP ,5 := GBP ,4) ';' (SubFrom GBP ,5,GBP ,2)),s) . (intpos 4) =
(Exec (SubFrom GBP ,5,GBP ,2),(Exec (GBP ,5 := GBP ,4),(Initialize s))) . (intpos 4)
by SCMPDS_5:47
.=
s . (intpos 4)
by A4, A7, AMI_3:52, SCMPDS_2:62
;
A11: (IExec (((GBP ,5 := GBP ,4) ';' (SubFrom GBP ,5,GBP ,2)) ';' (GBP ,3 := GBP ,2)),s) . (intpos 4) =
(Exec (GBP ,3 := GBP ,2),(IExec ((GBP ,5 := GBP ,4) ';' (SubFrom GBP ,5,GBP ,2)),s)) . (intpos 4)
by SCMPDS_5:46
.=
s . (intpos 4)
by A10, A9, AMI_3:52, SCMPDS_2:59
;
A12:
(Initialize s) . (intpos 2) = s . (intpos 2)
by SCMPDS_5:40;
then A13:
(Exec (GBP ,5 := GBP ,4),(Initialize s)) . (intpos 2) = s . (intpos 2)
by A2, AMI_3:52, SCMPDS_2:59;
A14: (IExec ((GBP ,5 := GBP ,4) ';' (SubFrom GBP ,5,GBP ,2)),s) . (intpos 5) =
(Exec (SubFrom GBP ,5,GBP ,2),(Exec (GBP ,5 := GBP ,4),(Initialize s))) . (intpos 5)
by SCMPDS_5:47
.=
((Exec (GBP ,5 := GBP ,4),(Initialize s)) . (intpos 5)) - ((Exec (GBP ,5 := GBP ,4),(Initialize s)) . (DataLoc ((Exec (GBP ,5 := GBP ,4),(Initialize s)) . GBP ),2))
by A7, SCMPDS_2:62
.=
((Exec (GBP ,5 := GBP ,4),(Initialize s)) . (intpos 5)) - ((Exec (GBP ,5 := GBP ,4),(Initialize s)) . (intpos (0 + 2)))
by A6, SCMP_GCD:5
.=
(s . (intpos 4)) - (s . (intpos 2))
by A12, A2, A3, AMI_3:52, SCMPDS_2:59
;
A15: (IExec (((GBP ,5 := GBP ,4) ';' (SubFrom GBP ,5,GBP ,2)) ';' (GBP ,3 := GBP ,2)),s) . (intpos 5) =
(Exec (GBP ,3 := GBP ,2),(IExec ((GBP ,5 := GBP ,4) ';' (SubFrom GBP ,5,GBP ,2)),s)) . (intpos 5)
by SCMPDS_5:46
.=
(s . (intpos 4)) - (s . (intpos 2))
by A14, A9, AMI_3:52, SCMPDS_2:59
;
A16: (IExec ((GBP ,5 := GBP ,4) ';' (SubFrom GBP ,5,GBP ,2)),s) . (intpos 2) =
(Exec (SubFrom GBP ,5,GBP ,2),(Exec (GBP ,5 := GBP ,4),(Initialize s))) . (intpos 2)
by SCMPDS_5:47
.=
s . (intpos 2)
by A13, A7, AMI_3:52, SCMPDS_2:62
;
A17: (IExec ((GBP ,5 := GBP ,4) ';' (SubFrom GBP ,5,GBP ,2)),s) . (intpos 1) =
(Exec (SubFrom GBP ,5,GBP ,2),(Exec (GBP ,5 := GBP ,4),(Initialize s))) . (intpos 1)
by SCMPDS_5:47
.=
s . (intpos 1)
by A5, A7, AMI_3:52, SCMPDS_2:62
;
A18: (IExec (((GBP ,5 := GBP ,4) ';' (SubFrom GBP ,5,GBP ,2)) ';' (GBP ,3 := GBP ,2)),s) . (intpos 1) =
(Exec (GBP ,3 := GBP ,2),(IExec ((GBP ,5 := GBP ,4) ';' (SubFrom GBP ,5,GBP ,2)),s)) . (intpos 1)
by SCMPDS_5:46
.=
s . (intpos 1)
by A17, A9, AMI_3:52, SCMPDS_2:59
;
A19: (IExec (((GBP ,5 := GBP ,4) ';' (SubFrom GBP ,5,GBP ,2)) ';' (GBP ,3 := GBP ,2)),s) . GBP =
(Exec (GBP ,3 := GBP ,2),(IExec ((GBP ,5 := GBP ,4) ';' (SubFrom GBP ,5,GBP ,2)),s)) . GBP
by SCMPDS_5:46
.=
0
by A8, A9, AMI_3:52, SCMPDS_2:59
;
then A20:
DataLoc ((IExec (((GBP ,5 := GBP ,4) ';' (SubFrom GBP ,5,GBP ,2)) ';' (GBP ,3 := GBP ,2)),s) . GBP ),3 = intpos (0 + 3)
by SCMP_GCD:5;
A21: (IExec (((GBP ,5 := GBP ,4) ';' (SubFrom GBP ,5,GBP ,2)) ';' (GBP ,3 := GBP ,2)),s) . (intpos 3) =
(Exec (GBP ,3 := GBP ,2),(IExec ((GBP ,5 := GBP ,4) ';' (SubFrom GBP ,5,GBP ,2)),s)) . (intpos 3)
by SCMPDS_5:46
.=
(IExec ((GBP ,5 := GBP ,4) ';' (SubFrom GBP ,5,GBP ,2)),s) . (DataLoc ((IExec ((GBP ,5 := GBP ,4) ';' (SubFrom GBP ,5,GBP ,2)),s) . GBP ),2)
by A9, SCMPDS_2:59
.=
s . (intpos 2)
by A8, A16, SCMP_GCD:5
;
A22: (IExec (((GBP ,5 := GBP ,4) ';' (SubFrom GBP ,5,GBP ,2)) ';' (GBP ,3 := GBP ,2)),s) . (intpos 2) =
(Exec (GBP ,3 := GBP ,2),(IExec ((GBP ,5 := GBP ,4) ';' (SubFrom GBP ,5,GBP ,2)),s)) . (intpos 2)
by SCMPDS_5:46
.=
s . (intpos 2)
by A16, A9, AMI_3:52, SCMPDS_2:59
;
thus (IExec ((((GBP ,5 := GBP ,4) ';' (SubFrom GBP ,5,GBP ,2)) ';' (GBP ,3 := GBP ,2)) ';' (AddTo GBP ,3,1)),s) . GBP =
(Exec (AddTo GBP ,3,1),(IExec (((GBP ,5 := GBP ,4) ';' (SubFrom GBP ,5,GBP ,2)) ';' (GBP ,3 := GBP ,2)),s)) . GBP
by SCMPDS_5:46
.=
0
by A19, A20, AMI_3:52, SCMPDS_2:60
; ( (IExec ((((GBP ,5 := GBP ,4) ';' (SubFrom GBP ,5,GBP ,2)) ';' (GBP ,3 := GBP ,2)) ';' (AddTo GBP ,3,1)),s) . (intpos 1) = s . (intpos 1) & (IExec ((((GBP ,5 := GBP ,4) ';' (SubFrom GBP ,5,GBP ,2)) ';' (GBP ,3 := GBP ,2)) ';' (AddTo GBP ,3,1)),s) . (intpos 2) = s . (intpos 2) & (IExec ((((GBP ,5 := GBP ,4) ';' (SubFrom GBP ,5,GBP ,2)) ';' (GBP ,3 := GBP ,2)) ';' (AddTo GBP ,3,1)),s) . (intpos 3) = (s . (intpos 2)) + 1 & (IExec ((((GBP ,5 := GBP ,4) ';' (SubFrom GBP ,5,GBP ,2)) ';' (GBP ,3 := GBP ,2)) ';' (AddTo GBP ,3,1)),s) . (intpos 4) = s . (intpos 4) & (IExec ((((GBP ,5 := GBP ,4) ';' (SubFrom GBP ,5,GBP ,2)) ';' (GBP ,3 := GBP ,2)) ';' (AddTo GBP ,3,1)),s) . (intpos 5) = (s . (intpos 4)) - (s . (intpos 2)) & ( for i being Element of NAT st i >= 8 holds
(IExec ((((GBP ,5 := GBP ,4) ';' (SubFrom GBP ,5,GBP ,2)) ';' (GBP ,3 := GBP ,2)) ';' (AddTo GBP ,3,1)),s) . (intpos i) = s . (intpos i) ) )
thus (IExec ((((GBP ,5 := GBP ,4) ';' (SubFrom GBP ,5,GBP ,2)) ';' (GBP ,3 := GBP ,2)) ';' (AddTo GBP ,3,1)),s) . (intpos 1) =
(Exec (AddTo GBP ,3,1),(IExec (((GBP ,5 := GBP ,4) ';' (SubFrom GBP ,5,GBP ,2)) ';' (GBP ,3 := GBP ,2)),s)) . (intpos 1)
by SCMPDS_5:46
.=
s . (intpos 1)
by A18, A20, AMI_3:52, SCMPDS_2:60
; ( (IExec ((((GBP ,5 := GBP ,4) ';' (SubFrom GBP ,5,GBP ,2)) ';' (GBP ,3 := GBP ,2)) ';' (AddTo GBP ,3,1)),s) . (intpos 2) = s . (intpos 2) & (IExec ((((GBP ,5 := GBP ,4) ';' (SubFrom GBP ,5,GBP ,2)) ';' (GBP ,3 := GBP ,2)) ';' (AddTo GBP ,3,1)),s) . (intpos 3) = (s . (intpos 2)) + 1 & (IExec ((((GBP ,5 := GBP ,4) ';' (SubFrom GBP ,5,GBP ,2)) ';' (GBP ,3 := GBP ,2)) ';' (AddTo GBP ,3,1)),s) . (intpos 4) = s . (intpos 4) & (IExec ((((GBP ,5 := GBP ,4) ';' (SubFrom GBP ,5,GBP ,2)) ';' (GBP ,3 := GBP ,2)) ';' (AddTo GBP ,3,1)),s) . (intpos 5) = (s . (intpos 4)) - (s . (intpos 2)) & ( for i being Element of NAT st i >= 8 holds
(IExec ((((GBP ,5 := GBP ,4) ';' (SubFrom GBP ,5,GBP ,2)) ';' (GBP ,3 := GBP ,2)) ';' (AddTo GBP ,3,1)),s) . (intpos i) = s . (intpos i) ) )
thus (IExec ((((GBP ,5 := GBP ,4) ';' (SubFrom GBP ,5,GBP ,2)) ';' (GBP ,3 := GBP ,2)) ';' (AddTo GBP ,3,1)),s) . (intpos 2) =
(Exec (AddTo GBP ,3,1),(IExec (((GBP ,5 := GBP ,4) ';' (SubFrom GBP ,5,GBP ,2)) ';' (GBP ,3 := GBP ,2)),s)) . (intpos 2)
by SCMPDS_5:46
.=
s . (intpos 2)
by A22, A20, AMI_3:52, SCMPDS_2:60
; ( (IExec ((((GBP ,5 := GBP ,4) ';' (SubFrom GBP ,5,GBP ,2)) ';' (GBP ,3 := GBP ,2)) ';' (AddTo GBP ,3,1)),s) . (intpos 3) = (s . (intpos 2)) + 1 & (IExec ((((GBP ,5 := GBP ,4) ';' (SubFrom GBP ,5,GBP ,2)) ';' (GBP ,3 := GBP ,2)) ';' (AddTo GBP ,3,1)),s) . (intpos 4) = s . (intpos 4) & (IExec ((((GBP ,5 := GBP ,4) ';' (SubFrom GBP ,5,GBP ,2)) ';' (GBP ,3 := GBP ,2)) ';' (AddTo GBP ,3,1)),s) . (intpos 5) = (s . (intpos 4)) - (s . (intpos 2)) & ( for i being Element of NAT st i >= 8 holds
(IExec ((((GBP ,5 := GBP ,4) ';' (SubFrom GBP ,5,GBP ,2)) ';' (GBP ,3 := GBP ,2)) ';' (AddTo GBP ,3,1)),s) . (intpos i) = s . (intpos i) ) )
thus (IExec ((((GBP ,5 := GBP ,4) ';' (SubFrom GBP ,5,GBP ,2)) ';' (GBP ,3 := GBP ,2)) ';' (AddTo GBP ,3,1)),s) . (intpos 3) =
(Exec (AddTo GBP ,3,1),(IExec (((GBP ,5 := GBP ,4) ';' (SubFrom GBP ,5,GBP ,2)) ';' (GBP ,3 := GBP ,2)),s)) . (intpos 3)
by SCMPDS_5:46
.=
(s . (intpos 2)) + 1
by A21, A20, SCMPDS_2:60
; ( (IExec ((((GBP ,5 := GBP ,4) ';' (SubFrom GBP ,5,GBP ,2)) ';' (GBP ,3 := GBP ,2)) ';' (AddTo GBP ,3,1)),s) . (intpos 4) = s . (intpos 4) & (IExec ((((GBP ,5 := GBP ,4) ';' (SubFrom GBP ,5,GBP ,2)) ';' (GBP ,3 := GBP ,2)) ';' (AddTo GBP ,3,1)),s) . (intpos 5) = (s . (intpos 4)) - (s . (intpos 2)) & ( for i being Element of NAT st i >= 8 holds
(IExec ((((GBP ,5 := GBP ,4) ';' (SubFrom GBP ,5,GBP ,2)) ';' (GBP ,3 := GBP ,2)) ';' (AddTo GBP ,3,1)),s) . (intpos i) = s . (intpos i) ) )
thus (IExec ((((GBP ,5 := GBP ,4) ';' (SubFrom GBP ,5,GBP ,2)) ';' (GBP ,3 := GBP ,2)) ';' (AddTo GBP ,3,1)),s) . (intpos 4) =
(Exec (AddTo GBP ,3,1),(IExec (((GBP ,5 := GBP ,4) ';' (SubFrom GBP ,5,GBP ,2)) ';' (GBP ,3 := GBP ,2)),s)) . (intpos 4)
by SCMPDS_5:46
.=
s . (intpos 4)
by A11, A20, AMI_3:52, SCMPDS_2:60
; ( (IExec ((((GBP ,5 := GBP ,4) ';' (SubFrom GBP ,5,GBP ,2)) ';' (GBP ,3 := GBP ,2)) ';' (AddTo GBP ,3,1)),s) . (intpos 5) = (s . (intpos 4)) - (s . (intpos 2)) & ( for i being Element of NAT st i >= 8 holds
(IExec ((((GBP ,5 := GBP ,4) ';' (SubFrom GBP ,5,GBP ,2)) ';' (GBP ,3 := GBP ,2)) ';' (AddTo GBP ,3,1)),s) . (intpos i) = s . (intpos i) ) )
thus (IExec ((((GBP ,5 := GBP ,4) ';' (SubFrom GBP ,5,GBP ,2)) ';' (GBP ,3 := GBP ,2)) ';' (AddTo GBP ,3,1)),s) . (intpos 5) =
(Exec (AddTo GBP ,3,1),(IExec (((GBP ,5 := GBP ,4) ';' (SubFrom GBP ,5,GBP ,2)) ';' (GBP ,3 := GBP ,2)),s)) . (intpos 5)
by SCMPDS_5:46
.=
(s . (intpos 4)) - (s . (intpos 2))
by A15, A20, AMI_3:52, SCMPDS_2:60
; for i being Element of NAT st i >= 8 holds
(IExec ((((GBP ,5 := GBP ,4) ';' (SubFrom GBP ,5,GBP ,2)) ';' (GBP ,3 := GBP ,2)) ';' (AddTo GBP ,3,1)),s) . (intpos i) = s . (intpos i)
A23:
now let i be
Element of
NAT ;
( i >= 8 implies (Exec (GBP ,5 := GBP ,4),(Initialize s)) . (intpos i) = s . (intpos i) )assume
i >= 8
;
(Exec (GBP ,5 := GBP ,4),(Initialize s)) . (intpos i) = s . (intpos i)then
i > 5
by XXREAL_0:2;
hence (Exec (GBP ,5 := GBP ,4),(Initialize s)) . (intpos i) =
(Initialize s) . (intpos i)
by A2, AMI_3:52, SCMPDS_2:59
.=
s . (intpos i)
by SCMPDS_5:40
;
verum end;
A24:
now let i be
Element of
NAT ;
( i >= 8 implies (IExec ((GBP ,5 := GBP ,4) ';' (SubFrom GBP ,5,GBP ,2)),s) . (intpos i) = s . (intpos i) )assume A25:
i >= 8
;
(IExec ((GBP ,5 := GBP ,4) ';' (SubFrom GBP ,5,GBP ,2)),s) . (intpos i) = s . (intpos i)then A26:
i > 5
by XXREAL_0:2;
thus (IExec ((GBP ,5 := GBP ,4) ';' (SubFrom GBP ,5,GBP ,2)),s) . (intpos i) =
(Exec (SubFrom GBP ,5,GBP ,2),(Exec (GBP ,5 := GBP ,4),(Initialize s))) . (intpos i)
by SCMPDS_5:47
.=
(Exec (GBP ,5 := GBP ,4),(Initialize s)) . (intpos i)
by A7, A26, AMI_3:52, SCMPDS_2:62
.=
s . (intpos i)
by A23, A25
;
verum end;
A27:
now let i be
Element of
NAT ;
( i >= 8 implies (IExec (((GBP ,5 := GBP ,4) ';' (SubFrom GBP ,5,GBP ,2)) ';' (GBP ,3 := GBP ,2)),s) . (intpos i) = s . (intpos i) )assume A28:
i >= 8
;
(IExec (((GBP ,5 := GBP ,4) ';' (SubFrom GBP ,5,GBP ,2)) ';' (GBP ,3 := GBP ,2)),s) . (intpos i) = s . (intpos i)then A29:
i > 3
by XXREAL_0:2;
thus (IExec (((GBP ,5 := GBP ,4) ';' (SubFrom GBP ,5,GBP ,2)) ';' (GBP ,3 := GBP ,2)),s) . (intpos i) =
(Exec (GBP ,3 := GBP ,2),(IExec ((GBP ,5 := GBP ,4) ';' (SubFrom GBP ,5,GBP ,2)),s)) . (intpos i)
by SCMPDS_5:46
.=
(IExec ((GBP ,5 := GBP ,4) ';' (SubFrom GBP ,5,GBP ,2)),s) . (intpos i)
by A9, A29, AMI_3:52, SCMPDS_2:59
.=
s . (intpos i)
by A24, A28
;
verum end;
hereby verum
let i be
Element of
NAT ;
( i >= 8 implies (IExec ((((GBP ,5 := GBP ,4) ';' (SubFrom GBP ,5,GBP ,2)) ';' (GBP ,3 := GBP ,2)) ';' (AddTo GBP ,3,1)),s) . (intpos i) = s . (intpos i) )assume A30:
i >= 8
;
(IExec ((((GBP ,5 := GBP ,4) ';' (SubFrom GBP ,5,GBP ,2)) ';' (GBP ,3 := GBP ,2)) ';' (AddTo GBP ,3,1)),s) . (intpos i) = s . (intpos i)then A31:
i > 3
by XXREAL_0:2;
thus (IExec ((((GBP ,5 := GBP ,4) ';' (SubFrom GBP ,5,GBP ,2)) ';' (GBP ,3 := GBP ,2)) ';' (AddTo GBP ,3,1)),s) . (intpos i) =
(Exec (AddTo GBP ,3,1),(IExec (((GBP ,5 := GBP ,4) ';' (SubFrom GBP ,5,GBP ,2)) ';' (GBP ,3 := GBP ,2)),s)) . (intpos i)
by SCMPDS_5:46
.=
(IExec (((GBP ,5 := GBP ,4) ';' (SubFrom GBP ,5,GBP ,2)) ';' (GBP ,3 := GBP ,2)),s) . (intpos i)
by A20, A31, AMI_3:52, SCMPDS_2:60
.=
s . (intpos i)
by A27, A30
;
verum
end;