:: SCM_COMP semantic presentation

begin

Lm1:  1 =  {  n where n is Element of NAT : n < 1  }
by AXIOMS:4;

Lm2:  5 =  {  n where n is Element of NAT : n < 5  }
by AXIOMS:4;

definition
func SCM-AE  ->  non empty strict with_terminals with_nonterminals with_useful_nonterminals binary DTConstrStr  means :Def1: :: SCM_COMP:def 1
( Terminals it = SCM-Data-Loc & NonTerminals it = [:1,5:] & ( for x, y, z being Symbol of it holds
( x ==> <*y,z*> iff x in [:1,5:] ) ) );
existence
 ex b1 being non empty strict with_terminals with_nonterminals with_useful_nonterminals binary DTConstrStr st
( Terminals b1 = SCM-Data-Loc & NonTerminals b1 = [:1,5:] & ( for x, y, z being Symbol of b1 holds
( x ==> <*y,z*> iff x in [:1,5:] ) ) )
proof
defpred S1[ set , set , set ] means $1 in [:1,5:];
consider G being non empty strict binary DTConstrStr  such that
A1: the carrier of G = SCM-Data-Loc \/ [:1,5:] and
A2: for x, y, z being Symbol of G holds
( x ==> <*y,z*> iff S1[x,y,z] ) from BINTREE1:sch_1();
A3: NonTerminals G =  {  t where t is Symbol of G : ex tnt being FinSequence st t ==> tnt  }  by LANG1:def_3;
A4: NonTerminals G = [:1,5:]
proof
thus  NonTerminals G c= [:1,5:] :: according to XBOOLE_0:def_10 ::_thesis: [:1,5:] c= NonTerminals G
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in NonTerminals G or x in [:1,5:] )
assume  x in NonTerminals G ; ::_thesis: x in [:1,5:]
then consider t being Symbol of G such that
A5: x = t and
A6: ex tnt being FinSequence st t ==> tnt by A3;
consider tnt being FinSequence such that
A7: t ==> tnt by A6;
 ex x1, x2 being Symbol of G st tnt = <*x1,x2*> by A7, BINTREE1:def_4;
hence  x in [:1,5:] by A2, A5, A7; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in [:1,5:] or x in NonTerminals G )
assume A8: x in [:1,5:] ; ::_thesis: x in NonTerminals G
then reconsider t = x as Symbol of G by A1, XBOOLE_0:def_3;
 t ==> <*t,t*> by A2, A8;
hence  x in NonTerminals G by A3; ::_thesis: verum
end;
then A9: G is with_nonterminals by DTCONSTR:def_4;
A10: Terminals G =  {  t where t is Symbol of G : for tnt being FinSequence holds not t ==> tnt  }  by LANG1:def_2;
A11: Terminals G = SCM-Data-Loc
proof
thus  Terminals G c= SCM-Data-Loc :: according to XBOOLE_0:def_10 ::_thesis: SCM-Data-Loc c= Terminals G
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Terminals G or x in SCM-Data-Loc )
assume  x in Terminals G ; ::_thesis: x in SCM-Data-Loc
then consider t being Symbol of G such that
A12: x = t and
A13: for tnt being FinSequence holds not t ==> tnt by A10;
assume  not x in SCM-Data-Loc ; ::_thesis: contradiction
then  t in [:1,5:] by A1, A12, XBOOLE_0:def_3;
then  t ==> <*t,t*> by A2;
hence  contradiction by A13; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in SCM-Data-Loc or x in Terminals G )
assume A14: x in SCM-Data-Loc ; ::_thesis: x in Terminals G
then A15: ex y, z being set st
( y in {1} & z in NAT & x = [y,z] ) by ZFMISC_1:84;
reconsider t = x as Symbol of G by A1, A14, XBOOLE_0:def_3;
assume  not x in Terminals G ; ::_thesis: contradiction
then consider tnt being FinSequence such that
A16: t ==> tnt by A10;
 ex x1, x2 being Symbol of G st tnt = <*x1,x2*> by A16, BINTREE1:def_4;
then  x in [:1,5:] by A2, A16;
then consider x1, x2 being set  such that
A17: x1 in 1 and
 x2 in 5 and
A18: x = [x1,x2] by ZFMISC_1:84;
 x = [0,x2] by A17, A18, CARD_1:49, TARSKI:def_1;
hence  contradiction by A15, XTUPLE_0:1; ::_thesis: verum
end;
now__::_thesis:_for_nt_being_Symbol_of_G_st_nt_in_NonTerminals_G_holds_
ex_p_being_FinSequence_of_TS_G_st_nt_==>_roots_p
A19: dl. 1 in SCM-Data-Loc by AMI_2:def_16;
A20: dl. 0 in SCM-Data-Loc by AMI_2:def_16;
then reconsider d0 = dl. 0, d1 = dl. 1 as Symbol of G by A1, A19, XBOOLE_0:def_3;
A21: root-tree d1 in TS G by A11, A19, DTCONSTR:def_1;
 root-tree d0 in TS G by A11, A20, DTCONSTR:def_1;
then reconsider p = <*(root-tree d0),(root-tree d1)*> as FinSequence of TS G by A21, FINSEQ_2:13;
let nt be Symbol of G; ::_thesis: ( nt in NonTerminals G implies ex p being FinSequence of TS G st nt ==> roots p )
assume A22: nt in NonTerminals G ; ::_thesis: ex p being FinSequence of TS G st nt ==> roots p
take p = p; ::_thesis: nt ==> roots p
roots p = <*((root-tree d0) . {}),((root-tree d1) . {})*> by DTCONSTR:6
.= <*((root-tree d0) . {}),d1*> by TREES_4:3
.= <*d0,d1*> by TREES_4:3 ;
hence  nt ==> roots p by A2, A4, A22; ::_thesis: verum
end;
then A23: G is with_useful_nonterminals by DTCONSTR:def_5;
 G is with_terminals by A11, DTCONSTR:def_3;
hence  ex b1 being non empty strict with_terminals with_nonterminals with_useful_nonterminals binary DTConstrStr st
( Terminals b1 = SCM-Data-Loc & NonTerminals b1 = [:1,5:] & ( for x, y, z being Symbol of b1 holds
( x ==> <*y,z*> iff x in [:1,5:] ) ) ) by A2, A11, A4, A9, A23; ::_thesis: verum
end;
uniqueness
 for b1, b2 being non empty strict with_terminals with_nonterminals with_useful_nonterminals binary DTConstrStr st Terminals b1 = SCM-Data-Loc & NonTerminals b1 = [:1,5:] & ( for x, y, z being Symbol of b1 holds
( x ==> <*y,z*> iff x in [:1,5:] ) ) & Terminals b2 = SCM-Data-Loc & NonTerminals b2 = [:1,5:] & ( for x, y, z being Symbol of b2 holds
( x ==> <*y,z*> iff x in [:1,5:] ) ) holds
b1 = b2
proof
let S1, S2 be non empty strict with_terminals with_nonterminals with_useful_nonterminals binary DTConstrStr ; ::_thesis: ( Terminals S1 = SCM-Data-Loc & NonTerminals S1 = [:1,5:] & ( for x, y, z being Symbol of S1 holds
( x ==> <*y,z*> iff x in [:1,5:] ) ) & Terminals S2 = SCM-Data-Loc & NonTerminals S2 = [:1,5:] & ( for x, y, z being Symbol of S2 holds
( x ==> <*y,z*> iff x in [:1,5:] ) ) implies S1 = S2 )
assume that
A24: ( Terminals S1 = SCM-Data-Loc & NonTerminals S1 = [:1,5:] ) and
A25: for x, y, z being Symbol of S1 holds
( x ==> <*y,z*> iff x in [:1,5:] ) ; ::_thesis: ( not Terminals S2 = SCM-Data-Loc or not NonTerminals S2 = [:1,5:] or ex x, y, z being Symbol of S2 st
( ( x ==> <*y,z*> implies x in [:1,5:] ) implies ( x in [:1,5:] & not x ==> <*y,z*> ) ) or S1 = S2 )
assume that
A26: ( Terminals S2 = SCM-Data-Loc & NonTerminals S2 = [:1,5:] ) and
A27: for x, y, z being Symbol of S2 holds
( x ==> <*y,z*> iff x in [:1,5:] ) ; ::_thesis: S1 = S2
A28: the carrier of S1 = (Terminals S1) \/ (NonTerminals S1) by LANG1:1
.= the carrier of S2 by A24, A26, LANG1:1 ;
 the Rules of S1 = the Rules of S2
proof
set p1 = the Rules of S1;
set p2 = the Rules of S2;
let a, b be set ; :: according to RELAT_1:def_2 ::_thesis: ( ( not [a,b] in the Rules of S1 or [a,b] in the Rules of S2 ) & ( not [a,b] in the Rules of S2 or [a,b] in the Rules of S1 ) )
hereby  ::_thesis: ( not [a,b] in the Rules of S2 or [a,b] in the Rules of S1 )
assume A29: [a,b] in the Rules of S1 ; ::_thesis: [a,b] in the Rules of S2
then reconsider l = a as Symbol of S1 by ZFMISC_1:87;
reconsider r = b as Element of the carrier of S1 * by A29, ZFMISC_1:87;
A30: l ==> r by A29, LANG1:def_1;
then consider x1, x2 being Symbol of S1 such that
A31: r = <*x1,x2*> by BINTREE1:def_4;
reconsider l = l, x1 = x1, x2 = x2 as Symbol of S2 by A28;
 l in [:1,5:] by A25, A30, A31;
then  l ==> <*x1,x2*> by A27;
hence  [a,b] in the Rules of S2 by A31, LANG1:def_1; ::_thesis: verum
end;
assume A32: [a,b] in the Rules of S2 ; ::_thesis: [a,b] in the Rules of S1
then reconsider l = a as Symbol of S2 by ZFMISC_1:87;
reconsider r = b as Element of the carrier of S2 * by A32, ZFMISC_1:87;
A33: l ==> r by A32, LANG1:def_1;
then consider x1, x2 being Symbol of S2 such that
A34: r = <*x1,x2*> by BINTREE1:def_4;
reconsider l = l, x1 = x1, x2 = x2 as Symbol of S1 by A28;
 l in [:1,5:] by A27, A33, A34;
then  l ==> <*x1,x2*> by A25;
hence  [a,b] in the Rules of S1 by A34, LANG1:def_1; ::_thesis: verum
end;
hence  S1 = S2 by A28; ::_thesis: verum
end;
end;

:: deftheorem Def1 defines SCM-AE SCM_COMP:def_1_:_
 for b1 being non empty strict with_terminals with_nonterminals with_useful_nonterminals binary DTConstrStr holds
( b1 = SCM-AE iff ( Terminals b1 = SCM-Data-Loc & NonTerminals b1 = [:1,5:] & ( for x, y, z being Symbol of b1 holds
( x ==> <*y,z*> iff x in [:1,5:] ) ) ) );

definition
mode bin-term is Element of TS SCM-AE;
end;

Lm3:  NonTerminals SCM-AE = [:1,5:]
by Def1;

definition
let nt be NonTerminal of SCM-AE;
let tl, tr be bin-term;
:: original: -tree
redefine funcnt -tree (tl,tr) ->  bin-term;
coherence
 nt -tree (tl,tr) is bin-term
proof
 nt ==> <*(root-label tl),(root-label tr)*> by Def1, Lm3;
then  nt ==> roots <*tl,tr*> by BINTREE1:2;
then  nt -tree <*tl,tr*> in TS SCM-AE by DTCONSTR:def_1;
hence  nt -tree (tl,tr) is bin-term by TREES_4:def_6; ::_thesis: verum
end;
end;

definition
let t be Terminal of SCM-AE;
:: original: root-tree
redefine func root-tree t ->  bin-term;
coherence
 root-tree t is bin-term by DTCONSTR:def_1;
end;

definition
let t be Terminal of SCM-AE;
func @ t ->  Data-Location equals :: SCM_COMP:def 2
t;
coherence
 t is Data-Location
proof
reconsider t = t as Element of SCM-Data-Loc by Def1;
 t in Data-Locations by AMI_3:27;
then reconsider t = t as Object of SCM ;
 t is Data-Location by AMI_2:def_16;
hence  t is Data-Location ; ::_thesis: verum
end;
end;

:: deftheorem  defines @ SCM_COMP:def_2_:_
 for t being Terminal of SCM-AE holds @ t = t;

theorem Th1: :: SCM_COMP:1
for nt being NonTerminal of SCM-AE holds
( nt = [0,0] or nt = [0,1] or nt = [0,2] or nt = [0,3] or nt = [0,4] )
proof
let nt be NonTerminal of SCM-AE; ::_thesis: ( nt = [0,0] or nt = [0,1] or nt = [0,2] or nt = [0,3] or nt = [0,4] )
consider x, y being set  such that
A1: x in 1 and
A2: y in 5 and
A3: nt = [x,y] by Lm3, ZFMISC_1:84;
A4: x = 0 by A1, CARD_1:49, TARSKI:def_1;
consider n being Element of NAT  such that
A5: y = n and
A6: n < 5 by A2, Lm2;
 5 = 4 + 1 ;
then  n <= 4 by A6, NAT_1:13;
hence  ( nt = [0,0] or nt = [0,1] or nt = [0,2] or nt = [0,3] or nt = [0,4] ) by A3, A4, A5, NAT_1:28; ::_thesis: verum
end;

theorem :: SCM_COMP:2
( [0,0] is NonTerminal of SCM-AE & [0,1] is NonTerminal of SCM-AE & [0,2] is NonTerminal of SCM-AE & [0,3] is NonTerminal of SCM-AE & [0,4] is NonTerminal of SCM-AE )
proof
A1: ( 3 in 5 & 4 in 5 ) by Lm2;
A2: ( 1 in 5 & 2 in 5 ) by Lm2;
 ( 0 in 1 & 0 in 5 ) by Lm1, Lm2;
hence  ( [0,0] is NonTerminal of SCM-AE & [0,1] is NonTerminal of SCM-AE & [0,2] is NonTerminal of SCM-AE & [0,3] is NonTerminal of SCM-AE & [0,4] is NonTerminal of SCM-AE ) by A2, A1, Lm3, ZFMISC_1:87; ::_thesis: verum
end;

then reconsider nt0 = [0,0], nt1 = [0,1], nt2 = [0,2], nt3 = [0,3], nt4 = [0,4] as NonTerminal of SCM-AE ;

definition
let t1, t2 be bin-term;
funct1 + t2 ->  bin-term equals :: SCM_COMP:def 3
[0,0] -tree (t1,t2);
coherence
 [0,0] -tree (t1,t2) is bin-term
proof
 nt0 -tree (t1,t2) in TS SCM-AE ;
hence  [0,0] -tree (t1,t2) is bin-term ; ::_thesis: verum
end;
funct1 - t2 ->  bin-term equals :: SCM_COMP:def 4
[0,1] -tree (t1,t2);
coherence
 [0,1] -tree (t1,t2) is bin-term
proof
 nt1 -tree (t1,t2) in TS SCM-AE ;
hence  [0,1] -tree (t1,t2) is bin-term ; ::_thesis: verum
end;
funct1 * t2 ->  bin-term equals :: SCM_COMP:def 5
[0,2] -tree (t1,t2);
coherence
 [0,2] -tree (t1,t2) is bin-term
proof
 nt2 -tree (t1,t2) in TS SCM-AE ;
hence  [0,2] -tree (t1,t2) is bin-term ; ::_thesis: verum
end;
funct1 div t2 ->  bin-term equals :: SCM_COMP:def 6
[0,3] -tree (t1,t2);
coherence
 [0,3] -tree (t1,t2) is bin-term
proof
 nt3 -tree (t1,t2) in TS SCM-AE ;
hence  [0,3] -tree (t1,t2) is bin-term ; ::_thesis: verum
end;
funct1 mod t2 ->  bin-term equals :: SCM_COMP:def 7
[0,4] -tree (t1,t2);
coherence
 [0,4] -tree (t1,t2) is bin-term
proof
 nt4 -tree (t1,t2) in TS SCM-AE ;
hence  [0,4] -tree (t1,t2) is bin-term ; ::_thesis: verum
end;
end;

:: deftheorem  defines + SCM_COMP:def_3_:_
 for t1, t2 being bin-term holds t1 + t2 = [0,0] -tree (t1,t2);

:: deftheorem  defines - SCM_COMP:def_4_:_
 for t1, t2 being bin-term holds t1 - t2 = [0,1] -tree (t1,t2);

:: deftheorem  defines * SCM_COMP:def_5_:_
 for t1, t2 being bin-term holds t1 * t2 = [0,2] -tree (t1,t2);

:: deftheorem  defines div SCM_COMP:def_6_:_
 for t1, t2 being bin-term holds t1 div t2 = [0,3] -tree (t1,t2);

:: deftheorem  defines mod SCM_COMP:def_7_:_
 for t1, t2 being bin-term holds t1 mod t2 = [0,4] -tree (t1,t2);

theorem :: SCM_COMP:3
for term being bin-term holds
( ex t being Terminal of SCM-AE st term = root-tree t or ex tl, tr being bin-term st
( term = tl + tr or term = tl - tr or term = tl * tr or term = tl div tr or term = tl mod tr ) )
proof
let term be bin-term; ::_thesis: ( ex t being Terminal of SCM-AE st term = root-tree t or ex tl, tr being bin-term st
( term = tl + tr or term = tl - tr or term = tl * tr or term = tl div tr or term = tl mod tr ) )
 root-label term in the carrier of SCM-AE ;
then  term . {} in the carrier of SCM-AE by BINTREE1:def_1;
then A1: term . {} in (Terminals SCM-AE) \/ (NonTerminals SCM-AE) by LANG1:1;
percases ( term . {} in Terminals SCM-AE or term . {} in NonTerminals SCM-AE ) by A1, XBOOLE_0:def_3;
suppose term . {} in Terminals SCM-AE ; ::_thesis: ( ex t being Terminal of SCM-AE st term = root-tree t or ex tl, tr being bin-term st
( term = tl + tr or term = tl - tr or term = tl * tr or term = tl div tr or term = tl mod tr ) )
then reconsider t = term . {} as Terminal of SCM-AE ;
 term = root-tree t by DTCONSTR:9;
hence  ( ex t being Terminal of SCM-AE st term = root-tree t or ex tl, tr being bin-term st
( term = tl + tr or term = tl - tr or term = tl * tr or term = tl div tr or term = tl mod tr ) ) ; ::_thesis: verum
end;
suppose term . {} in NonTerminals SCM-AE ; ::_thesis: ( ex t being Terminal of SCM-AE st term = root-tree t or ex tl, tr being bin-term st
( term = tl + tr or term = tl - tr or term = tl * tr or term = tl div tr or term = tl mod tr ) )
then reconsider nt = term . {} as NonTerminal of SCM-AE ;
consider ts being FinSequence of TS SCM-AE such that
A2: term = nt -tree ts and
A3: nt ==> roots ts by DTCONSTR:10;
 ex x1, x2 being Symbol of SCM-AE st roots ts = <*x1,x2*> by A3, BINTREE1:def_4;
then  len (roots ts) = 2 by FINSEQ_1:44;
then A4: ( dom (roots ts) = dom ts & dom (roots ts) = Seg 2 ) by FINSEQ_1:def_3, TREES_3:def_18;
A5: 2 in Seg 2 by FINSEQ_1:2, TARSKI:def_2;
then consider tr being DecoratedTree such that
A6: tr = ts . 2 and
 (roots ts) . 2 = tr . {} by A4, TREES_3:def_18;
A7: 1 in Seg 2 by FINSEQ_1:2, TARSKI:def_2;
then consider tl being DecoratedTree such that
A8: tl = ts . 1 and
 (roots ts) . 1 = tl . {} by A4, TREES_3:def_18;
reconsider tl = tl, tr = tr as bin-term by A4, A7, A5, A8, A6, FINSEQ_2:11;
 len ts = 2 by A4, FINSEQ_1:def_3;
