session matrices_ring_simp = NTP4Verif +
theories
  "matrices_ring_simp_Symb_symb_oppqtvc"
  "matrices_ring_simp_Symb_lm_merge_okqtvc"
  "matrices_ring_simp_Symb_lm_dump_okqtvc"
  "matrices_ring_simp_Symb_symb_mulqtvc"
  "matrices_ring_simp_Symb_symb_subqtvc"
  "matrices_ring_simp_Symb_cat_okqtvc"
  "matrices_ring_simp_Symb_symb_regqtvc"
  "matrices_ring_simp_Symb_l_mdl_okqtvc"
  "matrices_ring_simp_Symb_harnessqtvc"
  "matrices_ring_simp_Symb_lm_distribute_okqtvc"
  "matrices_ring_simp_Symb_m_collapse_okqtvc"
  "matrices_ring_simp_Symb_m_mdl_okqtvc"
  "matrices_ring_simp_Symb_lm_collapse_okqtvc"
  "matrices_ring_simp_Symb_l_compare_zeroqtvc"
  "matrices_ring_simp_Symb_symb_addqtvc"
  "matrices_ring_simp_Symb_cat_rev_okqtvc"
  "matrices_ring_simp_Symb_extends_rwqtvc"
  "matrices_ring_simp_Symb_lm_mdl_okqtvc"
  "matrices_ring_simp_Symb_m_distribute_okqtvc"
  "matrices_ring_simp_Symb_lm_opp_okqtvc"
  "matrices_ring_simp_Symb_m_mul_okqtvc"
  "matrices_ring_simp_Symb_lm_mdl_sameqtvc"
  "matrices_ring_simp_Symb_symb_envqtvc"
