let p be Instruction-Sequence of SCM+FSA; :: thesis: for s being State of SCM+FSA
for I being good InitHalting Program of SCM+FSA
for a being read-write Int-Location st not I destroys a & s . a > 0 holds
ex s2 being State of SCM+FSA ex p2 being Instruction-Sequence of SCM+FSA ex k being Element of NAT st
( s2 = Initialized s & p2 = p +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) & k = (LifeSpan ((p +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialized s))) + 1 & (Comput (p2,s2,k)) . a = (s . a) - 1 & (Comput (p2,s2,k)) . (intloc 0) = 1 & ( for b being read-write Int-Location st b <> a holds
(Comput (p2,s2,k)) . b = (IExec (I,p,s)) . b ) & ( for f being FinSeq-Location holds (Comput (p2,s2,k)) . f = (IExec (I,p,s)) . f ) & IC (Comput (p2,s2,k)) = 0 & ( for n being Element of NAT st n <= k holds
IC (Comput (p2,s2,n)) in dom (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ) )
let s be State of SCM+FSA; :: thesis: for I being good InitHalting Program of SCM+FSA
for a being read-write Int-Location st not I destroys a & s . a > 0 holds
ex s2 being State of SCM+FSA ex p2 being Instruction-Sequence of SCM+FSA ex k being Element of NAT st
( s2 = Initialized s & p2 = p +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) & k = (LifeSpan ((p +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialized s))) + 1 & (Comput (p2,s2,k)) . a = (s . a) - 1 & (Comput (p2,s2,k)) . (intloc 0) = 1 & ( for b being read-write Int-Location st b <> a holds
(Comput (p2,s2,k)) . b = (IExec (I,p,s)) . b ) & ( for f being FinSeq-Location holds (Comput (p2,s2,k)) . f = (IExec (I,p,s)) . f ) & IC (Comput (p2,s2,k)) = 0 & ( for n being Element of NAT st n <= k holds
IC (Comput (p2,s2,n)) in dom (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ) )
let I be good InitHalting Program of SCM+FSA; :: thesis: for a being read-write Int-Location st not I destroys a & s . a > 0 holds
ex s2 being State of SCM+FSA ex p2 being Instruction-Sequence of SCM+FSA ex k being Element of NAT st
( s2 = Initialized s & p2 = p +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) & k = (LifeSpan ((p +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialized s))) + 1 & (Comput (p2,s2,k)) . a = (s . a) - 1 & (Comput (p2,s2,k)) . (intloc 0) = 1 & ( for b being read-write Int-Location st b <> a holds
(Comput (p2,s2,k)) . b = (IExec (I,p,s)) . b ) & ( for f being FinSeq-Location holds (Comput (p2,s2,k)) . f = (IExec (I,p,s)) . f ) & IC (Comput (p2,s2,k)) = 0 & ( for n being Element of NAT st n <= k holds
IC (Comput (p2,s2,n)) in dom (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ) )
let a be read-write Int-Location ; :: thesis: ( not I destroys a & s . a > 0 implies ex s2 being State of SCM+FSA ex p2 being Instruction-Sequence of SCM+FSA ex k being Element of NAT st
( s2 = Initialized s & p2 = p +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) & k = (LifeSpan ((p +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialized s))) + 1 & (Comput (p2,s2,k)) . a = (s . a) - 1 & (Comput (p2,s2,k)) . (intloc 0) = 1 & ( for b being read-write Int-Location st b <> a holds
(Comput (p2,s2,k)) . b = (IExec (I,p,s)) . b ) & ( for f being FinSeq-Location holds (Comput (p2,s2,k)) . f = (IExec (I,p,s)) . f ) & IC (Comput (p2,s2,k)) = 0 & ( for n being Element of NAT st n <= k holds
IC (Comput (p2,s2,n)) in dom (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ) ) )
assume A1: not I destroys a ; :: thesis: ( not s . a > 0 or ex s2 being State of SCM+FSA ex p2 being Instruction-Sequence of SCM+FSA ex k being Element of NAT st
( s2 = Initialized s & p2 = p +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) & k = (LifeSpan ((p +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialized s))) + 1 & (Comput (p2,s2,k)) . a = (s . a) - 1 & (Comput (p2,s2,k)) . (intloc 0) = 1 & ( for b being read-write Int-Location st b <> a holds
(Comput (p2,s2,k)) . b = (IExec (I,p,s)) . b ) & ( for f being FinSeq-Location holds (Comput (p2,s2,k)) . f = (IExec (I,p,s)) . f ) & IC (Comput (p2,s2,k)) = 0 & ( for n being Element of NAT st n <= k holds
IC (Comput (p2,s2,n)) in dom (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ) ) )
reconsider I1 = I ';' (SubFrom (a,(intloc 0))) as InitHalting Program of SCM+FSA ;
set P = if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))));
assume A2: s . a > 0 ; :: thesis: ex s2 being State of SCM+FSA ex p2 being Instruction-Sequence of SCM+FSA ex k being Element of NAT st
( s2 = Initialized s & p2 = p +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) & k = (LifeSpan ((p +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialized s))) + 1 & (Comput (p2,s2,k)) . a = (s . a) - 1 & (Comput (p2,s2,k)) . (intloc 0) = 1 & ( for b being read-write Int-Location st b <> a holds
(Comput (p2,s2,k)) . b = (IExec (I,p,s)) . b ) & ( for f being FinSeq-Location holds (Comput (p2,s2,k)) . f = (IExec (I,p,s)) . f ) & IC (Comput (p2,s2,k)) = 0 & ( for n being Element of NAT st n <= k holds
IC (Comput (p2,s2,n)) in dom (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ) )
set Is = Initialized (Initialized s);
take s2 = Initialized s; :: thesis: ex p2 being Instruction-Sequence of SCM+FSA ex k being Element of NAT st
( s2 = Initialized s & p2 = p +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) & k = (LifeSpan ((p +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialized s))) + 1 & (Comput (p2,s2,k)) . a = (s . a) - 1 & (Comput (p2,s2,k)) . (intloc 0) = 1 & ( for b being read-write Int-Location st b <> a holds
(Comput (p2,s2,k)) . b = (IExec (I,p,s)) . b ) & ( for f being FinSeq-Location holds (Comput (p2,s2,k)) . f = (IExec (I,p,s)) . f ) & IC (Comput (p2,s2,k)) = 0 & ( for n being Element of NAT st n <= k holds
IC (Comput (p2,s2,n)) in dom (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ) )
take p2 = p +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))); :: thesis: ex k being Element of NAT st
( s2 = Initialized s & p2 = p +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) & k = (LifeSpan ((p +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialized s))) + 1 & (Comput (p2,s2,k)) . a = (s . a) - 1 & (Comput (p2,s2,k)) . (intloc 0) = 1 & ( for b being read-write Int-Location st b <> a holds
(Comput (p2,s2,k)) . b = (IExec (I,p,s)) . b ) & ( for f being FinSeq-Location holds (Comput (p2,s2,k)) . f = (IExec (I,p,s)) . f ) & IC (Comput (p2,s2,k)) = 0 & ( for n being Element of NAT st n <= k holds
IC (Comput (p2,s2,n)) in dom (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ) )
set s1 = Initialized s;
set p1 = p +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))));
take k = (LifeSpan ((p +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialized s))) + 1; :: thesis: ( s2 = Initialized s & p2 = p +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) & k = (LifeSpan ((p +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialized s))) + 1 & (Comput (p2,s2,k)) . a = (s . a) - 1 & (Comput (p2,s2,k)) . (intloc 0) = 1 & ( for b being read-write Int-Location st b <> a holds
(Comput (p2,s2,k)) . b = (IExec (I,p,s)) . b ) & ( for f being FinSeq-Location holds (Comput (p2,s2,k)) . f = (IExec (I,p,s)) . f ) & IC (Comput (p2,s2,k)) = 0 & ( for n being Element of NAT st n <= k holds
IC (Comput (p2,s2,n)) in dom (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ) )
thus ( s2 = Initialized s & p2 = p +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) & k = (LifeSpan ((p +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialized s))) + 1 ) ; :: thesis: ( (Comput (p2,s2,k)) . a = (s . a) - 1 & (Comput (p2,s2,k)) . (intloc 0) = 1 & ( for b being read-write Int-Location st b <> a holds
(Comput (p2,s2,k)) . b = (IExec (I,p,s)) . b ) & ( for f being FinSeq-Location holds (Comput (p2,s2,k)) . f = (IExec (I,p,s)) . f ) & IC (Comput (p2,s2,k)) = 0 & ( for n being Element of NAT st n <= k holds
IC (Comput (p2,s2,n)) in dom (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ) )
A3: Initialized (Initialized s) = s +* ((Initialize ((intloc 0) .--> 1)) +* (Start-At (0,SCM+FSA))) by FUNCT_4:93
.= Initialize (Initialized s) by FUNCT_4:14 ;
A4: I1 is_halting_onInit s,p by Th36;
then A5: I1 is_halting_on Initialized s,p by Th41;
I1 is_closed_onInit s,p by Th35;
then A6: IExec ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))),p,s) = (IExec (I1,p,s)) +* (Start-At ((((card (Goto 2)) + (card I1)) + 3),SCM+FSA)) by A2, A4, Th46;
then A7: (IExec ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))),p,s)) . a = (IExec (I1,p,s)) . a by SCMFSA_3:3;
( I1 is_closed_onInit s,p & I1 is_halting_onInit s,p ) by Th35, Th36;
then A8: ( if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))) is_closed_onInit s,p & if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))) is_halting_onInit s,p ) by A2, Th45;
Comput (p2,s2,((LifeSpan ((p +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialized s))) + 1)) = Following (p2,(Comput (p2,s2,(LifeSpan ((p +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialized s)))))) by EXTPRO_1:3
.= Exec ((CurInstr (p2,(Comput (p2,s2,(LifeSpan ((p +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialized s))))))),(Comput (p2,s2,(LifeSpan ((p +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialized s)))))) ;
then A9: Comput (p2,s2,((LifeSpan ((p +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialized s))) + 1)) = Exec ((goto 0),(Comput (p2,s2,(LifeSpan ((p +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialized s)))))) by A8, Th71;
A10: ( I1 is_closed_onInit s,p & I1 is_halting_onInit s,p ) by Th35, Th36;
then if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))) is_closed_onInit s,p by A2, Th45;
then A11: if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))) is_closed_on Initialized s,p by Th40;
if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))) is_halting_onInit s,p by A2, A10, Th45;
then A12: if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))) is_halting_on Initialized s,p by Th41;
XX: Comput ((p +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialized (Initialized s)),(LifeSpan ((p +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialized (Initialized s))))) = Comput ((p +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Initialized (Initialized s)),(LifeSpan ((p +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialized (Initialized s))))) by A8, Th68;
(Comput (p2,s2,((LifeSpan ((p +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialized s))) + 1))) . a = (Comput ((p +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialized (Initialized s)),(LifeSpan ((p +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialized (Initialized s)))))) . a by XX, A9, SCMFSA_2:69
.= (IExec ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))),p,s)) . a by A3, A12, SCMFSA8C:58 ;
hence (Comput (p2,s2,k)) . a = (Comput ((p +* I1),(Initialize (Initialized s)),(LifeSpan ((p +* I1),(Initialize (Initialized s)))))) . a by A5, A7, SCMFSA8C:58
.= (s . a) - 1 by A1, Th64 ;
:: thesis: ( (Comput (p2,s2,k)) . (intloc 0) = 1 & ( for b being read-write Int-Location st b <> a holds
(Comput (p2,s2,k)) . b = (IExec (I,p,s)) . b ) & ( for f being FinSeq-Location holds (Comput (p2,s2,k)) . f = (IExec (I,p,s)) . f ) & IC (Comput (p2,s2,k)) = 0 & ( for n being Element of NAT st n <= k holds
IC (Comput (p2,s2,n)) in dom (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ) )
(Comput (p2,s2,((LifeSpan ((p +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialized s))) + 1))) . (intloc 0) = (Comput ((p +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialized (Initialized s)),(LifeSpan ((p +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialized (Initialized s)))))) . (intloc 0) by XX, A9, SCMFSA_2:69
.= 1 by A12, A11, A3, SCMFSA8C:67 ;
hence (Comput (p2,s2,k)) . (intloc 0) = 1 ; :: thesis: ( ( for b being read-write Int-Location st b <> a holds
(Comput (p2,s2,k)) . b = (IExec (I,p,s)) . b ) & ( for f being FinSeq-Location holds (Comput (p2,s2,k)) . f = (IExec (I,p,s)) . f ) & IC (Comput (p2,s2,k)) = 0 & ( for n being Element of NAT st n <= k holds
IC (Comput (p2,s2,n)) in dom (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ) )
hereby :: thesis: ( ( for f being FinSeq-Location holds (Comput (p2,s2,k)) . f = (IExec (I,p,s)) . f ) & IC (Comput (p2,s2,k)) = 0 & ( for n being Element of NAT st n <= k holds
IC (Comput (p2,s2,n)) in dom (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ) )
let b be read-write Int-Location ; :: thesis: ( b <> a implies (Comput (p2,s2,k)) . b = (IExec (I,p,s)) . b )
assume A15: b <> a ; :: thesis: (Comput (p2,s2,k)) . b = (IExec (I,p,s)) . b
thus (Comput (p2,s2,k)) . b = (Comput ((p +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialized (Initialized s)),(LifeSpan ((p +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialized (Initialized s)))))) . b by XX, A9, SCMFSA_2:69
.= (IExec ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))),p,s)) . b by A3, A12, SCMFSA8C:58
.= (IExec (I1,p,s)) . b by A6, SCMFSA_3:3
.= (Exec ((SubFrom (a,(intloc 0))),(IExec (I,p,s)))) . b by Th33
.= (IExec (I,p,s)) . b by A15, SCMFSA_2:65 ; :: thesis: verum
end;
hereby :: thesis: ( IC (Comput (p2,s2,k)) = 0 & ( for n being Element of NAT st n <= k holds
IC (Comput (p2,s2,n)) in dom (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ) )
let f be FinSeq-Location ; :: thesis: (Comput (p2,s2,k)) . f = (IExec (I,p,s)) . f
thus (Comput (p2,s2,k)) . f = (Comput ((p +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialized (Initialized s)),(LifeSpan ((p +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialized (Initialized s)))))) . f by XX, A9, SCMFSA_2:69
.= (IExec ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))),p,s)) . f by A3, A12, SCMFSA8C:58
.= (IExec (I1,p,s)) . f by A6, SCMFSA_3:4
.= (Exec ((SubFrom (a,(intloc 0))),(IExec (I,p,s)))) . f by Th34
.= (IExec (I,p,s)) . f by SCMFSA_2:65 ; :: thesis: verum
end;
thus IC (Comput (p2,s2,k)) = 0 by A9, SCMFSA_2:69; :: thesis: for n being Element of NAT st n <= k holds
IC (Comput (p2,s2,n)) in dom (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))
A16: IC (Comput (p2,s2,((LifeSpan ((p +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialized s))) + 1))) = 0 by A9, SCMFSA_2:69;
hereby :: thesis: verum
let n be Element of NAT ; :: thesis: ( n <= k implies IC (Comput (p2,s2,b1)) in dom (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) )
assume A17: n <= k ; :: thesis: IC (Comput (p2,s2,b1)) in dom (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))
per cases ( n <= LifeSpan ((p +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialized s)) or n = (LifeSpan ((p +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialized s))) + 1 ) by A17, NAT_1:8;
suppose A18: n <= LifeSpan ((p +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialized s)) ; :: thesis: IC (Comput (p2,s2,b1)) in dom (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))
A19: ( I1 is_closed_onInit s,p & I1 is_halting_onInit s,p ) by Th35, Th36;
then A20: if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))) is_closed_onInit s,p by A2, Th45;
if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))) is_halting_onInit s,p by A2, A19, Th45;
then A21: IC (Comput (p2,s2,n)) = IC (Comput ((p +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialized s),n)) by A18, A20, Th68;
IC (Comput ((p +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialized s),n)) in dom (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) by A20, Def4;
hence IC (Comput (p2,s2,n)) in dom (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) by A21, FUNCT_4:99; :: thesis: verum
end;
suppose A22: n = (LifeSpan ((p +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialized s))) + 1 ; :: thesis: IC (Comput (p2,s2,b1)) in dom (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))
A23: card (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) = ((card (Goto 2)) + (card I1)) + 4 by SCMFSA8B:11
.= ((card I1) + 1) + 4 by SCMFSA8A:15
.= ((card I1) + 3) + 2 ;
card (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) = card (dom (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))) by CARD_1:62
.= card (dom (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) by FUNCT_4:99
.= card (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) by CARD_1:62 ;
hence IC (Comput (p2,s2,n)) in dom (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) by A16, A22, A23, AFINSQ_1:66; :: thesis: verum
end;
end;
end;