then  ts = <*tl,tr*> by A8, A6, FINSEQ_1:44;
then  term = nt -tree (tl,tr) by A2, TREES_4:def_6;
then  ( term = tl + tr or term = tl - tr or term = tl * tr or term = tl div tr or term = tl mod tr ) by Th1;
hence  ( ex t being Terminal of SCM-AE st term = root-tree t or ex tl, tr being bin-term st
( term = tl + tr or term = tl - tr or term = tl * tr or term = tl div tr or term = tl mod tr ) ) ; ::_thesis: verum
end;
end;
end;

definition
let o be NonTerminal of SCM-AE;
let i, j be Integer;
funco -Meaning_on (i,j) ->  Integer equals :Def8: :: SCM_COMP:def 8
i + j if o = [0,0]
i - j if o = [0,1]
i * j if o = [0,2]
i div j if o = [0,3]
i mod j if o = [0,4]
;
coherence
 ( ( o = [0,0] implies i + j is Integer ) & ( o = [0,1] implies i - j is Integer ) & ( o = [0,2] implies i * j is Integer ) & ( o = [0,3] implies i div j is Integer ) & ( o = [0,4] implies i mod j is Integer ) ) ;
consistency
 for b1 being Integer holds
( ( o = [0,0] & o = [0,1] implies ( b1 = i + j iff b1 = i - j ) ) & ( o = [0,0] & o = [0,2] implies ( b1 = i + j iff b1 = i * j ) ) & ( o = [0,0] & o = [0,3] implies ( b1 = i + j iff b1 = i div j ) ) & ( o = [0,0] & o = [0,4] implies ( b1 = i + j iff b1 = i mod j ) ) & ( o = [0,1] & o = [0,2] implies ( b1 = i - j iff b1 = i * j ) ) & ( o = [0,1] & o = [0,3] implies ( b1 = i - j iff b1 = i div j ) ) & ( o = [0,1] & o = [0,4] implies ( b1 = i - j iff b1 = i mod j ) ) & ( o = [0,2] & o = [0,3] implies ( b1 = i * j iff b1 = i div j ) ) & ( o = [0,2] & o = [0,4] implies ( b1 = i * j iff b1 = i mod j ) ) & ( o = [0,3] & o = [0,4] implies ( b1 = i div j iff b1 = i mod j ) ) )
proof
A1: ( [0,2] `2 = 2 & [0,3] `2 = 3 ) ;
 ( [0,0] `2 = 0 & [0,1] `2 = 1 ) ;
hence  for b1 being Integer holds
( ( o = [0,0] & o = [0,1] implies ( b1 = i + j iff b1 = i - j ) ) & ( o = [0,0] & o = [0,2] implies ( b1 = i + j iff b1 = i * j ) ) & ( o = [0,0] & o = [0,3] implies ( b1 = i + j iff b1 = i div j ) ) & ( o = [0,0] & o = [0,4] implies ( b1 = i + j iff b1 = i mod j ) ) & ( o = [0,1] & o = [0,2] implies ( b1 = i - j iff b1 = i * j ) ) & ( o = [0,1] & o = [0,3] implies ( b1 = i - j iff b1 = i div j ) ) & ( o = [0,1] & o = [0,4] implies ( b1 = i - j iff b1 = i mod j ) ) & ( o = [0,2] & o = [0,3] implies ( b1 = i * j iff b1 = i div j ) ) & ( o = [0,2] & o = [0,4] implies ( b1 = i * j iff b1 = i mod j ) ) & ( o = [0,3] & o = [0,4] implies ( b1 = i div j iff b1 = i mod j ) ) ) by A1, MCART_1:7; ::_thesis: verum
end;
end;

:: deftheorem Def8 defines -Meaning_on SCM_COMP:def_8_:_
 for o being NonTerminal of SCM-AE
for i, j being Integer holds
( ( o = [0,0] implies o -Meaning_on (i,j) = i + j ) & ( o = [0,1] implies o -Meaning_on (i,j) = i - j ) & ( o = [0,2] implies o -Meaning_on (i,j) = i * j ) & ( o = [0,3] implies o -Meaning_on (i,j) = i div j ) & ( o = [0,4] implies o -Meaning_on (i,j) = i mod j ) );

registration
let s be State of SCM;
let t be Terminal of SCM-AE;
clusters . t ->  integer ;
coherence
 s . t is integer
proof
 s . (@ t) = s . t ;
hence  s . t is integer ; ::_thesis: verum
end;
end;

definition
let D be non empty set ;
let f be Function of INT,D;
let x be Integer;
:: original: .
redefine funcf . x ->  Element of D;
coherence
 f . x is Element of D
proof
reconsider x = x as Element of INT by INT_1:def_2;
 f . x is Element of D ;
hence  f . x is Element of D ; ::_thesis: verum
end;
end;

set i2i = id INT;

deffunc H1( NonTerminal of SCM-AE, set , set , Integer, Integer) ->  Element of INT = (id INT) . ($1 -Meaning_on ($4,$5));

definition
let s be State of SCM;
let term be bin-term;
functerm @ s ->  Integer means :Def9: :: SCM_COMP:def 9
 ex f being Function of (TS SCM-AE),INT st
( it = f . term & ( for t being Terminal of SCM-AE holds f . (root-tree t) = s . t ) & ( for nt being NonTerminal of SCM-AE
for tl, tr being bin-term
for rtl, rtr being Symbol of SCM-AE st rtl = root-label tl & rtr = root-label tr & nt ==> <*rtl,rtr*> holds
for xl, xr being Element of INT st xl = f . tl & xr = f . tr holds
f . (nt -tree (tl,tr)) = nt -Meaning_on (xl,xr) ) );
existence
 ex b1 being Integer ex f being Function of (TS SCM-AE),INT st
( b1 = f . term & ( for t being Terminal of SCM-AE holds f . (root-tree t) = s . t ) & ( for nt being NonTerminal of SCM-AE
for tl, tr being bin-term
for rtl, rtr being Symbol of SCM-AE st rtl = root-label tl & rtr = root-label tr & nt ==> <*rtl,rtr*> holds
for xl, xr being Element of INT st xl = f . tl & xr = f . tr holds
f . (nt -tree (tl,tr)) = nt -Meaning_on (xl,xr) ) )
proof
deffunc H2( Terminal of SCM-AE) ->  Element of INT = (id INT) . (s . $1);
consider f being Function of (TS SCM-AE),INT such that
A1: ( ( for t being Terminal of SCM-AE holds f . (root-tree t) = H2(t) ) & ( for nt being NonTerminal of SCM-AE
for tl, tr being bin-term
for rtl, rtr being Symbol of SCM-AE st rtl = root-label tl & rtr = root-label tr & nt ==> <*rtl,rtr*> holds
for xl, xr being Element of INT st xl = f . tl & xr = f . tr holds
f . (nt -tree (tl,tr)) = H1(nt,rtl,rtr,xl,xr) ) ) from BINTREE1:sch_3();
reconsider IT = f . term as Element of INT ;
take  IT ; ::_thesis: ex f being Function of (TS SCM-AE),INT st
( IT = f . term & ( for t being Terminal of SCM-AE holds f . (root-tree t) = s . t ) & ( for nt being NonTerminal of SCM-AE
for tl, tr being bin-term
for rtl, rtr being Symbol of SCM-AE st rtl = root-label tl & rtr = root-label tr & nt ==> <*rtl,rtr*> holds
for xl, xr being Element of INT st xl = f . tl & xr = f . tr holds
f . (nt -tree (tl,tr)) = nt -Meaning_on (xl,xr) ) )
take  f ; ::_thesis: ( IT = f . term & ( for t being Terminal of SCM-AE holds f . (root-tree t) = s . t ) & ( for nt being NonTerminal of SCM-AE
for tl, tr being bin-term
for rtl, rtr being Symbol of SCM-AE st rtl = root-label tl & rtr = root-label tr & nt ==> <*rtl,rtr*> holds
for xl, xr being Element of INT st xl = f . tl & xr = f . tr holds
f . (nt -tree (tl,tr)) = nt -Meaning_on (xl,xr) ) )
thus  IT = f . term ; ::_thesis: ( ( for t being Terminal of SCM-AE holds f . (root-tree t) = s . t ) & ( for nt being NonTerminal of SCM-AE
for tl, tr being bin-term
for rtl, rtr being Symbol of SCM-AE st rtl = root-label tl & rtr = root-label tr & nt ==> <*rtl,rtr*> holds
for xl, xr being Element of INT st xl = f . tl & xr = f . tr holds
f . (nt -tree (tl,tr)) = nt -Meaning_on (xl,xr) ) )
hereby  ::_thesis: for nt being NonTerminal of SCM-AE
for tl, tr being bin-term
for rtl, rtr being Symbol of SCM-AE st rtl = root-label tl & rtr = root-label tr & nt ==> <*rtl,rtr*> holds
for xl, xr being Element of INT st xl = f . tl & xr = f . tr holds
f . (nt -tree (tl,tr)) = nt -Meaning_on (xl,xr)
let t be Terminal of SCM-AE; ::_thesis: f . (root-tree t) = s . t
 s . t in INT by INT_1:def_2;
then  (id INT) . (s . t) = s . t by FUNCT_1:18;
hence  f . (root-tree t) = s . t by A1; ::_thesis: verum
end;
let nt be NonTerminal of SCM-AE; ::_thesis: for tl, tr being bin-term
for rtl, rtr being Symbol of SCM-AE st rtl = root-label tl & rtr = root-label tr & nt ==> <*rtl,rtr*> holds
for xl, xr being Element of INT st xl = f . tl & xr = f . tr holds
f . (nt -tree (tl,tr)) = nt -Meaning_on (xl,xr)
let tl, tr be bin-term; ::_thesis: for rtl, rtr being Symbol of SCM-AE st rtl = root-label tl & rtr = root-label tr & nt ==> <*rtl,rtr*> holds
for xl, xr being Element of INT st xl = f . tl & xr = f . tr holds
f . (nt -tree (tl,tr)) = nt -Meaning_on (xl,xr)
let rtl, rtr be Symbol of SCM-AE; ::_thesis: ( rtl = root-label tl & rtr = root-label tr & nt ==> <*rtl,rtr*> implies for xl, xr being Element of INT st xl = f . tl & xr = f . tr holds
f . (nt -tree (tl,tr)) = nt -Meaning_on (xl,xr) )
assume A2: ( rtl = root-label tl & rtr = root-label tr & nt ==> <*rtl,rtr*> ) ; ::_thesis: for xl, xr being Element of INT st xl = f . tl & xr = f . tr holds
f . (nt -tree (tl,tr)) = nt -Meaning_on (xl,xr)
let xl, xr be Element of INT ; ::_thesis: ( xl = f . tl & xr = f . tr implies f . (nt -tree (tl,tr)) = nt -Meaning_on (xl,xr) )
 nt -Meaning_on (xl,xr) in INT by INT_1:def_2;
then  (id INT) . (nt -Meaning_on (xl,xr)) = nt -Meaning_on (xl,xr) by FUNCT_1:18;
hence  ( xl = f . tl & xr = f . tr implies f . (nt -tree (tl,tr)) = nt -Meaning_on (xl,xr) ) by A1, A2; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Integer st ex f being Function of (TS SCM-AE),INT st
( b1 = f . term & ( for t being Terminal of SCM-AE holds f . (root-tree t) = s . t ) & ( for nt being NonTerminal of SCM-AE
for tl, tr being bin-term
for rtl, rtr being Symbol of SCM-AE st rtl = root-label tl & rtr = root-label tr & nt ==> <*rtl,rtr*> holds
for xl, xr being Element of INT st xl = f . tl & xr = f . tr holds
f . (nt -tree (tl,tr)) = nt -Meaning_on (xl,xr) ) ) & ex f being Function of (TS SCM-AE),INT st
( b2 = f . term & ( for t being Terminal of SCM-AE holds f . (root-tree t) = s . t ) & ( for nt being NonTerminal of SCM-AE
for tl, tr being bin-term
for rtl, rtr being Symbol of SCM-AE st rtl = root-label tl & rtr = root-label tr & nt ==> <*rtl,rtr*> holds
for xl, xr being Element of INT st xl = f . tl & xr = f . tr holds
f . (nt -tree (tl,tr)) = nt -Meaning_on (xl,xr) ) ) holds
b1 = b2
proof
deffunc H2( Terminal of SCM-AE) ->  Element of INT = (id INT) . (s . $1);
let it1, it2 be Integer; ::_thesis: ( ex f being Function of (TS SCM-AE),INT st
( it1 = f . term & ( for t being Terminal of SCM-AE holds f . (root-tree t) = s . t ) & ( for nt being NonTerminal of SCM-AE
for tl, tr being bin-term
for rtl, rtr being Symbol of SCM-AE st rtl = root-label tl & rtr = root-label tr & nt ==> <*rtl,rtr*> holds
for xl, xr being Element of INT st xl = f . tl & xr = f . tr holds
f . (nt -tree (tl,tr)) = nt -Meaning_on (xl,xr) ) ) & ex f being Function of (TS SCM-AE),INT st
( it2 = f . term & ( for t being Terminal of SCM-AE holds f . (root-tree t) = s . t ) & ( for nt being NonTerminal of SCM-AE
for tl, tr being bin-term
for rtl, rtr being Symbol of SCM-AE st rtl = root-label tl & rtr = root-label tr & nt ==> <*rtl,rtr*> holds
for xl, xr being Element of INT st xl = f . tl & xr = f . tr holds
f . (nt -tree (tl,tr)) = nt -Meaning_on (xl,xr) ) ) implies it1 = it2 )
given f1 being Function of (TS SCM-AE),INT such that A3: it1 = f1 . term and
A4: for t being Terminal of SCM-AE holds f1 . (root-tree t) = s . t and
A5: for nt being NonTerminal of SCM-AE
for tl, tr being bin-term
for rtl, rtr being Symbol of SCM-AE st rtl = root-label tl & rtr = root-label tr & nt ==> <*rtl,rtr*> holds
for xl, xr being Element of INT st xl = f1 . tl & xr = f1 . tr holds
f1 . (nt -tree (tl,tr)) = nt -Meaning_on (xl,xr) ; ::_thesis: ( for f being Function of (TS SCM-AE),INT holds
( not it2 = f . term or ex t being Terminal of SCM-AE st not f . (root-tree t) = s . t or ex nt being NonTerminal of SCM-AE ex tl, tr being bin-term ex rtl, rtr being Symbol of SCM-AE st
( rtl = root-label tl & rtr = root-label tr & nt ==> <*rtl,rtr*> & ex xl, xr being Element of INT st
( xl = f . tl & xr = f . tr & not f . (nt -tree (tl,tr)) = nt -Meaning_on (xl,xr) ) ) ) or it1 = it2 )
A6: now__::_thesis:_(_(_for_t_being_Terminal_of_SCM-AE_holds_f1_._(root-tree_t)_=_H2(t)_)_&_(_for_nt_being_NonTerminal_of_SCM-AE
for_tl,_tr_being_bin-term
for_rtl,_rtr_being_Symbol_of_SCM-AE_st_rtl_=_root-label_tl_&_rtr_=_root-label_tr_&_nt_==>_<*rtl,rtr*>_holds_
for_xl,_xr_being_Element_of_INT_st_xl_=_f1_._tl_&_xr_=_f1_._tr_holds_
f1_._(nt_-tree_(tl,tr))_=_H1(nt,rtl,rtr,xl,xr)_)_)
hereby  ::_thesis: for nt being NonTerminal of SCM-AE
for tl, tr being bin-term
for rtl, rtr being Symbol of SCM-AE st rtl = root-label tl & rtr = root-label tr & nt ==> <*rtl,rtr*> holds
for xl, xr being Element of INT st xl = f1 . tl & xr = f1 . tr holds
f1 . (nt -tree (tl,tr)) = H1(nt,rtl,rtr,xl,xr)
let t be Terminal of SCM-AE; ::_thesis: f1 . (root-tree t) = H2(t)
 s . t in INT by INT_1:def_2;
then  (id INT) . (s . t) = s . t by FUNCT_1:18;
hence  f1 . (root-tree t) = H2(t) by A4; ::_thesis: verum
end;
let nt be NonTerminal of SCM-AE; ::_thesis: for tl, tr being bin-term
for rtl, rtr being Symbol of SCM-AE st rtl = root-label tl & rtr = root-label tr & nt ==> <*rtl,rtr*> holds
for xl, xr being Element of INT st xl = f1 . tl & xr = f1 . tr holds
f1 . (nt -tree (tl,tr)) = H1(nt,rtl,rtr,xl,xr)
let tl, tr be bin-term; ::_thesis: for rtl, rtr being Symbol of SCM-AE st rtl = root-label tl & rtr = root-label tr & nt ==> <*rtl,rtr*> holds
for xl, xr being Element of INT st xl = f1 . tl & xr = f1 . tr holds
f1 . (nt -tree (tl,tr)) = H1(nt,rtl,rtr,xl,xr)
let rtl, rtr be Symbol of SCM-AE; ::_thesis: ( rtl = root-label tl & rtr = root-label tr & nt ==> <*rtl,rtr*> implies for xl, xr being Element of INT st xl = f1 . tl & xr = f1 . tr holds
f1 . (nt -tree (tl,tr)) = H1(nt,rtl,rtr,xl,xr) )
assume A7: ( rtl = root-label tl & rtr = root-label tr & nt ==> <*rtl,rtr*> ) ; ::_thesis: for xl, xr being Element of INT st xl = f1 . tl & xr = f1 . tr holds
f1 . (nt -tree (tl,tr)) = H1(nt,rtl,rtr,xl,xr)
let xl, xr be Element of INT ; ::_thesis: ( xl = f1 . tl & xr = f1 . tr implies f1 . (nt -tree (tl,tr)) = H1(nt,rtl,rtr,xl,xr) )
assume A8: ( xl = f1 . tl & xr = f1 . tr ) ; ::_thesis: f1 . (nt -tree (tl,tr)) = H1(nt,rtl,rtr,xl,xr)
 nt -Meaning_on (xl,xr) in INT by INT_1:def_2;
then  (id INT) . (nt -Meaning_on (xl,xr)) = nt -Meaning_on (xl,xr) by FUNCT_1:18;
hence  f1 . (nt -tree (tl,tr)) = H1(nt,rtl,rtr,xl,xr) by A5, A7, A8; ::_thesis: verum
end;
given f2 being Function of (TS SCM-AE),INT such that A9: it2 = f2 . term and
A10: for t being Terminal of SCM-AE holds f2 . (root-tree t) = s . t and
A11: for nt being NonTerminal of SCM-AE
for tl, tr being bin-term
for rtl, rtr being Symbol of SCM-AE st rtl = root-label tl & rtr = root-label tr & nt ==> <*rtl,rtr*> holds
for xl, xr being Element of INT st xl = f2 . tl & xr = f2 . tr holds
f2 . (nt -tree (tl,tr)) = nt -Meaning_on (xl,xr) ; ::_thesis: it1 = it2
A12: now__::_thesis:_(_(_for_t_being_Terminal_of_SCM-AE_holds_f2_._(root-tree_t)_=_H2(t)_)_&_(_for_nt_being_NonTerminal_of_SCM-AE
for_tl,_tr_being_bin-term
for_rtl,_rtr_being_Symbol_of_SCM-AE_st_rtl_=_root-label_tl_&_rtr_=_root-label_tr_&_nt_==>_<*rtl,rtr*>_holds_
for_xl,_xr_being_Element_of_INT_st_xl_=_f2_._tl_&_xr_=_f2_._tr_holds_
f2_._(nt_-tree_(tl,tr))_=_H1(nt,rtl,rtr,xl,xr)_)_)
hereby  ::_thesis: for nt being NonTerminal of SCM-AE
for tl, tr being bin-term
for rtl, rtr being Symbol of SCM-AE st rtl = root-label tl & rtr = root-label tr & nt ==> <*rtl,rtr*> holds
for xl, xr being Element of INT st xl = f2 . tl & xr = f2 . tr holds
f2 . (nt -tree (tl,tr)) = H1(nt,rtl,rtr,xl,xr)
let t be Terminal of SCM-AE; ::_thesis: f2 . (root-tree t) = H2(t)
 s . t in INT by INT_1:def_2;
