Clear[bbi,bbo,bbs,bbso]
bbi[n_]:=If[n≤10,n,F[bbi[Quotient[n,4]],Mod[n,4]]]
bbo[n_]:=pl[tm[4,bbi[Quotient[n,4]]],Mod[n,4]]
bbso[n_]:=S[bbs[Quotient[n,10]],Mod[n,10]]
bbs[n_Integer]:=If[n≤10,n,bbso[n]]
bbs[n_]:=Message[General::args,"bbs["<>ToString[n]<>"]"]

Clear[eval]
eval[F[a_,b_]]:=4eval[a]+eval[b]
eval[S[a_,b_]]:=10eval[a]+eval[b]
eval[pl[a_,b_]]:=eval[a]+eval[b]
eval[pw[a_,b_]]:=eval[a]^eval[b]
eval[tm[a_,b_]]:=eval[a]eval[b]
eval[n_Integer]:=n
eval[N]:=4001

print[eq[a_,b_]]:=" |- "<>print[a]<>" = "<>print[b]
print[lt[a_,b_]]:=" |- "<>print[a]<>" < "<>print[b]
print[tm[a_,b_]]:="( "<>print[a]<>" x. "<>print[b]<>" )"
print[pw[a_,b_]]:="( "<>print[a]<>" ^ "<>print[b]<>" )"
print[pl[a_,b_]]:="( "<>print[a]<>" + "<>print[b]<>" )"
print[F[a_,b_]]:="( "<>print[a]<>" F "<>print[b]<>" )"
print[S[a_,b_]]:="; "<>print[a]<>" "<>print[b]
print[elN[a_]]:=" |- "<>print[a]<>" e. NN"
print[elN0[a_]]:=" |- "<>print[a]<>" e. NN0"
print[elC[a_]]:=" |- "<>print[a]<>" e. CC"
print[n_Integer]:=ToString[n]
print[N]:="N"

decode[s_]:=If[Length[#]==1,#[[1]],Null]&[StringSplit[s," "]/.Table[ToString[n]->n,{n,0,10}]/."N"->N//.{{a___,"(",x_,"F",y_,")",b___}->{a,F[x,y],b},
{a___,"(",x_,"+",y_,")",b___}->{a,pl[x,y],b},
{a___,"(",x_,"x.",y_,")",b___}->{a,tm[x,y],b},
{a___,"(",x_,"^",y_,")",b___}->{a,pw[x,y],b},
{a___,";",x_,y_,b___}/;!Head[x]===String->{a,S[x,y],b},
{a___,"|-",x_,"e.","NN",b___}->{a,elN[x],b},
{a___,"|-",x_,"e.","NN0",b___}->{a,elN0[x],b},
{a___,"|-",x_,"e.","CC",b___}->{a,elC[x],b},
{a___,"|-",x_,"=",y_,b___}->{a,eq[x,y],b},
{a___,"|-",x_,"<",y_,b___}->{a,lt[x,y],b}}]

