set D = Int-Locations \/ FinSeq-Locations ;
let s be State of SCM+FSA ; :: thesis: for I, J being Program of SCM+FSA
for a being read-write Int-Location st s . a = 0 & Directed I is_pseudo-closed_on s holds
( if=0 a,I,J is_halting_on s & if=0 a,I,J is_closed_on s & LifeSpan (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))) = (LifeSpan (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 ))))) + 1 )
let I, J be Program of SCM+FSA ; :: thesis: for a being read-write Int-Location st s . a = 0 & Directed I is_pseudo-closed_on s holds
( if=0 a,I,J is_halting_on s & if=0 a,I,J is_closed_on s & LifeSpan (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))) = (LifeSpan (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 ))))) + 1 )
let a be read-write Int-Location ; :: thesis: ( s . a = 0 & Directed I is_pseudo-closed_on s implies ( if=0 a,I,J is_halting_on s & if=0 a,I,J is_closed_on s & LifeSpan (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))) = (LifeSpan (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 ))))) + 1 ) )
set I0 = Directed I;
set I1 = I ';' (Stop SCM+FSA );
set s00 = s +* ((Directed I) +* (Start-At (insloc 0 )));
set s3 = s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )));
set s4 = Computation (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),1;
set i = a =0_goto (insloc ((card J) + 3));
assume A1: s . a = 0 ; :: thesis: ( not Directed I is_pseudo-closed_on s or ( if=0 a,I,J is_halting_on s & if=0 a,I,J is_closed_on s & LifeSpan (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))) = (LifeSpan (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 ))))) + 1 ) )
assume A2: Directed I is_pseudo-closed_on s ; :: thesis: ( if=0 a,I,J is_halting_on s & if=0 a,I,J is_closed_on s & LifeSpan (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))) = (LifeSpan (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 ))))) + 1 )
A3: if=0 a,I,J = ((((a =0_goto (insloc ((card J) + 3))) ';' J) ';' (Goto (insloc ((card I) + 1)))) ';' I) ';' (Stop SCM+FSA ) by SCMFSA8B:def 1;
A4: (Directed I) +* (Start-At (insloc 0 )) c= s +* ((Directed I) +* (Start-At (insloc 0 ))) by FUNCT_4:26;
DataPart s = DataPart (s +* ((Directed I) +* (Start-At (insloc 0 )))) by SCMFSA8A:11;
then A5: Directed I is_pseudo-closed_on s +* ((Directed I) +* (Start-At (insloc 0 ))) by A2, Th52;
A6: insloc 0 in dom (if=0 a,I,J) by Th54;
if=0 a,I,J c= (if=0 a,I,J) +* (Start-At (insloc 0 )) by SCMFSA8A:9;
then A7: dom (if=0 a,I,J) c= dom ((if=0 a,I,J) +* (Start-At (insloc 0 ))) by GRFUNC_1:8;
A8: IC SCM+FSA in dom ((if=0 a,I,J) +* (Start-At (insloc 0 ))) by SF_MASTR:65;
A9: now
thus IC (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))) = ((if=0 a,I,J) +* (Start-At (insloc 0 ))) . (IC SCM+FSA ) by A8, FUNCT_4:14
.= insloc 0 by SF_MASTR:66 ; :: thesis: verum
end;
A10: now
thus (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))) . (insloc 0 ) = ((if=0 a,I,J) +* (Start-At (insloc 0 ))) . (insloc 0 ) by A6, A7, FUNCT_4:14
.= (if=0 a,I,J) . (insloc 0 ) by A6, SCMFSA6B:7
.= a =0_goto (insloc ((card J) + 3)) by Th55 ; :: thesis: verum
end;
A11: now
thus Computation (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),(0 + 1) = Following (Computation (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),0 ) by AMI_1:14
.= Following (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))) by AMI_1:13
.= Exec (a =0_goto (insloc ((card J) + 3))),(s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))) by A9, A10 ; :: thesis: verum
end;
A12: now
thus card (((a =0_goto (insloc ((card J) + 3))) ';' J) ';' (Goto (insloc ((card I) + 1)))) = (card ((Macro (a =0_goto (insloc ((card J) + 3)))) ';' J)) + (card (Goto (insloc ((card I) + 1)))) by SCMFSA6A:61
.= (card ((Macro (a =0_goto (insloc ((card J) + 3)))) ';' J)) + 1 by SCMFSA8A:29
.= ((card (Macro (a =0_goto (insloc ((card J) + 3))))) + (card J)) + 1 by SCMFSA6A:61
.= ((card J) + 2) + 1 by SCMFSA7B:6
.= (card J) + (2 + 1) ; :: thesis: verum
end;
( not a in dom ((if=0 a,I,J) +* (Start-At (insloc 0 ))) & a in dom s ) by SCMFSA6B:12, SCMFSA_2:66;
then A13: (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))) . a = 0 by A1, FUNCT_4:12;
A14: (if=0 a,I,J) +* (Start-At (insloc 0 )) c= s +* ((if=0 a,I,J) +* (Start-At (insloc 0 ))) by FUNCT_4:26;
if=0 a,I,J c= (if=0 a,I,J) +* (Start-At (insloc 0 )) by SCMFSA8A:9;
then A15: if=0 a,I,J c= s +* ((if=0 a,I,J) +* (Start-At (insloc 0 ))) by A14, XBOOLE_1:1;
if=0 a,I,J = (((a =0_goto (insloc ((card J) + 3))) ';' J) ';' (Goto (insloc ((card I) + 1)))) ';' (I ';' (Stop SCM+FSA )) by A3, SCMFSA6A:67;
then ProgramPart (Relocated (I ';' (Stop SCM+FSA )),((card J) + 3)) c= if=0 a,I,J by A12, FUNCT_4:26;
then ProgramPart (Relocated (I ';' (Stop SCM+FSA )),((card J) + 3)) c= s +* ((if=0 a,I,J) +* (Start-At (insloc 0 ))) by A15, XBOOLE_1:1;
then ProgramPart [(ProgramPart (Relocated (I ';' (Stop SCM+FSA )),((card J) + 3)))] c= Computation (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),1 by AMI_1:99;
then A16: ProgramPart (Relocated (I ';' (Stop SCM+FSA )),((card J) + 3)) c= Computation (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),1 by AMI_1:105;
ProgramPart (Relocated (Directed I),((card J) + 3)) c= ProgramPart (Relocated (I ';' (Stop SCM+FSA )),((card J) + 3)) by Th12, SCMFSA6A:55;
then A17: ProgramPart (Relocated (Directed I),((card J) + 3)) c= Computation (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),1 by A16, XBOOLE_1:1;
A18: IC (Computation (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),1) = insloc ((card J) + 3) by A11, A13, SCMFSA_2:96;
A19: DataPart (s +* ((Directed I) +* (Start-At (insloc 0 )))) = DataPart (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))) by SCMFSA6A:39, SCMFSA8A:14;
A20: now
let a be Int-Location ; :: thesis: (s +* ((Directed I) +* (Start-At (insloc 0 )))) . a = (Computation (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),1) . a
thus (s +* ((Directed I) +* (Start-At (insloc 0 )))) . a = (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))) . a by A19, SCMFSA6A:38
.= (Computation (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),1) . a by A11, SCMFSA_2:96 ; :: thesis: verum
end;
now
let f be FinSeq-Location ; :: thesis: (s +* ((Directed I) +* (Start-At (insloc 0 )))) . f = (Computation (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),1) . f
thus (s +* ((Directed I) +* (Start-At (insloc 0 )))) . f = (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))) . f by A19, SCMFSA6A:38
.= (Computation (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),1) . f by A11, SCMFSA_2:96 ; :: thesis: verum
end;
then A21: DataPart (s +* ((Directed I) +* (Start-At (insloc 0 )))) = DataPart (Computation (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),1) by A20, SCMFSA6A:38;
A22: if=0 a,I,J c= s +* ((if=0 a,I,J) +* (Start-At (insloc 0 ))) by FUNCT_4:26, SCMFSA6B:5;
now
thus card (if=0 a,I,J) = ((card I) + (card J)) + (3 + 1) by SCMFSA8B:14
.= (((card I) + (card J)) + 3) + 1 ; :: thesis: verum
end;
then ((card I) + (card J)) + 3 < card (if=0 a,I,J) by NAT_1:13;
then A23: insloc (((card I) + (card J)) + 3) in dom (if=0 a,I,J) by SCMFSA6A:15;
A24: now
thus IC (Computation (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),((pseudo-LifeSpan (s +* ((Directed I) +* (Start-At (insloc 0 )))),(Directed I)) + 1)) = IC (Computation (Computation (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),1),(pseudo-LifeSpan (s +* ((Directed I) +* (Start-At (insloc 0 )))),(Directed I))) by AMI_1:51
.= (IC (Computation (s +* ((Directed I) +* (Start-At (insloc 0 )))),(pseudo-LifeSpan (s +* ((Directed I) +* (Start-At (insloc 0 )))),(Directed I)))) + ((card J) + 3) by A4, A5, A17, A18, A21, Th51
.= (IC (Computation (s +* ((Directed I) +* (Start-At (insloc 0 )))),(pseudo-LifeSpan s,(Directed I)))) + ((card J) + 3) by A2, Th50
.= (insloc (card (ProgramPart (Directed I)))) + ((card J) + 3) by A2, SCMFSA8A:def 5
.= (insloc (card (Directed I))) + ((card J) + 3) by AMI_1:105
.= insloc ((card I) + ((card J) + 3)) by SCMFSA8A:34
.= insloc (((card I) + (card J)) + 3) ; :: thesis: verum
end;
then A25: CurInstr (Computation (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),((pseudo-LifeSpan (s +* ((Directed I) +* (Start-At (insloc 0 )))),(Directed I)) + 1)) = (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))) . (insloc (((card I) + (card J)) + 3)) by AMI_1:54
.= (if=0 a,I,J) . (insloc (((card I) + (card J)) + 3)) by A22, A23, GRFUNC_1:8
.= halt SCM+FSA by Th61 ;
then A26: s +* ((if=0 a,I,J) +* (Start-At (insloc 0 ))) is halting by AMI_1:def 20;
hence if=0 a,I,J is_halting_on s by SCMFSA7B:def 8; :: thesis: ( if=0 a,I,J is_closed_on s & LifeSpan (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))) = (LifeSpan (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 ))))) + 1 )
now
let k be Element of NAT ; :: thesis: IC (Computation (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),b1) in dom (if=0 a,I,J)
per cases ( k = 0 or ( 0 < k & k < (pseudo-LifeSpan (s +* ((Directed I) +* (Start-At (insloc 0 )))),(Directed I)) + 1 ) or ( 0 < k & (pseudo-LifeSpan (s +* ((Directed I) +* (Start-At (insloc 0 )))),(Directed I)) + 1 <= k ) ) ;
suppose k = 0 ; :: thesis: IC (Computation (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),b1) in dom (if=0 a,I,J)
then Computation (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),k = s +* ((if=0 a,I,J) +* (Start-At (insloc 0 ))) by AMI_1:13;
then IC (Computation (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),k) = insloc 0 by Th31;
hence IC (Computation (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),k) in dom (if=0 a,I,J) by Th54; :: thesis: verum
end;
suppose A27: ( 0 < k & k < (pseudo-LifeSpan (s +* ((Directed I) +* (Start-At (insloc 0 )))),(Directed I)) + 1 ) ; :: thesis: IC (Computation (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),b1) in dom (if=0 a,I,J)
then 0 + 1 <= k by INT_1:20;
then consider k1 being Nat such that
A28: 1 + k1 = k by NAT_1:10;
reconsider k1 = k1 as Element of NAT by ORDINAL1:def 13;
A29: k1 < pseudo-LifeSpan (s +* ((Directed I) +* (Start-At (insloc 0 )))),(Directed I) by A27, A28, XREAL_1:8;
then A30: k1 < pseudo-LifeSpan s,(Directed I) by A2, Th50;
A31: IC (Computation (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),k) = IC (Computation (Computation (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),1),k1) by A28, AMI_1:51
.= (IC (Computation (s +* ((Directed I) +* (Start-At (insloc 0 )))),k1)) + ((card J) + 3) by A4, A5, A17, A18, A21, A29, Th51 ;
reconsider n = IC (Computation (s +* ((Directed I) +* (Start-At (insloc 0 )))),k1) as Element of NAT by ORDINAL1:def 13;
insloc n in dom (Directed I) by A2, A30, SCMFSA8A:31;
then n < card (Directed I) by SCMFSA6A:15;
then n + ((card J) + 3) < (card (Directed I)) + ((card J) + 3) by XREAL_1:8;
then A33: n + ((card J) + 3) < (card I) + ((card J) + 3) by SCMFSA8A:34;
card (if=0 a,I,J) = ((card I) + (card J)) + (3 + 1) by SCMFSA8B:14
.= (((card I) + (card J)) + 3) + 1 ;
then ((card I) + (card J)) + 3 < card (if=0 a,I,J) by XREAL_1:31;
then n + ((card J) + 3) < card (if=0 a,I,J) by A33, XXREAL_0:2;
hence IC (Computation (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),k) in dom (if=0 a,I,J) by A31, SCMFSA6A:15; :: thesis: verum
end;
suppose ( 0 < k & (pseudo-LifeSpan (s +* ((Directed I) +* (Start-At (insloc 0 )))),(Directed I)) + 1 <= k ) ; :: thesis: IC (Computation (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),b1) in dom (if=0 a,I,J)
hence IC (Computation (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),k) in dom (if=0 a,I,J) by A23, A24, A25, AMI_1:52; :: thesis: verum
end;
end;
end;
hence if=0 a,I,J is_closed_on s by SCMFSA7B:def 7; :: thesis: LifeSpan (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))) = (LifeSpan (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 ))))) + 1
now
let k be Element of NAT ; :: thesis: ( CurInstr (Computation (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),k) = halt SCM+FSA implies (pseudo-LifeSpan (s +* ((Directed I) +* (Start-At (insloc 0 )))),(Directed I)) + 1 <= k )
assume A34: CurInstr (Computation (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),k) = halt SCM+FSA ; :: thesis: (pseudo-LifeSpan (s +* ((Directed I) +* (Start-At (insloc 0 )))),(Directed I)) + 1 <= k
assume not (pseudo-LifeSpan (s +* ((Directed I) +* (Start-At (insloc 0 )))),(Directed I)) + 1 <= k ; :: thesis: contradiction
then A35: k <= pseudo-LifeSpan (s +* ((Directed I) +* (Start-At (insloc 0 )))),(Directed I) by NAT_1:13;
A36: insloc 0 in dom (if=0 a,I,J) by Th54;
A37: ( InsCode (halt SCM+FSA ) = 0 & InsCode (a =0_goto (insloc ((card J) + 3))) = 7 ) by SCMFSA_2:48, SCMFSA_2:124;
CurInstr (Computation (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),0 ) = CurInstr (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))) by AMI_1:13
.= (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))) . (insloc 0 ) by Th31
.= (if=0 a,I,J) . (insloc 0 ) by A36, Th26
.= a =0_goto (insloc ((card J) + 3)) by Th55 ;
then consider k1 being Nat such that
A38: k1 + 1 = k by A34, A37, NAT_1:6;
reconsider k1 = k1 as Element of NAT by ORDINAL1:def 13;
k1 < k by A38, XREAL_1:31;
then A39: k1 < pseudo-LifeSpan (s +* ((Directed I) +* (Start-At (insloc 0 )))),(Directed I) by A35, XXREAL_0:2;
A40: IC (Computation (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),k) = IC (Computation (Computation (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),1),k1) by A38, AMI_1:51
.= (IC (Computation (s +* ((Directed I) +* (Start-At (insloc 0 )))),k1)) + ((card J) + 3) by A4, A5, A17, A18, A21, A39, Th51 ;
reconsider n = IC (Computation (s +* ((Directed I) +* (Start-At (insloc 0 )))),k1) as Element of NAT by ORDINAL1:def 13;
k1 < pseudo-LifeSpan s,(Directed I) by A2, A39, Th50;
then insloc n in dom (Directed I) by A2, SCMFSA8A:31;
then n < card (Directed I) by SCMFSA6A:15;
then n + ((card J) + 3) < (card (Directed I)) + ((card J) + 3) by XREAL_1:8;
then A42: n + ((card J) + 3) < (card I) + ((card J) + 3) by SCMFSA8A:34;
card (if=0 a,I,J) = ((card I) + (card J)) + (3 + 1) by SCMFSA8B:14
.= (((card I) + (card J)) + 3) + 1 ;
then ((card I) + (card J)) + 3 < card (if=0 a,I,J) by XREAL_1:31;
then n + ((card J) + 3) < card (if=0 a,I,J) by A42, XXREAL_0:2;
then A43: IC (Computation (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),k) in dom (if=0 a,I,J) by A40, SCMFSA6A:15;
set J1 = (((a =0_goto (insloc ((card J) + 3))) ';' J) ';' (Goto (insloc ((card I) + 1)))) ';' I;
card ((((a =0_goto (insloc ((card J) + 3))) ';' J) ';' (Goto (insloc ((card I) + 1)))) ';' I) = (card (((Macro (a =0_goto (insloc ((card J) + 3)))) ';' J) ';' (Goto (insloc ((card I) + 1))))) + (card I) by SCMFSA6A:61
.= ((card ((Macro (a =0_goto (insloc ((card J) + 3)))) ';' J)) + (card (Goto (insloc ((card I) + 1))))) + (card I) by SCMFSA6A:61
.= ((card ((Macro (a =0_goto (insloc ((card J) + 3)))) ';' J)) + 1) + (card I) by SCMFSA8A:29
.= (((card (Macro (a =0_goto (insloc ((card J) + 3))))) + (card J)) + 1) + (card I) by SCMFSA6A:61
.= ((2 + (card J)) + 1) + (card I) by SCMFSA7B:6
.= ((card I) + (card J)) + 3 ;
then IC (Computation (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),k) in dom ((((a =0_goto (insloc ((card J) + 3))) ';' J) ';' (Goto (insloc ((card I) + 1)))) ';' I) by A40, A42, SCMFSA6A:15;
then A44: IC (Computation (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),k) in dom (Directed ((((a =0_goto (insloc ((card J) + 3))) ';' J) ';' (Goto (insloc ((card I) + 1)))) ';' I)) by FUNCT_4:105;
Directed ((((a =0_goto (insloc ((card J) + 3))) ';' J) ';' (Goto (insloc ((card I) + 1)))) ';' I) c= if=0 a,I,J by A3, SCMFSA6A:55;
then A45: (if=0 a,I,J) . (IC (Computation (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),k)) = (Directed ((((a =0_goto (insloc ((card J) + 3))) ';' J) ';' (Goto (insloc ((card I) + 1)))) ';' I)) . (IC (Computation (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),k)) by A44, GRFUNC_1:8;
A46: (Directed ((((a =0_goto (insloc ((card J) + 3))) ';' J) ';' (Goto (insloc ((card I) + 1)))) ';' I)) . (IC (Computation (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),k)) in rng (Directed ((((a =0_goto (insloc ((card J) + 3))) ';' J) ';' (Goto (insloc ((card I) + 1)))) ';' I)) by A44, FUNCT_1:def 5;
CurInstr (Computation (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),k) = (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))) . (IC (Computation (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),k)) by AMI_1:54
.= (if=0 a,I,J) . (IC (Computation (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),k)) by A43, Th26 ;
hence contradiction by A34, A45, A46, AMI_1:def 52; :: thesis: verum
end;
then A47: LifeSpan (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))) = (pseudo-LifeSpan (s +* ((Directed I) +* (Start-At (insloc 0 )))),(Directed I)) + 1 by A25, A26, AMI_1:def 46;
pseudo-LifeSpan s,(Directed I) = LifeSpan (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))) by A2, Th58;
hence LifeSpan (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))) = (LifeSpan (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 ))))) + 1 by A2, A47, Th50; :: thesis: verum