mizar-rs and Larus mizar export

Good news,

Larus can export a file in the Mizar format: (see https://github.com/janicicpredrag/Larus) mizar-rs can correctly check this mizar file.

Test (Larus export: ./proofs/PROOF030_lemma_ray4_3pQF_BV.miz" from https://github.com/janicicpredrag/Larus/blob/master/benchmarks/tptp-problems/euclid-native-eq/030_lemma_ray4_3.p) rename tlarus.miz:

$ mv miz/mizshare/mml/mml.lar miz/mizshare/mml/mml.lar.bak
$ echo "tlarus" >> miz/mizshare/mml/mml.lar
$ cat >> tlarus.miz << EOF
environ

begin

scheme SMyT { eqnative[object,object], betS[object,object,object], 
cong[object,object,object,object], out[object,object,object], 
betScong0[object,object,object,object,object], 
betSbetS3[object,object,object,object] }:
  for A, B, E being object  holds betS[A,B,E] & A <> B implies out[A,B,E]
provided
lemmaextension: for A, B, P, Q being object  holds A <> B & P <> Q implies  ex 
X being object st betS[A,B,X] & cong[B,X,P,Q] and

axiombetweennesssymmetry: for A, B, C being object  holds betS[A,B,C] implies 
betS[C,B,A] and

axiominnertransitivity: for A, B, C, D being object  holds betS[A,B,D] & 
betS[B,C,D] implies betS[A,B,C] and

defray: for A, B, C being object  holds out[A,B,C] implies  ex X being object 
st betS[X,A,C] & betS[X,A,B] and

defray2: for A, B, C, X being object  holds betS[X,A,C] & betS[X,A,B] implies 
out[A,B,C] and

lemma37b: for A, B, C, D being object  holds betS[A,B,C] & betS[B,C,D] implies 
betS[A,B,D]

  proof 
  let a, b, c  be object;
  assume H0: betS[a,b,c];
  assume H1: a <> b;
  H2: b <> a by H1;
    consider c34 being object  such that H3: betS[b,a,c34] & cong[a,c34,b,a] by 
H2,H2,lemmaextension;
  H4: c34 = c34;
  H5: betS[b,a,c34] by H3;
  H6: betS[c34,a,b] by H5,axiombetweennesssymmetry;
  H7: betS[c34,a,c] by H6,H0,lemma37b;
  H8: out[a,b,c] by H7,H6,defray2;
  H9: out[a,b,c] by H4,H8;
  thus thesis by H9;
  end;
EOF

$ cargo run --release
    Finished release [optimized + debuginfo] target(s) in 0.09s
     Running `target/release/miz-rs`
   0: tlarus   in 0.004s                                                                
success: 9                                                                              
$

digama0 / mizar-rs

mizar-rs and Larus mizar export #6