let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty stored-program IC-Ins-separated definite standard-ins standard homogeneous regular J/A-independent AMI-Struct of N
for F being NAT -defined the Instructions of b₁ -valued non empty initial FinPartState of
for G being NAT -defined the Instructions of b₁ -valued non empty FinPartState of holds
( card (F ';' G) = ((card F) + (card G)) - 1 & card (F ';' G) = ((card F) + (card G)) -' 1 )
let S be non empty stored-program IC-Ins-separated definite standard-ins standard homogeneous regular J/A-independent AMI-Struct of N; :: thesis: for F being NAT -defined the Instructions of S -valued non empty initial FinPartState of
for G being NAT -defined the Instructions of S -valued non empty FinPartState of holds
( card (F ';' G) = ((card F) + (card G)) - 1 & card (F ';' G) = ((card F) + (card G)) -' 1 )
let F be NAT -defined the Instructions of S -valued non empty initial FinPartState of ; :: thesis: for G being NAT -defined the Instructions of S -valued non empty FinPartState of holds
( card (F ';' G) = ((card F) + (card G)) - 1 & card (F ';' G) = ((card F) + (card G)) -' 1 )
let G be NAT -defined the Instructions of S -valued non empty FinPartState of ; :: thesis: ( card (F ';' G) = ((card F) + (card G)) - 1 & card (F ';' G) = ((card F) + (card G)) -' 1 )
set k = (card F) -' 1;
dom (IncAddr G,((card F) -' 1)), dom (Shift (IncAddr G,((card F) -' 1)),((card F) -' 1)) are_equipotent by VALUED_1:28;
then A1: IncAddr G,((card F) -' 1), Shift (IncAddr G,((card F) -' 1)),((card F) -' 1) are_equipotent by PRE_CIRC:26;
dom (CutLastLoc F) misses dom (Shift (IncAddr G,((card F) -' 1)),((card F) -' 1)) by Th50;
hence card (F ';' G) = (card (CutLastLoc F)) + (card (Shift (IncAddr G,((card F) -' 1)),((card F) -' 1))) by PRE_CIRC:27
.= (card (CutLastLoc F)) + (card (IncAddr G,((card F) -' 1))) by A1, CARD_1:21
.= (card (CutLastLoc F)) + (card (dom (IncAddr G,((card F) -' 1)))) by CARD_1:104
.= (card (CutLastLoc F)) + (card (dom G)) by Def15
.= (card (CutLastLoc F)) + (card G) by CARD_1:104
.= ((card F) - 1) + (card G) by VALUED_1:39
.= ((card F) + (card G)) - 1 ;
:: thesis: card (F ';' G) = ((card F) + (card G)) -' 1
hence card (F ';' G) = ((card F) + (card G)) -' 1 by XREAL_0:def 2; :: thesis: verum