then  (id INT) . (s . t) = s . t by FUNCT_1:18;
hence  f2 . (root-tree t) = H2(t) by A10; ::_thesis: verum
end;
let nt be NonTerminal of SCM-AE; ::_thesis: for tl, tr being bin-term
for rtl, rtr being Symbol of SCM-AE st rtl = root-label tl & rtr = root-label tr & nt ==> <*rtl,rtr*> holds
for xl, xr being Element of INT st xl = f2 . tl & xr = f2 . tr holds
f2 . (nt -tree (tl,tr)) = H1(nt,rtl,rtr,xl,xr)
let tl, tr be bin-term; ::_thesis: for rtl, rtr being Symbol of SCM-AE st rtl = root-label tl & rtr = root-label tr & nt ==> <*rtl,rtr*> holds
for xl, xr being Element of INT st xl = f2 . tl & xr = f2 . tr holds
f2 . (nt -tree (tl,tr)) = H1(nt,rtl,rtr,xl,xr)
let rtl, rtr be Symbol of SCM-AE; ::_thesis: ( rtl = root-label tl & rtr = root-label tr & nt ==> <*rtl,rtr*> implies for xl, xr being Element of INT st xl = f2 . tl & xr = f2 . tr holds
f2 . (nt -tree (tl,tr)) = H1(nt,rtl,rtr,xl,xr) )
assume A13: ( rtl = root-label tl & rtr = root-label tr & nt ==> <*rtl,rtr*> ) ; ::_thesis: for xl, xr being Element of INT st xl = f2 . tl & xr = f2 . tr holds
f2 . (nt -tree (tl,tr)) = H1(nt,rtl,rtr,xl,xr)
let xl, xr be Element of INT ; ::_thesis: ( xl = f2 . tl & xr = f2 . tr implies f2 . (nt -tree (tl,tr)) = H1(nt,rtl,rtr,xl,xr) )
assume A14: ( xl = f2 . tl & xr = f2 . tr ) ; ::_thesis: f2 . (nt -tree (tl,tr)) = H1(nt,rtl,rtr,xl,xr)
 nt -Meaning_on (xl,xr) in INT by INT_1:def_2;
then  (id INT) . (nt -Meaning_on (xl,xr)) = nt -Meaning_on (xl,xr) by FUNCT_1:18;
hence  f2 . (nt -tree (tl,tr)) = H1(nt,rtl,rtr,xl,xr) by A11, A13, A14; ::_thesis: verum
end;
 f1 = f2 from BINTREE1:sch_4(A6, A12);
hence  it1 = it2 by A3, A9; ::_thesis: verum
end;
end;

:: deftheorem Def9 defines @ SCM_COMP:def_9_:_
 for s being State of SCM
for term being bin-term
for b3 being Integer holds
( b3 = term @ s iff ex f being Function of (TS SCM-AE),INT st
( b3 = f . term & ( for t being Terminal of SCM-AE holds f . (root-tree t) = s . t ) & ( for nt being NonTerminal of SCM-AE
for tl, tr being bin-term
for rtl, rtr being Symbol of SCM-AE st rtl = root-label tl & rtr = root-label tr & nt ==> <*rtl,rtr*> holds
for xl, xr being Element of INT st xl = f . tl & xr = f . tr holds
f . (nt -tree (tl,tr)) = nt -Meaning_on (xl,xr) ) ) );

theorem Th4: :: SCM_COMP:4
for s being State of SCM
for t being Terminal of SCM-AE holds (root-tree t) @ s = s . t
proof
let s be State of SCM; ::_thesis: for t being Terminal of SCM-AE holds (root-tree t) @ s = s . t
let t be Terminal of SCM-AE; ::_thesis: (root-tree t) @ s = s . t
 ex f being Function of (TS SCM-AE),INT st
( (root-tree t) @ s = f . (root-tree t) & ( for t being Terminal of SCM-AE holds f . (root-tree t) = s . t ) & ( for nt being NonTerminal of SCM-AE
for tl, tr being bin-term
for rtl, rtr being Symbol of SCM-AE st rtl = root-label tl & rtr = root-label tr & nt ==> <*rtl,rtr*> holds
for xl, xr being Element of INT st xl = f . tl & xr = f . tr holds
f . (nt -tree (tl,tr)) = nt -Meaning_on (xl,xr) ) ) by Def9;
hence  (root-tree t) @ s = s . t ; ::_thesis: verum
end;

theorem Th5: :: SCM_COMP:5
for s being State of SCM
for nt being NonTerminal of SCM-AE
for tl, tr being bin-term holds (nt -tree (tl,tr)) @ s = nt -Meaning_on ((tl @ s),(tr @ s))
proof
let s be State of SCM; ::_thesis: for nt being NonTerminal of SCM-AE
for tl, tr being bin-term holds (nt -tree (tl,tr)) @ s = nt -Meaning_on ((tl @ s),(tr @ s))
let nt be NonTerminal of SCM-AE; ::_thesis: for tl, tr being bin-term holds (nt -tree (tl,tr)) @ s = nt -Meaning_on ((tl @ s),(tr @ s))
let tl, tr be bin-term; ::_thesis: (nt -tree (tl,tr)) @ s = nt -Meaning_on ((tl @ s),(tr @ s))
consider f being Function of (TS SCM-AE),INT such that
A1: (nt -tree (tl,tr)) @ s = f . (nt -tree (tl,tr)) and
A2: for t being Terminal of SCM-AE holds f . (root-tree t) = s . t and
A3: for nt being NonTerminal of SCM-AE
for tl, tr being bin-term
for rtl, rtr being Symbol of SCM-AE st rtl = root-label tl & rtr = root-label tr & nt ==> <*rtl,rtr*> holds
for xl, xr being Element of INT st xl = f . tl & xr = f . tr holds
f . (nt -tree (tl,tr)) = nt -Meaning_on (xl,xr) by Def9;
A4: nt ==> <*(root-label tl),(root-label tr)*> by Def1, Lm3;
 ( tl @ s = f . tl & tr @ s = f . tr ) by A2, A3, Def9;
hence  (nt -tree (tl,tr)) @ s = nt -Meaning_on ((tl @ s),(tr @ s)) by A1, A3, A4; ::_thesis: verum
end;

theorem :: SCM_COMP:6
for s being State of SCM
for tl, tr being bin-term holds
( (tl + tr) @ s = (tl @ s) + (tr @ s) & (tl - tr) @ s = (tl @ s) - (tr @ s) & (tl * tr) @ s = (tl @ s) * (tr @ s) & (tl div tr) @ s = (tl @ s) div (tr @ s) & (tl mod tr) @ s = (tl @ s) mod (tr @ s) )
proof
let s be State of SCM; ::_thesis: for tl, tr being bin-term holds
( (tl + tr) @ s = (tl @ s) + (tr @ s) & (tl - tr) @ s = (tl @ s) - (tr @ s) & (tl * tr) @ s = (tl @ s) * (tr @ s) & (tl div tr) @ s = (tl @ s) div (tr @ s) & (tl mod tr) @ s = (tl @ s) mod (tr @ s) )
let tl, tr be bin-term; ::_thesis: ( (tl + tr) @ s = (tl @ s) + (tr @ s) & (tl - tr) @ s = (tl @ s) - (tr @ s) & (tl * tr) @ s = (tl @ s) * (tr @ s) & (tl div tr) @ s = (tl @ s) div (tr @ s) & (tl mod tr) @ s = (tl @ s) mod (tr @ s) )
thus (tl + tr) @ s = nt0 -Meaning_on ((tl @ s),(tr @ s)) by Th5
.= (tl @ s) + (tr @ s) by Def8 ; ::_thesis: ( (tl - tr) @ s = (tl @ s) - (tr @ s) & (tl * tr) @ s = (tl @ s) * (tr @ s) & (tl div tr) @ s = (tl @ s) div (tr @ s) & (tl mod tr) @ s = (tl @ s) mod (tr @ s) )
thus (tl - tr) @ s = nt1 -Meaning_on ((tl @ s),(tr @ s)) by Th5
.= (tl @ s) - (tr @ s) by Def8 ; ::_thesis: ( (tl * tr) @ s = (tl @ s) * (tr @ s) & (tl div tr) @ s = (tl @ s) div (tr @ s) & (tl mod tr) @ s = (tl @ s) mod (tr @ s) )
thus (tl * tr) @ s = nt2 -Meaning_on ((tl @ s),(tr @ s)) by Th5
.= (tl @ s) * (tr @ s) by Def8 ; ::_thesis: ( (tl div tr) @ s = (tl @ s) div (tr @ s) & (tl mod tr) @ s = (tl @ s) mod (tr @ s) )
thus (tl div tr) @ s = nt3 -Meaning_on ((tl @ s),(tr @ s)) by Th5
.= (tl @ s) div (tr @ s) by Def8 ; ::_thesis: (tl mod tr) @ s = (tl @ s) mod (tr @ s)
thus (tl mod tr) @ s = nt4 -Meaning_on ((tl @ s),(tr @ s)) by Th5
.= (tl @ s) mod (tr @ s) by Def8 ; ::_thesis: verum
end;

definition
let nt be NonTerminal of SCM-AE;
let n be Element of NAT ;
func Selfwork (nt,n) ->  XFinSequence of the InstructionsF of SCM equals :Def10: :: SCM_COMP:def 10
<%(AddTo ((dl. n),(dl. (n + 1))))%> if nt = [0,0]
<%(SubFrom ((dl. n),(dl. (n + 1))))%> if nt = [0,1]
<%(MultBy ((dl. n),(dl. (n + 1))))%> if nt = [0,2]
<%(Divide ((dl. n),(dl. (n + 1))))%> if nt = [0,3]
<%(Divide ((dl. n),(dl. (n + 1)))),((dl. n) := (dl. (n + 1)))%> if nt = [0,4]
;
coherence
 ( ( nt = [0,0] implies <%(AddTo ((dl. n),(dl. (n + 1))))%> is XFinSequence of the InstructionsF of SCM ) & ( nt = [0,1] implies <%(SubFrom ((dl. n),(dl. (n + 1))))%> is XFinSequence of the InstructionsF of SCM ) & ( nt = [0,2] implies <%(MultBy ((dl. n),(dl. (n + 1))))%> is XFinSequence of the InstructionsF of SCM ) & ( nt = [0,3] implies <%(Divide ((dl. n),(dl. (n + 1))))%> is XFinSequence of the InstructionsF of SCM ) & ( nt = [0,4] implies <%(Divide ((dl. n),(dl. (n + 1)))),((dl. n) := (dl. (n + 1)))%> is XFinSequence of the InstructionsF of SCM ) ) ;
consistency
 for b1 being XFinSequence of the InstructionsF of SCM holds
( ( nt = [0,0] & nt = [0,1] implies ( b1 = <%(AddTo ((dl. n),(dl. (n + 1))))%> iff b1 = <%(SubFrom ((dl. n),(dl. (n + 1))))%> ) ) & ( nt = [0,0] & nt = [0,2] implies ( b1 = <%(AddTo ((dl. n),(dl. (n + 1))))%> iff b1 = <%(MultBy ((dl. n),(dl. (n + 1))))%> ) ) & ( nt = [0,0] & nt = [0,3] implies ( b1 = <%(AddTo ((dl. n),(dl. (n + 1))))%> iff b1 = <%(Divide ((dl. n),(dl. (n + 1))))%> ) ) & ( nt = [0,0] & nt = [0,4] implies ( b1 = <%(AddTo ((dl. n),(dl. (n + 1))))%> iff b1 = <%(Divide ((dl. n),(dl. (n + 1)))),((dl. n) := (dl. (n + 1)))%> ) ) & ( nt = [0,1] & nt = [0,2] implies ( b1 = <%(SubFrom ((dl. n),(dl. (n + 1))))%> iff b1 = <%(MultBy ((dl. n),(dl. (n + 1))))%> ) ) & ( nt = [0,1] & nt = [0,3] implies ( b1 = <%(SubFrom ((dl. n),(dl. (n + 1))))%> iff b1 = <%(Divide ((dl. n),(dl. (n + 1))))%> ) ) & ( nt = [0,1] & nt = [0,4] implies ( b1 = <%(SubFrom ((dl. n),(dl. (n + 1))))%> iff b1 = <%(Divide ((dl. n),(dl. (n + 1)))),((dl. n) := (dl. (n + 1)))%> ) ) & ( nt = [0,2] & nt = [0,3] implies ( b1 = <%(MultBy ((dl. n),(dl. (n + 1))))%> iff b1 = <%(Divide ((dl. n),(dl. (n + 1))))%> ) ) & ( nt = [0,2] & nt = [0,4] implies ( b1 = <%(MultBy ((dl. n),(dl. (n + 1))))%> iff b1 = <%(Divide ((dl. n),(dl. (n + 1)))),((dl. n) := (dl. (n + 1)))%> ) ) & ( nt = [0,3] & nt = [0,4] implies ( b1 = <%(Divide ((dl. n),(dl. (n + 1))))%> iff b1 = <%(Divide ((dl. n),(dl. (n + 1)))),((dl. n) := (dl. (n + 1)))%> ) ) )
proof
A1: ( [0,2] `2 = 2 & [0,3] `2 = 3 ) ;
 ( [0,0] `2 = 0 & [0,1] `2 = 1 ) ;
hence  for b1 being XFinSequence of the InstructionsF of SCM holds
( ( nt = [0,0] & nt = [0,1] implies ( b1 = <%(AddTo ((dl. n),(dl. (n + 1))))%> iff b1 = <%(SubFrom ((dl. n),(dl. (n + 1))))%> ) ) & ( nt = [0,0] & nt = [0,2] implies ( b1 = <%(AddTo ((dl. n),(dl. (n + 1))))%> iff b1 = <%(MultBy ((dl. n),(dl. (n + 1))))%> ) ) & ( nt = [0,0] & nt = [0,3] implies ( b1 = <%(AddTo ((dl. n),(dl. (n + 1))))%> iff b1 = <%(Divide ((dl. n),(dl. (n + 1))))%> ) ) & ( nt = [0,0] & nt = [0,4] implies ( b1 = <%(AddTo ((dl. n),(dl. (n + 1))))%> iff b1 = <%(Divide ((dl. n),(dl. (n + 1)))),((dl. n) := (dl. (n + 1)))%> ) ) & ( nt = [0,1] & nt = [0,2] implies ( b1 = <%(SubFrom ((dl. n),(dl. (n + 1))))%> iff b1 = <%(MultBy ((dl. n),(dl. (n + 1))))%> ) ) & ( nt = [0,1] & nt = [0,3] implies ( b1 = <%(SubFrom ((dl. n),(dl. (n + 1))))%> iff b1 = <%(Divide ((dl. n),(dl. (n + 1))))%> ) ) & ( nt = [0,1] & nt = [0,4] implies ( b1 = <%(SubFrom ((dl. n),(dl. (n + 1))))%> iff b1 = <%(Divide ((dl. n),(dl. (n + 1)))),((dl. n) := (dl. (n + 1)))%> ) ) & ( nt = [0,2] & nt = [0,3] implies ( b1 = <%(MultBy ((dl. n),(dl. (n + 1))))%> iff b1 = <%(Divide ((dl. n),(dl. (n + 1))))%> ) ) & ( nt = [0,2] & nt = [0,4] implies ( b1 = <%(MultBy ((dl. n),(dl. (n + 1))))%> iff b1 = <%(Divide ((dl. n),(dl. (n + 1)))),((dl. n) := (dl. (n + 1)))%> ) ) & ( nt = [0,3] & nt = [0,4] implies ( b1 = <%(Divide ((dl. n),(dl. (n + 1))))%> iff b1 = <%(Divide ((dl. n),(dl. (n + 1)))),((dl. n) := (dl. (n + 1)))%> ) ) ) by A1, MCART_1:7; ::_thesis: verum
end;
end;

:: deftheorem Def10 defines Selfwork SCM_COMP:def_10_:_
 for nt being NonTerminal of SCM-AE
for n being Element of NAT holds
( ( nt = [0,0] implies Selfwork (nt,n) = <%(AddTo ((dl. n),(dl. (n + 1))))%> ) & ( nt = [0,1] implies Selfwork (nt,n) = <%(SubFrom ((dl. n),(dl. (n + 1))))%> ) & ( nt = [0,2] implies Selfwork (nt,n) = <%(MultBy ((dl. n),(dl. (n + 1))))%> ) & ( nt = [0,3] implies Selfwork (nt,n) = <%(Divide ((dl. n),(dl. (n + 1))))%> ) & ( nt = [0,4] implies Selfwork (nt,n) = <%(Divide ((dl. n),(dl. (n + 1)))),((dl. n) := (dl. (n + 1)))%> ) );

definition
deffunc H2( NonTerminal of SCM-AE, Function of NAT,( the InstructionsF of SCM ^omega), Function of NAT,( the InstructionsF of SCM ^omega), Element of NAT ) ->  Element of the InstructionsF of SCM ^omega = (($2 . $4) ^ ($3 . ($4 + 1))) ^ (Down (Selfwork ($1,$4)));
deffunc H3( Terminal of SCM-AE, Element of NAT ) ->  Element of the InstructionsF of SCM ^omega = Down <%((dl. $2) := (@ $1))%>;
func SCM-Compile  ->  Function of (TS SCM-AE),(Funcs (NAT,( the InstructionsF of SCM ^omega))) means :Def11: :: SCM_COMP:def 11
( ( for t being Terminal of SCM-AE ex g being Function of NAT,( the InstructionsF of SCM ^omega) st
( g = it . (root-tree t) & ( for n being Element of NAT holds g . n = <%((dl. n) := (@ t))%> ) ) ) & ( for nt being NonTerminal of SCM-AE
for t1, t2 being bin-term
for rtl, rtr being Symbol of SCM-AE st rtl = root-label t1 & rtr = root-label t2 & nt ==> <*rtl,rtr*> holds
ex g, f1, f2 being Function of NAT,( the InstructionsF of SCM ^omega) st
( g = it . (nt -tree (t1,t2)) & f1 = it . t1 & f2 = it . t2 & ( for n being Element of NAT holds g . n = ((f1 . n) ^ (f2 . (n + 1))) ^ (Selfwork (nt,n)) ) ) ) );
existence
 ex b1 being Function of (TS SCM-AE),(Funcs (NAT,( the InstructionsF of SCM ^omega))) st
