let s be State of SCMPDS ; ( s . (intpos 1) > 0 & s . (intpos 2) > 0 implies ( (IExec ((((GBP := 0 ) ';' (GBP ,3 := GBP ,1)) ';' (SubFrom GBP ,3,GBP ,2)) ';' (while<>0 GBP ,3,(((if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))) ';' (GBP ,3 := GBP ,1)) ';' (SubFrom GBP ,3,GBP ,2)))),s) . (intpos 1) = (s . (intpos 1)) gcd (s . (intpos 2)) & (IExec ((((GBP := 0 ) ';' (GBP ,3 := GBP ,1)) ';' (SubFrom GBP ,3,GBP ,2)) ';' (while<>0 GBP ,3,(((if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))) ';' (GBP ,3 := GBP ,1)) ';' (SubFrom GBP ,3,GBP ,2)))),s) . (intpos 2) = (s . (intpos 1)) gcd (s . (intpos 2)) & (((GBP := 0 ) ';' (GBP ,3 := GBP ,1)) ';' (SubFrom GBP ,3,GBP ,2)) ';' (while<>0 GBP ,3,(((if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))) ';' (GBP ,3 := GBP ,1)) ';' (SubFrom GBP ,3,GBP ,2))) is_closed_on s & (((GBP := 0 ) ';' (GBP ,3 := GBP ,1)) ';' (SubFrom GBP ,3,GBP ,2)) ';' (while<>0 GBP ,3,(((if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))) ';' (GBP ,3 := GBP ,1)) ';' (SubFrom GBP ,3,GBP ,2))) is_halting_on s ) )
assume A1:
( s . (intpos 1) > 0 & s . (intpos 2) > 0 )
; ( (IExec ((((GBP := 0 ) ';' (GBP ,3 := GBP ,1)) ';' (SubFrom GBP ,3,GBP ,2)) ';' (while<>0 GBP ,3,(((if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))) ';' (GBP ,3 := GBP ,1)) ';' (SubFrom GBP ,3,GBP ,2)))),s) . (intpos 1) = (s . (intpos 1)) gcd (s . (intpos 2)) & (IExec ((((GBP := 0 ) ';' (GBP ,3 := GBP ,1)) ';' (SubFrom GBP ,3,GBP ,2)) ';' (while<>0 GBP ,3,(((if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))) ';' (GBP ,3 := GBP ,1)) ';' (SubFrom GBP ,3,GBP ,2)))),s) . (intpos 2) = (s . (intpos 1)) gcd (s . (intpos 2)) & (((GBP := 0 ) ';' (GBP ,3 := GBP ,1)) ';' (SubFrom GBP ,3,GBP ,2)) ';' (while<>0 GBP ,3,(((if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))) ';' (GBP ,3 := GBP ,1)) ';' (SubFrom GBP ,3,GBP ,2))) is_closed_on s & (((GBP := 0 ) ';' (GBP ,3 := GBP ,1)) ';' (SubFrom GBP ,3,GBP ,2)) ';' (while<>0 GBP ,3,(((if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))) ';' (GBP ,3 := GBP ,1)) ';' (SubFrom GBP ,3,GBP ,2))) is_halting_on s )
set t0 = Initialize s;
set t1 = IExec (((GBP := 0 ) ';' (GBP ,3 := GBP ,1)) ';' (SubFrom GBP ,3,GBP ,2)),s;
set t2 = IExec ((GBP := 0 ) ';' (GBP ,3 := GBP ,1)),s;
set t3 = Exec (GBP := 0 ),(Initialize s);
set a = GBP ;
A2: (Exec (GBP := 0 ),(Initialize s)) . (intpos 1) =
(Initialize s) . (intpos 1)
by AMI_3:52, SCMPDS_2:57
.=
s . (intpos 1)
by SCMPDS_5:40
;
A3:
(Exec (GBP := 0 ),(Initialize s)) . GBP = 0
by SCMPDS_2:57;
then A4:
DataLoc ((Exec (GBP := 0 ),(Initialize s)) . GBP ),3 = intpos (0 + 3)
by SCMP_GCD:5;
1 <> abs (((Exec (GBP := 0 ),(Initialize s)) . GBP ) + 3)
by A3, ABSVALUE:def 1;
then A5:
intpos 1 <> DataLoc ((Exec (GBP := 0 ),(Initialize s)) . GBP ),3
by ZFMISC_1:33;
A6: (IExec ((GBP := 0 ) ';' (GBP ,3 := GBP ,1)),s) . (intpos 1) =
(Exec (GBP ,3 := GBP ,1),(Exec (GBP := 0 ),(Initialize s))) . (intpos 1)
by SCMPDS_5:47
.=
s . (intpos 1)
by A2, A5, SCMPDS_2:59
;
A7: (Exec (GBP := 0 ),(Initialize s)) . (intpos 2) =
(Initialize s) . (intpos 2)
by AMI_3:52, SCMPDS_2:57
.=
s . (intpos 2)
by SCMPDS_5:40
;
A8: (IExec ((GBP := 0 ) ';' (GBP ,3 := GBP ,1)),s) . (intpos 3) =
(Exec (GBP ,3 := GBP ,1),(Exec (GBP := 0 ),(Initialize s))) . (intpos 3)
by SCMPDS_5:47
.=
(Exec (GBP := 0 ),(Initialize s)) . (DataLoc ((Exec (GBP := 0 ),(Initialize s)) . GBP ),1)
by A4, SCMPDS_2:59
.=
s . (intpos 1)
by A3, A2, SCMP_GCD:5
;
2 <> abs (((Exec (GBP := 0 ),(Initialize s)) . GBP ) + 3)
by A3, ABSVALUE:def 1;
then A9:
intpos 2 <> DataLoc ((Exec (GBP := 0 ),(Initialize s)) . GBP ),3
by ZFMISC_1:33;
A10: (IExec ((GBP := 0 ) ';' (GBP ,3 := GBP ,1)),s) . (intpos 2) =
(Exec (GBP ,3 := GBP ,1),(Exec (GBP := 0 ),(Initialize s))) . (intpos 2)
by SCMPDS_5:47
.=
s . (intpos 2)
by A7, A9, SCMPDS_2:59
;
0 <> abs (((Exec (GBP := 0 ),(Initialize s)) . GBP ) + 3)
by A3, ABSVALUE:def 1;
then A11:
GBP <> DataLoc ((Exec (GBP := 0 ),(Initialize s)) . GBP ),3
by ZFMISC_1:33;
A12: (IExec ((GBP := 0 ) ';' (GBP ,3 := GBP ,1)),s) . GBP =
(Exec (GBP ,3 := GBP ,1),(Exec (GBP := 0 ),(Initialize s))) . GBP
by SCMPDS_5:47
.=
0
by A3, A11, SCMPDS_2:59
;
then A13:
DataLoc ((IExec ((GBP := 0 ) ';' (GBP ,3 := GBP ,1)),s) . GBP ),3 = intpos (0 + 3)
by SCMP_GCD:5;
0 <> abs (((IExec ((GBP := 0 ) ';' (GBP ,3 := GBP ,1)),s) . GBP ) + 3)
by A12, ABSVALUE:def 1;
then A14:
GBP <> DataLoc ((IExec ((GBP := 0 ) ';' (GBP ,3 := GBP ,1)),s) . GBP ),3
by ZFMISC_1:33;
A15: (IExec (((GBP := 0 ) ';' (GBP ,3 := GBP ,1)) ';' (SubFrom GBP ,3,GBP ,2)),s) . GBP =
(Exec (SubFrom GBP ,3,GBP ,2),(IExec ((GBP := 0 ) ';' (GBP ,3 := GBP ,1)),s)) . GBP
by SCMPDS_5:46
.=
0
by A12, A14, SCMPDS_2:62
;
1 <> abs (((IExec ((GBP := 0 ) ';' (GBP ,3 := GBP ,1)),s) . GBP ) + 3)
by A12, ABSVALUE:def 1;
then A16:
intpos 1 <> DataLoc ((IExec ((GBP := 0 ) ';' (GBP ,3 := GBP ,1)),s) . GBP ),3
by ZFMISC_1:33;
A17: (IExec (((GBP := 0 ) ';' (GBP ,3 := GBP ,1)) ';' (SubFrom GBP ,3,GBP ,2)),s) . (intpos 1) =
(Exec (SubFrom GBP ,3,GBP ,2),(IExec ((GBP := 0 ) ';' (GBP ,3 := GBP ,1)),s)) . (intpos 1)
by SCMPDS_5:46
.=
s . (intpos 1)
by A6, A16, SCMPDS_2:62
;
2 <> abs (((IExec ((GBP := 0 ) ';' (GBP ,3 := GBP ,1)),s) . GBP ) + 3)
by A12, ABSVALUE:def 1;
then A18:
intpos 2 <> DataLoc ((IExec ((GBP := 0 ) ';' (GBP ,3 := GBP ,1)),s) . GBP ),3
by ZFMISC_1:33;
A19: (IExec (((GBP := 0 ) ';' (GBP ,3 := GBP ,1)) ';' (SubFrom GBP ,3,GBP ,2)),s) . (intpos 2) =
(Exec (SubFrom GBP ,3,GBP ,2),(IExec ((GBP := 0 ) ';' (GBP ,3 := GBP ,1)),s)) . (intpos 2)
by SCMPDS_5:46
.=
s . (intpos 2)
by A10, A18, SCMPDS_2:62
;
A20: (IExec (((GBP := 0 ) ';' (GBP ,3 := GBP ,1)) ';' (SubFrom GBP ,3,GBP ,2)),s) . (intpos 3) =
(Exec (SubFrom GBP ,3,GBP ,2),(IExec ((GBP := 0 ) ';' (GBP ,3 := GBP ,1)),s)) . (intpos 3)
by SCMPDS_5:46
.=
((IExec ((GBP := 0 ) ';' (GBP ,3 := GBP ,1)),s) . (intpos 3)) - ((IExec ((GBP := 0 ) ';' (GBP ,3 := GBP ,1)),s) . (DataLoc ((IExec ((GBP := 0 ) ';' (GBP ,3 := GBP ,1)),s) . GBP ),2))
by A13, SCMPDS_2:62
.=
((IExec (((GBP := 0 ) ';' (GBP ,3 := GBP ,1)) ';' (SubFrom GBP ,3,GBP ,2)),s) . (intpos 1)) - ((IExec (((GBP := 0 ) ';' (GBP ,3 := GBP ,1)) ';' (SubFrom GBP ,3,GBP ,2)),s) . (intpos 2))
by A12, A10, A8, A17, A19, SCMP_GCD:5
;
then A21:
( while<>0 GBP ,3,(((if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))) ';' (GBP ,3 := GBP ,1)) ';' (SubFrom GBP ,3,GBP ,2)) is_closed_on IExec (((GBP := 0 ) ';' (GBP ,3 := GBP ,1)) ';' (SubFrom GBP ,3,GBP ,2)),s & while<>0 GBP ,3,(((if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))) ';' (GBP ,3 := GBP ,1)) ';' (SubFrom GBP ,3,GBP ,2)) is_halting_on IExec (((GBP := 0 ) ';' (GBP ,3 := GBP ,1)) ';' (SubFrom GBP ,3,GBP ,2)),s )
by A1, A15, A17, A19, Lm15;
(IExec (while<>0 GBP ,3,(((if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))) ';' (GBP ,3 := GBP ,1)) ';' (SubFrom GBP ,3,GBP ,2))),(IExec (((GBP := 0 ) ';' (GBP ,3 := GBP ,1)) ';' (SubFrom GBP ,3,GBP ,2)),s)) . (intpos 1) = ((IExec (((GBP := 0 ) ';' (GBP ,3 := GBP ,1)) ';' (SubFrom GBP ,3,GBP ,2)),s) . (intpos 1)) gcd ((IExec (((GBP := 0 ) ';' (GBP ,3 := GBP ,1)) ';' (SubFrom GBP ,3,GBP ,2)),s) . (intpos 2))
by A1, A15, A17, A19, A20, Lm15;
hence
(IExec ((((GBP := 0 ) ';' (GBP ,3 := GBP ,1)) ';' (SubFrom GBP ,3,GBP ,2)) ';' (while<>0 GBP ,3,(((if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))) ';' (GBP ,3 := GBP ,1)) ';' (SubFrom GBP ,3,GBP ,2)))),s) . (intpos 1) = (s . (intpos 1)) gcd (s . (intpos 2))
by A17, A19, A21, SCPISORT:8; ( (IExec ((((GBP := 0 ) ';' (GBP ,3 := GBP ,1)) ';' (SubFrom GBP ,3,GBP ,2)) ';' (while<>0 GBP ,3,(((if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))) ';' (GBP ,3 := GBP ,1)) ';' (SubFrom GBP ,3,GBP ,2)))),s) . (intpos 2) = (s . (intpos 1)) gcd (s . (intpos 2)) & (((GBP := 0 ) ';' (GBP ,3 := GBP ,1)) ';' (SubFrom GBP ,3,GBP ,2)) ';' (while<>0 GBP ,3,(((if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))) ';' (GBP ,3 := GBP ,1)) ';' (SubFrom GBP ,3,GBP ,2))) is_closed_on s & (((GBP := 0 ) ';' (GBP ,3 := GBP ,1)) ';' (SubFrom GBP ,3,GBP ,2)) ';' (while<>0 GBP ,3,(((if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))) ';' (GBP ,3 := GBP ,1)) ';' (SubFrom GBP ,3,GBP ,2))) is_halting_on s )
(IExec (while<>0 GBP ,3,(((if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))) ';' (GBP ,3 := GBP ,1)) ';' (SubFrom GBP ,3,GBP ,2))),(IExec (((GBP := 0 ) ';' (GBP ,3 := GBP ,1)) ';' (SubFrom GBP ,3,GBP ,2)),s)) . (intpos 2) = ((IExec (((GBP := 0 ) ';' (GBP ,3 := GBP ,1)) ';' (SubFrom GBP ,3,GBP ,2)),s) . (intpos 1)) gcd ((IExec (((GBP := 0 ) ';' (GBP ,3 := GBP ,1)) ';' (SubFrom GBP ,3,GBP ,2)),s) . (intpos 2))
by A1, A15, A17, A19, A20, Lm15;
hence
(IExec ((((GBP := 0 ) ';' (GBP ,3 := GBP ,1)) ';' (SubFrom GBP ,3,GBP ,2)) ';' (while<>0 GBP ,3,(((if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))) ';' (GBP ,3 := GBP ,1)) ';' (SubFrom GBP ,3,GBP ,2)))),s) . (intpos 2) = (s . (intpos 1)) gcd (s . (intpos 2))
by A17, A19, A21, SCPISORT:8; ( (((GBP := 0 ) ';' (GBP ,3 := GBP ,1)) ';' (SubFrom GBP ,3,GBP ,2)) ';' (while<>0 GBP ,3,(((if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))) ';' (GBP ,3 := GBP ,1)) ';' (SubFrom GBP ,3,GBP ,2))) is_closed_on s & (((GBP := 0 ) ';' (GBP ,3 := GBP ,1)) ';' (SubFrom GBP ,3,GBP ,2)) ';' (while<>0 GBP ,3,(((if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))) ';' (GBP ,3 := GBP ,1)) ';' (SubFrom GBP ,3,GBP ,2))) is_halting_on s )
thus
( (((GBP := 0 ) ';' (GBP ,3 := GBP ,1)) ';' (SubFrom GBP ,3,GBP ,2)) ';' (while<>0 GBP ,3,(((if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))) ';' (GBP ,3 := GBP ,1)) ';' (SubFrom GBP ,3,GBP ,2))) is_closed_on s & (((GBP := 0 ) ';' (GBP ,3 := GBP ,1)) ';' (SubFrom GBP ,3,GBP ,2)) ';' (while<>0 GBP ,3,(((if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))) ';' (GBP ,3 := GBP ,1)) ';' (SubFrom GBP ,3,GBP ,2))) is_halting_on s )
by A21, SCPISORT:10; verum