Update README.md

README.md

@@ -25,6 +25,79 @@ pvs_sft5
 └── training_args.bin
 ```
 
+## Data examples (newlines should match):
+
+```
+Current Sequent:
+[1]   norm((# x := -1, y := 0 #)) = 1
+
+Prev Command 1: (EXPAND "point_on_polygon_perimeter?")
+Prev Command 2: (INST + "s")
+Prev Command 3: (HIDE-ALL-BUT 1)
+Next Command:
+```
+
+```
+Current Sequent:
+{1}   expt(c, (3 + 4 * n)) = expt(c, (1 + 4 * n)) * expt(c, 2)
+
+Prev Command 1: (PROPAX)
+Prev Command 2: (HIDE 2)
+Prev Command 3: (EXPAND "^")
+Next Command:
+```
+
+```
+Current Sequent:
+[-1]  derivable?(sin, x!1) AND derivable?(sin, x!1) IMPLIES deriv(sin * sin, x!1) = 2 * (deriv(sin, x!1) * sin(x!1))
+[-2]  derivable?[real](sin * sin, x!1)
+[-3]  derivable?[real](cos * cos, x!1)
+[-4]  FORALL (x: real): derivable?[real](sin, x)
+{-5}  FORALL (x: real): derivable?[real](cos, x)
+[1]   deriv(cos * cos, x!1) + deriv(sin * sin, x!1) = const_fun(0)(x!1)
+
+Prev Command 1: (ASSERT)
+Prev Command 2: (EXPAND "derivable?" -4)
+Prev Command 3: (EXPAND "derivable?" -5)
+Next Command:
+```
+
+```
+Current Sequent:
+[1]   FORALL (x: real): LET S = LAMBDA (n: nat): powerseq(cos_coef, x)(2 * n) IN conv_series?(S) AND cos(x) = inf_sum(S)
+
+Prev Command 1: (ASSERT)
+Prev Command 2: (ASSERT)
+Prev Command 3: (HIDE 2)
+Next Command:
+```
+
+
+Current Sequent:
+{-1}  FORALL (a: {x: real | 0 < x AND x <= pi / 2}): sin(a) > 0
+[-2]  a <= pi / 2
+[1]   sin(a) > 0
+
+```
+Prev Command 1: (SKEEP)
+Prev Command 2: (CASE "a <= pi/2")
+Prev Command 3: (LEMMA "sin_pos_0tohalfpi")
+Next Command:
+```
+
+```
+Current Sequent:
+{-1}  FORALL (x_1: real): NOT (key_arb_intersections(p, v, G)(x_1) OR parallel_intersections(p, v, G)(x_1))
+{1}   FORALL (x: real): NOT key_arb_intersections(p, v, G)(x)
+
+Prev Command 1: (EXPAND "empty?")
+Prev Command 2: (EXPAND "member")
+Prev Command 3: (GROUND)
+Next Command:
+```
+
+
+
 ## Start the web server with the model running
 
 ```python -m uvicorn sft_fastapi:app --host 0.0.0.0 --port 8000```