let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty stored-program IC-Ins-separated definite standard-ins homogeneous regular J/A-independent COM-Struct of N
for F being non empty NAT -defined the Instructions of b₁ -valued initial FinPartState of
for G being non empty NAT -defined the Instructions of b₁ -valued 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 homogeneous regular J/A-independent COM-Struct of N; :: thesis: for F being non empty NAT -defined the Instructions of S -valued initial FinPartState of
for G being non empty NAT -defined the Instructions of S -valued FinPartState of holds
( card (F ';' G) = ((card F) + (card G)) - 1 & card (F ';' G) = ((card F) + (card G)) -' 1 )
let F be non empty NAT -defined the Instructions of S -valued initial FinPartState of ; :: thesis: for G being non empty NAT -defined the Instructions of S -valued FinPartState of holds
( card (F ';' G) = ((card F) + (card G)) - 1 & card (F ';' G) = ((card F) + (card G)) -' 1 )
let G be non empty NAT -defined the Instructions of S -valued 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 Th100;
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