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: pi (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 AMI_1:def 47
.= ((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 SCMFSA7B:6, LL ;
then A9: not 3 in dom ((Macro (a =0_goto ((card (Stop SCM+FSA )) + 3))) ';' (Stop SCM+FSA )) by SCMFSA6A:15;
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 Th12, 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 1
.= (((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
.= (IncAddr (Shift (ProgramPart ((Goto ((card (I ';' (Goto 0 ))) + 1)) ';' ((I ';' (Goto 0 )) ';' (Stop SCM+FSA )))),3),3) . 3 by SCMFSA_5:2
.= (IncAddr (Shift ((Goto ((card (I ';' (Goto 0 ))) + 1)) ';' ((I ';' (Goto 0 )) ';' (Stop SCM+FSA ))),3),3) . 3 by AMI_1:105
.= 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