set J = Stop SCM+FSA;
let a be Int-Location ; :: thesis: for I being Program of SCM+FSA holds (while>0 (a,I)) . 3 = goto ((card I) + 5)
let I be Program of SCM+FSA; :: thesis: (while>0 (a,I)) . 3 = goto ((card I) + 5)
set I1 = I ';' (Goto 0);
set f = ((card I) + 4) .--> (goto 0);
set i = a >0_goto ((card (Stop SCM+FSA)) + 3);
set Mi = (Macro (a >0_goto ((card (Stop SCM+FSA)) + 3))) ';' (Stop SCM+FSA);
set G = Goto ((card (I ';' (Goto 0))) + 1);
set J2 = (I ';' (Goto 0)) ';' (Stop SCM+FSA);
set J1 = (Goto ((card (I ';' (Goto 0))) + 1)) ';' ((I ';' (Goto 0)) ';' (Stop SCM+FSA));
A1: 0 in dom (Goto ((card (I ';' (Goto 0))) + 1)) by SCMFSA8A:47;
A2: (Goto ((card (I ';' (Goto 0))) + 1)) . 0 = goto ((card (I ';' (Goto 0))) + 1) by SCMFSA8A:47
.= goto (((card I) + (card (Goto 0))) + 1) by SCMFSA6A:61
.= goto (((card I) + 1) + 1) by SCMFSA8A:29
.= goto ((card I) + (1 + 1)) ;
then A3: (Goto ((card (I ';' (Goto 0))) + 1)) . 0 <> halt SCM+FSA by SCMFSA_2:47, SCMFSA_2:124;
dom ((Goto ((card (I ';' (Goto 0))) + 1)) ';' ((I ';' (Goto 0)) ';' (Stop SCM+FSA))) = (dom (Directed (Goto ((card (I ';' (Goto 0))) + 1)))) \/ (dom (ProgramPart (Relocated (((I ';' (Goto 0)) ';' (Stop SCM+FSA)),(card (Goto ((card (I ';' (Goto 0))) + 1))))))) by FUNCT_4:def 1
.= (dom (Goto ((card (I ';' (Goto 0))) + 1))) \/ (dom (ProgramPart (Relocated (((I ';' (Goto 0)) ';' (Stop SCM+FSA)),(card (Goto ((card (I ';' (Goto 0))) + 1))))))) by FUNCT_4:105 ;
then A4: 0 in dom ((Goto ((card (I ';' (Goto 0))) + 1)) ';' ((I ';' (Goto 0)) ';' (Stop SCM+FSA))) by A1, XBOOLE_0:def 3;
then 0 + 3 in { (il + 3) where il is Element of NAT : il in dom ((Goto ((card (I ';' (Goto 0))) + 1)) ';' ((I ';' (Goto 0)) ';' (Stop SCM+FSA))) } ;
then A5: 3 in dom (Shift (((Goto ((card (I ';' (Goto 0))) + 1)) ';' ((I ';' (Goto 0)) ';' (Stop SCM+FSA))),3)) by VALUED_1:def 12;
then A6: (Shift (((Goto ((card (I ';' (Goto 0))) + 1)) ';' ((I ';' (Goto 0)) ';' (Stop SCM+FSA))),3)) /. 3 = (Shift (((Goto ((card (I ';' (Goto 0))) + 1)) ';' ((I ';' (Goto 0)) ';' (Stop SCM+FSA))),3)) . (0 + 3) by PARTFUN1:def 8
.= ((Goto ((card (I ';' (Goto 0))) + 1)) ';' ((I ';' (Goto 0)) ';' (Stop SCM+FSA))) . 0 by A4, VALUED_1:def 12
.= (Directed (Goto ((card (I ';' (Goto 0))) + 1))) . 0 by A1, SCMFSA8A:28
.= goto ((card I) + 2) by A1, A2, A3, SCMFSA8A:30 ;
( dom (((card I) + 4) .--> (goto 0)) = {((card I) + 4)} & 3 <> (card I) + 4 ) by FUNCOP_1:19, NAT_1:11;
then A7: not 3 in dom (((card I) + 4) .--> (goto 0)) by TARSKI:def 1;
A8: card ((Macro (a >0_goto ((card (Stop SCM+FSA)) + 3))) ';' (Stop SCM+FSA)) = (card (Macro (a >0_goto ((card (Stop SCM+FSA)) + 3)))) + (card (Stop SCM+FSA)) by SCMFSA6A:61
.= 2 + 1 by LL, COMPOS_1:150 ;
then A9: not 3 in dom ((Macro (a >0_goto ((card (Stop SCM+FSA)) + 3))) ';' (Stop SCM+FSA)) ;
A10: ( 3 in dom (while>0 (a,I)) & dom (while>0 (a,I)) = (dom (if>0 (a,(I ';' (Goto 0)),(Stop SCM+FSA)))) \/ (dom (((card I) + 4) .--> (goto 0))) ) by Th37, FUNCT_4:def 1;
then A11: 3 in dom (if>0 (a,(I ';' (Goto 0)),(Stop SCM+FSA))) by A7, XBOOLE_0:def 3;
A12: if>0 (a,(I ';' (Goto 0)),(Stop SCM+FSA)) = ((((a >0_goto ((card (Stop SCM+FSA)) + 3)) ';' (Stop SCM+FSA)) ';' (Goto ((card (I ';' (Goto 0))) + 1))) ';' (I ';' (Goto 0))) ';' (Stop SCM+FSA) by SCMFSA8B:def 2
.= (((a >0_goto ((card (Stop SCM+FSA)) + 3)) ';' (Stop SCM+FSA)) ';' (Goto ((card (I ';' (Goto 0))) + 1))) ';' ((I ';' (Goto 0)) ';' (Stop SCM+FSA)) by SCMFSA6A:67
.= ((Macro (a >0_goto ((card (Stop SCM+FSA)) + 3))) ';' (Stop SCM+FSA)) ';' ((Goto ((card (I ';' (Goto 0))) + 1)) ';' ((I ';' (Goto 0)) ';' (Stop SCM+FSA))) by SCMFSA6A:67
.= (Directed ((Macro (a >0_goto ((card (Stop SCM+FSA)) + 3))) ';' (Stop SCM+FSA))) +* (ProgramPart (Relocated (((Goto ((card (I ';' (Goto 0))) + 1)) ';' ((I ';' (Goto 0)) ';' (Stop SCM+FSA))),3))) by A8 ;
then A13: dom (if>0 (a,(I ';' (Goto 0)),(Stop SCM+FSA))) = (dom (Directed ((Macro (a >0_goto ((card (Stop SCM+FSA)) + 3))) ';' (Stop SCM+FSA)))) \/ (dom (ProgramPart (Relocated (((Goto ((card (I ';' (Goto 0))) + 1)) ';' ((I ';' (Goto 0)) ';' (Stop SCM+FSA))),3)))) by FUNCT_4:def 1;
then dom (if>0 (a,(I ';' (Goto 0)),(Stop SCM+FSA))) = (dom ((Macro (a >0_goto ((card (Stop SCM+FSA)) + 3))) ';' (Stop SCM+FSA))) \/ (dom (ProgramPart (Relocated (((Goto ((card (I ';' (Goto 0))) + 1)) ';' ((I ';' (Goto 0)) ';' (Stop SCM+FSA))),3)))) by FUNCT_4:105;
then A14: 3 in dom (ProgramPart (Relocated (((Goto ((card (I ';' (Goto 0))) + 1)) ';' ((I ';' (Goto 0)) ';' (Stop SCM+FSA))),3))) by A11, A9, XBOOLE_0:def 3;
thus (while>0 (a,I)) . 3 = ((Directed ((Macro (a >0_goto ((card (Stop SCM+FSA)) + 3))) ';' (Stop SCM+FSA))) +* (ProgramPart (Relocated (((Goto ((card (I ';' (Goto 0))) + 1)) ';' ((I ';' (Goto 0)) ';' (Stop SCM+FSA))),3)))) . 3 by A7, A10, A12, FUNCT_4:def 1
.= (ProgramPart (Relocated (((Goto ((card (I ';' (Goto 0))) + 1)) ';' ((I ';' (Goto 0)) ';' (Stop SCM+FSA))),3))) . 3 by A11, A13, A14, FUNCT_4:def 1
.= (Reloc ((ProgramPart ((Goto ((card (I ';' (Goto 0))) + 1)) ';' ((I ';' (Goto 0)) ';' (Stop SCM+FSA)))),3)) . 3 by COMPOS_1:116
.= (Reloc (((Goto ((card (I ';' (Goto 0))) + 1)) ';' ((I ';' (Goto 0)) ';' (Stop SCM+FSA))),3)) . 3 by RELAT_1:209
.= IncAddr ((goto ((card I) + 2)),3) by A5, A6, SCMFSA_4:24
.= goto (((card I) + 2) + 3) by SCMFSA_4:14
.= goto ((card I) + 5) ; :: thesis: verum