Clear[prove,proveeq,proveeq2,provelt,basiceq,basiceq2,num0]
prove[elN[n_Integer]]/;n>0:={{},elN[n],ToString[n]<>"nn"}
prove[elN[x:S[a_,b_]]]:=If[b===0,{{prove@elN[a]},elN[x],"decnncl2"},{{prove@elN0[a],prove@elN[b]},elN[x],"decnncl"}]
prove[elN0[n_Integer]]:=With[{s=ToString[n]},{{},elN0[n],s<>"nn0"}]
prove[x:elN0[S[a_,b_]]]:={{prove@elN0[a],prove@elN0[b]},x,"deccl"}
prove[x:elN0[tm[a_,b_]]]:={{prove@elN0[a],prove@elN0[b]},x,"nn0mulcli"}
prove[x:elN0[pl[a_,b_]]]:={{prove@elN0[a],prove@elN0[b]},x,"nn0addcli"}
prove[x:elN0[pw[a_,b_]]]:={{prove@elN0[a],prove@elN0[b]},x,"nn0expcli"}
prove[elC[n_Integer]]:=With[{s=ToString[n]},If[n<4,{{},elC[n],If[n==1,"ax-1cn",s<>"cn"]},{{prove[elN[n]]},elC[n],"nncni"}]]
prove[x:elC[s_S]]:={{prove@elN0[s]},x,"nn0cni"}
prove[x:elC[tm[a_,b_]]]:={{prove@elC[a],prove@elC[b]},x,"mulcli"}
prove[x:elC[pl[a_,b_]]]:={{prove@elC[a],prove@elC[b]},x,"addcli"}
prove[x_]:={{},x,"?"}
prove[lt[x_,y_]]/;eval[x]<eval[y]:=If[x===bbs@eval[x],If[y===bbs@eval[y],provelt[x,y],{{prove@lt[x,bbs@eval[y]],proveeq2[y]},lt[x,y],"breqtrri"}],{{proveeq2[x],prove@lt[bbs@eval[x],y]},lt[x,y],"eqbrtri"}]
prove[eq[x_,y_]]/;eval[x]==eval[y]:=If[y===bbs@eval[y],proveeq2[x],{{proveeq2[x],proveeq2[y]},eq[x,y],"eqtr4i"}]
provelt[x_Integer,y_Integer]:={{},lt[x,y],If[x==0,ToString[y]<>"pos",ToString[x]<>"lt"<>ToString[y]]}
provelt[x_Integer,y:S[a_,b_]]:=
If[x<10,{{prove@elN[a],prove@elN0[b],prove@elN0[x],provelt[x,10]},lt[x,y],"declti"},{{num0[x],provelt[bbso[x],y]},lt[x,y],"eqbrtri"}]
provelt[x:S[a_,c_],y:S[b_,d_]]:=If[a===b,{{prove@elN0[a],prove@elN0[c],prove@elN[d],provelt[c,d]},lt[x,y],"declt"},{{prove@elN0[a],prove@elN0[b],prove@elN0[c],prove@elN0[d],provelt[c,10],provelt[a,b]},lt[x,y],"decltc"}]
proveeq2[x_]:=proveeq[x,bbs@eval[x]]
num0[x_]:=If[x===bbs@eval[x],If[eval[x]<10,{{prove@elN0[x]},eq[x,S[0,x]],"dec0h"},proveeq[x,bbso@eval[x]]],If[eval[x]≤10,{{proveeq2[x],num0[eval[x]]},eq[x,bbso@eval[x]],"eqtri"},proveeq2[x]]]
basiceq[x:tm[a_,0]]:={{prove@elC[a]},eq[x,0],"mul01i"}
basiceq[x:tm[0,a_]]:={{prove@elC[a]},eq[x,0],"mul02i"}
basiceq[x:pw[a_,0]]:={{prove@elN0[a]},eq[x,1],"numexp0"}
basiceq[x:pw[a_,1]]:={{prove@elN0[a]},eq[x,a],"numexp1"}
basiceq[x:pl[a_,b_]]:=If[a===eval[a]&&b===eval[b],basiceq2[x],{{If[a===eval[a],{{basiceq[b]},eq[pl[a,b],pl[a,eval[b]]],"oveq2i"},If[b===eval[b],{{basiceq[a]},eq[pl[a,b],pl[eval[a],b]],"oveq1i"},
{{basiceq[a],basiceq[b]},eq[pl[a,b],pl[eval[a],eval[b]]],"oveq12i"}]],basiceq[pl[eval[a],eval[b]]]},eq[x,bbs@eval[x]],"eqtri"}]
basiceq[x:tm[a_,b_]]:=If[a===eval[a]&&b===eval[b],basiceq2[x],{{If[a===eval[a],{{basiceq[b]},eq[tm[a,b],tm[a,eval[b]]],"oveq2i"},If[b===eval[b],{{basiceq[a]},eq[tm[a,b],tm[eval[a],b]],"oveq1i"},
{{basiceq[a],basiceq[b]},eq[tm[a,b],tm[eval[a],eval[b]]],"oveq12i"}]],basiceq[tm[eval[a],eval[b]]]},eq[x,bbs@eval[x]],"eqtri"}]
basiceq2[x:pl[a_,0]]:={{prove@elC[a]},eq[x,a],"addid1i"}
basiceq2[x:pl[0,a_]]:={{prove@elC[a]},eq[x,a],"addid2i"}
basiceq2[x:tm[a_,1]]:={{prove@elC[a]},eq[x,a],"mulid1i"}
basiceq2[x:tm[1,a_]]:={{prove@elC[a]},eq[x,a],"mulid2i"}
basiceq2[x:pl[a_,b_]]/;a≥b≥1:={{},eq[x,bbs@eval[x]],ToString[a]<>"p"<>ToString[b]<>"e"<>ToString[a+b]}
basiceq2[x:pl[a_,b_]]:={{prove@elC[b],prove@elC[a],basiceq[pl[b,a]]},eq[x,bbs@eval[x]],"addcomli"}
basiceq2[x:tm[a_,b_]]/;a≥b>1:={{},eq[x,bbs@eval[x]],ToString[a]<>"t"<>ToString[b]<>"e"<>ToString[a b]}
basiceq2[x:tm[a_,b_]]:={{prove@elC[b],prove@elC[a],basiceq[tm[b,a]]},eq[x,bbs@eval[x]],"mulcomli"}
basiceq[x:S[a_,b_]]:=If[x===bbs@eval[x],{{},eq[x,x],"eqid"},{{num0@eval[x]},eq[x,bbs@eval[x]],"eqcomi"}]
basiceq[x_]:={{},eq[x,eval[x]],"?"}
proveeq[x_,x_]:={{},eq[x,x],"eqid"}
proveeq[10,S[1,0]]:={{},eq[10,S[1,0]],"dec10"}
proveeq[x_,y_Integer]:=basiceq[x]
proveeq[x:pl[a_,1],y_Integer]:={{basiceq[pl[eval[a],1]],{{proveeq2[a]},eq[pl[a,1],pl[bbs@eval[a],1]],"oveq1i"}},eq[x,y],"eqtri"}
proveeq[x:pl[a_,0],y_]:=If[a===y,{{prove@elC[a]},eq[x,y],"addid1i"},{{{{proveeq2[a]},eq[x,pl[y,0]],"oveq1i"},proveeq2@pl[y,0]},eq[x,y],"eqtri"}]
proveeq[x:pl[0,a_],y_]:=If[a===y,{{prove@elC[a]},eq[x,y],"addid2i"},{{{{proveeq2[a]},eq[x,pl[0,y]],"oveq2i"},proveeq2@pl[0,y]},eq[x,y],"eqtri"}]
proveeq[x:tm[a_,1],y_]:=If[a===y,{{prove@elC[a]},eq[x,y],"mulid1i"},{{{{proveeq2[a]},eq[x,tm[y,1]],"oveq1i"},proveeq2@tm[y,1]},eq[x,y],"eqtri"}]
proveeq[x:tm[1,a_],y_]:=If[a===y,{{prove@elC[a]},eq[x,y],"mulid2i"},{{{{proveeq2[a]},eq[x,tm[1,y]],"oveq2i"},proveeq2@tm[1,y]},eq[x,y],"eqtri"}]
proveeq[x:pl[a_,b_],y_]/;eval[a]<10&&eval[b]<10:=basiceq[x]
proveeq[x:tm[a_,b_],y_]/;eval[a]<10&&eval[b]<10:=basiceq[x]
proveeq[x:pl[z:tm[m_,p_],n_],y:S[e_,f_]]/;eval[p]≥ 10||eval[m]≥10:=If[eval[p]<10,If[eval[m]<10,{{{{basiceq[z]},eq[x,pl[bbs@eval[z],n]],"oveq1i"},proveeq2@pl[bbs@eval[z],n]},eq[x,y],"eqtri"},Module[{ab=bbso@eval[m],cd=bbso@eval[n],gf},gf=bbso@eval[ab[[2]]p+cd[[2]]];{{prove@elN0[ab[[1]]],prove@elN0[ab[[2]]],prove@elN0[cd[[1]]],prove@elN0[cd[[2]]],num0[m],num0[n],prove@elN0[p],prove@elN0[gf[[2]]],prove@elN0[gf[[1]]],proveeq2@pl[tm[ab[[1]],p],pl[cd[[1]],gf[[1]]]],
num0@pl[tm[ab[[2]],p],cd[[2]]]},eq[x,y],"decmac"}]],Module[{ab=bbso@eval[p],cd=bbso@eval[n],gf},gf=bbso[ab[[2]]eval@m+cd[[2]]];{{prove@elN0[ab[[1]]],prove@elN0[ab[[2]]],prove@elN0[cd[[1]]],prove@elN0[cd[[2]]],num0[p],num0[n],prove@elN0[m],prove@elN0[gf[[2]]],prove@elN0[gf[[1]]],proveeq2@pl[tm[m,ab[[1]]],pl[cd[[1]],gf[[1]]]],
num0@pl[tm[m,ab[[2]]],cd[[2]]]},eq[x,y],"decma2c"}]]
proveeq[x:tm[n_,p_],y:S[c_,d_]]:=If[eval[p]<10,Module[{ab=bbso@eval[n],ed},ed=bbso@eval[ab[[2]]p];{{prove@elN0[p],prove@elN0[ab[[1]]],prove@elN0[ab[[2]]],num0[n],prove@elN0[d],prove@elN0[ed[[1]]],proveeq2@pl[tm[ab[[1]],p],ed[[1]]],
num0@tm[ab[[2]],p]},eq[x,y],"decmul1c"}],Module[{ab=bbso@eval[p],ed},ed=bbso[eval@ab[[2]]eval@n];{{prove@elN0[n],prove@elN0[ab[[1]]],prove@elN0[ab[[2]]],num0[p],prove@elN0[d],prove@elN0[ed[[1]]],proveeq2@pl[tm[n,ab[[1]]],ed[[1]]],
num0@tm[n,ab[[2]]]},eq[x,y],"decmul2c"}]]
proveeq[x:pl[m_,n_],y:S[e_,f_]]:=Module[{ab=bbso@eval[m],cd=bbso@eval[n]},If[cd[[1]]===0,If[n===cd[[2]],{Join[{prove@elN0[ab[[1]]],prove@elN0[ab[[2]]],prove@elN0[n],num0[m]},If[ab[[2]]+cd[[2]]<10,{},{proveeq2@pl[ab[[1]],1]}],If[ab[[2]]+cd[[2]]≤10,{},{prove@elN0[f]}],{proveeq2@pl[ab[[2]],n]}],eq[x,y],"decadd"<>If[ab[[2]]+cd[[2]]<10,"i",If[ab[[2]]+cd[[2]]==10,"ci2","ci"]]},{{{{proveeq2[n]},eq[x,pl[m,eval[n]]],"oveq2i"},proveeq2@pl[m,eval[n]]},eq[x,y],"eqtri"}],{Join[{prove@elN0[ab[[1]]],prove@elN0[ab[[2]]],prove@elN0[cd[[1]]],prove@elN0[cd[[2]]],num0[m],num0[n],proveeq2@If[ab[[2]]+cd[[2]]<10,pl[ab[[1]],cd[[1]]],pl[pl[ab[[1]],cd[[1]]],1]]},If[ab[[2]]+cd[[2]]≤10,{},{prove@elN0[f]}],{proveeq2@pl[ab[[2]],cd[[2]]]}],eq[x,y],"decadd"<>If[ab[[2]]+cd[[2]]<10,"",If[ab[[2]]+cd[[2]]==10,"c2","c"]]}]]
proveeq[x:pl[c_,1],y:S[a_,b_]]:=If[b==0,{{prove@elN0[bbs[eval@a-1]],proveeq2[pl[bbs[eval@a-1],1]],proveeq2[c]},eq[x,y],"decsucc"},{{prove@elN0[a],prove@elN0[b-1],proveeq2@pl[b-1,1],prove@eq[c,S[a,b-1]]},eq[x,y],"decsuc"}]
proveeq[x:pw[a_,b_],y_]/;b>0:=If[b===1,{{prove@elN0[a]},eq[x,y],"numexp1"},{{prove@elN0[a],prove@elN0[bbs@eval[b-1]],proveeq2@pl[bbs[eval@b-1],1],proveeq2@tm[pw[a,bbs[eval@b-1]],a]},eq[x,y],"numexpp1"}]
proveeq[x_,y_]:={{},eq[x,y],"?"}

