set J = Stop SCM+FSA;
let a be Int-Location ; :: thesis: for I being Program of holds (while>0 (a,I)) . 3 = goto ((card I) + 5)
let I be Program of ; :: 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:31;
A2: (Goto ((card (I ';' (Goto 0))) + 1)) . 0 = goto ((card (I ';' (Goto 0))) + 1) by SCMFSA8A:31
.= goto (((card I) + (card (Goto 0))) + 1) by SCMFSA6A:21
.= goto (((card I) + 1) + 1) by SCMFSA8A:15
.= goto ((card I) + (1 + 1)) ;
dom ((Goto ((card (I ';' (Goto 0))) + 1)) ';' ((I ';' (Goto 0)) ';' (Stop SCM+FSA))) = (dom (Directed (Goto ((card (I ';' (Goto 0))) + 1)))) \/ (dom (Reloc (((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 (Reloc (((I ';' (Goto 0)) ';' (Stop SCM+FSA)),(card (Goto ((card (I ';' (Goto 0))) + 1)))))) by FUNCT_4:99 ;
then A3: 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 A4: 3 in dom (Shift (((Goto ((card (I ';' (Goto 0))) + 1)) ';' ((I ';' (Goto 0)) ';' (Stop SCM+FSA))),3)) by VALUED_1:def 12;
then A5: (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 6
.= ((Goto ((card (I ';' (Goto 0))) + 1)) ';' ((I ';' (Goto 0)) ';' (Stop SCM+FSA))) . 0 by A3, VALUED_1:def 12
.= (Directed (Goto ((card (I ';' (Goto 0))) + 1))) . 0 by A1, SCMFSA8A:14
.= goto ((card I) + 2) by A1, A2, SCMFSA8A:16 ;
( dom (((card I) + 4) .--> (goto 0)) = {((card I) + 4)} & 3 <> (card I) + 4 ) by FUNCOP_1:13, NAT_1:11;
then A6: not 3 in dom (((card I) + 4) .--> (goto 0)) by TARSKI:def 1;
A7: 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:21
.= 2 + 1 by Lm1, COMPOS_1:56 ;
then A8: not 3 in dom ((Macro (a >0_goto ((card (Stop SCM+FSA)) + 3))) ';' (Stop SCM+FSA)) ;
A9: ( 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 A10: 3 in dom (if>0 (a,(I ';' (Goto 0)),(Stop SCM+FSA))) by A6, XBOOLE_0:def 3;
A11: 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:25
.= ((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:25
.= (Directed ((Macro (a >0_goto ((card (Stop SCM+FSA)) + 3))) ';' (Stop SCM+FSA))) +* (Reloc (((Goto ((card (I ';' (Goto 0))) + 1)) ';' ((I ';' (Goto 0)) ';' (Stop SCM+FSA))),3)) by A7 ;
then A12: 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 (Reloc (((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 (Reloc (((Goto ((card (I ';' (Goto 0))) + 1)) ';' ((I ';' (Goto 0)) ';' (Stop SCM+FSA))),3))) by FUNCT_4:99;
then A13: 3 in dom (Reloc (((Goto ((card (I ';' (Goto 0))) + 1)) ';' ((I ';' (Goto 0)) ';' (Stop SCM+FSA))),3)) by A10, A8, XBOOLE_0:def 3;
thus (while>0 (a,I)) . 3 = ((Directed ((Macro (a >0_goto ((card (Stop SCM+FSA)) + 3))) ';' (Stop SCM+FSA))) +* (Reloc (((Goto ((card (I ';' (Goto 0))) + 1)) ';' ((I ';' (Goto 0)) ';' (Stop SCM+FSA))),3))) . 3 by A6, A9, A11, FUNCT_4:def 1
.= (Reloc (((Goto ((card (I ';' (Goto 0))) + 1)) ';' ((I ';' (Goto 0)) ';' (Stop SCM+FSA))),3)) . 3 by A10, A12, A13, FUNCT_4:def 1
.= IncAddr ((goto ((card I) + 2)),3) by A4, A5, COMPOS_1:def 19
.= goto (((card I) + 2) + 3) by SCMFSA_4:1
.= goto ((card I) + 5) ; :: thesis: verum