( ( for t being Terminal of SCM-AE ex g being Function of NAT,( the InstructionsF of SCM ^omega) st
( g = b1 . (root-tree t) & ( for n being Element of NAT holds g . n = <%((dl. n) := (@ t))%> ) ) ) & ( for nt being NonTerminal of SCM-AE
for t1, t2 being bin-term
for rtl, rtr being Symbol of SCM-AE st rtl = root-label t1 & rtr = root-label t2 & nt ==> <*rtl,rtr*> holds
ex g, f1, f2 being Function of NAT,( the InstructionsF of SCM ^omega) st
( g = b1 . (nt -tree (t1,t2)) & f1 = b1 . t1 & f2 = b1 . t2 & ( for n being Element of NAT holds g . n = ((f1 . n) ^ (f2 . (n + 1))) ^ (Selfwork (nt,n)) ) ) ) )
proof
consider f being Function of (TS SCM-AE),(Funcs (NAT,( the InstructionsF of SCM ^omega))) such that
A1: ( ( for t being Terminal of SCM-AE ex g being Function of NAT,( the InstructionsF of SCM ^omega) st
( g = f . (root-tree t) & ( for n being Element of NAT holds g . n = H3(t,n) ) ) ) & ( for nt being NonTerminal of SCM-AE
for t1, t2 being bin-term
for rtl, rtr being Symbol of SCM-AE st rtl = root-label t1 & rtr = root-label t2 & nt ==> <*rtl,rtr*> holds
ex g, f1, f2 being Function of NAT,( the InstructionsF of SCM ^omega) st
( g = f . (nt -tree (t1,t2)) & f1 = f . t1 & f2 = f . t2 & ( for n being Element of NAT holds g . n = H2(nt,f1,f2,n) ) ) ) ) from BINTREE1:sch_5();
take  f ; ::_thesis: ( ( for t being Terminal of SCM-AE ex g being Function of NAT,( the InstructionsF of SCM ^omega) st
( g = f . (root-tree t) & ( for n being Element of NAT holds g . n = <%((dl. n) := (@ t))%> ) ) ) & ( for nt being NonTerminal of SCM-AE
for t1, t2 being bin-term
for rtl, rtr being Symbol of SCM-AE st rtl = root-label t1 & rtr = root-label t2 & nt ==> <*rtl,rtr*> holds
ex g, f1, f2 being Function of NAT,( the InstructionsF of SCM ^omega) st
( g = f . (nt -tree (t1,t2)) & f1 = f . t1 & f2 = f . t2 & ( for n being Element of NAT holds g . n = ((f1 . n) ^ (f2 . (n + 1))) ^ (Selfwork (nt,n)) ) ) ) )
 ( ( for t being Terminal of SCM-AE ex g being Function of NAT,( the InstructionsF of SCM ^omega) st
( g = f . (root-tree t) & ( for n being Element of NAT holds g . n = <%((dl. n) := (@ t))%> ) ) ) & ( for nt being NonTerminal of SCM-AE
for t1, t2 being bin-term
for rtl, rtr being Symbol of SCM-AE st rtl = root-label t1 & rtr = root-label t2 & nt ==> <*rtl,rtr*> holds
ex g, f1, f2 being Function of NAT,( the InstructionsF of SCM ^omega) st
( g = f . (nt -tree (t1,t2)) & f1 = f . t1 & f2 = f . t2 & ( for n being Element of NAT holds g . n = ((f1 . n) ^ (f2 . (n + 1))) ^ (Selfwork (nt,n)) ) ) ) )
proof
thus  for t being Terminal of SCM-AE ex g being Function of NAT,( the InstructionsF of SCM ^omega) st
( g = f . (root-tree t) & ( for n being Element of NAT holds g . n = <%((dl. n) := (@ t))%> ) ) ::_thesis: for nt being NonTerminal of SCM-AE
for t1, t2 being bin-term
for rtl, rtr being Symbol of SCM-AE st rtl = root-label t1 & rtr = root-label t2 & nt ==> <*rtl,rtr*> holds
ex g, f1, f2 being Function of NAT,( the InstructionsF of SCM ^omega) st
( g = f . (nt -tree (t1,t2)) & f1 = f . t1 & f2 = f . t2 & ( for n being Element of NAT holds g . n = ((f1 . n) ^ (f2 . (n + 1))) ^ (Selfwork (nt,n)) ) )
proof
let t be Terminal of SCM-AE; ::_thesis: ex g being Function of NAT,( the InstructionsF of SCM ^omega) st
( g = f . (root-tree t) & ( for n being Element of NAT holds g . n = <%((dl. n) := (@ t))%> ) )
consider g being Function of NAT,( the InstructionsF of SCM ^omega) such that
A2: g = f . (root-tree t) and
A3: for n being Element of NAT holds g . n = H3(t,n) by A1;
take  g ; ::_thesis: ( g = f . (root-tree t) & ( for n being Element of NAT holds g . n = <%((dl. n) := (@ t))%> ) )
thus  g = f . (root-tree t) by A2; ::_thesis: for n being Element of NAT holds g . n = <%((dl. n) := (@ t))%>
let n be Element of NAT ; ::_thesis: g . n = <%((dl. n) := (@ t))%>
 g . n = H3(t,n) by A3;
hence  g . n = <%((dl. n) := (@ t))%> ; ::_thesis: verum
end;
thus  for nt being NonTerminal of SCM-AE
for t1, t2 being bin-term
for rtl, rtr being Symbol of SCM-AE st rtl = root-label t1 & rtr = root-label t2 & nt ==> <*rtl,rtr*> holds
ex g, f1, f2 being Function of NAT,( the InstructionsF of SCM ^omega) st
( g = f . (nt -tree (t1,t2)) & f1 = f . t1 & f2 = f . t2 & ( for n being Element of NAT holds g . n = ((f1 . n) ^ (f2 . (n + 1))) ^ (Selfwork (nt,n)) ) ) ::_thesis: verum
proof
let nt be NonTerminal of SCM-AE; ::_thesis: for t1, t2 being bin-term
for rtl, rtr being Symbol of SCM-AE st rtl = root-label t1 & rtr = root-label t2 & nt ==> <*rtl,rtr*> holds
ex g, f1, f2 being Function of NAT,( the InstructionsF of SCM ^omega) st
( g = f . (nt -tree (t1,t2)) & f1 = f . t1 & f2 = f . t2 & ( for n being Element of NAT holds g . n = ((f1 . n) ^ (f2 . (n + 1))) ^ (Selfwork (nt,n)) ) )
let t1, t2 be bin-term; ::_thesis: for rtl, rtr being Symbol of SCM-AE st rtl = root-label t1 & rtr = root-label t2 & nt ==> <*rtl,rtr*> holds
ex g, f1, f2 being Function of NAT,( the InstructionsF of SCM ^omega) st
( g = f . (nt -tree (t1,t2)) & f1 = f . t1 & f2 = f . t2 & ( for n being Element of NAT holds g . n = ((f1 . n) ^ (f2 . (n + 1))) ^ (Selfwork (nt,n)) ) )
let rtl, rtr be Symbol of SCM-AE; ::_thesis: ( rtl = root-label t1 & rtr = root-label t2 & nt ==> <*rtl,rtr*> implies ex g, f1, f2 being Function of NAT,( the InstructionsF of SCM ^omega) st
( g = f . (nt -tree (t1,t2)) & f1 = f . t1 & f2 = f . t2 & ( for n being Element of NAT holds g . n = ((f1 . n) ^ (f2 . (n + 1))) ^ (Selfwork (nt,n)) ) ) )
assume A4: ( rtl = root-label t1 & rtr = root-label t2 & nt ==> <*rtl,rtr*> ) ; ::_thesis: ex g, f1, f2 being Function of NAT,( the InstructionsF of SCM ^omega) st
( g = f . (nt -tree (t1,t2)) & f1 = f . t1 & f2 = f . t2 & ( for n being Element of NAT holds g . n = ((f1 . n) ^ (f2 . (n + 1))) ^ (Selfwork (nt,n)) ) )
consider g, f1, f2 being Function of NAT,( the InstructionsF of SCM ^omega) such that
A5: ( g = f . (nt -tree (t1,t2)) & f1 = f . t1 & f2 = f . t2 ) and
A6: for n being Element of NAT holds g . n = H2(nt,f1,f2,n) by A4, A1;
take  g ; ::_thesis: ex f1, f2 being Function of NAT,( the InstructionsF of SCM ^omega) st
( g = f . (nt -tree (t1,t2)) & f1 = f . t1 & f2 = f . t2 & ( for n being Element of NAT holds g . n = ((f1 . n) ^ (f2 . (n + 1))) ^ (Selfwork (nt,n)) ) )
take  f1 ; ::_thesis: ex f2 being Function of NAT,( the InstructionsF of SCM ^omega) st
( g = f . (nt -tree (t1,t2)) & f1 = f . t1 & f2 = f . t2 & ( for n being Element of NAT holds g . n = ((f1 . n) ^ (f2 . (n + 1))) ^ (Selfwork (nt,n)) ) )
take  f2 ; ::_thesis: ( g = f . (nt -tree (t1,t2)) & f1 = f . t1 & f2 = f . t2 & ( for n being Element of NAT holds g . n = ((f1 . n) ^ (f2 . (n + 1))) ^ (Selfwork (nt,n)) ) )
thus  ( g = f . (nt -tree (t1,t2)) & f1 = f . t1 & f2 = f . t2 ) by A5; ::_thesis: for n being Element of NAT holds g . n = ((f1 . n) ^ (f2 . (n + 1))) ^ (Selfwork (nt,n))
let n be Element of NAT ; ::_thesis: g . n = ((f1 . n) ^ (f2 . (n + 1))) ^ (Selfwork (nt,n))
 g . n = H2(nt,f1,f2,n) by A6;
hence  g . n = ((f1 . n) ^ (f2 . (n + 1))) ^ (Selfwork (nt,n)) ; ::_thesis: verum
end;
end;
hence  ( ( for t being Terminal of SCM-AE ex g being Function of NAT,( the InstructionsF of SCM ^omega) st
( g = f . (root-tree t) & ( for n being Element of NAT holds g . n = <%((dl. n) := (@ t))%> ) ) ) & ( for nt being NonTerminal of SCM-AE
for t1, t2 being bin-term
for rtl, rtr being Symbol of SCM-AE st rtl = root-label t1 & rtr = root-label t2 & nt ==> <*rtl,rtr*> holds
ex g, f1, f2 being Function of NAT,( the InstructionsF of SCM ^omega) st
( g = f . (nt -tree (t1,t2)) & f1 = f . t1 & f2 = f . t2 & ( for n being Element of NAT holds g . n = ((f1 . n) ^ (f2 . (n + 1))) ^ (Selfwork (nt,n)) ) ) ) ) ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Function of (TS SCM-AE),(Funcs (NAT,( the InstructionsF of SCM ^omega))) st ( for t being Terminal of SCM-AE ex g being Function of NAT,( the InstructionsF of SCM ^omega) st
( g = b1 . (root-tree t) & ( for n being Element of NAT holds g . n = <%((dl. n) := (@ t))%> ) ) ) & ( for nt being NonTerminal of SCM-AE
for t1, t2 being bin-term
for rtl, rtr being Symbol of SCM-AE st rtl = root-label t1 & rtr = root-label t2 & nt ==> <*rtl,rtr*> holds
ex g, f1, f2 being Function of NAT,( the InstructionsF of SCM ^omega) st
( g = b1 . (nt -tree (t1,t2)) & f1 = b1 . t1 & f2 = b1 . t2 & ( for n being Element of NAT holds g . n = ((f1 . n) ^ (f2 . (n + 1))) ^ (Selfwork (nt,n)) ) ) ) & ( for t being Terminal of SCM-AE ex g being Function of NAT,( the InstructionsF of SCM ^omega) st
( g = b2 . (root-tree t) & ( for n being Element of NAT holds g . n = <%((dl. n) := (@ t))%> ) ) ) & ( for nt being NonTerminal of SCM-AE
for t1, t2 being bin-term
for rtl, rtr being Symbol of SCM-AE st rtl = root-label t1 & rtr = root-label t2 & nt ==> <*rtl,rtr*> holds
ex g, f1, f2 being Function of NAT,( the InstructionsF of SCM ^omega) st
( g = b2 . (nt -tree (t1,t2)) & f1 = b2 . t1 & f2 = b2 . t2 & ( for n being Element of NAT holds g . n = ((f1 . n) ^ (f2 . (n + 1))) ^ (Selfwork (nt,n)) ) ) ) holds
b1 = b2
proof
let f1, f2 be Function of (TS SCM-AE),(Funcs (NAT,( the InstructionsF of SCM ^omega))); ::_thesis: ( ( for t being Terminal of SCM-AE ex g being Function of NAT,( the InstructionsF of SCM ^omega) st
( g = f1 . (root-tree t) & ( for n being Element of NAT holds g . n = <%((dl. n) := (@ t))%> ) ) ) & ( for nt being NonTerminal of SCM-AE
for t1, t2 being bin-term
for rtl, rtr being Symbol of SCM-AE st rtl = root-label t1 & rtr = root-label t2 & nt ==> <*rtl,rtr*> holds
ex g, f1, f2 being Function of NAT,( the InstructionsF of SCM ^omega) st
( g = f1 . (nt -tree (t1,t2)) & f1 = f1 . t1 & f2 = f1 . t2 & ( for n being Element of NAT holds g . n = ((f1 . n) ^ (f2 . (n + 1))) ^ (Selfwork (nt,n)) ) ) ) & ( for t being Terminal of SCM-AE ex g being Function of NAT,( the InstructionsF of SCM ^omega) st
( g = f2 . (root-tree t) & ( for n being Element of NAT holds g . n = <%((dl. n) := (@ t))%> ) ) ) & ( for nt being NonTerminal of SCM-AE
for t1, t2 being bin-term
for rtl, rtr being Symbol of SCM-AE st rtl = root-label t1 & rtr = root-label t2 & nt ==> <*rtl,rtr*> holds
ex g, f1, f2 being Function of NAT,( the InstructionsF of SCM ^omega) st
( g = f2 . (nt -tree (t1,t2)) & f1 = f2 . t1 & f2 = f2 . t2 & ( for n being Element of NAT holds g . n = ((f1 . n) ^ (f2 . (n + 1))) ^ (Selfwork (nt,n)) ) ) ) implies f1 = f2 )
assume that
A7: ( ( for t being Terminal of SCM-AE ex g being Function of NAT,( the InstructionsF of SCM ^omega) st
( g = f1 . (root-tree t) & ( for n being Element of NAT holds g . n = <%((dl. n) := (@ t))%> ) ) ) & ( for nt being NonTerminal of SCM-AE
for t1, t2 being bin-term
for rtl, rtr being Symbol of SCM-AE st rtl = root-label t1 & rtr = root-label t2 & nt ==> <*rtl,rtr*> holds
ex g, g1, g2 being Function of NAT,( the InstructionsF of SCM ^omega) st
( g = f1 . (nt -tree (t1,t2)) & g1 = f1 . t1 & g2 = f1 . t2 & ( for n being Element of NAT holds g . n = ((g1 . n) ^ (g2 . (n + 1))) ^ (Selfwork (nt,n)) ) ) ) ) and
A8: ( ( for t being Terminal of SCM-AE ex g being Function of NAT,( the InstructionsF of SCM ^omega) st
( g = f2 . (root-tree t) & ( for n being Element of NAT holds g . n = <%((dl. n) := (@ t))%> ) ) ) & ( for nt being NonTerminal of SCM-AE
for t1, t2 being bin-term
for rtl, rtr being Symbol of SCM-AE st rtl = root-label t1 & rtr = root-label t2 & nt ==> <*rtl,rtr*> holds
ex g, g1, g2 being Function of NAT,( the InstructionsF of SCM ^omega) st
( g = f2 . (nt -tree (t1,t2)) & g1 = f2 . t1 & g2 = f2 . t2 & ( for n being Element of NAT holds g . n = ((g1 . n) ^ (g2 . (n + 1))) ^ (Selfwork (nt,n)) ) ) ) ) ; ::_thesis: f1 = f2
A9: ( ( for t being Terminal of SCM-AE ex g being Function of NAT,( the InstructionsF of SCM ^omega) st
( g = f1 . (root-tree t) & ( for n being Element of NAT holds g . n = H3(t,n) ) ) ) & ( for nt being NonTerminal of SCM-AE
for t1, t2 being bin-term
for rtl, rtr being Symbol of SCM-AE st rtl = root-label t1 & rtr = root-label t2 & nt ==> <*rtl,rtr*> holds
ex g, g1, g2 being Function of NAT,( the InstructionsF of SCM ^omega) st
( g = f1 . (nt -tree (t1,t2)) & g1 = f1 . t1 & g2 = f1 . t2 & ( for n being Element of NAT holds g . n = H2(nt,g1,g2,n) ) ) ) )
proof
thus  for t being Terminal of SCM-AE ex g being Function of NAT,( the InstructionsF of SCM ^omega) st
( g = f1 . (root-tree t) & ( for n being Element of NAT holds g . n = H3(t,n) ) ) ::_thesis: for nt being NonTerminal of SCM-AE
for t1, t2 being bin-term
for rtl, rtr being Symbol of SCM-AE st rtl = root-label t1 & rtr = root-label t2 & nt ==> <*rtl,rtr*> holds
ex g, g1, g2 being Function of NAT,( the InstructionsF of SCM ^omega) st
( g = f1 . (nt -tree (t1,t2)) & g1 = f1 . t1 & g2 = f1 . t2 & ( for n being Element of NAT holds g . n = H2(nt,g1,g2,n) ) )
proof
let t be Terminal of SCM-AE; ::_thesis: ex g being Function of NAT,( the InstructionsF of SCM ^omega) st
( g = f1 . (root-tree t) & ( for n being Element of NAT holds g . n = H3(t,n) ) )
consider g being Function of NAT,( the InstructionsF of SCM ^omega) such that
A10: ( g = f1 . (root-tree t) & ( for n being Element of NAT holds g . n = <%((dl. n) := (@ t))%> ) ) by A7;
take  g ; ::_thesis: ( g = f1 . (root-tree t) & ( for n being Element of NAT holds g . n = H3(t,n) ) )
thus  ( g = f1 . (root-tree t) & ( for n being Element of NAT holds g . n = H3(t,n) ) ) by A10; ::_thesis: verum
end;
thus  for nt being NonTerminal of SCM-AE
for t1, t2 being bin-term
for rtl, rtr being Symbol of SCM-AE st rtl = root-label t1 & rtr = root-label t2 & nt ==> <*rtl,rtr*> holds
ex g, g1, g2 being Function of NAT,( the InstructionsF of SCM ^omega) st
( g = f1 . (nt -tree (t1,t2)) & g1 = f1 . t1 & g2 = f1 . t2 & ( for n being Element of NAT holds g . n = H2(nt,g1,g2,n) ) ) ::_thesis: verum
proof
let nt be NonTerminal of SCM-AE; ::_thesis: for t1, t2 being bin-term
for rtl, rtr being Symbol of SCM-AE st rtl = root-label t1 & rtr = root-label t2 & nt ==> <*rtl,rtr*> holds
ex g, g1, g2 being Function of NAT,( the InstructionsF of SCM ^omega) st
( g = f1 . (nt -tree (t1,t2)) & g1 = f1 . t1 & g2 = f1 . t2 & ( for n being Element of NAT holds g . n = H2(nt,g1,g2,n) ) )
let t1, t2 be bin-term; ::_thesis: for rtl, rtr being Symbol of SCM-AE st rtl = root-label t1 & rtr = root-label t2 & nt ==> <*rtl,rtr*> holds
ex g, g1, g2 being Function of NAT,( the InstructionsF of SCM ^omega) st
( g = f1 . (nt -tree (t1,t2)) & g1 = f1 . t1 & g2 = f1 . t2 & ( for n being Element of NAT holds g . n = H2(nt,g1,g2,n) ) )
let rtl, rtr be Symbol of SCM-AE; ::_thesis: ( rtl = root-label t1 & rtr = root-label t2 & nt ==> <*rtl,rtr*> implies ex g, g1, g2 being Function of NAT,( the InstructionsF of SCM ^omega) st
( g = f1 . (nt -tree (t1,t2)) & g1 = f1 . t1 & g2 = f1 . t2 & ( for n being Element of NAT holds g . n = H2(nt,g1,g2,n) ) ) )
assume A11: ( rtl = root-label t1 & rtr = root-label t2 & nt ==> <*rtl,rtr*> ) ; ::_thesis: ex g, g1, g2 being Function of NAT,( the InstructionsF of SCM ^omega) st
( g = f1 . (nt -tree (t1,t2)) & g1 = f1 . t1 & g2 = f1 . t2 & ( for n being Element of NAT holds g . n = H2(nt,g1,g2,n) ) )
consider g, g1, g2 being Function of NAT,( the InstructionsF of SCM ^omega) such that
A12: ( g = f1 . (nt -tree (t1,t2)) & g1 = f1 . t1 & g2 = f1 . t2 & ( for n being Element of NAT holds g . n = ((g1 . n) ^ (g2 . (n + 1))) ^ (Selfwork (nt,n)) ) ) by A7, A11;
take  g ; ::_thesis: ex g1, g2 being Function of NAT,( the InstructionsF of SCM ^omega) st
( g = f1 . (nt -tree (t1,t2)) & g1 = f1 . t1 & g2 = f1 . t2 & ( for n being Element of NAT holds g . n = H2(nt,g1,g2,n) ) )
take  g1 ; ::_thesis: ex g2 being Function of NAT,( the InstructionsF of SCM ^omega) st
( g = f1 . (nt -tree (t1,t2)) & g1 = f1 . t1 & g2 = f1 . t2 & ( for n being Element of NAT holds g . n = H2(nt,g1,g2,n) ) )
take  g2 ; ::_thesis: ( g = f1 . (nt -tree (t1,t2)) & g1 = f1 . t1 & g2 = f1 . t2 & ( for n being Element of NAT holds g . n = H2(nt,g1,g2,n) ) )
thus  ( g = f1 . (nt -tree (t1,t2)) & g1 = f1 . t1 & g2 = f1 . t2 & ( for n being Element of NAT holds g . n = H2(nt,g1,g2,n) ) ) by A12; ::_thesis: verum
end;
end;
A13: ( ( for t being Terminal of SCM-AE ex g being Function of NAT,( the InstructionsF of SCM ^omega) st
( g = f2 . (root-tree t) & ( for n being Element of NAT holds g . n = H3(t,n) ) ) ) & ( for nt being NonTerminal of SCM-AE
for t1, t2 being bin-term
for rtl, rtr being Symbol of SCM-AE st rtl = root-label t1 & rtr = root-label t2 & nt ==> <*rtl,rtr*> holds
ex g, g1, g2 being Function of NAT,( the InstructionsF of SCM ^omega) st
( g = f2 . (nt -tree (t1,t2)) & g1 = f2 . t1 & g2 = f2 . t2 & ( for n being Element of NAT holds g . n = H2(nt,g1,g2,n) ) ) ) )
proof
thus  for t being Terminal of SCM-AE ex g being Function of NAT,( the InstructionsF of SCM ^omega) st
( g = f2 . (root-tree t) & ( for n being Element of NAT holds g . n = H3(t,n) ) ) ::_thesis: for nt being NonTerminal of SCM-AE
for t1, t2 being bin-term
for rtl, rtr being Symbol of SCM-AE st rtl = root-label t1 & rtr = root-label t2 & nt ==> <*rtl,rtr*> holds
ex g, g1, g2 being Function of NAT,( the InstructionsF of SCM ^omega) st
( g = f2 . (nt -tree (t1,t2)) & g1 = f2 . t1 & g2 = f2 . t2 & ( for n being Element of NAT holds g . n = H2(nt,g1,g2,n) ) )
proof
let t be Terminal of SCM-AE; ::_thesis: ex g being Function of NAT,( the InstructionsF of SCM ^omega) st
( g = f2 . (root-tree t) & ( for n being Element of NAT holds g . n = H3(t,n) ) )
consider g being Function of NAT,( the InstructionsF of SCM ^omega) such that
A14: ( g = f2 . (root-tree t) & ( for n being Element of NAT holds g . n = <%((dl. n) := (@ t))%> ) ) by A8;
take  g ; ::_thesis: ( g = f2 . (root-tree t) & ( for n being Element of NAT holds g . n = H3(t,n) ) )
thus  ( g = f2 . (root-tree t) & ( for n being Element of NAT holds g . n = H3(t,n) ) ) by A14; ::_thesis: verum
end;
thus  for nt being NonTerminal of SCM-AE
for t1, t2 being bin-term
for rtl, rtr being Symbol of SCM-AE st rtl = root-label t1 & rtr = root-label t2 & nt ==> <*rtl,rtr*> holds
ex g, g1, g2 being Function of NAT,( the InstructionsF of SCM ^omega) st
( g = f2 . (nt -tree (t1,t2)) & g1 = f2 . t1 & g2 = f2 . t2 & ( for n being Element of NAT holds g . n = H2(nt,g1,g2,n) ) ) ::_thesis: verum
proof
let nt be NonTerminal of SCM-AE; ::_thesis: for t1, t2 being bin-term
for rtl, rtr being Symbol of SCM-AE st rtl = root-label t1 & rtr = root-label t2 & nt ==> <*rtl,rtr*> holds
ex g, g1, g2 being Function of NAT,( the InstructionsF of SCM ^omega) st
( g = f2 . (nt -tree (t1,t2)) & g1 = f2 . t1 & g2 = f2 . t2 & ( for n being Element of NAT holds g . n = H2(nt,g1,g2,n) ) )
let t1, t2 be bin-term; ::_thesis: for rtl, rtr being Symbol of SCM-AE st rtl = root-label t1 & rtr = root-label t2 & nt ==> <*rtl,rtr*> holds
ex g, g1, g2 being Function of NAT,( the InstructionsF of SCM ^omega) st
( g = f2 . (nt -tree (t1,t2)) & g1 = f2 . t1 & g2 = f2 . t2 & ( for n being Element of NAT holds g . n = H2(nt,g1,g2,n) ) )
let rtl, rtr be Symbol of SCM-AE; ::_thesis: ( rtl = root-label t1 & rtr = root-label t2 & nt ==> <*rtl,rtr*> implies ex g, g1, g2 being Function of NAT,( the InstructionsF of SCM ^omega) st
( g = f2 . (nt -tree (t1,t2)) & g1 = f2 . t1 & g2 = f2 . t2 & ( for n being Element of NAT holds g . n = H2(nt,g1,g2,n) ) ) )
assume A15: ( rtl = root-label t1 & rtr = root-label t2 & nt ==> <*rtl,rtr*> ) ; ::_thesis: ex g, g1, g2 being Function of NAT,( the InstructionsF of SCM ^omega) st
( g = f2 . (nt -tree (t1,t2)) & g1 = f2 . t1 & g2 = f2 . t2 & ( for n being Element of NAT holds g . n = H2(nt,g1,g2,n) ) )
consider g, g1, g2 being Function of NAT,( the InstructionsF of SCM ^omega) such that
A16: ( g = f2 . (nt -tree (t1,t2)) & g1 = f2 . t1 & g2 = f2 . t2 & ( for n being Element of NAT holds g . n = ((g1 . n) ^ (g2 . (n + 1))) ^ (Selfwork (nt,n)) ) ) by A8, A15;
take  g ; ::_thesis: ex g1, g2 being Function of NAT,( the InstructionsF of SCM ^omega) st
( g = f2 . (nt -tree (t1,t2)) & g1 = f2 . t1 & g2 = f2 . t2 & ( for n being Element of NAT holds g . n = H2(nt,g1,g2,n) ) )
take  g1 ; ::_thesis: ex g2 being Function of NAT,( the InstructionsF of SCM ^omega) st
( g = f2 . (nt -tree (t1,t2)) & g1 = f2 . t1 & g2 = f2 . t2 & ( for n being Element of NAT holds g . n = H2(nt,g1,g2,n) ) )
take  g2 ; ::_thesis: ( g = f2 . (nt -tree (t1,t2)) & g1 = f2 . t1 & g2 = f2 . t2 & ( for n being Element of NAT holds g . n = H2(nt,g1,g2,n) ) )
thus  ( g = f2 . (nt -tree (t1,t2)) & g1 = f2 . t1 & g2 = f2 . t2 & ( for n being Element of NAT holds g . n = H2(nt,g1,g2,n) ) ) by A16; ::_thesis: verum
end;
end;
thus  f1 = f2 from BINTREE1:sch_6(A9, A13); ::_thesis: verum
end;
end;

