removing unneeded lemmas from vsync_paxos_ms

test/vsync_paxos.ivy

@@ -163,12 +163,16 @@ action start(e:epoch, e_prev: epoch, n:node, s:stake, nset:nodeset.set, c:config
 #        (s < K2) -> (epoch_ended(e_prev) -> c = config_decided(e_prev));
     assume epoch_ended(e_prev) -> c = config_decided(e_prev);
 
+# true but not needed...
+
 #    assume epoch_ended(e_prev) -> s = epoch_stake(e_prev) & c = config_decided(e_prev);
-    assert E1 = e_prev & K = s & C = c & N = nodeset.common(nset,nset) -> accept_msg(e_prev,s,c);
-    assume accept_msg(e_prev,s,c);
+#    assert E1 = e_prev & K = s & C = c & N = nodeset.common(nset,nset) -> accept_msg(e_prev,s,c);
+#    assume accept_msg(e_prev,s,c);
     
+# true but not needed...
+
 #    assert forall C,K,E1,N,E2. C = c & K = s & E1 = e_prev & N = nodeset.common(nset,nset) & E2 < e_prev -> epoch_ended(E2);
-    assume forall E2. (E2 < e_prev -> epoch_ended(E2));
+#    assume forall E2. (E2 < e_prev -> epoch_ended(E2));
 
 #    assert forall C,K,E1,N,E2,N1,I,V1,S2,K2,C2. C = c & K = s & E1 = e_prev & S1 = accept_maj(E1,s) & N = nodeset.common(S1,S1) & S2 = epoch_maj(E2) & K2 = epoch_stake(E2) & C2 = config_decided(E2)
 #         & E2 < e_prev & nodeset.member(N1,epoch_maj(E2)) & vote(E2,N1,I,V1) -> val_at(c,I,V1);