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