let s be State of SCM+FSA; :: thesis: for I being Program of SCM+FSA st Directed I is_pseudo-closed_on s holds
( I ';' (Stop SCM+FSA) is_closed_on s & I ';' (Stop SCM+FSA) is_halting_on s & LifeSpan ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))) = pseudo-LifeSpan (s,(Directed I)) & ( for n being Element of NAT st n < pseudo-LifeSpan (s,(Directed I)) holds
IC (Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),n)) = IC (Comput ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),n)) ) & ( for n being Element of NAT st n <= pseudo-LifeSpan (s,(Directed I)) holds
DataPart (Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),n)) = DataPart (Comput ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),n)) ) )
set D = Int-Locations \/ FinSeq-Locations;
set A = NAT ;
let I be Program of SCM+FSA; :: thesis: ( Directed I is_pseudo-closed_on s implies ( I ';' (Stop SCM+FSA) is_closed_on s & I ';' (Stop SCM+FSA) is_halting_on s & LifeSpan ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))) = pseudo-LifeSpan (s,(Directed I)) & ( for n being Element of NAT st n < pseudo-LifeSpan (s,(Directed I)) holds
IC (Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),n)) = IC (Comput ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),n)) ) & ( for n being Element of NAT st n <= pseudo-LifeSpan (s,(Directed I)) holds
DataPart (Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),n)) = DataPart (Comput ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),n)) ) ) )
set I0 = Directed I;
set I1 = I ';' (Stop SCM+FSA);
set s00 = s +* ((Directed I) +* (Start-At (0,SCM+FSA)));
set s10 = s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)));
reconsider k = pseudo-LifeSpan ((s +* ((Directed I) +* (Start-At (0,SCM+FSA)))),(Directed I)) as Element of NAT ;
(Stop SCM+FSA) . 0 = halt SCM+FSA by AFINSQ_1:38;
then A1: halt SCM+FSA = (Stop SCM+FSA) . ((card I) -' (card I)) by XREAL_1:234;
A2: DataPart (s +* ((Directed I) +* (Start-At (0,SCM+FSA)))) = DataPart s by SCMFSA8A:11
.= DataPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))) by SCMFSA8A:11 ;
assume A3: Directed I is_pseudo-closed_on s ; :: thesis: ( I ';' (Stop SCM+FSA) is_closed_on s & I ';' (Stop SCM+FSA) is_halting_on s & LifeSpan ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))) = pseudo-LifeSpan (s,(Directed I)) & ( for n being Element of NAT st n < pseudo-LifeSpan (s,(Directed I)) holds
IC (Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),n)) = IC (Comput ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),n)) ) & ( for n being Element of NAT st n <= pseudo-LifeSpan (s,(Directed I)) holds
DataPart (Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),n)) = DataPart (Comput ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),n)) ) )
then A4: Directed I is_pseudo-closed_on s +* ((Directed I) +* (Start-At (0,SCM+FSA))) by Th50;
defpred S1[ Nat] means ( k <= $1 implies ( IC (Comput ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),$1)) = card I & CurInstr ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(Comput ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),$1))) = halt SCM+FSA ) );
A5: (I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)) c= s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))) by FUNCT_4:26;
I ';' (Stop SCM+FSA) c= (I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)) by SCMFSA8A:9;
then A6: I ';' (Stop SCM+FSA) c= s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))) by A5, XBOOLE_1:1;
A7: Directed I c= I ';' (Stop SCM+FSA) by SCMFSA6A:55;
then A8: dom (Directed I) c= dom (I ';' (Stop SCM+FSA)) by GRFUNC_1:8;
ProgramPart (Relocated ((Directed I),0)) c= I ';' (Stop SCM+FSA) by A7, Th9;
then A9: ProgramPart (Relocated ((Directed I),0)) c= s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))) by A6, XBOOLE_1:1;
s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))) = (s +* (I ';' (Stop SCM+FSA))) +* (Start-At (0,SCM+FSA)) by FUNCT_4:15;
then A10: IC (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))) = 0 by FUNCT_4:121;
A11: (Directed I) +* (Start-At (0,SCM+FSA)) c= s +* ((Directed I) +* (Start-At (0,SCM+FSA))) by FUNCT_4:26;
A12: now
let n be Element of NAT ; :: thesis: ( n <= pseudo-LifeSpan ((s +* ((Directed I) +* (Start-At (0,SCM+FSA)))),(Directed I)) implies ( IC (Comput ((ProgramPart (s +* ((Directed I) +* (Start-At (0,SCM+FSA))))),(s +* ((Directed I) +* (Start-At (0,SCM+FSA)))),n)) = IC (Comput ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),n)) & DataPart (Comput ((ProgramPart (s +* ((Directed I) +* (Start-At (0,SCM+FSA))))),(s +* ((Directed I) +* (Start-At (0,SCM+FSA)))),n)) = DataPart (Comput ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),n)) ) )
assume A13: n <= pseudo-LifeSpan ((s +* ((Directed I) +* (Start-At (0,SCM+FSA)))),(Directed I)) ; :: thesis: ( IC (Comput ((ProgramPart (s +* ((Directed I) +* (Start-At (0,SCM+FSA))))),(s +* ((Directed I) +* (Start-At (0,SCM+FSA)))),n)) = IC (Comput ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),n)) & DataPart (Comput ((ProgramPart (s +* ((Directed I) +* (Start-At (0,SCM+FSA))))),(s +* ((Directed I) +* (Start-At (0,SCM+FSA)))),n)) = DataPart (Comput ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),n)) )
then (IC (Comput ((ProgramPart (s +* ((Directed I) +* (Start-At (0,SCM+FSA))))),(s +* ((Directed I) +* (Start-At (0,SCM+FSA)))),n))) + 0 = IC (Comput ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),n)) by A11, A4, A9, A10, A2, Th51;
hence IC (Comput ((ProgramPart (s +* ((Directed I) +* (Start-At (0,SCM+FSA))))),(s +* ((Directed I) +* (Start-At (0,SCM+FSA)))),n)) = IC (Comput ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),n)) ; :: thesis: DataPart (Comput ((ProgramPart (s +* ((Directed I) +* (Start-At (0,SCM+FSA))))),(s +* ((Directed I) +* (Start-At (0,SCM+FSA)))),n)) = DataPart (Comput ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),n))
thus DataPart (Comput ((ProgramPart (s +* ((Directed I) +* (Start-At (0,SCM+FSA))))),(s +* ((Directed I) +* (Start-At (0,SCM+FSA)))),n)) = DataPart (Comput ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),n)) by A11, A4, A9, A10, A2, A13, Th51; :: thesis: verum
end;
A14: k = pseudo-LifeSpan (s,(Directed I)) by A3, Th50;
A15: (s +* ((Directed I) +* (Start-At (0,SCM+FSA)))) +* ((Directed I) +* (Start-At (0,SCM+FSA))) = s +* (((Directed I) +* (Start-At (0,SCM+FSA))) +* ((Directed I) +* (Start-At (0,SCM+FSA)))) by FUNCT_4:15
.= s +* ((Directed I) +* (Start-At (0,SCM+FSA))) ;
A16: now
let n be Element of NAT ; :: thesis: ( n < pseudo-LifeSpan ((s +* ((Directed I) +* (Start-At (0,SCM+FSA)))),(Directed I)) implies ( CurInstr ((ProgramPart (Comput ((ProgramPart (s +* ((Directed I) +* (Start-At (0,SCM+FSA))))),(s +* ((Directed I) +* (Start-At (0,SCM+FSA)))),n))),(Comput ((ProgramPart (s +* ((Directed I) +* (Start-At (0,SCM+FSA))))),(s +* ((Directed I) +* (Start-At (0,SCM+FSA)))),n))) = CurInstr ((ProgramPart (Comput ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),n))),(Comput ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),n))) & IC (Comput ((ProgramPart (s +* ((Directed I) +* (Start-At (0,SCM+FSA))))),(s +* ((Directed I) +* (Start-At (0,SCM+FSA)))),n)) in dom (Directed I) & CurInstr ((ProgramPart (Comput ((ProgramPart (s +* ((Directed I) +* (Start-At (0,SCM+FSA))))),(s +* ((Directed I) +* (Start-At (0,SCM+FSA)))),n))),(Comput ((ProgramPart (s +* ((Directed I) +* (Start-At (0,SCM+FSA))))),(s +* ((Directed I) +* (Start-At (0,SCM+FSA)))),n))) <> halt SCM+FSA ) )
assume A17: n < pseudo-LifeSpan ((s +* ((Directed I) +* (Start-At (0,SCM+FSA)))),(Directed I)) ; :: thesis: ( CurInstr ((ProgramPart (Comput ((ProgramPart (s +* ((Directed I) +* (Start-At (0,SCM+FSA))))),(s +* ((Directed I) +* (Start-At (0,SCM+FSA)))),n))),(Comput ((ProgramPart (s +* ((Directed I) +* (Start-At (0,SCM+FSA))))),(s +* ((Directed I) +* (Start-At (0,SCM+FSA)))),n))) = CurInstr ((ProgramPart (Comput ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),n))),(Comput ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),n))) & IC (Comput ((ProgramPart (s +* ((Directed I) +* (Start-At (0,SCM+FSA))))),(s +* ((Directed I) +* (Start-At (0,SCM+FSA)))),n)) in dom (Directed I) & CurInstr ((ProgramPart (Comput ((ProgramPart (s +* ((Directed I) +* (Start-At (0,SCM+FSA))))),(s +* ((Directed I) +* (Start-At (0,SCM+FSA)))),n))),(Comput ((ProgramPart (s +* ((Directed I) +* (Start-At (0,SCM+FSA))))),(s +* ((Directed I) +* (Start-At (0,SCM+FSA)))),n))) <> halt SCM+FSA )
then IncAddr ((CurInstr ((ProgramPart (Comput ((ProgramPart (s +* ((Directed I) +* (Start-At (0,SCM+FSA))))),(s +* ((Directed I) +* (Start-At (0,SCM+FSA)))),n))),(Comput ((ProgramPart (s +* ((Directed I) +* (Start-At (0,SCM+FSA))))),(s +* ((Directed I) +* (Start-At (0,SCM+FSA)))),n)))),0) = CurInstr ((ProgramPart (Comput ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),n))),(Comput ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),n))) by A11, A4, A9, A10, A2, Th51;
hence CurInstr ((ProgramPart (Comput ((ProgramPart (s +* ((Directed I) +* (Start-At (0,SCM+FSA))))),(s +* ((Directed I) +* (Start-At (0,SCM+FSA)))),n))),(Comput ((ProgramPart (s +* ((Directed I) +* (Start-At (0,SCM+FSA))))),(s +* ((Directed I) +* (Start-At (0,SCM+FSA)))),n))) = CurInstr ((ProgramPart (Comput ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),n))),(Comput ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),n))) by COMPOS_1:91; :: thesis: ( IC (Comput ((ProgramPart (s +* ((Directed I) +* (Start-At (0,SCM+FSA))))),(s +* ((Directed I) +* (Start-At (0,SCM+FSA)))),n)) in dom (Directed I) & CurInstr ((ProgramPart (Comput ((ProgramPart (s +* ((Directed I) +* (Start-At (0,SCM+FSA))))),(s +* ((Directed I) +* (Start-At (0,SCM+FSA)))),n))),(Comput ((ProgramPart (s +* ((Directed I) +* (Start-At (0,SCM+FSA))))),(s +* ((Directed I) +* (Start-At (0,SCM+FSA)))),n))) <> halt SCM+FSA )
thus IC (Comput ((ProgramPart (s +* ((Directed I) +* (Start-At (0,SCM+FSA))))),(s +* ((Directed I) +* (Start-At (0,SCM+FSA)))),n)) in dom (Directed I) by A15, A4, A17, SCMFSA8A:31; :: thesis: CurInstr ((ProgramPart (Comput ((ProgramPart (s +* ((Directed I) +* (Start-At (0,SCM+FSA))))),(s +* ((Directed I) +* (Start-At (0,SCM+FSA)))),n))),(Comput ((ProgramPart (s +* ((Directed I) +* (Start-At (0,SCM+FSA))))),(s +* ((Directed I) +* (Start-At (0,SCM+FSA)))),n))) <> halt SCM+FSA
thus CurInstr ((ProgramPart (Comput ((ProgramPart (s +* ((Directed I) +* (Start-At (0,SCM+FSA))))),(s +* ((Directed I) +* (Start-At (0,SCM+FSA)))),n))),(Comput ((ProgramPart (s +* ((Directed I) +* (Start-At (0,SCM+FSA))))),(s +* ((Directed I) +* (Start-At (0,SCM+FSA)))),n))) <> halt SCM+FSA by A15, A4, A17, SCMFSA8A:31; :: thesis: verum
end;
A18: now
let n be Element of NAT ; :: thesis: ( CurInstr ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(Comput ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),n))) = halt SCM+FSA implies not k > n )
assume A19: CurInstr ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(Comput ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),n))) = halt SCM+FSA ; :: thesis: not k > n
reconsider l = IC (Comput ((ProgramPart (s +* ((Directed I) +* (Start-At (0,SCM+FSA))))),(s +* ((Directed I) +* (Start-At (0,SCM+FSA)))),n)) as Element of NAT ;
Z: (ProgramPart (Comput ((ProgramPart (s +* ((Directed I) +* (Start-At (0,SCM+FSA))))),(s +* ((Directed I) +* (Start-At (0,SCM+FSA)))),n))) /. (IC (Comput ((ProgramPart (s +* ((Directed I) +* (Start-At (0,SCM+FSA))))),(s +* ((Directed I) +* (Start-At (0,SCM+FSA)))),n))) = (Comput ((ProgramPart (s +* ((Directed I) +* (Start-At (0,SCM+FSA))))),(s +* ((Directed I) +* (Start-At (0,SCM+FSA)))),n)) . (IC (Comput ((ProgramPart (s +* ((Directed I) +* (Start-At (0,SCM+FSA))))),(s +* ((Directed I) +* (Start-At (0,SCM+FSA)))),n))) by COMPOS_1:38;
TX10: ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))) = ProgramPart (Comput ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),n)) by AMI_1:123;
assume A20: k > n ; :: thesis: contradiction
then A21: l in dom (Directed I) by A3, A14, SCMFSA8A:def 5;
CurInstr ((ProgramPart (Comput ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),n))),(Comput ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),n))) = CurInstr ((ProgramPart (Comput ((ProgramPart (s +* ((Directed I) +* (Start-At (0,SCM+FSA))))),(s +* ((Directed I) +* (Start-At (0,SCM+FSA)))),n))),(Comput ((ProgramPart (s +* ((Directed I) +* (Start-At (0,SCM+FSA))))),(s +* ((Directed I) +* (Start-At (0,SCM+FSA)))),n))) by A16, A20
.= (s +* ((Directed I) +* (Start-At (0,SCM+FSA)))) . l by Z, AMI_1:54
.= (Directed I) . l by A21, Th26 ;
then halt SCM+FSA in rng (Directed I) by A19, A21, TX10, FUNCT_1:def 5;
hence contradiction by COMPOS_1:def 7; :: thesis: verum
end;
z: card (Stop SCM+FSA) = 1 by COMPOS_1:46;
then card (I ';' (Stop SCM+FSA)) = (card I) + 1 by SCMFSA6A:61;
then card I < card (I ';' (Stop SCM+FSA)) by NAT_1:13;
then A22: card I in dom (I ';' (Stop SCM+FSA)) by AFINSQ_1:70;
card I < (card I) + (card (Stop SCM+FSA)) by z, NAT_1:13;
then (I ';' (Stop SCM+FSA)) . (card I) = IncAddr ((halt SCM+FSA),(card I)) by A1, Th13
.= halt SCM+FSA by SCMFSA_4:8 ;
then A23: (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))) . (card I) = halt SCM+FSA by A22, Th26;
A24: for n being Element of NAT st S1[n] holds
S1[n + 1]
proof
let n be Element of NAT ; :: thesis: ( S1[n] implies S1[n + 1] )
assume A25: S1[n] ; :: thesis: S1[n + 1]
Z: (ProgramPart (Comput ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),(n + 1)))) /. (IC (Comput ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),(n + 1)))) = (Comput ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),(n + 1))) . (IC (Comput ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),(n + 1)))) by COMPOS_1:38;
assume A26: k <= n + 1 ; :: thesis: ( IC (Comput ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),(n + 1))) = card I & CurInstr ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(Comput ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),(n + 1)))) = halt SCM+FSA )
TX: ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))) = ProgramPart (Comput ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),(n + 1))) by AMI_1:123;
hereby :: thesis: CurInstr ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(Comput ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),(n + 1)))) = halt SCM+FSA
per cases ( k = n + 1 or k <= n ) by A26, NAT_1:8;
suppose k = n + 1 ; :: thesis: IC (Comput ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),(n + 1))) = card I
hence IC (Comput ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),(n + 1))) = IC (Comput ((ProgramPart (s +* ((Directed I) +* (Start-At (0,SCM+FSA))))),(s +* ((Directed I) +* (Start-At (0,SCM+FSA)))),k)) by A12
.= card (ProgramPart (Directed I)) by A3, A14, SCMFSA8A:def 5
.= card (Directed I) by RELAT_1:209
.= card I by SCMFSA8A:34 ;
:: thesis: verum
end;
suppose A27: k <= n ; :: thesis: IC (Comput ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),(n + 1))) = card I
Comput ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),(n + 1)) = Following ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(Comput ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),n))) by EXTPRO_1:4
.= Exec ((CurInstr ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(Comput ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),n)))),(Comput ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),n))) ;
hence IC (Comput ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),(n + 1))) = card I by A25, A27, EXTPRO_1:def 3; :: thesis: verum
end;
end;
end;
hence CurInstr ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(Comput ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),(n + 1)))) = halt SCM+FSA by A23, Z, TX, AMI_1:54; :: thesis: verum
end;
Y: (ProgramPart (Comput ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),0))) /. (IC (Comput ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),0))) = (Comput ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),0)) . (IC (Comput ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),0))) by COMPOS_1:38;
TX0: ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))) = ProgramPart (Comput ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),0)) by AMI_1:123;
A28: S1[ 0 ]
proof
assume k <= 0 ; :: thesis: ( IC (Comput ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),0)) = card I & CurInstr ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(Comput ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),0))) = halt SCM+FSA )
then k = 0 ;
hence IC (Comput ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),0)) = IC (Comput ((ProgramPart (s +* ((Directed I) +* (Start-At (0,SCM+FSA))))),(s +* ((Directed I) +* (Start-At (0,SCM+FSA)))),k)) by A12
.= card (ProgramPart (Directed I)) by A3, A14, SCMFSA8A:def 5
.= card (Directed I) by RELAT_1:209
.= card I by SCMFSA8A:34 ;
:: thesis: CurInstr ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(Comput ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),0))) = halt SCM+FSA
hence CurInstr ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(Comput ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),0))) = halt SCM+FSA by A23, Y, TX0, EXTPRO_1:3; :: thesis: verum
end;
A29: for n being Element of NAT holds S1[n] from NAT_1:sch 1(A28, A24);
now
let n be Element of NAT ; :: thesis: IC (Comput ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),b1)) in dom (I ';' (Stop SCM+FSA))
per cases ( n < k or k <= n ) ;
suppose A30: n < k ; :: thesis: IC (Comput ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),b1)) in dom (I ';' (Stop SCM+FSA))
then IC (Comput ((ProgramPart (s +* ((Directed I) +* (Start-At (0,SCM+FSA))))),(s +* ((Directed I) +* (Start-At (0,SCM+FSA)))),n)) = IC (Comput ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),n)) by A12;
then IC (Comput ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),n)) in dom (Directed I) by A3, A14, A30, SCMFSA8A:def 5;
hence IC (Comput ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),n)) in dom (I ';' (Stop SCM+FSA)) by A8; :: thesis: verum
end;
end;
end;
hence I ';' (Stop SCM+FSA) is_closed_on s by SCMFSA7B:def 7; :: thesis: ( I ';' (Stop SCM+FSA) is_halting_on s & LifeSpan ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))) = pseudo-LifeSpan (s,(Directed I)) & ( for n being Element of NAT st n < pseudo-LifeSpan (s,(Directed I)) holds
IC (Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),n)) = IC (Comput ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),n)) ) & ( for n being Element of NAT st n <= pseudo-LifeSpan (s,(Directed I)) holds
DataPart (Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),n)) = DataPart (Comput ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),n)) ) )
set s1 = s +* (I +* (Start-At (0,SCM+FSA)));
A31: card (ProgramPart (Directed I)) = card (Directed I) by RELAT_1:209
.= card I by SCMFSA8A:34 ;
S1[k] by A29;
then A32: ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))) halts_on s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))) by EXTPRO_1:30;
hence I ';' (Stop SCM+FSA) is_halting_on s by SCMFSA7B:def 8; :: thesis: ( LifeSpan ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))) = pseudo-LifeSpan (s,(Directed I)) & ( for n being Element of NAT st n < pseudo-LifeSpan (s,(Directed I)) holds
IC (Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),n)) = IC (Comput ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),n)) ) & ( for n being Element of NAT st n <= pseudo-LifeSpan (s,(Directed I)) holds
DataPart (Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),n)) = DataPart (Comput ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),n)) ) )
CurInstr ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(Comput ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),k))) = halt SCM+FSA by A29;
then A33: LifeSpan ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))) = k by A32, A18, EXTPRO_1:def 14;
defpred S2[ Nat] means ( $1 < pseudo-LifeSpan (s,(Directed I)) implies ( IC (Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),$1)) in dom I & IC (Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),$1)) = IC (Comput ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),$1)) & DataPart (Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),$1)) = DataPart (Comput ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),$1)) ) );
A34: for n being Element of NAT st S2[n] holds
S2[n + 1]
proof
let n be Element of NAT ; :: thesis: ( S2[n] implies S2[n + 1] )
set l = IC (Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),n));
set l0 = IC (Comput ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),n));
assume A35: S2[n] ; :: thesis: S2[n + 1]
assume A36: n + 1 < pseudo-LifeSpan (s,(Directed I)) ; :: thesis: ( IC (Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),(n + 1))) in dom I & IC (Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),(n + 1))) = IC (Comput ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),(n + 1))) & DataPart (Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),(n + 1))) = DataPart (Comput ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),(n + 1))) )
then A37: IC (Comput ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),n)) in dom (Directed I) by A35, FUNCT_4:105, NAT_1:12;
A38: for f being FinSeq-Location holds (Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),n)) . f = (Comput ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),n)) . f by A35, A36, NAT_1:12, SCMFSA6A:38;
for a being Int-Location holds (Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),n)) . a = (Comput ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),n)) . a by A35, A36, NAT_1:12, SCMFSA6A:38;
then A39: Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),n), Comput ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),n) equal_outside NAT by A35, A36, A38, NAT_1:12, SCMFSA10:91;
A40: now
A41: dom I = dom (Directed I) by FUNCT_4:105;
assume A42: I . (IC (Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),n))) = halt SCM+FSA ; :: thesis: contradiction
Y: (ProgramPart (Comput ((ProgramPart (s +* ((Directed I) +* (Start-At (0,SCM+FSA))))),(s +* ((Directed I) +* (Start-At (0,SCM+FSA)))),n))) /. (IC (Comput ((ProgramPart (s +* ((Directed I) +* (Start-At (0,SCM+FSA))))),(s +* ((Directed I) +* (Start-At (0,SCM+FSA)))),n))) = (Comput ((ProgramPart (s +* ((Directed I) +* (Start-At (0,SCM+FSA))))),(s +* ((Directed I) +* (Start-At (0,SCM+FSA)))),n)) . (IC (Comput ((ProgramPart (s +* ((Directed I) +* (Start-At (0,SCM+FSA))))),(s +* ((Directed I) +* (Start-At (0,SCM+FSA)))),n))) by COMPOS_1:38;
n < k by A14, A36, NAT_1:12;
then A43: CurInstr ((ProgramPart (Comput ((ProgramPart (s +* ((Directed I) +* (Start-At (0,SCM+FSA))))),(s +* ((Directed I) +* (Start-At (0,SCM+FSA)))),n))),(Comput ((ProgramPart (s +* ((Directed I) +* (Start-At (0,SCM+FSA))))),(s +* ((Directed I) +* (Start-At (0,SCM+FSA)))),n))) = (Comput ((ProgramPart (s +* ((Directed I) +* (Start-At (0,SCM+FSA))))),(s +* ((Directed I) +* (Start-At (0,SCM+FSA)))),n)) . (IC (Comput ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),n))) by A12, Y
.= (s +* ((Directed I) +* (Start-At (0,SCM+FSA)))) . (IC (Comput ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),n))) by AMI_1:54
.= (Directed I) . (IC (Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),n))) by A35, A36, A41, Th26, NAT_1:12
.= goto (card I) by A35, A36, A42, NAT_1:12, SCMFSA8A:30 ;
T: ProgramPart (s +* ((Directed I) +* (Start-At (0,SCM+FSA)))) = ProgramPart (Comput ((ProgramPart (s +* ((Directed I) +* (Start-At (0,SCM+FSA))))),(s +* ((Directed I) +* (Start-At (0,SCM+FSA)))),n)) by AMI_1:123;
A44: IC (Comput ((ProgramPart (s +* ((Directed I) +* (Start-At (0,SCM+FSA))))),(s +* ((Directed I) +* (Start-At (0,SCM+FSA)))),(n + 1))) = IC (Following ((ProgramPart (s +* ((Directed I) +* (Start-At (0,SCM+FSA))))),(Comput ((ProgramPart (s +* ((Directed I) +* (Start-At (0,SCM+FSA))))),(s +* ((Directed I) +* (Start-At (0,SCM+FSA)))),n)))) by EXTPRO_1:4
.= card I by A43, T, SCMFSA_2:95
.= card (Directed I) by SCMFSA8A:34 ;
IC (Comput ((ProgramPart (s +* ((Directed I) +* (Start-At (0,SCM+FSA))))),(s +* ((Directed I) +* (Start-At (0,SCM+FSA)))),(n + 1))) in dom (Directed I) by A3, A36, SCMFSA8A:31;
hence contradiction by A44; :: thesis: verum
end;
Y: (ProgramPart (Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),n))) /. (IC (Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),n))) = (Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),n)) . (IC (Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),n))) by COMPOS_1:38;
U: (ProgramPart (Comput ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),n))) /. (IC (Comput ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),n))) = (Comput ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),n)) . (IC (Comput ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),n))) by COMPOS_1:38;
A45: CurInstr ((ProgramPart (Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),n))),(Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),n))) = (s +* (I +* (Start-At (0,SCM+FSA)))) . (IC (Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),n))) by Y, AMI_1:54
.= I . (IC (Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),n))) by A35, A36, Th26, NAT_1:12
.= (Directed I) . (IC (Comput ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),n))) by A35, A36, A40, NAT_1:12, SCMFSA8A:30
.= (I ';' (Stop SCM+FSA)) . (IC (Comput ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),n))) by A7, A37, GRFUNC_1:8
.= (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))) . (IC (Comput ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),n))) by A8, A37, Th26
.= CurInstr ((ProgramPart (Comput ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),n))),(Comput ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),n))) by U, AMI_1:54 ;
T: ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))) = ProgramPart (Comput ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),n)) by AMI_1:123;
A46: Comput ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),(n + 1)) = Following ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(Comput ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),n))) by EXTPRO_1:4
.= Exec ((CurInstr ((ProgramPart (Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),n))),(Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),n)))),(Comput ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),n))) by A45, T ;
pseudo-LifeSpan (s,(Directed I)) = k by A3, Th50;
then A47: IC (Comput ((ProgramPart (s +* ((Directed I) +* (Start-At (0,SCM+FSA))))),(s +* ((Directed I) +* (Start-At (0,SCM+FSA)))),(n + 1))) = IC (Comput ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),(n + 1))) by A12, A36;
A48: dom (Directed I) = dom I by FUNCT_4:105;
T: ProgramPart (s +* (I +* (Start-At (0,SCM+FSA)))) = ProgramPart (Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),n)) by AMI_1:123;
A49: Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),(n + 1)) = Following ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),n))) by EXTPRO_1:4
.= Exec ((CurInstr ((ProgramPart (Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),n))),(Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),n)))),(Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),n))) by T ;
then A50: for f being FinSeq-Location holds (Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),(n + 1))) . f = (Comput ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),(n + 1))) . f by A46, A39, SCMFSA10:93, SCMFSA6A:32;
IC (Comput ((ProgramPart (s +* ((Directed I) +* (Start-At (0,SCM+FSA))))),(s +* ((Directed I) +* (Start-At (0,SCM+FSA)))),(n + 1))) in dom (Directed I) by A3, A36, SCMFSA8A:31;
hence IC (Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),(n + 1))) in dom I by A47, A49, A46, A39, A48, COMPOS_1:24, SCMFSA6A:32; :: thesis: ( IC (Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),(n + 1))) = IC (Comput ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),(n + 1))) & DataPart (Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),(n + 1))) = DataPart (Comput ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),(n + 1))) )
thus IC (Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),(n + 1))) = IC (Comput ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),(n + 1))) by A49, A46, A39, COMPOS_1:24, SCMFSA6A:32; :: thesis: DataPart (Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),(n + 1))) = DataPart (Comput ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),(n + 1)))
for a being Int-Location holds (Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),(n + 1))) . a = (Comput ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),(n + 1))) . a by A49, A46, A39, SCMFSA10:92, SCMFSA6A:32;
hence DataPart (Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),(n + 1))) = DataPart (Comput ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),(n + 1))) by A50, SCMFSA6A:38; :: thesis: verum
end;
IC (Comput ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),k)) = card I by A29;
then A51: IC (Comput ((ProgramPart (s +* ((Directed I) +* (Start-At (0,SCM+FSA))))),(s +* ((Directed I) +* (Start-At (0,SCM+FSA)))),(LifeSpan ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))))))) = card I by A12, A33;
for n being Element of NAT st not IC (Comput ((ProgramPart (s +* ((Directed I) +* (Start-At (0,SCM+FSA))))),(s +* ((Directed I) +* (Start-At (0,SCM+FSA)))),n)) in dom (Directed I) holds
LifeSpan ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))) <= n by A16, A33;
hence LifeSpan ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))) = pseudo-LifeSpan (s,(Directed I)) by A3, A51, A31, SCMFSA8A:def 5; :: thesis: ( ( for n being Element of NAT st n < pseudo-LifeSpan (s,(Directed I)) holds
IC (Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),n)) = IC (Comput ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),n)) ) & ( for n being Element of NAT st n <= pseudo-LifeSpan (s,(Directed I)) holds
DataPart (Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),n)) = DataPart (Comput ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),n)) ) )
A52: S2[ 0 ]
proof
A53: IC (Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),0)) = IC (s +* (I +* (Start-At (0,SCM+FSA)))) by EXTPRO_1:3
.= IC ((s +* I) +* (Start-At (0,SCM+FSA))) by FUNCT_4:15
.= 0 by FUNCT_4:121 ;
assume 0 < pseudo-LifeSpan (s,(Directed I)) ; :: thesis: ( IC (Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),0)) in dom I & IC (Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),0)) = IC (Comput ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),0)) & DataPart (Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),0)) = DataPart (Comput ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),0)) )
then IC (Comput ((ProgramPart (s +* ((Directed I) +* (Start-At (0,SCM+FSA))))),(s +* ((Directed I) +* (Start-At (0,SCM+FSA)))),0)) in dom (Directed I) by A3, SCMFSA8A:31;
then IC (s +* ((Directed I) +* (Start-At (0,SCM+FSA)))) in dom (Directed I) by EXTPRO_1:3;
then 0 in dom (Directed I) by Th31;
hence IC (Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),0)) in dom I by A53, FUNCT_4:105; :: thesis: ( IC (Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),0)) = IC (Comput ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),0)) & DataPart (Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),0)) = DataPart (Comput ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),0)) )
thus IC (Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),0)) = IC (Comput ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),0)) by A10, A53, EXTPRO_1:3; :: thesis: DataPart (Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),0)) = DataPart (Comput ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),0))
thus DataPart (Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),0)) = DataPart (s +* (I +* (Start-At (0,SCM+FSA)))) by EXTPRO_1:3
.= DataPart s by SCMFSA8A:11
.= DataPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))) by SCMFSA8A:11
.= DataPart (Comput ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),0)) by EXTPRO_1:3 ; :: thesis: verum
end;
A54: for n being Element of NAT holds S2[n] from NAT_1:sch 1(A52, A34);
 hence for n being Element of NAT st n < pseudo-LifeSpan (s,(Directed I)) holds
