let s be State of SCM+FSA ; :: thesis: for a being read-write Int-Location
for bb, cc being Int-Location
for Ig being good Program of SCM+FSA
for k being Element of NAT st ((StepForUp a,bb,cc,Ig,s) . k) . (intloc 0 ) = 1 & Ig is_closed_on (StepForUp a,bb,cc,Ig,s) . k & Ig is_halting_on (StepForUp a,bb,cc,Ig,s) . k holds
((StepForUp a,bb,cc,Ig,s) . (k + 1)) . (intloc 0 ) = 1
let a be read-write Int-Location ; :: thesis: for bb, cc being Int-Location
for Ig being good Program of SCM+FSA
for k being Element of NAT st ((StepForUp a,bb,cc,Ig,s) . k) . (intloc 0 ) = 1 & Ig is_closed_on (StepForUp a,bb,cc,Ig,s) . k & Ig is_halting_on (StepForUp a,bb,cc,Ig,s) . k holds
((StepForUp a,bb,cc,Ig,s) . (k + 1)) . (intloc 0 ) = 1
let bb, cc be Int-Location ; :: thesis: for Ig being good Program of SCM+FSA
for k being Element of NAT st ((StepForUp a,bb,cc,Ig,s) . k) . (intloc 0 ) = 1 & Ig is_closed_on (StepForUp a,bb,cc,Ig,s) . k & Ig is_halting_on (StepForUp a,bb,cc,Ig,s) . k holds
((StepForUp a,bb,cc,Ig,s) . (k + 1)) . (intloc 0 ) = 1
let Ig be good Program of SCM+FSA ; :: thesis: for k being Element of NAT st ((StepForUp a,bb,cc,Ig,s) . k) . (intloc 0 ) = 1 & Ig is_closed_on (StepForUp a,bb,cc,Ig,s) . k & Ig is_halting_on (StepForUp a,bb,cc,Ig,s) . k holds
((StepForUp a,bb,cc,Ig,s) . (k + 1)) . (intloc 0 ) = 1
let k be Element of NAT ; :: thesis: ( ((StepForUp a,bb,cc,Ig,s) . k) . (intloc 0 ) = 1 & Ig is_closed_on (StepForUp a,bb,cc,Ig,s) . k & Ig is_halting_on (StepForUp a,bb,cc,Ig,s) . k implies ((StepForUp a,bb,cc,Ig,s) . (k + 1)) . (intloc 0 ) = 1 )
set D = Int-Locations \/ FinSeq-Locations ;
set I = Ig;
assume that
A1:
((StepForUp a,bb,cc,Ig,s) . k) . (intloc 0 ) = 1
and
A2:
Ig is_closed_on (StepForUp a,bb,cc,Ig,s) . k
and
A3:
Ig is_halting_on (StepForUp a,bb,cc,Ig,s) . k
; :: thesis: ((StepForUp a,bb,cc,Ig,s) . (k + 1)) . (intloc 0 ) = 1
set aux = 1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig));
set IB = (Ig ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0 ));
set SW2 = StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),((Ig ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0 ))),((s +* (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(((s . cc) - (s . bb)) + 1)) +* a,(s . bb));
A4:
(Ig ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0 )) = Ig ';' ((AddTo a,(intloc 0 )) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0 )))
by SCMFSA6A:70;
per cases
( ((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),((Ig ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0 ))),((s +* (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(((s . cc) - (s . bb)) + 1)) +* a,(s . bb))) . k) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))) <= 0 or ((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),((Ig ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0 ))),((s +* (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(((s . cc) - (s . bb)) + 1)) +* a,(s . bb))) . k) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))) > 0 )
;
suppose
((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),((Ig ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0 ))),((s +* (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(((s . cc) - (s . bb)) + 1)) +* a,(s . bb))) . k) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))) <= 0
;
:: thesis: ((StepForUp a,bb,cc,Ig,s) . (k + 1)) . (intloc 0 ) = 1then
DataPart ((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),((Ig ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0 ))),((s +* (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(((s . cc) - (s . bb)) + 1)) +* a,(s . bb))) . (k + 1)) = DataPart ((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),((Ig ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0 ))),((s +* (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(((s . cc) - (s . bb)) + 1)) +* a,(s . bb))) . k)
by SCMFSA9A:37;
hence
((StepForUp a,bb,cc,Ig,s) . (k + 1)) . (intloc 0 ) = 1
by A1, SCMFSA6A:38;
:: thesis: verum end; suppose A5:
((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),((Ig ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0 ))),((s +* (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(((s . cc) - (s . bb)) + 1)) +* a,(s . bb))) . k) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))) > 0
;
:: thesis: ((StepForUp a,bb,cc,Ig,s) . (k + 1)) . (intloc 0 ) = 1A6:
Ig is_closed_on Initialize ((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),((Ig ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0 ))),((s +* (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(((s . cc) - (s . bb)) + 1)) +* a,(s . bb))) . k)
by A1, A2, SFMASTR2:4;
A7:
Ig is_halting_on Initialize ((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),((Ig ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0 ))),((s +* (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(((s . cc) - (s . bb)) + 1)) +* a,(s . bb))) . k)
by A1, A2, A3, SFMASTR2:5;
A8:
(AddTo a,(intloc 0 )) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0 )) is_closed_on IExec Ig,
((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),((Ig ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0 ))),((s +* (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(((s . cc) - (s . bb)) + 1)) +* a,(s . bb))) . k)
by SCMFSA7B:24;
A9:
(AddTo a,(intloc 0 )) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0 )) is_halting_on IExec Ig,
((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),((Ig ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0 ))),((s +* (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(((s . cc) - (s . bb)) + 1)) +* a,(s . bb))) . k)
by SCMFSA7B:25;
A10:
(Ig ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0 )) is_closed_on Initialize ((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),((Ig ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0 ))),((s +* (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(((s . cc) - (s . bb)) + 1)) +* a,(s . bb))) . k)
by A4, A6, A7, A8, SFMASTR1:3;
A11:
DataPart ((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),((Ig ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0 ))),((s +* (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(((s . cc) - (s . bb)) + 1)) +* a,(s . bb))) . (k + 1)) = DataPart (IExec ((Ig ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0 ))),((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),((Ig ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0 ))),((s +* (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(((s . cc) - (s . bb)) + 1)) +* a,(s . bb))) . k))
by A1, A5, A10, A4, A6, A7, A8, A9, SCMFSA9A:38, SFMASTR1:4;
(IExec ((Ig ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0 ))),((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),((Ig ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0 ))),((s +* (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(((s . cc) - (s . bb)) + 1)) +* a,(s . bb))) . k)) . (intloc 0 ) =
(IExec ((AddTo a,(intloc 0 )) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0 ))),(IExec Ig,((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),((Ig ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0 ))),((s +* (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(((s . cc) - (s . bb)) + 1)) +* a,(s . bb))) . k))) . (intloc 0 )
by A4, A6, A7, SFMASTR1:8
.=
(Exec (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0 )),(Exec (AddTo a,(intloc 0 )),(Initialize (IExec Ig,((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),((Ig ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0 ))),((s +* (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(((s . cc) - (s . bb)) + 1)) +* a,(s . bb))) . k))))) . (intloc 0 )
by SCMFSA6C:9
.=
(Exec (AddTo a,(intloc 0 )),(Initialize (IExec Ig,((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),((Ig ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0 ))),((s +* (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(((s . cc) - (s . bb)) + 1)) +* a,(s . bb))) . k)))) . (intloc 0 )
by SCMFSA_2:91
.=
(Initialize (IExec Ig,((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),((Ig ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0 ))),((s +* (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(((s . cc) - (s . bb)) + 1)) +* a,(s . bb))) . k))) . (intloc 0 )
by SCMFSA_2:90
.=
1
by SCMFSA6C:3
;
hence
((StepForUp a,bb,cc,Ig,s) . (k + 1)) . (intloc 0 ) = 1
by A11, SCMFSA6A:38;
:: thesis: verum end;