set a = GBP ;
let s be State of SCMPDS ; :: thesis: for m3, m4 being Element of NAT st s . GBP = 0 & s . (intpos 5) > 0 & s . (intpos 3) = m3 & s . (intpos 4) = m4 & m3 > 6 & m4 > 6 holds
( (IExec (if>0 GBP ,5,((((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)) ';' (AddTo GBP ,4,(- 1)))),s) . GBP = 0 & (IExec (if>0 GBP ,5,((((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)) ';' (AddTo GBP ,4,(- 1)))),s) . (intpos 1) = s . (intpos 1) & (IExec (if>0 GBP ,5,((((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)) ';' (AddTo GBP ,4,(- 1)))),s) . (intpos 2) = s . (intpos 2) & (IExec (if>0 GBP ,5,((((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)) ';' (AddTo GBP ,4,(- 1)))),s) . (intpos m3) = s . (intpos m4) & (IExec (if>0 GBP ,5,((((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)) ';' (AddTo GBP ,4,(- 1)))),s) . (intpos m4) = s . (intpos m3) & (IExec (if>0 GBP ,5,((((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)) ';' (AddTo GBP ,4,(- 1)))),s) . (intpos 3) = (s . (intpos 3)) + 1 & (IExec (if>0 GBP ,5,((((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)) ';' (AddTo GBP ,4,(- 1)))),s) . (intpos 4) = (s . (intpos 4)) - 1 & (IExec (if>0 GBP ,5,((((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)) ';' (AddTo GBP ,4,(- 1)))),s) . (intpos 5) = (s . (intpos 5)) - 2 & ( for i being Element of NAT st i >= 8 & i <> m3 & i <> m4 holds
(IExec (if>0 GBP ,5,((((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)) ';' (AddTo GBP ,4,(- 1)))),s) . (intpos i) = s . (intpos i) ) )
let m3, m4 be Element of NAT ; :: thesis: ( s . GBP = 0 & s . (intpos 5) > 0 & s . (intpos 3) = m3 & s . (intpos 4) = m4 & m3 > 6 & m4 > 6 implies ( (IExec (if>0 GBP ,5,((((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)) ';' (AddTo GBP ,4,(- 1)))),s) . GBP = 0 & (IExec (if>0 GBP ,5,((((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)) ';' (AddTo GBP ,4,(- 1)))),s) . (intpos 1) = s . (intpos 1) & (IExec (if>0 GBP ,5,((((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)) ';' (AddTo GBP ,4,(- 1)))),s) . (intpos 2) = s . (intpos 2) & (IExec (if>0 GBP ,5,((((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)) ';' (AddTo GBP ,4,(- 1)))),s) . (intpos m3) = s . (intpos m4) & (IExec (if>0 GBP ,5,((((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)) ';' (AddTo GBP ,4,(- 1)))),s) . (intpos m4) = s . (intpos m3) & (IExec (if>0 GBP ,5,((((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)) ';' (AddTo GBP ,4,(- 1)))),s) . (intpos 3) = (s . (intpos 3)) + 1 & (IExec (if>0 GBP ,5,((((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)) ';' (AddTo GBP ,4,(- 1)))),s) . (intpos 4) = (s . (intpos 4)) - 1 & (IExec (if>0 GBP ,5,((((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)) ';' (AddTo GBP ,4,(- 1)))),s) . (intpos 5) = (s . (intpos 5)) - 2 & ( for i being Element of NAT st i >= 8 & i <> m3 & i <> m4 holds
(IExec (if>0 GBP ,5,((((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)) ';' (AddTo GBP ,4,(- 1)))),s) . (intpos i) = s . (intpos i) ) ) )
assume that
A1: s . GBP = 0 and
A2: s . (intpos 5) > 0 and
A3: s . (intpos 3) = m3 and
A4: s . (intpos 4) = m4 and
A5: m3 > 6 and
A6: m4 > 6 ; :: thesis: ( (IExec (if>0 GBP ,5,((((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)) ';' (AddTo GBP ,4,(- 1)))),s) . GBP = 0 & (IExec (if>0 GBP ,5,((((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)) ';' (AddTo GBP ,4,(- 1)))),s) . (intpos 1) = s . (intpos 1) & (IExec (if>0 GBP ,5,((((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)) ';' (AddTo GBP ,4,(- 1)))),s) . (intpos 2) = s . (intpos 2) & (IExec (if>0 GBP ,5,((((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)) ';' (AddTo GBP ,4,(- 1)))),s) . (intpos m3) = s . (intpos m4) & (IExec (if>0 GBP ,5,((((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)) ';' (AddTo GBP ,4,(- 1)))),s) . (intpos m4) = s . (intpos m3) & (IExec (if>0 GBP ,5,((((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)) ';' (AddTo GBP ,4,(- 1)))),s) . (intpos 3) = (s . (intpos 3)) + 1 & (IExec (if>0 GBP ,5,((((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)) ';' (AddTo GBP ,4,(- 1)))),s) . (intpos 4) = (s . (intpos 4)) - 1 & (IExec (if>0 GBP ,5,((((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)) ';' (AddTo GBP ,4,(- 1)))),s) . (intpos 5) = (s . (intpos 5)) - 2 & ( for i being Element of NAT st i >= 8 & i <> m3 & i <> m4 holds
(IExec (if>0 GBP ,5,((((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)) ';' (AddTo GBP ,4,(- 1)))),s) . (intpos i) = s . (intpos i) ) )
A7: m4 > 3 by A6, XXREAL_0:2;
set x = intpos m3;
set y = intpos m4;
set t0 = Initialize s;
set t1 = IExec ((((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)) ';' (AddTo GBP ,4,(- 1))),s;
set t2 = IExec (((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)),s;
set t3 = IExec ((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))),s;
set t4 = IExec (((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)),s;
set t5 = IExec ((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )),s;
set t6 = Exec (GBP ,6 := (intpos 4),0 ),(Initialize s);
A8: (Initialize s) . GBP = 0 by A1, SCMPDS_5:40;
then A9: DataLoc ((Initialize s) . GBP ),6 = intpos (0 + 6) by SCMP_GCD:5;
then A10: (Exec (GBP ,6 := (intpos 4),0 ),(Initialize s)) . GBP = 0 by A8, AMI_3:52, SCMPDS_2:59;
A11: (Initialize s) . (intpos 4) = m4 by A4, SCMPDS_5:40;
then A12: (Exec (GBP ,6 := (intpos 4),0 ),(Initialize s)) . (intpos 4) = m4 by A9, AMI_3:52, SCMPDS_2:59;
then A13: DataLoc ((Exec (GBP ,6 := (intpos 4),0 ),(Initialize s)) . (intpos 4)),0 = intpos (m4 + 0 ) by SCMP_GCD:5;
A14: (IExec ((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )),s) . GBP = (Exec ((intpos 4),0 := (intpos 3),0 ),(Exec (GBP ,6 := (intpos 4),0 ),(Initialize s))) . GBP by SCMPDS_5:47
.= 0 by A6, A10, A13, AMI_3:52, SCMPDS_2:59 ;
A15: (Exec (GBP ,6 := (intpos 4),0 ),(Initialize s)) . (intpos 6) = (Initialize s) . (DataLoc ((Initialize s) . (intpos 4)),0 ) by A9, SCMPDS_2:59
.= (Initialize s) . (intpos (m4 + 0 )) by A11, SCMP_GCD:5
.= s . (intpos m4) by SCMPDS_5:40 ;
(IExec ((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )),s) . (intpos 6) = (Exec ((intpos 4),0 := (intpos 3),0 ),(Exec (GBP ,6 := (intpos 4),0 ),(Initialize s))) . (intpos 6) by SCMPDS_5:47
.= s . (intpos m4) by A6, A15, A13, AMI_3:52, SCMPDS_2:59 ;
then A16: (IExec ((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )),s) . (DataLoc ((IExec ((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )),s) . GBP ),6) = s . (intpos m4) by A14, SCMP_GCD:5;
(Initialize s) . (intpos 3) = m3 by A3, SCMPDS_5:40;
then A17: (Exec (GBP ,6 := (intpos 4),0 ),(Initialize s)) . (intpos 3) = m3 by A9, AMI_3:52, SCMPDS_2:59;
A18: (IExec ((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )),s) . (intpos 3) = (Exec ((intpos 4),0 := (intpos 3),0 ),(Exec (GBP ,6 := (intpos 4),0 ),(Initialize s))) . (intpos 3) by SCMPDS_5:47
.= m3 by A7, A17, A13, AMI_3:52, SCMPDS_2:59 ;
then A19: DataLoc ((IExec ((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )),s) . (intpos 3)),0 = intpos (m3 + 0 ) by SCMP_GCD:5;
A20: (Initialize s) . (intpos m3) = s . (intpos m3) by SCMPDS_5:40;
A21: (IExec ((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )),s) . (intpos m4) = (Exec ((intpos 4),0 := (intpos 3),0 ),(Exec (GBP ,6 := (intpos 4),0 ),(Initialize s))) . (intpos m4) by SCMPDS_5:47
.= (Exec (GBP ,6 := (intpos 4),0 ),(Initialize s)) . (DataLoc ((Exec (GBP ,6 := (intpos 4),0 ),(Initialize s)) . (intpos 3)),0 ) by A13, SCMPDS_2:59
.= (Exec (GBP ,6 := (intpos 4),0 ),(Initialize s)) . (intpos (m3 + 0 )) by A17, SCMP_GCD:5
.= s . (intpos m3) by A5, A20, A9, AMI_3:52, SCMPDS_2:59 ;

A22: now

per cases ( intpos m4 <> DataLoc ((IExec ((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )),s) . (intpos 3)),0 or intpos m4 = DataLoc ((IExec ((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )),s) . (intpos 3)),0 ) ;

suppose A23: intpos m4 <> DataLoc ((IExec ((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )),s) . (intpos 3)),0 ; :: thesis: (IExec (((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)),s) . (intpos m4) = s . (intpos m3)

thus (IExec (((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)),s) . (intpos m4) = (Exec ((intpos 3),0 := GBP ,6),(IExec ((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )),s)) . (intpos m4) by SCMPDS_5:46
.= s . (intpos m3) by A21, A23, SCMPDS_2:59 ; :: thesis: verum

end;

suppose A24: intpos m4 = DataLoc ((IExec ((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )),s) . (intpos 3)),0 ; :: thesis: (IExec (((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)),s) . (intpos m4) = s . (intpos m3)

thus (IExec (((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)),s) . (intpos m4) = (Exec ((intpos 3),0 := GBP ,6),(IExec ((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )),s)) . (intpos m4) by SCMPDS_5:46
.= s . (intpos m3) by A19, A16, A24, SCMPDS_2:59 ; :: thesis: verum

end;

end;

end;

(Initialize s) . (intpos 2) = s . (intpos 2) by SCMPDS_5:40;
then A25: (Exec (GBP ,6 := (intpos 4),0 ),(Initialize s)) . (intpos 2) = s . (intpos 2) by A9, AMI_3:52, SCMPDS_2:59;
A26: m4 > 2 by A6, XXREAL_0:2;
A27: m3 > 5 by A5, XXREAL_0:2;
A28: (IExec (((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)),s) . GBP = (Exec ((intpos 3),0 := GBP ,6),(IExec ((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )),s)) . GBP by SCMPDS_5:46
.= 0 by A5, A14, A19, AMI_3:52, SCMPDS_2:59 ;
then A29: DataLoc ((IExec (((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)),s) . GBP ),5 = intpos (0 + 5) by SCMP_GCD:5;
A30: (IExec ((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))),s) . GBP = (Exec (AddTo GBP ,5,(- 2)),(IExec (((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)),s)) . GBP by SCMPDS_5:46
.= 0 by A28, A29, AMI_3:52, SCMPDS_2:60 ;
then A31: GBP <> DataLoc ((IExec ((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))),s) . GBP ),3 by AMI_3:52, SCMP_GCD:5;
A32: m3 > 3 by A5, XXREAL_0:2;
then A33: intpos m3 <> DataLoc ((IExec ((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))),s) . GBP ),3 by A30, AMI_3:52, SCMP_GCD:5;
A34: (IExec (((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)),s) . (intpos 3) = (Exec ((intpos 3),0 := GBP ,6),(IExec ((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )),s)) . (intpos 3) by SCMPDS_5:46
.= m3 by A32, A18, A19, AMI_3:52, SCMPDS_2:59 ;
A35: (IExec ((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))),s) . (intpos 3) = (Exec (AddTo GBP ,5,(- 2)),(IExec (((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)),s)) . (intpos 3) by SCMPDS_5:46
.= m3 by A34, A29, AMI_3:52, SCMPDS_2:60 ;
A36: DataLoc ((IExec ((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))),s) . GBP ),3 = intpos (0 + 3) by A30, SCMP_GCD:5;
A37: (IExec (((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)),s) . (intpos 3) = (Exec (AddTo GBP ,3,1),(IExec ((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))),s)) . (intpos 3) by SCMPDS_5:46
.= m3 + 1 by A35, A36, SCMPDS_2:60 ;
A38: m3 > 2 by A5, XXREAL_0:2;
A39: m4 > 5 by A6, XXREAL_0:2;
A40: (IExec ((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )),s) . (intpos 2) = (Exec ((intpos 4),0 := (intpos 3),0 ),(Exec (GBP ,6 := (intpos 4),0 ),(Initialize s))) . (intpos 2) by SCMPDS_5:47
.= s . (intpos 2) by A25, A13, A26, AMI_3:52, SCMPDS_2:59 ;
A41: (IExec (((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)),s) . (intpos m3) = (Exec ((intpos 3),0 := GBP ,6),(IExec ((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )),s)) . (intpos m3) by SCMPDS_5:46
.= s . (intpos m4) by A19, A16, SCMPDS_2:59 ;
A42: (IExec ((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))),s) . (intpos m3) = (Exec (AddTo GBP ,5,(- 2)),(IExec (((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)),s)) . (intpos m3) by SCMPDS_5:46
.= s . (intpos m4) by A27, A41, A29, AMI_3:52, SCMPDS_2:60 ;
A43: (IExec (((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)),s) . (intpos m3) = (Exec (AddTo GBP ,3,1),(IExec ((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))),s)) . (intpos m3) by SCMPDS_5:46
.= s . (intpos m4) by A42, A33, SCMPDS_2:60 ;
A44: (IExec ((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))),s) . (intpos m4) = (Exec (AddTo GBP ,5,(- 2)),(IExec (((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)),s)) . (intpos m4) by SCMPDS_5:46
.= s . (intpos m3) by A39, A22, A29, AMI_3:52, SCMPDS_2:60 ;
A45: intpos m4 <> DataLoc ((IExec ((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))),s) . GBP ),3 by A7, A30, AMI_3:52, SCMP_GCD:5;
A46: (IExec (((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)),s) . (intpos m4) = (Exec (AddTo GBP ,3,1),(IExec ((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))),s)) . (intpos m4) by SCMPDS_5:46
.= s . (intpos m3) by A44, A45, SCMPDS_2:60 ;
A47: (IExec (((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)),s) . (intpos 2) = (Exec ((intpos 3),0 := GBP ,6),(IExec ((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )),s)) . (intpos 2) by SCMPDS_5:46
.= s . (intpos 2) by A40, A19, A38, AMI_3:52, SCMPDS_2:59 ;
A48: (IExec ((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))),s) . (intpos 2) = (Exec (AddTo GBP ,5,(- 2)),(IExec (((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)),s)) . (intpos 2) by SCMPDS_5:46
.= s . (intpos 2) by A47, A29, AMI_3:52, SCMPDS_2:60 ;
A49: intpos 2 <> DataLoc ((IExec ((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))),s) . GBP ),3 by A30, AMI_3:52, SCMP_GCD:5;
A50: (IExec (((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)),s) . (intpos 2) = (Exec (AddTo GBP ,3,1),(IExec ((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))),s)) . (intpos 2) by SCMPDS_5:46
.= s . (intpos 2) by A48, A49, SCMPDS_2:60 ;
A51: m4 > 1 by A6, XXREAL_0:2;
A52: DataLoc (s . GBP ),5 = intpos (0 + 5) by A1, SCMP_GCD:5;
(Initialize s) . (intpos 5) = s . (intpos 5) by SCMPDS_5:40;
then A53: (Exec (GBP ,6 := (intpos 4),0 ),(Initialize s)) . (intpos 5) = s . (intpos 5) by A9, AMI_3:52, SCMPDS_2:59;
A54: (IExec ((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )),s) . (intpos 5) = (Exec ((intpos 4),0 := (intpos 3),0 ),(Exec (GBP ,6 := (intpos 4),0 ),(Initialize s))) . (intpos 5) by SCMPDS_5:47
.= s . (intpos 5) by A39, A53, A13, AMI_3:52, SCMPDS_2:59 ;
A55: (IExec (((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)),s) . (intpos 5) = (Exec ((intpos 3),0 := GBP ,6),(IExec ((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )),s)) . (intpos 5) by SCMPDS_5:46
.= s . (intpos 5) by A27, A54, A19, AMI_3:52, SCMPDS_2:59 ;
A56: (IExec ((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))),s) . (intpos 5) = (Exec (AddTo GBP ,5,(- 2)),(IExec (((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)),s)) . (intpos 5) by SCMPDS_5:46
.= ((IExec (((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)),s) . (intpos 5)) + (- 2) by A29, SCMPDS_2:60
.= (s . (intpos 5)) - 2 by A55 ;
A57: intpos 5 <> DataLoc ((IExec ((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))),s) . GBP ),3 by A30, AMI_3:52, SCMP_GCD:5;
A58: (IExec (((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)),s) . (intpos 5) = (Exec (AddTo GBP ,3,1),(IExec ((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))),s)) . (intpos 5) by SCMPDS_5:46
.= (s . (intpos 5)) - 2 by A56, A57, SCMPDS_2:60 ;
(Initialize s) . (intpos 1) = s . (intpos 1) by SCMPDS_5:40;
then A59: (Exec (GBP ,6 := (intpos 4),0 ),(Initialize s)) . (intpos 1) = s . (intpos 1) by A9, AMI_3:52, SCMPDS_2:59;
A60: m3 > 1 by A5, XXREAL_0:2;
A61: (IExec (((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)),s) . GBP = (Exec (AddTo GBP ,3,1),(IExec ((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))),s)) . GBP by SCMPDS_5:46
.= 0 by A30, A31, SCMPDS_2:60 ;
then A62: GBP <> DataLoc ((IExec (((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)),s) . GBP ),4 by AMI_3:52, SCMP_GCD:5;
A63: m4 > 4 by A6, XXREAL_0:2;
then A64: intpos m4 <> DataLoc ((IExec (((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)),s) . GBP ),4 by A61, AMI_3:52, SCMP_GCD:5;
A65: m3 > 4 by A5, XXREAL_0:2;
then A66: intpos m3 <> DataLoc ((IExec (((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)),s) . GBP ),4 by A61, AMI_3:52, SCMP_GCD:5;
A67: intpos 4 <> DataLoc ((IExec ((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))),s) . GBP ),3 by A30, AMI_3:52, SCMP_GCD:5;
A68: (IExec ((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )),s) . (intpos 4) = (Exec ((intpos 4),0 := (intpos 3),0 ),(Exec (GBP ,6 := (intpos 4),0 ),(Initialize s))) . (intpos 4) by SCMPDS_5:47
.= m4 by A63, A12, A13, AMI_3:52, SCMPDS_2:59 ;
A69: (IExec (((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)),s) . (intpos 4) = (Exec ((intpos 3),0 := GBP ,6),(IExec ((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )),s)) . (intpos 4) by SCMPDS_5:46
.= m4 by A65, A68, A19, AMI_3:52, SCMPDS_2:59 ;
A70: (IExec ((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))),s) . (intpos 4) = (Exec (AddTo GBP ,5,(- 2)),(IExec (((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)),s)) . (intpos 4) by SCMPDS_5:46
.= m4 by A69, A29, AMI_3:52, SCMPDS_2:60 ;
A71: (IExec (((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)),s) . (intpos 4) = (Exec (AddTo GBP ,3,1),(IExec ((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))),s)) . (intpos 4) by SCMPDS_5:46
.= m4 by A70, A67, SCMPDS_2:60 ;
A72: intpos 3 <> DataLoc ((IExec (((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)),s) . GBP ),4 by A61, AMI_3:52, SCMP_GCD:5;
A73: (IExec ((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )),s) . (intpos 1) = (Exec ((intpos 4),0 := (intpos 3),0 ),(Exec (GBP ,6 := (intpos 4),0 ),(Initialize s))) . (intpos 1) by SCMPDS_5:47
.= s . (intpos 1) by A59, A13, A51, AMI_3:52, SCMPDS_2:59 ;
A74: (IExec (((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)),s) . (intpos 1) = (Exec ((intpos 3),0 := GBP ,6),(IExec ((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )),s)) . (intpos 1) by SCMPDS_5:46
.= s . (intpos 1) by A73, A19, A60, AMI_3:52, SCMPDS_2:59 ;
A75: (IExec ((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))),s) . (intpos 1) = (Exec (AddTo GBP ,5,(- 2)),(IExec (((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)),s)) . (intpos 1) by SCMPDS_5:46
.= s . (intpos 1) by A74, A29, AMI_3:52, SCMPDS_2:60 ;
A76: intpos 1 <> DataLoc ((IExec ((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))),s) . GBP ),3 by A30, AMI_3:52, SCMP_GCD:5;
A77: (IExec (((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)),s) . (intpos 1) = (Exec (AddTo GBP ,3,1),(IExec ((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))),s)) . (intpos 1) by SCMPDS_5:46
.= s . (intpos 1) by A75, A76, SCMPDS_2:60 ;
A78: intpos 1 <> DataLoc ((IExec (((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)),s) . GBP ),4 by A61, AMI_3:52, SCMP_GCD:5;
(IExec ((((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)) ';' (AddTo GBP ,4,(- 1))),s) . GBP = (Exec (AddTo GBP ,4,(- 1)),(IExec (((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)),s)) . GBP by SCMPDS_5:46
.= 0 by A61, A62, SCMPDS_2:60 ;
hence (IExec (if>0 GBP ,5,((((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)) ';' (AddTo GBP ,4,(- 1)))),s) . GBP = 0 by A2, A52, SCMPDS_6:97; :: thesis: ( (IExec (if>0 GBP ,5,((((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)) ';' (AddTo GBP ,4,(- 1)))),s) . (intpos 1) = s . (intpos 1) & (IExec (if>0 GBP ,5,((((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)) ';' (AddTo GBP ,4,(- 1)))),s) . (intpos 2) = s . (intpos 2) & (IExec (if>0 GBP ,5,((((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)) ';' (AddTo GBP ,4,(- 1)))),s) . (intpos m3) = s . (intpos m4) & (IExec (if>0 GBP ,5,((((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)) ';' (AddTo GBP ,4,(- 1)))),s) . (intpos m4) = s . (intpos m3) & (IExec (if>0 GBP ,5,((((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)) ';' (AddTo GBP ,4,(- 1)))),s) . (intpos 3) = (s . (intpos 3)) + 1 & (IExec (if>0 GBP ,5,((((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)) ';' (AddTo GBP ,4,(- 1)))),s) . (intpos 4) = (s . (intpos 4)) - 1 & (IExec (if>0 GBP ,5,((((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)) ';' (AddTo GBP ,4,(- 1)))),s) . (intpos 5) = (s . (intpos 5)) - 2 & ( for i being Element of NAT st i >= 8 & i <> m3 & i <> m4 holds
(IExec (if>0 GBP ,5,((((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)) ';' (AddTo GBP ,4,(- 1)))),s) . (intpos i) = s . (intpos i) ) )
(IExec ((((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)) ';' (AddTo GBP ,4,(- 1))),s) . (intpos 1) = (Exec (AddTo GBP ,4,(- 1)),(IExec (((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)),s)) . (intpos 1) by SCMPDS_5:46
.= s . (intpos 1) by A77, A78, SCMPDS_2:60 ;
hence (IExec (if>0 GBP ,5,((((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)) ';' (AddTo GBP ,4,(- 1)))),s) . (intpos 1) = s . (intpos 1) by A2, A52, SCMPDS_6:97; :: thesis: ( (IExec (if>0 GBP ,5,((((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)) ';' (AddTo GBP ,4,(- 1)))),s) . (intpos 2) = s . (intpos 2) & (IExec (if>0 GBP ,5,((((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)) ';' (AddTo GBP ,4,(- 1)))),s) . (intpos m3) = s . (intpos m4) & (IExec (if>0 GBP ,5,((((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)) ';' (AddTo GBP ,4,(- 1)))),s) . (intpos m4) = s . (intpos m3) & (IExec (if>0 GBP ,5,((((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)) ';' (AddTo GBP ,4,(- 1)))),s) . (intpos 3) = (s . (intpos 3)) + 1 & (IExec (if>0 GBP ,5,((((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)) ';' (AddTo GBP ,4,(- 1)))),s) . (intpos 4) = (s . (intpos 4)) - 1 & (IExec (if>0 GBP ,5,((((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)) ';' (AddTo GBP ,4,(- 1)))),s) . (intpos 5) = (s . (intpos 5)) - 2 & ( for i being Element of NAT st i >= 8 & i <> m3 & i <> m4 holds
(IExec (if>0 GBP ,5,((((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)) ';' (AddTo GBP ,4,(- 1)))),s) . (intpos i) = s . (intpos i) ) )
A79: intpos 2 <> DataLoc ((IExec (((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)),s) . GBP ),4 by A61, AMI_3:52, SCMP_GCD:5;
(IExec ((((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)) ';' (AddTo GBP ,4,(- 1))),s) . (intpos 2) = (Exec (AddTo GBP ,4,(- 1)),(IExec (((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)),s)) . (intpos 2) by SCMPDS_5:46
.= s . (intpos 2) by A50, A79, SCMPDS_2:60 ;
hence (IExec (if>0 GBP ,5,((((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)) ';' (AddTo GBP ,4,(- 1)))),s) . (intpos 2) = s . (intpos 2) by A2, A52, SCMPDS_6:97; :: thesis: ( (IExec (if>0 GBP ,5,((((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)) ';' (AddTo GBP ,4,(- 1)))),s) . (intpos m3) = s . (intpos m4) & (IExec (if>0 GBP ,5,((((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)) ';' (AddTo GBP ,4,(- 1)))),s) . (intpos m4) = s . (intpos m3) & (IExec (if>0 GBP ,5,((((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)) ';' (AddTo GBP ,4,(- 1)))),s) . (intpos 3) = (s . (intpos 3)) + 1 & (IExec (if>0 GBP ,5,((((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)) ';' (AddTo GBP ,4,(- 1)))),s) . (intpos 4) = (s . (intpos 4)) - 1 & (IExec (if>0 GBP ,5,((((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)) ';' (AddTo GBP ,4,(- 1)))),s) . (intpos 5) = (s . (intpos 5)) - 2 & ( for i being Element of NAT st i >= 8 & i <> m3 & i <> m4 holds
(IExec (if>0 GBP ,5,((((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)) ';' (AddTo GBP ,4,(- 1)))),s) . (intpos i) = s . (intpos i) ) )
(IExec ((((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)) ';' (AddTo GBP ,4,(- 1))),s) . (intpos m3) = (Exec (AddTo GBP ,4,(- 1)),(IExec (((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)),s)) . (intpos m3) by SCMPDS_5:46
.= s . (intpos m4) by A43, A66, SCMPDS_2:60 ;
hence (IExec (if>0 GBP ,5,((((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)) ';' (AddTo GBP ,4,(- 1)))),s) . (intpos m3) = s . (intpos m4) by A2, A52, SCMPDS_6:97; :: thesis: ( (IExec (if>0 GBP ,5,((((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)) ';' (AddTo GBP ,4,(- 1)))),s) . (intpos m4) = s . (intpos m3) & (IExec (if>0 GBP ,5,((((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)) ';' (AddTo GBP ,4,(- 1)))),s) . (intpos 3) = (s . (intpos 3)) + 1 & (IExec (if>0 GBP ,5,((((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)) ';' (AddTo GBP ,4,(- 1)))),s) . (intpos 4) = (s . (intpos 4)) - 1 & (IExec (if>0 GBP ,5,((((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)) ';' (AddTo GBP ,4,(- 1)))),s) . (intpos 5) = (s . (intpos 5)) - 2 & ( for i being Element of NAT st i >= 8 & i <> m3 & i <> m4 holds
(IExec (if>0 GBP ,5,((((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)) ';' (AddTo GBP ,4,(- 1)))),s) . (intpos i) = s . (intpos i) ) )
(IExec ((((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)) ';' (AddTo GBP ,4,(- 1))),s) . (intpos m4) = (Exec (AddTo GBP ,4,(- 1)),(IExec (((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)),s)) . (intpos m4) by SCMPDS_5:46
.= s . (intpos m3) by A46, A64, SCMPDS_2:60 ;
hence (IExec (if>0 GBP ,5,((((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)) ';' (AddTo GBP ,4,(- 1)))),s) . (intpos m4) = s . (intpos m3) by A2, A52, SCMPDS_6:97; :: thesis: ( (IExec (if>0 GBP ,5,((((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)) ';' (AddTo GBP ,4,(- 1)))),s) . (intpos 3) = (s . (intpos 3)) + 1 & (IExec (if>0 GBP ,5,((((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)) ';' (AddTo GBP ,4,(- 1)))),s) . (intpos 4) = (s . (intpos 4)) - 1 & (IExec (if>0 GBP ,5,((((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)) ';' (AddTo GBP ,4,(- 1)))),s) . (intpos 5) = (s . (intpos 5)) - 2 & ( for i being Element of NAT st i >= 8 & i <> m3 & i <> m4 holds
(IExec (if>0 GBP ,5,((((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)) ';' (AddTo GBP ,4,(- 1)))),s) . (intpos i) = s . (intpos i) ) )
A80: DataLoc ((IExec (((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)),s) . GBP ),4 = intpos (0 + 4) by A61, SCMP_GCD:5;
(IExec ((((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)) ';' (AddTo GBP ,4,(- 1))),s) . (intpos 3) = (Exec (AddTo GBP ,4,(- 1)),(IExec (((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)),s)) . (intpos 3) by SCMPDS_5:46
.= m3 + 1 by A37, A72, SCMPDS_2:60 ;
hence (IExec (if>0 GBP ,5,((((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)) ';' (AddTo GBP ,4,(- 1)))),s) . (intpos 3) = (s . (intpos 3)) + 1 by A2, A3, A52, SCMPDS_6:97; :: thesis: ( (IExec (if>0 GBP ,5,((((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)) ';' (AddTo GBP ,4,(- 1)))),s) . (intpos 4) = (s . (intpos 4)) - 1 & (IExec (if>0 GBP ,5,((((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)) ';' (AddTo GBP ,4,(- 1)))),s) . (intpos 5) = (s . (intpos 5)) - 2 & ( for i being Element of NAT st i >= 8 & i <> m3 & i <> m4 holds
(IExec (if>0 GBP ,5,((((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)) ';' (AddTo GBP ,4,(- 1)))),s) . (intpos i) = s . (intpos i) ) )
(IExec ((((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)) ';' (AddTo GBP ,4,(- 1))),s) . (intpos 4) = (Exec (AddTo GBP ,4,(- 1)),(IExec (((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)),s)) . (intpos 4) by SCMPDS_5:46
.= ((IExec (((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)),s) . (intpos 4)) + (- 1) by A80, SCMPDS_2:60
.= (s . (intpos 4)) - 1 by A4, A71 ;
hence (IExec (if>0 GBP ,5,((((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)) ';' (AddTo GBP ,4,(- 1)))),s) . (intpos 4) = (s . (intpos 4)) - 1 by A2, A52, SCMPDS_6:97; :: thesis: ( (IExec (if>0 GBP ,5,((((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)) ';' (AddTo GBP ,4,(- 1)))),s) . (intpos 5) = (s . (intpos 5)) - 2 & ( for i being Element of NAT st i >= 8 & i <> m3 & i <> m4 holds
(IExec (if>0 GBP ,5,((((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)) ';' (AddTo GBP ,4,(- 1)))),s) . (intpos i) = s . (intpos i) ) )
A81: intpos 5 <> DataLoc ((IExec (((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)),s) . GBP ),4 by A61, AMI_3:52, SCMP_GCD:5;
(IExec ((((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)) ';' (AddTo GBP ,4,(- 1))),s) . (intpos 5) = (Exec (AddTo GBP ,4,(- 1)),(IExec (((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)),s)) . (intpos 5) by SCMPDS_5:46
.= (s . (intpos 5)) - 2 by A58, A81, SCMPDS_2:60 ;
hence (IExec (if>0 GBP ,5,((((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)) ';' (AddTo GBP ,4,(- 1)))),s) . (intpos 5) = (s . (intpos 5)) - 2 by A2, A52, SCMPDS_6:97; :: thesis: for i being Element of NAT st i >= 8 & i <> m3 & i <> m4 holds
(IExec (if>0 GBP ,5,((((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)) ';' (AddTo GBP ,4,(- 1)))),s) . (intpos i) = s . (intpos i)

A82: now

let i be Element of NAT ; :: thesis: ( i >= 8 & i <> m3 & i <> m4 implies (Exec (GBP ,6 := (intpos 4),0 ),(Initialize s)) . (intpos i) = s . (intpos i) )
assume that
A83: i >= 8 and
i <> m3 and
i <> m4 ; :: thesis: (Exec (GBP ,6 := (intpos 4),0 ),(Initialize s)) . (intpos i) = s . (intpos i)
i > 6 by A83, XXREAL_0:2;
hence (Exec (GBP ,6 := (intpos 4),0 ),(Initialize s)) . (intpos i) = (Initialize s) . (intpos i) by A9, AMI_3:52, SCMPDS_2:59
.= s . (intpos i) by SCMPDS_5:40 ;
:: thesis: verum

end;

A84: now

let i be Element of NAT ; :: thesis: ( i >= 8 & i <> m3 & i <> m4 implies (IExec ((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )),s) . (intpos i) = s . (intpos i) )
assume that
A85: i >= 8 and
A86: i <> m3 and
A87: i <> m4 ; :: thesis: (IExec ((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )),s) . (intpos i) = s . (intpos i)
thus (IExec ((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )),s) . (intpos i) = (Exec ((intpos 4),0 := (intpos 3),0 ),(Exec (GBP ,6 := (intpos 4),0 ),(Initialize s))) . (intpos i) by SCMPDS_5:47
.= (Exec (GBP ,6 := (intpos 4),0 ),(Initialize s)) . (intpos i) by A13, A87, AMI_3:52, SCMPDS_2:59
.= s . (intpos i) by A82, A85, A86, A87 ; :: thesis: verum

end;

A88: now

let i be Element of NAT ; :: thesis: ( i >= 8 & i <> m3 & i <> m4 implies (IExec (((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)),s) . (intpos i) = s . (intpos i) )
assume that
A89: i >= 8 and
A90: i <> m3 and
A91: i <> m4 ; :: thesis: (IExec (((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)),s) . (intpos i) = s . (intpos i)
thus (IExec (((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)),s) . (intpos i) = (Exec ((intpos 3),0 := GBP ,6),(IExec ((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )),s)) . (intpos i) by SCMPDS_5:46
.= (IExec ((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )),s) . (intpos i) by A19, A90, AMI_3:52, SCMPDS_2:59
.= s . (intpos i) by A84, A89, A90, A91 ; :: thesis: verum

end;

A92: now

let i be Element of NAT ; :: thesis: ( i >= 8 & i <> m3 & i <> m4 implies (IExec ((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))),s) . (intpos i) = s . (intpos i) )
assume that
A93: i >= 8 and
A94: i <> m3 and
A95: i <> m4 ; :: thesis: (IExec ((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))),s) . (intpos i) = s . (intpos i)
A96: i > 5 by A93, XXREAL_0:2;
thus (IExec ((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))),s) . (intpos i) = (Exec (AddTo GBP ,5,(- 2)),(IExec (((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)),s)) . (intpos i) by SCMPDS_5:46
.= (IExec (((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)),s) . (intpos i) by A29, A96, AMI_3:52, SCMPDS_2:60
.= s . (intpos i) by A88, A93, A94, A95 ; :: thesis: verum

end;

A97: now

let i be Element of NAT ; :: thesis: ( i >= 8 & i <> m3 & i <> m4 implies (IExec (((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)),s) . (intpos i) = s . (intpos i) )
assume that
A98: i >= 8 and
A99: i <> m3 and
A100: i <> m4 ; :: thesis: (IExec (((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)),s) . (intpos i) = s . (intpos i)
i > 3 by A98, XXREAL_0:2;
then A101: intpos i <> DataLoc ((IExec ((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))),s) . GBP ),3 by A30, AMI_3:52, SCMP_GCD:5;
thus (IExec (((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)),s) . (intpos i) = (Exec (AddTo GBP ,3,1),(IExec ((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))),s)) . (intpos i) by SCMPDS_5:46
.= (IExec ((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))),s) . (intpos i) by A101, SCMPDS_2:60
.= s . (intpos i) by A92, A98, A99, A100 ; :: thesis: verum

end;

A102: now

let i be Element of NAT ; :: thesis: ( i >= 8 & i <> m3 & i <> m4 implies (IExec ((((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)) ';' (AddTo GBP ,4,(- 1))),s) . (intpos i) = s . (intpos i) )
assume that
A103: i >= 8 and
A104: i <> m3 and
A105: i <> m4 ; :: thesis: (IExec ((((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)) ';' (AddTo GBP ,4,(- 1))),s) . (intpos i) = s . (intpos i)
i > 4 by A103, XXREAL_0:2;
then A106: intpos i <> DataLoc ((IExec (((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)),s) . GBP ),4 by A61, AMI_3:52, SCMP_GCD:5;
thus (IExec ((((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)) ';' (AddTo GBP ,4,(- 1))),s) . (intpos i) = (Exec (AddTo GBP ,4,(- 1)),(IExec (((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)),s)) . (intpos i) by SCMPDS_5:46
.= (IExec (((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)),s) . (intpos i) by A106, SCMPDS_2:60
.= s . (intpos i) by A97, A103, A104, A105 ; :: thesis: verum

end;

hereby :: thesis: verum

let i be Element of NAT ; :: thesis: ( i >= 8 & i <> m3 & i <> m4 implies (IExec (if>0 GBP ,5,((((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)) ';' (AddTo GBP ,4,(- 1)))),s) . (intpos i) = s . (intpos i) )
assume that
A107: i >= 8 and
A108: i <> m3 and
A109: i <> m4 ; :: thesis: (IExec (if>0 GBP ,5,((((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)) ';' (AddTo GBP ,4,(- 1)))),s) . (intpos i) = s . (intpos i)
thus (IExec (if>0 GBP ,5,((((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)) ';' (AddTo GBP ,4,(- 1)))),s) . (intpos i) = (IExec ((((((GBP ,6 := (intpos 4),0 ) ';' ((intpos 4),0 := (intpos 3),0 )) ';' ((intpos 3),0 := GBP ,6)) ';' (AddTo GBP ,5,(- 2))) ';' (AddTo GBP ,3,1)) ';' (AddTo GBP ,4,(- 1))),s) . (intpos i) by A2, A52, SCMPDS_6:97
.= s . (intpos i) by A102, A107, A108, A109 ; :: thesis: verum

end;