IC (Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),n)) = IC (Comput ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),n)) ; :: thesis: for n being Element of NAT st n <= pseudo-LifeSpan (s,(Directed I)) holds
DataPart (Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),n)) = DataPart (Comput ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),n))
let n be Element of NAT ; :: thesis: ( n <= pseudo-LifeSpan (s,(Directed I)) implies DataPart (Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),n)) = DataPart (Comput ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),n)) )
assume A55: n <= pseudo-LifeSpan (s,(Directed I)) ; :: thesis: DataPart (Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),n)) = DataPart (Comput ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),n))
per cases ( n < pseudo-LifeSpan (s,(Directed I)) or n = pseudo-LifeSpan (s,(Directed I)) ) by A55, XXREAL_0:1;
suppose n < pseudo-LifeSpan (s,(Directed I)) ; :: thesis: DataPart (Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),n)) = DataPart (Comput ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),n))
hence DataPart (Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),n)) = DataPart (Comput ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),n)) by A54; :: thesis: verum
end;
suppose A56: n = pseudo-LifeSpan (s,(Directed I)) ; :: thesis: DataPart (Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),n)) = DataPart (Comput ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),n))
hereby :: thesis: verum
per cases ( n = 0 or ex m being Nat st n = m + 1 ) by NAT_1:6;
suppose ex m being Nat st n = m + 1 ; :: thesis: DataPart (Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),n)) = DataPart (Comput ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),n))
then consider m being Nat such that
A58: n = m + 1 ;
reconsider m = m as Element of NAT by ORDINAL1:def 13;
T: ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))) = ProgramPart (Comput ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),m)) by AMI_1:123;
A59: Comput ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),n) = Following ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(Comput ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),m))) by A58, EXTPRO_1:4
.= Exec ((CurInstr ((ProgramPart (Comput ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),m))),(Comput ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),m)))),(Comput ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),m))) by T ;
set i = CurInstr ((ProgramPart (Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),m))),(Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),m)));
T: ProgramPart (s +* (I +* (Start-At (0,SCM+FSA)))) = ProgramPart (Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),m)) by AMI_1:123;
A60: Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),n) = Following ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),m))) by A58, EXTPRO_1:4
.= Exec ((CurInstr ((ProgramPart (Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),m))),(Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),m)))),(Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),m))) by T ;
set l0 = IC (Comput ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),m));
set l = IC (Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),m));
A61: m + 0 < pseudo-LifeSpan (s,(Directed I)) by A56, A58, XREAL_1:8;
then A62: IC (Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),m)) = IC (Comput ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),m)) by A54;
A63: IC (Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),m)) in dom I by A54, A61;
then A64: IC (Comput ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),m)) in dom (Directed I) by A62, FUNCT_4:105;
Y: (ProgramPart (Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),m))) /. (IC (Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),m))) = (Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),m)) . (IC (Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),m))) by COMPOS_1:38;
Z: (ProgramPart (Comput ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),m))) /. (IC (Comput ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),m))) = (Comput ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),m)) . (IC (Comput ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),m))) by COMPOS_1:38;
A65: CurInstr ((ProgramPart (Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),m))),(Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),m))) = (s +* (I +* (Start-At (0,SCM+FSA)))) . (IC (Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),m))) by Y, AMI_1:54
.= I . (IC (Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),m))) by A54, A61, Th26 ;
Directed I c= I ';' (Stop SCM+FSA) by SCMFSA6A:55;
then A66: (Directed I) . (IC (Comput ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),m))) = (I ';' (Stop SCM+FSA)) . (IC (Comput ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),m))) by A64, GRFUNC_1:8
.= (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))) . (IC (Comput ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),m))) by A8, A64, Th26
.= CurInstr ((ProgramPart (Comput ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),m))),(Comput ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),m))) by Z, AMI_1:54 ;
A67: DataPart (Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),m)) = DataPart (Comput ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),m)) by A54, A61;
hereby :: thesis: verum
per cases ( CurInstr ((ProgramPart (Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),m))),(Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),m))) = halt SCM+FSA or CurInstr ((ProgramPart (Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),m))),(Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),m))) <> halt SCM+FSA ) ;
suppose A68: CurInstr ((ProgramPart (Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),m))),(Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),m))) = halt SCM+FSA ; :: thesis: DataPart (Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),n)) = DataPart (Comput ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),n))
then CurInstr ((ProgramPart (Comput ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),m))),(Comput ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),m))) = goto (card I) by A63, A62, A65, A66, SCMFSA8A:30;
then InsCode (CurInstr ((ProgramPart (Comput ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),m))),(Comput ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),m)))) = 6 by SCMFSA_2:47;
then A69: InsCode (CurInstr ((ProgramPart (Comput ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),m))),(Comput ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),m)))) in {0,6,7,8} by ENUMSET1:def 2;
thus DataPart (Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),n)) = DataPart (Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),m)) by A60, A68, EXTPRO_1:def 3
.= DataPart (Comput ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),m)) by A54, A61
.= DataPart (Comput ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),n)) by A59, A69, Th32 ; :: thesis: verum
end;
suppose CurInstr ((ProgramPart (Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),m))),(Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),m))) <> halt SCM+FSA ; :: thesis: DataPart (Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),n)) = DataPart (Comput ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),n))
then CurInstr ((ProgramPart (Comput ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),m))),(Comput ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),m))) = CurInstr ((ProgramPart (Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),m))),(Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),m))) by A63, A62, A65, A66, SCMFSA8A:30;
hence DataPart (Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),n)) = DataPart (Comput ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),n)) by A60, A59, A67, SCMFSA6C:5; :: thesis: verum
end;
end;
end;
end;
end;
end;
end;
end;