:: deftheorem Def11 defines SCM-Compile SCM_COMP:def_11_:_
 for b1 being Function of (TS SCM-AE),(Funcs (NAT,( the InstructionsF of SCM ^omega))) holds
( b1 = SCM-Compile iff ( ( for t being Terminal of SCM-AE ex g being Function of NAT,( the InstructionsF of SCM ^omega) st
( g = b1 . (root-tree t) & ( for n being Element of NAT holds g . n = <%((dl. n) := (@ t))%> ) ) ) & ( for nt being NonTerminal of SCM-AE
for t1, t2 being bin-term
for rtl, rtr being Symbol of SCM-AE st rtl = root-label t1 & rtr = root-label t2 & nt ==> <*rtl,rtr*> holds
ex g, f1, f2 being Function of NAT,( the InstructionsF of SCM ^omega) st
( g = b1 . (nt -tree (t1,t2)) & f1 = b1 . t1 & f2 = b1 . t2 & ( for n being Element of NAT holds g . n = ((f1 . n) ^ (f2 . (n + 1))) ^ (Selfwork (nt,n)) ) ) ) ) );

definition
let term be bin-term;
let aux be Element of NAT ;
func SCM-Compile (term,aux) ->  XFinSequence of the InstructionsF of SCM equals :: SCM_COMP:def 12
(SCM-Compile . term) . aux;
coherence
 (SCM-Compile . term) . aux is XFinSequence of the InstructionsF of SCM
proof
reconsider f = SCM-Compile . term as Function of NAT,( the InstructionsF of SCM ^omega) by FUNCT_2:66;
 f . aux in the InstructionsF of SCM ^omega ;
hence  (SCM-Compile . term) . aux is XFinSequence of the InstructionsF of SCM by AFINSQ_1:def_7; ::_thesis: verum
end;
end;

:: deftheorem  defines SCM-Compile SCM_COMP:def_12_:_
 for term being bin-term
for aux being Element of NAT holds SCM-Compile (term,aux) = (SCM-Compile . term) . aux;

theorem Th7: :: SCM_COMP:7
for t being Terminal of SCM-AE
for n being Element of NAT holds SCM-Compile ((root-tree t),n) = <%((dl. n) := (@ t))%>
proof
let t be Terminal of SCM-AE; ::_thesis: for n being Element of NAT holds SCM-Compile ((root-tree t),n) = <%((dl. n) := (@ t))%>
let n be Element of NAT ; ::_thesis: SCM-Compile ((root-tree t),n) = <%((dl. n) := (@ t))%>
consider g being Function of NAT,( the InstructionsF of SCM ^omega) such that
A1: g = SCM-Compile . (root-tree t) and
A2: for n being Element of NAT holds g . n = <%((dl. n) := (@ t))%> by Def11;
thus  SCM-Compile ((root-tree t),n) = <%((dl. n) := (@ t))%> by A1, A2; ::_thesis: verum
end;

theorem Th8: :: SCM_COMP:8
for nt being NonTerminal of SCM-AE
for t1, t2 being bin-term
for n being Element of NAT
for rtl, rtr being Symbol of SCM-AE st rtl = root-label t1 & rtr = root-label t2 & nt ==> <*rtl,rtr*> holds
SCM-Compile ((nt -tree (t1,t2)),n) = ((SCM-Compile (t1,n)) ^ (SCM-Compile (t2,(n + 1)))) ^ (Selfwork (nt,n))
proof
let nt be NonTerminal of SCM-AE; ::_thesis: for t1, t2 being bin-term
for n being Element of NAT
for rtl, rtr being Symbol of SCM-AE st rtl = root-label t1 & rtr = root-label t2 & nt ==> <*rtl,rtr*> holds
SCM-Compile ((nt -tree (t1,t2)),n) = ((SCM-Compile (t1,n)) ^ (SCM-Compile (t2,(n + 1)))) ^ (Selfwork (nt,n))
let t1, t2 be bin-term; ::_thesis: for n being Element of NAT
for rtl, rtr being Symbol of SCM-AE st rtl = root-label t1 & rtr = root-label t2 & nt ==> <*rtl,rtr*> holds
SCM-Compile ((nt -tree (t1,t2)),n) = ((SCM-Compile (t1,n)) ^ (SCM-Compile (t2,(n + 1)))) ^ (Selfwork (nt,n))
let n be Element of NAT ; ::_thesis: for rtl, rtr being Symbol of SCM-AE st rtl = root-label t1 & rtr = root-label t2 & nt ==> <*rtl,rtr*> holds
SCM-Compile ((nt -tree (t1,t2)),n) = ((SCM-Compile (t1,n)) ^ (SCM-Compile (t2,(n + 1)))) ^ (Selfwork (nt,n))
let rtl, rtr be Symbol of SCM-AE; ::_thesis: ( rtl = root-label t1 & rtr = root-label t2 & nt ==> <*rtl,rtr*> implies SCM-Compile ((nt -tree (t1,t2)),n) = ((SCM-Compile (t1,n)) ^ (SCM-Compile (t2,(n + 1)))) ^ (Selfwork (nt,n)) )
assume A1: ( rtl = root-label t1 & rtr = root-label t2 & nt ==> <*rtl,rtr*> ) ; ::_thesis: SCM-Compile ((nt -tree (t1,t2)),n) = ((SCM-Compile (t1,n)) ^ (SCM-Compile (t2,(n + 1)))) ^ (Selfwork (nt,n))
consider g, f1, f2 being Function of NAT,( the InstructionsF of SCM ^omega) such that
A2: g = SCM-Compile . (nt -tree (t1,t2)) and
A3: f1 = SCM-Compile . t1 and
A4: f2 = SCM-Compile . t2 and
A5: for n being Element of NAT holds g . n = ((f1 . n) ^ (f2 . (n + 1))) ^ (Selfwork (nt,n)) by A1, Def11;
thus  SCM-Compile ((nt -tree (t1,t2)),n) = ((SCM-Compile (t1,n)) ^ (SCM-Compile (t2,(n + 1)))) ^ (Selfwork (nt,n)) by A3, A4, A5, A2; ::_thesis: verum
end;

definition
let t be Terminal of SCM-AE;
func d". t ->  Element of NAT  means :Def13: :: SCM_COMP:def 13
 dl. it = t;
existence
 ex b1 being Element of NAT st dl. b1 = t
proof
 Terminals SCM-AE = [:{1},NAT:] by Def1;
then consider x, y being set  such that
A1: x in {1} and
A2: y in NAT and
A3: t = [x,y] by ZFMISC_1:84;
reconsider k = y as Element of NAT by A2;
take  k ; ::_thesis: dl. k = t
thus  dl. k = t by A1, A3, TARSKI:def_1; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Element of NAT st dl. b1 = t & dl. b2 = t holds
b1 = b2 by AMI_3:10;
end;

:: deftheorem Def13 defines d". SCM_COMP:def_13_:_
 for t being Terminal of SCM-AE
