let a be Int-Location; :: thesis: for I, J being MacroInstruction of SCM+FSA holds
( 1 in dom (if=0 (a,I,J)) & 1 in dom (if>0 (a,I,J)) )
let I, J be MacroInstruction of SCM+FSA ; :: thesis: ( 1 in dom (if=0 (a,I,J)) & 1 in dom (if>0 (a,I,J)) )
set i = a =0_goto ((card J) + 3);
if=0 (a,I,J) = ((((a =0_goto ((card J) + 3)) ";" J) ";" (Goto ((card I) + 1))) ";" I) ";" (Stop SCM+FSA)
.= (((a =0_goto ((card J) + 3)) ";" J) ";" (Goto ((card I) + 1))) ";" (I ";" (Stop SCM+FSA)) by SCMFSA6A:25
.= ((a =0_goto ((card J) + 3)) ";" J) ";" ((Goto ((card I) + 1)) ";" (I ";" (Stop SCM+FSA))) by SCMFSA6A:25
.= (a =0_goto ((card J) + 3)) ";" (J ";" ((Goto ((card I) + 1)) ";" (I ";" (Stop SCM+FSA)))) by SCMFSA6A:29
.= (Macro (a =0_goto ((card J) + 3))) ";" (J ";" ((Goto ((card I) + 1)) ";" (I ";" (Stop SCM+FSA)))) ;
then A1: dom (Macro (a =0_goto ((card J) + 3))) c= dom (if=0 (a,I,J)) by SCMFSA6A:17;
dom (Macro (a =0_goto ((card J) + 3))) = {0,1} by COMPOS_1:61;
then A2: 1 in dom (Macro (a =0_goto ((card J) + 3))) by TARSKI:def 2;
thus 1 in dom (if=0 (a,I,J)) by A1, A2; :: thesis: 1 in dom (if>0 (a,I,J))
set i = a >0_goto ((card J) + 3);
if>0 (a,I,J) = ((((a >0_goto ((card J) + 3)) ";" J) ";" (Goto ((card I) + 1))) ";" I) ";" (Stop SCM+FSA)
.= (((a >0_goto ((card J) + 3)) ";" J) ";" (Goto ((card I) + 1))) ";" (I ";" (Stop SCM+FSA)) by SCMFSA6A:25
.= ((a >0_goto ((card J) + 3)) ";" J) ";" ((Goto ((card I) + 1)) ";" (I ";" (Stop SCM+FSA))) by SCMFSA6A:25
.= (a >0_goto ((card J) + 3)) ";" (J ";" ((Goto ((card I) + 1)) ";" (I ";" (Stop SCM+FSA)))) by SCMFSA6A:29
.= (Macro (a >0_goto ((card J) + 3))) ";" (J ";" ((Goto ((card I) + 1)) ";" (I ";" (Stop SCM+FSA)))) ;
then A3: dom (Macro (a >0_goto ((card J) + 3))) c= dom (if>0 (a,I,J)) by SCMFSA6A:17;
dom (Macro (a >0_goto ((card J) + 3))) = {0,1} by COMPOS_1:61;
then A4: 1 in dom (Macro (a >0_goto ((card J) + 3))) by TARSKI:def 2;
thus 1 in dom (if>0 (a,I,J)) by A3, A4; :: thesis: verum