let P be Instruction-Sequence of SCM+FSA; for s being State of SCM+FSA
for I being MacroInstruction of SCM+FSA
for a being read-write Int-Location st s . a <> 0 holds
while=0 (a,I) is_halting_on s,P
let s be State of SCM+FSA; for I being MacroInstruction of SCM+FSA
for a being read-write Int-Location st s . a <> 0 holds
while=0 (a,I) is_halting_on s,P
let I be MacroInstruction of SCM+FSA ; for a being read-write Int-Location st s . a <> 0 holds
while=0 (a,I) is_halting_on s,P
let a be read-write Int-Location; ( s . a <> 0 implies while=0 (a,I) is_halting_on s,P )
assume A1:
s . a <> 0
; while=0 (a,I) is_halting_on s,P
set i = a =0_goto 3;
set s1 = Initialize s;
set P1 = P +* (while=0 (a,I));
A2:
IC in dom (Start-At (0,SCM+FSA))
by MEMSTR_0:15;
A3: IC (Initialize s) =
IC (Start-At (0,SCM+FSA))
by A2, FUNCT_4:13
.=
0
by FUNCOP_1:72
;
set loc5 = (card I) + 4;
set s5 = Comput ((P +* (while=0 (a,I))),(Initialize s),3);
set s4 = Comput ((P +* (while=0 (a,I))),(Initialize s),2);
set s2 = Comput ((P +* (while=0 (a,I))),(Initialize s),1);
A4:
1 in dom (while=0 (a,I))
by SCMFSA_X:5;
not a in dom (Start-At (0,SCM+FSA))
by SCMFSA_2:102;
then A5:
(Initialize s) . a = s . a
by FUNCT_4:11;
A6:
(P +* (while=0 (a,I))) /. (IC (Initialize s)) = (P +* (while=0 (a,I))) . (IC (Initialize s))
by PBOOLE:143;
0 in dom (while=0 (a,I))
by AFINSQ_1:65;
then (P +* (while=0 (a,I))) . 0 =
(while=0 (a,I)) . 0
by FUNCT_4:13
.=
a =0_goto 3
by SCMFSA_X:10
;
then A7:
CurInstr ((P +* (while=0 (a,I))),(Initialize s)) = a =0_goto 3
by A3, A6;
A8: Comput ((P +* (while=0 (a,I))),(Initialize s),(0 + 1)) =
Following ((P +* (while=0 (a,I))),(Comput ((P +* (while=0 (a,I))),(Initialize s),0)))
by EXTPRO_1:3
.=
Exec ((a =0_goto 3),(Initialize s))
by A7
;
A9:
IC (Comput ((P +* (while=0 (a,I))),(Initialize s),1)) = 0 + 1
by A1, A3, A8, A5, SCMFSA_2:70;
A10:
(P +* (while=0 (a,I))) /. (IC (Comput ((P +* (while=0 (a,I))),(Initialize s),1))) = (P +* (while=0 (a,I))) . (IC (Comput ((P +* (while=0 (a,I))),(Initialize s),1)))
by PBOOLE:143;
(P +* (while=0 (a,I))) . 1 =
(while=0 (a,I)) . 1
by A4, FUNCT_4:13
.=
goto 2
by SCMFSA_X:10
;
then A11:
CurInstr ((P +* (while=0 (a,I))),(Comput ((P +* (while=0 (a,I))),(Initialize s),1))) = goto 2
by A9, A10;
A12: Comput ((P +* (while=0 (a,I))),(Initialize s),(1 + 1)) =
Following ((P +* (while=0 (a,I))),(Comput ((P +* (while=0 (a,I))),(Initialize s),1)))
by EXTPRO_1:3
.=
Exec ((goto 2),(Comput ((P +* (while=0 (a,I))),(Initialize s),1)))
by A11
;
A13:
IC (Comput ((P +* (while=0 (a,I))),(Initialize s),2)) = 2
by A12, SCMFSA_2:69;
A14:
2 in dom (while=0 (a,I))
by SCMFSA_X:5;
A15:
(card I) + 4 in dom (while=0 (a,I))
by SCMFSA_X:6;
A16:
(P +* (while=0 (a,I))) /. (IC (Comput ((P +* (while=0 (a,I))),(Initialize s),2))) = (P +* (while=0 (a,I))) . (IC (Comput ((P +* (while=0 (a,I))),(Initialize s),2)))
by PBOOLE:143;
(P +* (while=0 (a,I))) . 2 =
(while=0 (a,I)) . 2
by A14, FUNCT_4:13
.=
goto ((card I) + 4)
by SCMFSA_X:12
;
then A17:
CurInstr ((P +* (while=0 (a,I))),(Comput ((P +* (while=0 (a,I))),(Initialize s),2))) = goto ((card I) + 4)
by A13, A16;
A18: Comput ((P +* (while=0 (a,I))),(Initialize s),(2 + 1)) =
Following ((P +* (while=0 (a,I))),(Comput ((P +* (while=0 (a,I))),(Initialize s),2)))
by EXTPRO_1:3
.=
Exec ((goto ((card I) + 4)),(Comput ((P +* (while=0 (a,I))),(Initialize s),2)))
by A17
;
A19:
IC (Comput ((P +* (while=0 (a,I))),(Initialize s),3)) = (card I) + 4
by A18, SCMFSA_2:69;
A20:
(P +* (while=0 (a,I))) /. (IC (Comput ((P +* (while=0 (a,I))),(Initialize s),3))) = (P +* (while=0 (a,I))) . (IC (Comput ((P +* (while=0 (a,I))),(Initialize s),3)))
by PBOOLE:143;
(P +* (while=0 (a,I))) . ((card I) + 4) =
(while=0 (a,I)) . ((card I) + 4)
by A15, FUNCT_4:13
.=
halt SCM+FSA
by SCMFSA_X:11
;
then
CurInstr ((P +* (while=0 (a,I))),(Comput ((P +* (while=0 (a,I))),(Initialize s),3))) = halt SCM+FSA
by A19, A20;
then
P +* (while=0 (a,I)) halts_on Initialize s
by EXTPRO_1:29;
hence
while=0 (a,I) is_halting_on s,P
by SCMFSA7B:def 7; verum
thus
verum
; verum