for b2 being Element of NAT holds
( b2 = d". t iff dl. b2 = t );

definition
deffunc H2( Terminal of SCM-AE) ->  Element of NAT = d". $1;
deffunc H3( NonTerminal of SCM-AE, set , set , Element of NAT , Element of NAT ) ->  Element of NAT = max ($4,$5);
let term be bin-term;
func max_Data-Loc_in term ->  Element of NAT  means :Def14: :: SCM_COMP:def 14
 ex f being Function of (TS SCM-AE),NAT st
( it = f . term & ( for t being Terminal of SCM-AE holds f . (root-tree t) = d". t ) & ( for nt being NonTerminal of SCM-AE
for tl, tr being bin-term
for rtl, rtr being Symbol of SCM-AE st rtl = root-label tl & rtr = root-label tr & nt ==> <*rtl,rtr*> holds
for xl, xr being Element of NAT st xl = f . tl & xr = f . tr holds
f . (nt -tree (tl,tr)) = max (xl,xr) ) );
existence
 ex b1 being Element of NAT ex f being Function of (TS SCM-AE),NAT st
( b1 = f . term & ( for t being Terminal of SCM-AE holds f . (root-tree t) = d". t ) & ( for nt being NonTerminal of SCM-AE
for tl, tr being bin-term
for rtl, rtr being Symbol of SCM-AE st rtl = root-label tl & rtr = root-label tr & nt ==> <*rtl,rtr*> holds
for xl, xr being Element of NAT st xl = f . tl & xr = f . tr holds
f . (nt -tree (tl,tr)) = max (xl,xr) ) )
proof
consider f being Function of (TS SCM-AE),NAT such that
A1: ( ( for t being Terminal of SCM-AE holds f . (root-tree t) = H2(t) ) & ( for nt being NonTerminal of SCM-AE
for tl, tr being bin-term
for rtl, rtr being Symbol of SCM-AE st rtl = root-label tl & rtr = root-label tr & nt ==> <*rtl,rtr*> holds
for xl, xr being Element of NAT st xl = f . tl & xr = f . tr holds
f . (nt -tree (tl,tr)) = H3(nt,rtl,rtr,xl,xr) ) ) from BINTREE1:sch_3();
reconsider fterm = f . term as Element of NAT ;
take  fterm ; ::_thesis: ex f being Function of (TS SCM-AE),NAT st
( fterm = f . term & ( for t being Terminal of SCM-AE holds f . (root-tree t) = d". t ) & ( for nt being NonTerminal of SCM-AE
for tl, tr being bin-term
for rtl, rtr being Symbol of SCM-AE st rtl = root-label tl & rtr = root-label tr & nt ==> <*rtl,rtr*> holds
for xl, xr being Element of NAT st xl = f . tl & xr = f . tr holds
f . (nt -tree (tl,tr)) = max (xl,xr) ) )
take  f ; ::_thesis: ( fterm = f . term & ( for t being Terminal of SCM-AE holds f . (root-tree t) = d". t ) & ( for nt being NonTerminal of SCM-AE
for tl, tr being bin-term
for rtl, rtr being Symbol of SCM-AE st rtl = root-label tl & rtr = root-label tr & nt ==> <*rtl,rtr*> holds
for xl, xr being Element of NAT st xl = f . tl & xr = f . tr holds
f . (nt -tree (tl,tr)) = max (xl,xr) ) )
thus  ( fterm = f . term & ( for t being Terminal of SCM-AE holds f . (root-tree t) = d". t ) & ( for nt being NonTerminal of SCM-AE
for tl, tr being bin-term
for rtl, rtr being Symbol of SCM-AE st rtl = root-label tl & rtr = root-label tr & nt ==> <*rtl,rtr*> holds
for xl, xr being Element of NAT st xl = f . tl & xr = f . tr holds
f . (nt -tree (tl,tr)) = max (xl,xr) ) ) by A1; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Element of NAT st ex f being Function of (TS SCM-AE),NAT st
( b1 = f . term & ( for t being Terminal of SCM-AE holds f . (root-tree t) = d". t ) & ( for nt being NonTerminal of SCM-AE
for tl, tr being bin-term
for rtl, rtr being Symbol of SCM-AE st rtl = root-label tl & rtr = root-label tr & nt ==> <*rtl,rtr*> holds
for xl, xr being Element of NAT st xl = f . tl & xr = f . tr holds
f . (nt -tree (tl,tr)) = max (xl,xr) ) ) & ex f being Function of (TS SCM-AE),NAT st
( b2 = f . term & ( for t being Terminal of SCM-AE holds f . (root-tree t) = d". t ) & ( for nt being NonTerminal of SCM-AE
for tl, tr being bin-term
for rtl, rtr being Symbol of SCM-AE st rtl = root-label tl & rtr = root-label tr & nt ==> <*rtl,rtr*> holds
for xl, xr being Element of NAT st xl = f . tl & xr = f . tr holds
f . (nt -tree (tl,tr)) = max (xl,xr) ) ) holds
b1 = b2
proof
let it1, it2 be Element of NAT ; ::_thesis: ( ex f being Function of (TS SCM-AE),NAT st
( it1 = f . term & ( for t being Terminal of SCM-AE holds f . (root-tree t) = d". t ) & ( for nt being NonTerminal of SCM-AE
for tl, tr being bin-term
for rtl, rtr being Symbol of SCM-AE st rtl = root-label tl & rtr = root-label tr & nt ==> <*rtl,rtr*> holds
for xl, xr being Element of NAT st xl = f . tl & xr = f . tr holds
f . (nt -tree (tl,tr)) = max (xl,xr) ) ) & ex f being Function of (TS SCM-AE),NAT st
( it2 = f . term & ( for t being Terminal of SCM-AE holds f . (root-tree t) = d". t ) & ( for nt being NonTerminal of SCM-AE
for tl, tr being bin-term
for rtl, rtr being Symbol of SCM-AE st rtl = root-label tl & rtr = root-label tr & nt ==> <*rtl,rtr*> holds
for xl, xr being Element of NAT st xl = f . tl & xr = f . tr holds
f . (nt -tree (tl,tr)) = max (xl,xr) ) ) implies it1 = it2 )
given f1 being Function of (TS SCM-AE),NAT such that A2: it1 = f1 . term and
A3: ( ( for t being Terminal of SCM-AE holds f1 . (root-tree t) = H2(t) ) & ( for nt being NonTerminal of SCM-AE
for tl, tr being bin-term
for rtl, rtr being Symbol of SCM-AE st rtl = root-label tl & rtr = root-label tr & nt ==> <*rtl,rtr*> holds
for xl, xr being Element of NAT st xl = f1 . tl & xr = f1 . tr holds
f1 . (nt -tree (tl,tr)) = H3(nt,rtl,rtr,xl,xr) ) ) ; ::_thesis: ( for f being Function of (TS SCM-AE),NAT holds
( not it2 = f . term or ex t being Terminal of SCM-AE st not f . (root-tree t) = d". t or ex nt being NonTerminal of SCM-AE ex tl, tr being bin-term ex rtl, rtr being Symbol of SCM-AE st
( rtl = root-label tl & rtr = root-label tr & nt ==> <*rtl,rtr*> & ex xl, xr being Element of NAT st
( xl = f . tl & xr = f . tr & not f . (nt -tree (tl,tr)) = max (xl,xr) ) ) ) or it1 = it2 )
given f2 being Function of (TS SCM-AE),NAT such that A4: it2 = f2 . term and
A5: ( ( for t being Terminal of SCM-AE holds f2 . (root-tree t) = H2(t) ) & ( for nt being NonTerminal of SCM-AE
for tl, tr being bin-term
for rtl, rtr being Symbol of SCM-AE st rtl = root-label tl & rtr = root-label tr & nt ==> <*rtl,rtr*> holds
for xl, xr being Element of NAT st xl = f2 . tl & xr = f2 . tr holds
f2 . (nt -tree (tl,tr)) = H3(nt,rtl,rtr,xl,xr) ) ) ; ::_thesis: it1 = it2
 f1 = f2 from BINTREE1:sch_4(A3, A5);
hence  it1 = it2 by A2, A4; ::_thesis: verum
end;
end;

:: deftheorem Def14 defines max_Data-Loc_in SCM_COMP:def_14_:_
 for term being bin-term
for b2 being Element of NAT holds
( b2 = max_Data-Loc_in term iff ex f being Function of (TS SCM-AE),NAT st
( b2 = f . term & ( for t being Terminal of SCM-AE holds f . (root-tree t) = d". t ) & ( for nt being NonTerminal of SCM-AE
for tl, tr being bin-term
for rtl, rtr being Symbol of SCM-AE st rtl = root-label tl & rtr = root-label tr & nt ==> <*rtl,rtr*> holds
for xl, xr being Element of NAT st xl = f . tl & xr = f . tr holds
f . (nt -tree (tl,tr)) = max (xl,xr) ) ) );

set Term = the bin-term;

consider f being Function of (TS SCM-AE),NAT such that
 max_Data-Loc_in the bin-term = f . the bin-term and
Lm4:  for t being Terminal of SCM-AE holds f . (root-tree t) = d". t and
Lm5:  for nt being NonTerminal of SCM-AE
for tl, tr being bin-term
for rtl, rtr being Symbol of SCM-AE st rtl = root-label tl & rtr = root-label tr & nt ==> <*rtl,rtr*> holds
for xl, xr being Element of NAT st xl = f . tl & xr = f . tr holds
f . (nt -tree (tl,tr)) = max (xl,xr) by Def14;

theorem Th9: :: SCM_COMP:9
for t being Terminal of SCM-AE holds max_Data-Loc_in (root-tree t) = d". t
proof
let t be Terminal of SCM-AE; ::_thesis: max_Data-Loc_in (root-tree t) = d". t
 max_Data-Loc_in (root-tree t) = f . (root-tree t) by Def14, Lm4, Lm5;
hence  max_Data-Loc_in (root-tree t) = d". t by Lm4; ::_thesis: verum
end;

Lm6:  NonTerminals SCM-AE = [:1,5:]
by Def1;

theorem Th10: :: SCM_COMP:10
for nt being NonTerminal of SCM-AE
for tl, tr being bin-term holds max_Data-Loc_in (nt -tree (tl,tr)) = max ((max_Data-Loc_in tl),(max_Data-Loc_in tr))
proof
let nt be NonTerminal of SCM-AE; ::_thesis: for tl, tr being bin-term holds max_Data-Loc_in (nt -tree (tl,tr)) = max ((max_Data-Loc_in tl),(max_Data-Loc_in tr))
let tl, tr be bin-term; ::_thesis: max_Data-Loc_in (nt -tree (tl,tr)) = max ((max_Data-Loc_in tl),(max_Data-Loc_in tr))
A1: ( max_Data-Loc_in tl = f . tl & max_Data-Loc_in tr = f . tr ) by Def14, Lm4, Lm5;
 ( nt ==> <*(root-label tl),(root-label tr)*> & max_Data-Loc_in (nt -tree (tl,tr)) = f . (nt -tree (tl,tr)) ) by Def1, Def14, Lm4, Lm5, Lm6;
hence  max_Data-Loc_in (nt -tree (tl,tr)) = max ((max_Data-Loc_in tl),(max_Data-Loc_in tr)) by A1, Lm5; ::_thesis: verum
end;

defpred S1[ bin-term] means  for s1, s2 being State of SCM st ( for dn being Element of NAT st dn <= max_Data-Loc_in $1 holds
s1 . (dl. dn) = s2 . (dl. dn) ) holds
$1 @ s1 = $1 @ s2;

Lm7: now__::_thesis:_for_s_being_Terminal_of_SCM-AE_holds_S1[_root-tree_s]
let s be Terminal of SCM-AE; ::_thesis: S1[ root-tree s]
thus  S1[ root-tree s] ::_thesis: verum
proof
let s1, s2 be State of SCM; ::_thesis: ( ( for dn being Element of NAT st dn <= max_Data-Loc_in (root-tree s) holds
s1 . (dl. dn) = s2 . (dl. dn) ) implies (root-tree s) @ s1 = (root-tree s) @ s2 )
assume A1: for dn being Element of NAT st dn <= max_Data-Loc_in (root-tree s) holds
s1 . (dl. dn) = s2 . (dl. dn) ; ::_thesis: (root-tree s) @ s1 = (root-tree s) @ s2
 d". s <= max_Data-Loc_in (root-tree s) by Th9;
then A2: s1 . (dl. (d". s)) = s2 . (dl. (d". s)) by A1;
A3: (root-tree s) @ s1 = s1 . s by Th4;
 ( s1 . s = s1 . (dl. (d". s)) & s2 . s = s2 . (dl. (d". s)) ) by Def13;
hence  (root-tree s) @ s1 = (root-tree s) @ s2 by A2, A3, Th4; ::_thesis: verum
end;
end;

Lm8: now__::_thesis:_for_nt_being_NonTerminal_of_SCM-AE
for_tl,_tr_being_Element_of_TS_SCM-AE_st_nt_==>_<*(root-label_tl),(root-label_tr)*>_&_S1[tl]_&_S1[tr]_holds_
S1[nt_-tree_(tl,tr)]
let nt be NonTerminal of SCM-AE; ::_thesis: for tl, tr being Element of TS SCM-AE st nt ==> <*(root-label tl),(root-label tr)*> & S1[tl] & S1[tr] holds
S1[nt -tree (tl,tr)]
let tl, tr be Element of TS SCM-AE; ::_thesis: ( nt ==> <*(root-label tl),(root-label tr)*> & S1[tl] & S1[tr] implies S1[nt -tree (tl,tr)] )
assume that
 nt ==> <*(root-label tl),(root-label tr)*> and
A1: S1[tl] and
A2: S1[tr] ; ::_thesis: S1[nt -tree (tl,tr)]
thus  S1[nt -tree (tl,tr)] ::_thesis: verum
proof
let s1, s2 be State of SCM; ::_thesis: ( ( for dn being Element of NAT st dn <= max_Data-Loc_in (nt -tree (tl,tr)) holds
s1 . (dl. dn) = s2 . (dl. dn) ) implies (nt -tree (tl,tr)) @ s1 = (nt -tree (tl,tr)) @ s2 )
assume A3: for dn being Element of NAT st dn <= max_Data-Loc_in (nt -tree (tl,tr)) holds
s1 . (dl. dn) = s2 . (dl. dn) ; ::_thesis: (nt -tree (tl,tr)) @ s1 = (nt -tree (tl,tr)) @ s2
now__::_thesis:_for_dn_being_Element_of_NAT_st_dn_<=_max_Data-Loc_in_tl_holds_
s1_._(dl._dn)_=_s2_._(dl._dn)
set ml = max_Data-Loc_in tl;
set mr = max_Data-Loc_in tr;
let dn be Element of NAT ; ::_thesis: ( dn <= max_Data-Loc_in tl implies s1 . (dl. dn) = s2 . (dl. dn) )
A4: max_Data-Loc_in tl <= max ((max_Data-Loc_in tl),(max_Data-Loc_in tr)) by XXREAL_0:25;
assume  dn <= max_Data-Loc_in tl ; ::_thesis: s1 . (dl. dn) = s2 . (dl. dn)
then  dn <= max ((max_Data-Loc_in tl),(max_Data-Loc_in tr)) by A4, XXREAL_0:2;
then  dn <= max_Data-Loc_in (nt -tree (tl,tr)) by Th10;
hence  s1 . (dl. dn) = s2 . (dl. dn) by A3; ::_thesis: verum
end;
then A5: tl @ s1 = tl @ s2 by A1;
now__::_thesis:_for_dn_being_Element_of_NAT_st_dn_<=_max_Data-Loc_in_tr_holds_
s1_._(dl._dn)_=_s2_._(dl._dn)
set ml = max_Data-Loc_in tl;
set mr = max_Data-Loc_in tr;
let dn be Element of NAT ; ::_thesis: ( dn <= max_Data-Loc_in tr implies s1 . (dl. dn) = s2 . (dl. dn) )
A6: max_Data-Loc_in tr <= max ((max_Data-Loc_in tl),(max_Data-Loc_in tr)) by XXREAL_0:25;
assume  dn <= max_Data-Loc_in tr ; ::_thesis: s1 . (dl. dn) = s2 . (dl. dn)
then  dn <= max ((max_Data-Loc_in tl),(max_Data-Loc_in tr)) by A6, XXREAL_0:2;
then  dn <= max_Data-Loc_in (nt -tree (tl,tr)) by Th10;
hence  s1 . (dl. dn) = s2 . (dl. dn) by A3; ::_thesis: verum
end;
then A7: tr @ s1 = tr @ s2 by A2;
 (nt -tree (tl,tr)) @ s1 = nt -Meaning_on ((tl @ s1),(tr @ s1)) by Th5;
hence  (nt -tree (tl,tr)) @ s1 = (nt -tree (tl,tr)) @ s2 by A5, A7, Th5; ::_thesis: verum
end;
end;

theorem Th11: :: SCM_COMP:11
for term being bin-term
for s1, s2 being State of SCM st ( for dn being Element of NAT st dn <= max_Data-Loc_in term holds
s1 . (dl. dn) = s2 . (dl. dn) ) holds
term @ s1 = term @ s2
proof
thus  for t being bin-term holds S1[t] from BINTREE1:sch_2(Lm7, Lm8); ::_thesis: verum
end;

 defpred S2[ bin-term] means  for F being Instruction-Sequence of SCM
for aux, n being Element of NAT st Shift ((SCM-Compile ($1,aux)),n) c= F holds
for s being b3 -started State of SCM st aux > max_Data-Loc_in $1 holds
ex i being Element of NAT ex u being State of SCM st
( u = Comput (F,s,(i + 1)) & i + 1 = len (SCM-Compile ($1,aux)) & IC (Comput (F,s,i)) = n + i & IC u = n + (i + 1) & u . (dl. aux) = $1 @ s & ( for dn being Element of NAT st dn < aux holds
s . (dl. dn) = u . (dl. dn) ) );

theorem Th12: :: SCM_COMP:12
for F being Instruction-Sequence of SCM
for term being bin-term
for aux, n being Element of NAT st Shift ((SCM-Compile (term,aux)),n) c= F holds
for s being b4 -started State of SCM st aux > max_Data-Loc_in term holds
ex i being Element of NAT ex u being State of SCM st
( u = Comput (F,s,(i + 1)) & i + 1 = len (SCM-Compile (term,aux)) & IC (Comput (F,s,i)) = n + i & IC u = n + (i + 1) & u . (dl. aux) = term @ s & ( for dn being Element of NAT st dn < aux holds
s . (dl. dn) = u . (dl. dn) ) )
proof
A1: for nt being NonTerminal of SCM-AE
for tl, tr being bin-term st nt ==> <*(root-label tl),(root-label tr)*> & S2[tl] & S2[tr] holds
S2[nt -tree (tl,tr)]
proof
let nt be NonTerminal of SCM-AE; ::_thesis: for tl, tr being bin-term st nt ==> <*(root-label tl),(root-label tr)*> & S2[tl] & S2[tr] holds
S2[nt -tree (tl,tr)]
let tl, tr be bin-term; ::_thesis: ( nt ==> <*(root-label tl),(root-label tr)*> & S2[tl] & S2[tr] implies S2[nt -tree (tl,tr)] )
assume that
A2: nt ==> <*(root-label tl),(root-label tr)*> and
A3: S2[tl] and
A4: S2[tr] ; ::_thesis: S2[nt -tree (tl,tr)]
let F be Instruction-Sequence of SCM; ::_thesis: for aux, n being Element of NAT st Shift ((SCM-Compile ((nt -tree (tl,tr)),aux)),n) c= F holds
for s being b2 -started State of SCM st aux > max_Data-Loc_in (nt -tree (tl,tr)) holds
ex i being Element of NAT ex u being State of SCM st
( u = Comput (F,s,(i + 1)) & i + 1 = len (SCM-Compile ((nt -tree (tl,tr)),aux)) & IC (Comput (F,s,i)) = n + i & IC u = n + (i + 1) & u . (dl. aux) = (nt -tree (tl,tr)) @ s & ( for dn being Element of NAT st dn < aux holds
s . (dl. dn) = u . (dl. dn) ) )
let aux, n be Element of NAT ; ::_thesis: ( Shift ((SCM-Compile ((nt -tree (tl,tr)),aux)),n) c= F implies for s being n -started State of SCM st aux > max_Data-Loc_in (nt -tree (tl,tr)) holds
ex i being Element of NAT ex u being State of SCM st
( u = Comput (F,s,(i + 1)) & i + 1 = len (SCM-Compile ((nt -tree (tl,tr)),aux)) & IC (Comput (F,s,i)) = n + i & IC u = n + (i + 1) & u . (dl. aux) = (nt -tree (tl,tr)) @ s & ( for dn being Element of NAT st dn < aux holds
s . (dl. dn) = u . (dl. dn) ) ) )
assume A5: Shift ((SCM-Compile ((nt -tree (tl,tr)),aux)),n) c= F ; ::_thesis: for s being n -started State of SCM st aux > max_Data-Loc_in (nt -tree (tl,tr)) holds
ex i being Element of NAT ex u being State of SCM st
( u = Comput (F,s,(i + 1)) & i + 1 = len (SCM-Compile ((nt -tree (tl,tr)),aux)) & IC (Comput (F,s,i)) = n + i & IC u = n + (i + 1) & u . (dl. aux) = (nt -tree (tl,tr)) @ s & ( for dn being Element of NAT st dn < aux holds
s . (dl. dn) = u . (dl. dn) ) )
let s be n -started State of SCM; ::_thesis: ( aux > max_Data-Loc_in (nt -tree (tl,tr)) implies ex i being Element of NAT ex u being State of SCM st
( u = Comput (F,s,(i + 1)) & i + 1 = len (SCM-Compile ((nt -tree (tl,tr)),aux)) & IC (Comput (F,s,i)) = n + i & IC u = n + (i + 1) & u . (dl. aux) = (nt -tree (tl,tr)) @ s & ( for dn being Element of NAT st dn < aux holds
s . (dl. dn) = u . (dl. dn) ) ) )
assume A6: aux > max_Data-Loc_in (nt -tree (tl,tr)) ; ::_thesis: ex i being Element of NAT ex u being State of SCM st
( u = Comput (F,s,(i + 1)) & i + 1 = len (SCM-Compile ((nt -tree (tl,tr)),aux)) & IC (Comput (F,s,i)) = n + i & IC u = n + (i + 1) & u . (dl. aux) = (nt -tree (tl,tr)) @ s & ( for dn being Element of NAT st dn < aux holds
s . (dl. dn) = u . (dl. dn) ) )
A7: max_Data-Loc_in (nt -tree (tl,tr)) = max ((max_Data-Loc_in tl),(max_Data-Loc_in tr)) by Th10;
then  max_Data-Loc_in tl <= max_Data-Loc_in (nt -tree (tl,tr)) by XXREAL_0:25;
then A8: max_Data-Loc_in tl < aux by A6, XXREAL_0:2;
 max_Data-Loc_in tr <= max_Data-Loc_in (nt -tree (tl,tr)) by A7, XXREAL_0:25;
then A9: max_Data-Loc_in tr < aux by A6, XXREAL_0:2;
then A10: max_Data-Loc_in tr < aux + 1 by NAT_1:13;
A11: SCM-Compile ((nt -tree (tl,tr)),aux) = ((SCM-Compile (tl,aux)) ^ (SCM-Compile (tr,(aux + 1)))) ^ (Selfwork (nt,aux)) by A2, Th8;
then  SCM-Compile ((nt -tree (tl,tr)),aux) = (SCM-Compile (tl,aux)) ^ ((SCM-Compile (tr,(aux + 1))) ^ (Selfwork (nt,aux))) by AFINSQ_1:27;
then  Shift ((SCM-Compile (tl,aux)),n) c= F by A5, AFINSQ_1:82;
then consider i1 being Element of NAT , u1 being State of SCM such that
A12: u1 = Comput (F,s,(i1 + 1)) and
A13: i1 + 1 = len (SCM-Compile (tl,aux)) and
 IC (Comput (F,s,i1)) = n + i1 and
A14: IC u1 = n + (i1 + 1) and
A15: u1 . (dl. aux) = tl @ s and
A16: for dn being Element of NAT st dn < aux holds
s . (dl. dn) = u1 . (dl. dn) by A3, A8;
A17: u1 is n + (i1 + 1) -started State of SCM by A14, MEMSTR_0:def_12;
 SCM-Compile ((nt -tree (tl,tr)),aux) = (SCM-Compile (tl,aux)) ^ ((SCM-Compile (tr,(aux + 1))) ^ (Selfwork (nt,aux))) by A11, AFINSQ_1:27;
then  Shift (((SCM-Compile (tr,(aux + 1))) ^ (Selfwork (nt,aux))),(n + (i1 + 1))) c= F by A5, A13, AFINSQ_1:83;
then  Shift ((SCM-Compile (tr,(aux + 1))),(n + (i1 + 1))) c= F by AFINSQ_1:82;
then consider i2 being Element of NAT , u2 being State of SCM such that
A18: u2 = Comput (F,u1,(i2 + 1)) and
A19: i2 + 1 = len (SCM-Compile (tr,(aux + 1))) and
 IC (Comput (F,u1,i2)) = (n + (i1 + 1)) + i2 and
A20: IC u2 = (n + (i1 + 1)) + (i2 + 1) and
A21: u2 . (dl. (aux + 1)) = tr @ u1 and
A22: for dn being Element of NAT st dn < aux + 1 holds
u1 . (dl. dn) = u2 . (dl. dn) by A4, A10, A17;
A23: u2 = Comput (F,s,((i1 + 1) + (i2 + 1))) by A12, A18, EXTPRO_1:4;
A24: now__::_thesis:_for_n_being_Element_of_NAT_st_n_<=_max_Data-Loc_in_tr_holds_
s_._(dl._n)_=_u1_._(dl._n)
let n be Element of NAT ; ::_thesis: ( n <= max_Data-Loc_in tr implies s . (dl. n) = u1 . (dl. n) )
assume  n <= max_Data-Loc_in tr ; ::_thesis: s . (dl. n) = u1 . (dl. n)
then  n < aux by A9, XXREAL_0:2;
hence  s . (dl. n) = u1 . (dl. n) by A16; ::_thesis: verum
end;
A25: aux < aux + 1 by NAT_1:13;
A26: (nt -tree (tl,tr)) @ s = nt -Meaning_on ((tl @ s),(tr @ s)) by Th5;
A27: len ((SCM-Compile (tl,aux)) ^ (SCM-Compile (tr,(aux + 1)))) = (i1 + 1) + (i2 + 1) by A13, A19, AFINSQ_1:17;
percases ( nt = [0,0] or nt = [0,1] or nt = [0,2] or nt = [0,3] or nt = [0,4] ) by Th1;
supposeA28: nt = [0,0] ; ::_thesis: ex i being Element of NAT ex u being State of SCM st
( u = Comput (F,s,(i + 1)) & i + 1 = len (SCM-Compile ((nt -tree (tl,tr)),aux)) & IC (Comput (F,s,i)) = n + i & IC u = n + (i + 1) & u . (dl. aux) = (nt -tree (tl,tr)) @ s & ( for dn being Element of NAT st dn < aux holds
s . (dl. dn) = u . (dl. dn) ) )
then A29: nt -Meaning_on ((tl @ s),(tr @ s)) = (tl @ s) + (tr @ s) by Def8;
take i = (i1 + 1) + (i2 + 1); ::_thesis: ex u being State of SCM st
( u = Comput (F,s,(i + 1)) & i + 1 = len (SCM-Compile ((nt -tree (tl,tr)),aux)) & IC (Comput (F,s,i)) = n + i & IC u = n + (i + 1) & u . (dl. aux) = (nt -tree (tl,tr)) @ s & ( for dn being Element of NAT st dn < aux holds
s . (dl. dn) = u . (dl. dn) ) )
take u = Comput (F,s,(i + 1)); ::_thesis: ( u = Comput (F,s,(i + 1)) & i + 1 = len (SCM-Compile ((nt -tree (tl,tr)),aux)) & IC (Comput (F,s,i)) = n + i & IC u = n + (i + 1) & u . (dl. aux) = (nt -tree (tl,tr)) @ s & ( for dn being Element of NAT st dn < aux holds
s . (dl. dn) = u . (dl. dn) ) )
thus  u = Comput (F,s,(i + 1)) ; ::_thesis: ( i + 1 = len (SCM-Compile ((nt -tree (tl,tr)),aux)) & IC (Comput (F,s,i)) = n + i & IC u = n + (i + 1) & u . (dl. aux) = (nt -tree (tl,tr)) @ s & ( for dn being Element of NAT st dn < aux holds
s . (dl. dn) = u . (dl. dn) ) )
A30: Selfwork (nt,aux) = <%(AddTo ((dl. aux),(dl. (aux + 1))))%> by A28, Def10;
then A31: len (Selfwork (nt,aux)) = 1 by AFINSQ_1:34;
hence  i + 1 = len (SCM-Compile ((nt -tree (tl,tr)),aux)) by A11, A27, AFINSQ_1:17; ::_thesis: ( IC (Comput (F,s,i)) = n + i & IC u = n + (i + 1) & u . (dl. aux) = (nt -tree (tl,tr)) @ s & ( for dn being Element of NAT st dn < aux holds
s . (dl. dn) = u . (dl. dn) ) )
thus  IC (Comput (F,s,i)) = n + i by A12, A18, A20, EXTPRO_1:4; ::_thesis: ( IC u = n + (i + 1) & u . (dl. aux) = (nt -tree (tl,tr)) @ s & ( for dn being Element of NAT st dn < aux holds
s . (dl. dn) = u . (dl. dn) ) )
 len (SCM-Compile ((nt -tree (tl,tr)),aux)) = ((i1 + 1) + (i2 + 1)) + 1 by A11, A27, A31, AFINSQ_1:17;
then  i < len (SCM-Compile ((nt -tree (tl,tr)),aux)) by NAT_1:13;
then  i in dom (SCM-Compile ((nt -tree (tl,tr)),aux)) by NAT_1:44;
then A32: F . (n + i) = (SCM-Compile ((nt -tree (tl,tr)),aux)) . i by A5, FINSEQ_2:146
.= AddTo ((dl. aux),(dl. (aux + 1))) by A27, A11, A30, AFINSQ_1:36 ;
hence  IC u = (n + i) + 1 by A20, A23, SCM_1:5
.= n + (i + 1) ;
::_thesis: ( u . (dl. aux) = (nt -tree (tl,tr)) @ s & ( for dn being Element of NAT st dn < aux holds
s . (dl. dn) = u . (dl. dn) ) )
thus u . (dl. aux) = (u2 . (dl. aux)) + (u2 . (dl. (aux + 1))) by A20, A23, A32, SCM_1:5
.= (u1 . (dl. aux)) + (tr @ u1) by A21, A22, A25
.= (nt -tree (tl,tr)) @ s by A15, A26, A24, A29, Th11 ; ::_thesis: for dn being Element of NAT st dn < aux holds
s . (dl. dn) = u . (dl. dn)
let dn be Element of NAT ; ::_thesis: ( dn < aux implies s . (dl. dn) = u . (dl. dn) )
assume A33: dn < aux ; ::_thesis: s . (dl. dn) = u . (dl. dn)
then  dn < aux + 1 by NAT_1:13;
then A34: u1 . (dl. dn) = u2 . (dl. dn) by A22;
 dl. dn <> dl. aux by A33, AMI_3:10;
then  u . (dl. dn) = u2 . (dl. dn) by A20, A23, A32, SCM_1:5;
hence  s . (dl. dn) = u . (dl. dn) by A16, A33, A34; ::_thesis: verum
end;
supposeA35: nt = [0,1] ; ::_thesis: ex i being Element of NAT ex u being State of SCM st
( u = Comput (F,s,(i + 1)) & i + 1 = len (SCM-Compile ((nt -tree (tl,tr)),aux)) & IC (Comput (F,s,i)) = n + i & IC u = n + (i + 1) & u . (dl. aux) = (nt -tree (tl,tr)) @ s & ( for dn being Element of NAT st dn < aux holds
s . (dl. dn) = u . (dl. dn) ) )
then A36: nt -Meaning_on ((tl @ s),(tr @ s)) = (tl @ s) - (tr @ s) by Def8;
take i = (i1 + 1) + (i2 + 1); ::_thesis: ex u being State of SCM st
( u = Comput (F,s,(i + 1)) & i + 1 = len (SCM-Compile ((nt -tree (tl,tr)),aux)) & IC (Comput (F,s,i)) = n + i & IC u = n + (i + 1) & u . (dl. aux) = (nt -tree (tl,tr)) @ s & ( for dn being Element of NAT st dn < aux holds
s . (dl. dn) = u . (dl. dn) ) )
take u = Comput (F,s,(i + 1)); ::_thesis: ( u = Comput (F,s,(i + 1)) & i + 1 = len (SCM-Compile ((nt -tree (tl,tr)),aux)) & IC (Comput (F,s,i)) = n + i & IC u = n + (i + 1) & u . (dl. aux) = (nt -tree (tl,tr)) @ s & ( for dn being Element of NAT st dn < aux holds
s . (dl. dn) = u . (dl. dn) ) )
thus  u = Comput (F,s,(i + 1)) ; ::_thesis: ( i + 1 = len (SCM-Compile ((nt -tree (tl,tr)),aux)) & IC (Comput (F,s,i)) = n + i & IC u = n + (i + 1) & u . (dl. aux) = (nt -tree (tl,tr)) @ s & ( for dn being Element of NAT st dn < aux holds
s . (dl. dn) = u . (dl. dn) ) )
A37: Selfwork (nt,aux) = <%(SubFrom ((dl. aux),(dl. (aux + 1))))%> by A35, Def10;
then A38: len (Selfwork (nt,aux)) = 1 by AFINSQ_1:34;
hence  i + 1 = len (SCM-Compile ((nt -tree (tl,tr)),aux)) by A11, A27, AFINSQ_1:17; ::_thesis: ( IC (Comput (F,s,i)) = n + i & IC u = n + (i + 1) & u . (dl. aux) = (nt -tree (tl,tr)) @ s & ( for dn being Element of NAT st dn < aux holds
s . (dl. dn) = u . (dl. dn) ) )
thus  IC (Comput (F,s,i)) = n + i by A12, A18, A20, EXTPRO_1:4; ::_thesis: ( IC u = n + (i + 1) & u . (dl. aux) = (nt -tree (tl,tr)) @ s & ( for dn being Element of NAT st dn < aux holds
s . (dl. dn) = u . (dl. dn) ) )
 len (SCM-Compile ((nt -tree (tl,tr)),aux)) = ((i1 + 1) + (i2 + 1)) + 1 by A11, A27, A38, AFINSQ_1:17;
then  i < len (SCM-Compile ((nt -tree (tl,tr)),aux)) by NAT_1:13;
then  i in dom (SCM-Compile ((nt -tree (tl,tr)),aux)) by NAT_1:44;
then A39: F . (n + i) = (SCM-Compile ((nt -tree (tl,tr)),aux)) . i by A5, FINSEQ_2:146
.= SubFrom ((dl. aux),(dl. (aux + 1))) by A11, A27, A37, AFINSQ_1:36 ;
hence  IC u = (n + i) + 1 by A20, A23, SCM_1:6
.= n + (i + 1) ;
::_thesis: ( u . (dl. aux) = (nt -tree (tl,tr)) @ s & ( for dn being Element of NAT st dn < aux holds
s . (dl. dn) = u . (dl. dn) ) )
thus u . (dl. aux) = (u2 . (dl. aux)) - (u2 . (dl. (aux + 1))) by A20, A23, A39, SCM_1:6
.= (u1 . (dl. aux)) - (tr @ u1) by A21, A22, A25
.= (nt -tree (tl,tr)) @ s by A15, A26, A24, A36, Th11 ; ::_thesis: for dn being Element of NAT st dn < aux holds
s . (dl. dn) = u . (dl. dn)
let dn be Element of NAT ; ::_thesis: ( dn < aux implies s . (dl. dn) = u . (dl. dn) )
assume A40: dn < aux ; ::_thesis: s . (dl. dn) = u . (dl. dn)
then  dn < aux + 1 by NAT_1:13;
then A41: u1 . (dl. dn) = u2 . (dl. dn) by A22;
 dl. dn <> dl. aux by A40, AMI_3:10;
then  u . (dl. dn) = u2 . (dl. dn) by A20, A23, A39, SCM_1:6;
hence  s . (dl. dn) = u . (dl. dn) by A16, A40, A41; ::_thesis: verum
end;
supposeA42: nt = [0,2] ; ::_thesis: ex i being Element of NAT ex u being State of SCM st
( u = Comput (F,s,(i + 1)) & i + 1 = len (SCM-Compile ((nt -tree (tl,tr)),aux)) & IC (Comput (F,s,i)) = n + i & IC u = n + (i + 1) & u . (dl. aux) = (nt -tree (tl,tr)) @ s & ( for dn being Element of NAT st dn < aux holds
s . (dl. dn) = u . (dl. dn) ) )
then A43: nt -Meaning_on ((tl @ s),(tr @ s)) = (tl @ s) * (tr @ s) by Def8;
take i = (i1 + 1) + (i2 + 1); ::_thesis: ex u being State of SCM st
( u = Comput (F,s,(i + 1)) & i + 1 = len (SCM-Compile ((nt -tree (tl,tr)),aux)) & IC (Comput (F,s,i)) = n + i & IC u = n + (i + 1) & u . (dl. aux) = (nt -tree (tl,tr)) @ s & ( for dn being Element of NAT st dn < aux holds
s . (dl. dn) = u . (dl. dn) ) )
take u = Comput (F,s,(i + 1)); ::_thesis: ( u = Comput (F,s,(i + 1)) & i + 1 = len (SCM-Compile ((nt -tree (tl,tr)),aux)) & IC (Comput (F,s,i)) = n + i & IC u = n + (i + 1) & u . (dl. aux) = (nt -tree (tl,tr)) @ s & ( for dn being Element of NAT st dn < aux holds
s . (dl. dn) = u . (dl. dn) ) )
thus  u = Comput (F,s,(i + 1)) ; ::_thesis: ( i + 1 = len (SCM-Compile ((nt -tree (tl,tr)),aux)) & IC (Comput (F,s,i)) = n + i & IC u = n + (i + 1) & u . (dl. aux) = (nt -tree (tl,tr)) @ s & ( for dn being Element of NAT st dn < aux holds
s . (dl. dn) = u . (dl. dn) ) )
A44: Selfwork (nt,aux) = <%(MultBy ((dl. aux),(dl. (aux + 1))))%> by A42, Def10;
then A45: len (Selfwork (nt,aux)) = 1 by AFINSQ_1:34;
hence  i + 1 = len (SCM-Compile ((nt -tree (tl,tr)),aux)) by A11, A27, AFINSQ_1:17; ::_thesis: ( IC (Comput (F,s,i)) = n + i & IC u = n + (i + 1) & u . (dl. aux) = (nt -tree (tl,tr)) @ s & ( for dn being Element of NAT st dn < aux holds
s . (dl. dn) = u . (dl. dn) ) )
thus  IC (Comput (F,s,i)) = n + i by A12, A18, A20, EXTPRO_1:4; ::_thesis: ( IC u = n + (i + 1) & u . (dl. aux) = (nt -tree (tl,tr)) @ s & ( for dn being Element of NAT st dn < aux holds
s . (dl. dn) = u . (dl. dn) ) )
 len (SCM-Compile ((nt -tree (tl,tr)),aux)) = ((i1 + 1) + (i2 + 1)) + 1 by A11, A27, A45, AFINSQ_1:17;
then  i < len (SCM-Compile ((nt -tree (tl,tr)),aux)) by NAT_1:13;
then  i in dom (SCM-Compile ((nt -tree (tl,tr)),aux)) by NAT_1:44;
then A46: F . (n + i) = (SCM-Compile ((nt -tree (tl,tr)),aux)) . i by A5, FINSEQ_2:146
.= MultBy ((dl. aux),(dl. (aux + 1))) by A11, A27, A44, AFINSQ_1:36 ;
hence  IC u = (n + i) + 1 by A20, A23, SCM_1:7
.= n + (i + 1) ;
::_thesis: ( u . (dl. aux) = (nt -tree (tl,tr)) @ s & ( for dn being Element of NAT st dn < aux holds
s . (dl. dn) = u . (dl. dn) ) )
thus u . (dl. aux) = (u2 . (dl. aux)) * (u2 . (dl. (aux + 1))) by A20, A23, A46, SCM_1:7
.= (u1 . (dl. aux)) * (tr @ u1) by A21, A22, A25
.= (nt -tree (tl,tr)) @ s by A15, A26, A24, A43, Th11 ; ::_thesis: for dn being Element of NAT st dn < aux holds
s . (dl. dn) = u . (dl. dn)
let dn be Element of NAT ; ::_thesis: ( dn < aux implies s . (dl. dn) = u . (dl. dn) )
assume A47: dn < aux ; ::_thesis: s . (dl. dn) = u . (dl. dn)
then  dn < aux + 1 by NAT_1:13;
then A48: u1 . (dl. dn) = u2 . (dl. dn) by A22;
 dl. dn <> dl. aux by A47, AMI_3:10;
then  u . (dl. dn) = u2 . (dl. dn) by A20, A23, A46, SCM_1:7;
hence  s . (dl. dn) = u . (dl. dn) by A16, A47, A48; ::_thesis: verum
end;
supposeA49: nt = [0,3] ; ::_thesis: ex i being Element of NAT ex u being State of SCM st
( u = Comput (F,s,(i + 1)) & i + 1 = len (SCM-Compile ((nt -tree (tl,tr)),aux)) & IC (Comput (F,s,i)) = n + i & IC u = n + (i + 1) & u . (dl. aux) = (nt -tree (tl,tr)) @ s & ( for dn being Element of NAT st dn < aux holds
s . (dl. dn) = u . (dl. dn) ) )
take i = (i1 + 1) + (i2 + 1); ::_thesis: ex u being State of SCM st
( u = Comput (F,s,(i + 1)) & i + 1 = len (SCM-Compile ((nt -tree (tl,tr)),aux)) & IC (Comput (F,s,i)) = n + i & IC u = n + (i + 1) & u . (dl. aux) = (nt -tree (tl,tr)) @ s & ( for dn being Element of NAT st dn < aux holds
s . (dl. dn) = u . (dl. dn) ) )
take u = Comput (F,s,(i + 1)); ::_thesis: ( u = Comput (F,s,(i + 1)) & i + 1 = len (SCM-Compile ((nt -tree (tl,tr)),aux)) & IC (Comput (F,s,i)) = n + i & IC u = n + (i + 1) & u . (dl. aux) = (nt -tree (tl,tr)) @ s & ( for dn being Element of NAT st dn < aux holds
s . (dl. dn) = u . (dl. dn) ) )
thus  u = Comput (F,s,(i + 1)) ; ::_thesis: ( i + 1 = len (SCM-Compile ((nt -tree (tl,tr)),aux)) & IC (Comput (F,s,i)) = n + i & IC u = n + (i + 1) & u . (dl. aux) = (nt -tree (tl,tr)) @ s & ( for dn being Element of NAT st dn < aux holds
s . (dl. dn) = u . (dl. dn) ) )
A50: Selfwork (nt,aux) = <%(Divide ((dl. aux),(dl. (aux + 1))))%> by A49, Def10;
then A51: len (Selfwork (nt,aux)) = 1 by AFINSQ_1:34;
hence  i + 1 = len (SCM-Compile ((nt -tree (tl,tr)),aux)) by A11, A27, AFINSQ_1:17; ::_thesis: ( IC (Comput (F,s,i)) = n + i & IC u = n + (i + 1) & u . (dl. aux) = (nt -tree (tl,tr)) @ s & ( for dn being Element of NAT st dn < aux holds
s . (dl. dn) = u . (dl. dn) ) )
 len (SCM-Compile ((nt -tree (tl,tr)),aux)) = ((i1 + 1) + (i2 + 1)) + 1 by A11, A27, A51, AFINSQ_1:17;
then  i < len (SCM-Compile ((nt -tree (tl,tr)),aux)) by NAT_1:13;
then  i in dom (SCM-Compile ((nt -tree (tl,tr)),aux)) by NAT_1:44;
then A52: F . (n + i) = (SCM-Compile ((nt -tree (tl,tr)),aux)) . i by A5, FINSEQ_2:146
.= Divide ((dl. aux),(dl. (aux + 1))) by A11, A27, A50, AFINSQ_1:36 ;
thus  IC (Comput (F,s,i)) = n + i by A12, A18, A20, EXTPRO_1:4; ::_thesis: ( IC u = n + (i + 1) & u . (dl. aux) = (nt -tree (tl,tr)) @ s & ( for dn being Element of NAT st dn < aux holds
s . (dl. dn) = u . (dl. dn) ) )
A53: nt -Meaning_on ((tl @ s),(tr @ s)) = (tl @ s) div (tr @ s) by A49, Def8;
 aux <> aux + 1 ;
then A54: dl. aux <> dl. (aux + 1) by AMI_3:10;
hence  IC u = (n + i) + 1 by A20, A23, A52, SCM_1:8
.= n + (i + 1) ;
::_thesis: ( u . (dl. aux) = (nt -tree (tl,tr)) @ s & ( for dn being Element of NAT st dn < aux holds
s . (dl. dn) = u . (dl. dn) ) )
thus u . (dl. aux) = (u2 . (dl. aux)) div (u2 . (dl. (aux + 1))) by A20, A23, A52, A54, SCM_1:8
.= (u1 . (dl. aux)) div (tr @ u1) by A21, A22, A25
.= (nt -tree (tl,tr)) @ s by A15, A26, A24, A53, Th11 ; ::_thesis: for dn being Element of NAT st dn < aux holds
s . (dl. dn) = u . (dl. dn)
let dn be Element of NAT ; ::_thesis: ( dn < aux implies s . (dl. dn) = u . (dl. dn) )
assume A55: dn < aux ; ::_thesis: s . (dl. dn) = u . (dl. dn)
then A56: dn < aux + 1 by NAT_1:13;
then A57: dl. dn <> dl. (aux + 1) by AMI_3:10;
A58: u1 . (dl. dn) = u2 . (dl. dn) by A22, A56;
 dl. dn <> dl. aux by A55, AMI_3:10;
then  u . (dl. dn) = u2 . (dl. dn) by A20, A23, A52, A54, A57, SCM_1:8;
hence  s . (dl. dn) = u . (dl. dn) by A16, A55, A58; ::_thesis: verum
end;
supposeA59: nt = [0,4] ; ::_thesis: ex i being Element of NAT ex u being State of SCM st
( u = Comput (F,s,(i + 1)) & i + 1 = len (SCM-Compile ((nt -tree (tl,tr)),aux)) & IC (Comput (F,s,i)) = n + i & IC u = n + (i + 1) & u . (dl. aux) = (nt -tree (tl,tr)) @ s & ( for dn being Element of NAT st dn < aux holds
s . (dl. dn) = u . (dl. dn) ) )
then A60: nt -Meaning_on ((tl @ s),(tr @ s)) = (tl @ s) mod (tr @ s) by Def8;
set i = (i1 + 1) + (i2 + 1);
set u = Comput (F,s,(((i1 + 1) + (i2 + 1)) + 1));
take k = ((i1 + 1) + (i2 + 1)) + 1; ::_thesis: ex u being State of SCM st
( u = Comput (F,s,(k + 1)) & k + 1 = len (SCM-Compile ((nt -tree (tl,tr)),aux)) & IC (Comput (F,s,k)) = n + k & IC u = n + (k + 1) & u . (dl. aux) = (nt -tree (tl,tr)) @ s & ( for dn being Element of NAT st dn < aux holds
s . (dl. dn) = u . (dl. dn) ) )
take v = Comput (F,s,(k + 1)); ::_thesis: ( v = Comput (F,s,(k + 1)) & k + 1 = len (SCM-Compile ((nt -tree (tl,tr)),aux)) & IC (Comput (F,s,k)) = n + k & IC v = n + (k + 1) & v . (dl. aux) = (nt -tree (tl,tr)) @ s & ( for dn being Element of NAT st dn < aux holds
s . (dl. dn) = v . (dl. dn) ) )
thus  v = Comput (F,s,(k + 1)) ; ::_thesis: ( k + 1 = len (SCM-Compile ((nt -tree (tl,tr)),aux)) & IC (Comput (F,s,k)) = n + k & IC v = n + (k + 1) & v . (dl. aux) = (nt -tree (tl,tr)) @ s & ( for dn being Element of NAT st dn < aux holds
s . (dl. dn) = v . (dl. dn) ) )
A61: Selfwork (nt,aux) = <%(Divide ((dl. aux),(dl. (aux + 1)))),((dl. aux) := (dl. (aux + 1)))%> by A59, Def10;
then A62: len (Selfwork (nt,aux)) = 2 by AFINSQ_1:38;
then A63: 0 in dom (Selfwork (nt,aux)) by CARD_1:50, TARSKI:def_2;
A64: len (SCM-Compile ((nt -tree (tl,tr)),aux)) = ((i1 + 1) + (i2 + 1)) + (1 + 1) by A11, A27, A62, AFINSQ_1:17;
hence  k + 1 = len (SCM-Compile ((nt -tree (tl,tr)),aux)) ; ::_thesis: ( IC (Comput (F,s,k)) = n + k & IC v = n + (k + 1) & v . (dl. aux) = (nt -tree (tl,tr)) @ s & ( for dn being Element of NAT st dn < aux holds
s . (dl. dn) = v . (dl. dn) ) )
A65: 1 in dom (Selfwork (nt,aux)) by A62, CARD_1:50, TARSKI:def_2;
 k < len (SCM-Compile ((nt -tree (tl,tr)),aux)) by A64, XREAL_1:6;
then  k in dom (SCM-Compile ((nt -tree (tl,tr)),aux)) by NAT_1:44;
then A66: F . (n + k) = (SCM-Compile ((nt -tree (tl,tr)),aux)) . k by A5, FINSEQ_2:146
.= (Selfwork (nt,aux)) . 1 by A11, A27, A65, AFINSQ_1:def_3
.= (dl. aux) := (dl. (aux + 1)) by A61, AFINSQ_1:38 ;
 ((i1 + 1) + (i2 + 1)) + 0 = (i1 + 1) + (i2 + 1) ;
then  (i1 + 1) + (i2 + 1) < len (SCM-Compile ((nt -tree (tl,tr)),aux)) by A64, XREAL_1:6;
then  (i1 + 1) + (i2 + 1) in dom (SCM-Compile ((nt -tree (tl,tr)),aux)) by NAT_1:44;
then A67: F . (n + ((i1 + 1) + (i2 + 1))) = (SCM-Compile ((nt -tree (tl,tr)),aux)) . (((i1 + 1) + (i2 + 1)) + 0) by A5, FINSEQ_2:146
.= (Selfwork (nt,aux)) . 0 by A11, A27, A63, AFINSQ_1:def_3
.= Divide ((dl. aux),(dl. (aux + 1))) by A61, AFINSQ_1:38 ;
 aux <> aux + 1 ;
then A68: dl. aux <> dl. (aux + 1) by AMI_3:10;
hence A69: IC (Comput (F,s,k)) = (n + ((i1 + 1) + (i2 + 1))) + 1 by A20, A23, A67, SCM_1:8
.= n + k ;
::_thesis: ( IC v = n + (k + 1) & v . (dl. aux) = (nt -tree (tl,tr)) @ s & ( for dn being Element of NAT st dn < aux holds
s . (dl. dn) = v . (dl. dn) ) )
hence  IC v = (n + k) + 1 by A66, SCM_1:4
.= n + (k + 1) ;
::_thesis: ( v . (dl. aux) = (nt -tree (tl,tr)) @ s & ( for dn being Element of NAT st dn < aux holds
s . (dl. dn) = v . (dl. dn) ) )
thus v . (dl. aux) = (Comput (F,s,(((i1 + 1) + (i2 + 1)) + 1))) . (dl. (aux + 1)) by A66, A69, SCM_1:4
.= (u2 . (dl. aux)) mod (u2 . (dl. (aux + 1))) by A20, A23, A67, A68, SCM_1:8
.= (u1 . (dl. aux)) mod (tr @ u1) by A21, A22, A25
.= (nt -tree (tl,tr)) @ s by A15, A26, A24, A60, Th11 ; ::_thesis: for dn being Element of NAT st dn < aux holds
s . (dl. dn) = v . (dl. dn)
let dn be Element of NAT ; ::_thesis: ( dn < aux implies s . (dl. dn) = v . (dl. dn) )
assume A70: dn < aux ; ::_thesis: s . (dl. dn) = v . (dl. dn)
then A71: dl. dn <> dl. aux by AMI_3:10;
A72: dn < aux + 1 by A70, NAT_1:13;
then A73: u1 . (dl. dn) = u2 . (dl. dn) by A22;
 dl. dn <> dl. (aux + 1) by A72, AMI_3:10;
then  (Comput (F,s,(((i1 + 1) + (i2 + 1)) + 1))) . (dl. dn) = u2 . (dl. dn) by A20, A23, A67, A68, A71, SCM_1:8;
then  s . (dl. dn) = (Comput (F,s,(((i1 + 1) + (i2 + 1)) + 1))) . (dl. dn) by A16, A70, A73;
hence  s . (dl. dn) = v . (dl. dn) by A66, A69, A71, SCM_1:4; ::_thesis: verum
end;
end;
end;
A74: for t being Terminal of SCM-AE holds S2[ root-tree t]
proof
let t be Terminal of SCM-AE; ::_thesis: S2[ root-tree t]
let F be Instruction-Sequence of SCM; ::_thesis: for aux, n being Element of NAT st Shift ((SCM-Compile ((root-tree t),aux)),n) c= F holds
for s being b2 -started State of SCM st aux > max_Data-Loc_in (root-tree t) holds
ex i being Element of NAT ex u being State of SCM st
( u = Comput (F,s,(i + 1)) & i + 1 = len (SCM-Compile ((root-tree t),aux)) & IC (Comput (F,s,i)) = n + i & IC u = n + (i + 1) & u . (dl. aux) = (root-tree t) @ s & ( for dn being Element of NAT st dn < aux holds
s . (dl. dn) = u . (dl. dn) ) )
let aux, n be Element of NAT ; ::_thesis: ( Shift ((SCM-Compile ((root-tree t),aux)),n) c= F implies for s being n -started State of SCM st aux > max_Data-Loc_in (root-tree t) holds
ex i being Element of NAT ex u being State of SCM st
( u = Comput (F,s,(i + 1)) & i + 1 = len (SCM-Compile ((root-tree t),aux)) & IC (Comput (F,s,i)) = n + i & IC u = n + (i + 1) & u . (dl. aux) = (root-tree t) @ s & ( for dn being Element of NAT st dn < aux holds
s . (dl. dn) = u . (dl. dn) ) ) )
assume A75: Shift ((SCM-Compile ((root-tree t),aux)),n) c= F ; ::_thesis: for s being n -started State of SCM st aux > max_Data-Loc_in (root-tree t) holds
ex i being Element of NAT ex u being State of SCM st
( u = Comput (F,s,(i + 1)) & i + 1 = len (SCM-Compile ((root-tree t),aux)) & IC (Comput (F,s,i)) = n + i & IC u = n + (i + 1) & u . (dl. aux) = (root-tree t) @ s & ( for dn being Element of NAT st dn < aux holds
s . (dl. dn) = u . (dl. dn) ) )
let s be n -started State of SCM; ::_thesis: ( aux > max_Data-Loc_in (root-tree t) implies ex i being Element of NAT ex u being State of SCM st
( u = Comput (F,s,(i + 1)) & i + 1 = len (SCM-Compile ((root-tree t),aux)) & IC (Comput (F,s,i)) = n + i & IC u = n + (i + 1) & u . (dl. aux) = (root-tree t) @ s & ( for dn being Element of NAT st dn < aux holds
s . (dl. dn) = u . (dl. dn) ) ) )
assume  aux > max_Data-Loc_in (root-tree t) ; ::_thesis: ex i being Element of NAT ex u being State of SCM st
( u = Comput (F,s,(i + 1)) & i + 1 = len (SCM-Compile ((root-tree t),aux)) & IC (Comput (F,s,i)) = n + i & IC u = n + (i + 1) & u . (dl. aux) = (root-tree t) @ s & ( for dn being Element of NAT st dn < aux holds
s . (dl. dn) = u . (dl. dn) ) )
take i = 0 ; ::_thesis: ex u being State of SCM st
( u = Comput (F,s,(i + 1)) & i + 1 = len (SCM-Compile ((root-tree t),aux)) & IC (Comput (F,s,i)) = n + i & IC u = n + (i + 1) & u . (dl. aux) = (root-tree t) @ s & ( for dn being Element of NAT st dn < aux holds
s . (dl. dn) = u . (dl. dn) ) )
take u = Comput (F,s,(0 + 1)); ::_thesis: ( u = Comput (F,s,(i + 1)) & i + 1 = len (SCM-Compile ((root-tree t),aux)) & IC (Comput (F,s,i)) = n + i & IC u = n + (i + 1) & u . (dl. aux) = (root-tree t) @ s & ( for dn being Element of NAT st dn < aux holds
s . (dl. dn) = u . (dl. dn) ) )
thus  u = Comput (F,s,(i + 1)) ; ::_thesis: ( i + 1 = len (SCM-Compile ((root-tree t),aux)) & IC (Comput (F,s,i)) = n + i & IC u = n + (i + 1) & u . (dl. aux) = (root-tree t) @ s & ( for dn being Element of NAT st dn < aux holds
s . (dl. dn) = u . (dl. dn) ) )
A76: <%((dl. aux) := (@ t))%> . 0 = (dl. aux) := (@ t) by AFINSQ_1:34;
A77: SCM-Compile ((root-tree t),aux) = <%((dl. aux) := (@ t))%> by Th7;
hence  i + 1 = len (SCM-Compile ((root-tree t),aux)) by AFINSQ_1:34; ::_thesis: ( IC (Comput (F,s,i)) = n + i & IC u = n + (i + 1) & u . (dl. aux) = (root-tree t) @ s & ( for dn being Element of NAT st dn < aux holds
s . (dl. dn) = u . (dl. dn) ) )
A78: s = Comput (F,s,0) by EXTPRO_1:2;
hence  IC (Comput (F,s,i)) = n + i by MEMSTR_0:def_12; ::_thesis: ( IC u = n + (i + 1) & u . (dl. aux) = (root-tree t) @ s & ( for dn being Element of NAT st dn < aux holds
s . (dl. dn) = u . (dl. dn) ) )
 ( len <%((dl. aux) := (@ t))%> = 1 & n + 0 = n ) by AFINSQ_1:34;
then  i in dom (SCM-Compile ((root-tree t),aux)) by A77, NAT_1:44;
then A79: ( IC s = n & F . (n + 0) = (dl. aux) := (@ t) ) by A77, A76, A75, FINSEQ_2:146, MEMSTR_0:def_12;
hence  IC u = n + (i + 1) by A78, SCM_1:4; ::_thesis: ( u . (dl. aux) = (root-tree t) @ s & ( for dn being Element of NAT st dn < aux holds
s . (dl. dn) = u . (dl. dn) ) )
thus u . (dl. aux) = s . t by A78, A79, SCM_1:4
.= (root-tree t) @ s by Th4 ; ::_thesis: for dn being Element of NAT st dn < aux holds
s . (dl. dn) = u . (dl. dn)
let dn be Element of NAT ; ::_thesis: ( dn < aux implies s . (dl. dn) = u . (dl. dn) )
assume  dn < aux ; ::_thesis: s . (dl. dn) = u . (dl. dn)
then  dl. dn <> dl. aux by AMI_3:10;
hence  s . (dl. dn) = u . (dl. dn) by A78, A79, SCM_1:4; ::_thesis: verum
end;
 for term being bin-term holds S2[term] from BINTREE1:sch_2(A74, A1);
hence  for F being Instruction-Sequence of SCM
for term being bin-term
for aux, n being Element of NAT st Shift ((SCM-Compile (term,aux)),n) c= F holds
for s being b4 -started State of SCM st aux > max_Data-Loc_in term holds
ex i being Element of NAT ex u being State of SCM st
( u = Comput (F,s,(i + 1)) & i + 1 = len (SCM-Compile (term,aux)) & IC (Comput (F,s,i)) = n + i & IC u = n + (i + 1) & u . (dl. aux) = term @ s & ( for dn being Element of NAT st dn < aux holds
s . (dl. dn) = u . (dl. dn) ) ) ; ::_thesis: verum
end;

theorem :: SCM_COMP:13
for F being Instruction-Sequence of SCM
for term being bin-term
for aux, n being Element of NAT st Shift (((SCM-Compile (term,aux)) ^ <%(halt SCM)%>),n) c= F holds
for s being b4 -started State of SCM st aux > max_Data-Loc_in term holds
( F halts_on s & (Result (F,s)) . (dl. aux) = term @ s & LifeSpan (F,s) = len (SCM-Compile (term,aux)) )
proof
let F be Instruction-Sequence of SCM; ::_thesis: for term being bin-term
for aux, n being Element of NAT st Shift (((SCM-Compile (term,aux)) ^ <%(halt SCM)%>),n) c= F holds
for s being b3 -started State of SCM st aux > max_Data-Loc_in term holds
( F halts_on s & (Result (F,s)) . (dl. aux) = term @ s & LifeSpan (F,s) = len (SCM-Compile (term,aux)) )
let term be bin-term; ::_thesis: for aux, n being Element of NAT st Shift (((SCM-Compile (term,aux)) ^ <%(halt SCM)%>),n) c= F holds
for s being b2 -started State of SCM st aux > max_Data-Loc_in term holds
( F halts_on s & (Result (F,s)) . (dl. aux) = term @ s & LifeSpan (F,s) = len (SCM-Compile (term,aux)) )
let aux, n be Element of NAT ; ::_thesis: ( Shift (((SCM-Compile (term,aux)) ^ <%(halt SCM)%>),n) c= F implies for s being n -started State of SCM st aux > max_Data-Loc_in term holds
( F halts_on s & (Result (F,s)) . (dl. aux) = term @ s & LifeSpan (F,s) = len (SCM-Compile (term,aux)) ) )
assume A1: Shift (((SCM-Compile (term,aux)) ^ <%(halt SCM)%>),n) c= F ; ::_thesis: for s being n -started State of SCM st aux > max_Data-Loc_in term holds
( F halts_on s & (Result (F,s)) . (dl. aux) = term @ s & LifeSpan (F,s) = len (SCM-Compile (term,aux)) )
let s be n -started State of SCM; ::_thesis: ( aux > max_Data-Loc_in term implies ( F halts_on s & (Result (F,s)) . (dl. aux) = term @ s & LifeSpan (F,s) = len (SCM-Compile (term,aux)) ) )
assume A2: aux > max_Data-Loc_in term ; ::_thesis: ( F halts_on s & (Result (F,s)) . (dl. aux) = term @ s & LifeSpan (F,s) = len (SCM-Compile (term,aux)) )
 Shift ((SCM-Compile (term,aux)),n) c= F by A1, AFINSQ_1:82;
then consider i being Element of NAT , u being State of SCM such that
A3: u = Comput (F,s,(i + 1)) and
A4: i + 1 = len (SCM-Compile (term,aux)) and
A5: IC (Comput (F,s,i)) = n + i and
A6: IC u = n + (i + 1) and
A7: u . (dl. aux) = term @ s and
 for dn being Element of NAT st dn < aux holds
s . (dl. dn) = u . (dl. dn) by A2, Th12;
 len <%(halt SCM)%> = 1 by AFINSQ_1:34;
then  len ((SCM-Compile (term,aux)) ^ <%(halt SCM)%>) = (i + 1) + 1 by A4, AFINSQ_1:17;
then  i + 1 < len ((SCM-Compile (term,aux)) ^ <%(halt SCM)%>) by NAT_1:13;
then  i + 1 in dom ((SCM-Compile (term,aux)) ^ <%(halt SCM)%>) by NAT_1:44;
then A8: F . (n + (i + 1)) = ((SCM-Compile (term,aux)) ^ <%(halt SCM)%>) . (i + 1) by A1, FINSEQ_2:146
.= halt SCM by A4, AFINSQ_1:36 ;
hence  F halts_on s by A3, A6, EXTPRO_1:30; ::_thesis: ( (Result (F,s)) . (dl. aux) = term @ s & LifeSpan (F,s) = len (SCM-Compile (term,aux)) )
thus  (Result (F,s)) . (dl. aux) = term @ s by A3, A6, A7, A8, EXTPRO_1:31; ::_thesis: LifeSpan (F,s) = len (SCM-Compile (term,aux))
 n + i <> n + (i + 1) ;
hence  LifeSpan (F,s) = len (SCM-Compile (term,aux)) by A3, A4, A5, A6, A8, EXTPRO_1:33; ::_thesis: verum
end;