How to use Redo example 1

Tetsuo Ida
Deployed at
https://www.wolframcloud.com/obj/ida.tetsuo.ge/Published/how-to-use-redo.nb

Load Eos

In[]:=
<<"EosHeader.m"
g3 Version 1.2.9
Eos3.31 (November 5,2020) running under Mathematica 12.1.1 for Mac OS X x86 (64-bit) (June 22, 2020)

Redo test

Suppose we have constructed an origami.
C1
...
Ck
Then, we need to change Ck to Ck’.
In general, we have to execute
C1
...
Ck’.
To avoid selecting C1 ... Ck’ and execute them.
We write Redo[] immediately after Ck. and execute Redo[]. Redo[] performs exactly the same commands C1 ... Ck-1 , in this order. Then, we execute Ck’. By Redo[], we do not have to select C1 ... Ck-1 again.
​
In[]:=
EosSession["Redo test"];
In[]:=
MarkOn[];

Construction

In[]:=
NewOrigami[10];
In[]:=
HO["A","B"]!
Redo test: Step 3
Out[]=
In[]:=
HO["C","B"]!
Redo test: Step 5
Out[]=
In[]:=
HO["A","I"]
Redo test: Step 6
Out[]=
In[]:=
Redo[];HO["B","I"]
Redo test: Step 6
Out[]=

Proof

In[]:=
Goal["A"=!="I"];
In[]:=
Prove["Redo example 1"]
ProofbyGB
::gbstart
:Proof by Groebner basis method started at November 21, 2020 at 11:22:07 AM JST.
​
ProofbyGB
::gbsuccess
:Proof by Groebner basis method is successful.CPU time used for Groebner basis computation is 0.01033 seconds.
​
Proof is successful.
Redo test: Step 6
Out[]=
{Success,0.01033,
Redo example 1.nb
}
In[]:=
EndSession[];

Reconstruction

After we finish the construction, remove the “cmd - redo” part in “cmd - redo - modifyCmd” part
In[]:=
EosSession["Redo test"];
In[]:=
MarkOn[];

Construction

In[]:=
NewOrigami[10];
In[]:=
HO["A","B"]!
Redo test: Step 3
Out[]=
In[]:=
HO["C","B"]!
Redo test: Step 5
Out[]=
In[]:=
HO["B","I"]
Redo test: Step 6
Out[]=
In[]:=
(***endofconstruction***)

Proof

In[]:=
Goal["A"=!="B"];
In[]:=
Prove["Redo-test"]
ProofbyGB
::gbstart
:Proof by Groebner basis method started at October 22, 2020 at 1:39:22 PM JST.
​
ProofbyGB
::gbsuccess
:Proof by Groebner basis method is successful.CPU time used for Groebner basis computation is 0.000582 seconds.
​
Proof is successful.
Redo test: Step 6
Out[]=
{Success,0.000582,
Redo-test.nb
}
In[]:=
EndSession[];