arithmeticProve[input_]:=Module[{spl=StringSplit[backup=Import[input],RegularExpression["\n(?=[^ ])"]],
  step,pf,ref,step2={},m,bin,pfx="a",n=1,repl,scan},
step=With[{q=StringSplit[#,WhitespaceCharacter..,2]},
  {Join[{StringReplace[#[[1]],"!"->""],If[#[[3]]==="",{"?"},#[[2]]]},#[[3;;]]]&@
  MapAt[StringSplit[#,","]&,StringSplit[q[[1]],":",All],2],#,decode@q[[2]]}]&/@
  Select[spl,StringMatchQ[repl[#]={#};#,RegularExpression["(?s)(\\!?)[a-z0-9].*"]]&];
scan[t_,v_:Null]:=With[{r=ref[t[[2]]]},
  If[Head[r]=!=ref,
      m={n,Null,t};
      If[v=!=Null,AppendTo[bin,v<>"::#"<>r[[1,1]]<>print@t[[2]]]];
      r[[1,1]],
    With[{hyps=scan/@t[[1]],label=If[v===Null,pfx<>ToString[n++],v]},
      ref[t[[2]]]={{label,hyps,t[[3]]},
        AppendTo[bin,#]&@StringReplace[StringJoin@
          {label,":",Riffle[hyps,","],":",t[[3]],print@t[[2]]},{"::?"->":?:"}],
        If[Head[t[[2]]]===eq&&eval[t[[2,1]]]≠eval[t[[2,2]]],Print[Style[t,Red]]];
        m={n,t}; t[[2]]};
      label]]];
Scan[(m=#;
  If[#[[3]]=!=Null,
    If[#[[1,2]]==={"?"},
      bin={};
      scan[prove@#[[3]],#[[1,1]]];
      repl[#[[2]]]=bin];
      ref[#[[3]]]=#])&,step];
StringJoin[{#,"\n"}&/@repl[#]&/@spl]]

(* prove arithmetic assertions *)
inputFile="C:\\metamath\\mmj2\\mmj2jar\\myproofs\\log2ub-orig.mmp";
outputFile="C:\\metamath\\mmj2\\mmj2jar\\myproofs\\log2ub.mmp";
Timing[arithmeticProve[inputFile]];
{%[[1]],If[%[[2]]=!=$Aborted,Export[outputFile,%[[2]],"Text"]]}