(def-theorem lct-obligation-1"#(restrict2{mul,b,b},[b%sort,b%sort,b%sort])"lemma (theory lct-theory) (proof ( sort-definedness simplify (apply-macete-with-minor-premises b%sort-defining-axiom_lct-theory) (apply-macete-with-minor-premises lct-macete) )))

(def-theorem lct-obligation-2"#(restrict{inv,b},[b%sort,b%sort])"lemma (theory lct-theory) (proof ( sort-definedness simplify (apply-macete-with-minor-premises b%sort-defining-axiom_lct-theory) (apply-macete-with-minor-premises lct-macete) )))

(def-theorem lct-obligation-3"#(restrict2{right%trans,a%cosets,b},[a%cosets%sort,b%sort,a%cosets%sort])"lemma (theory lct-theory) (proof ( sort-definedness direct-inference (case-split ("#(xx_0,sets[gg])")) simplify (unfold-single-defined-constant-globally a%cosets) simplify direct-and-antecedent-inference-strategy (apply-macete-with-minor-premises a%cosets%sort-defining-axiom_lct-theory) simplify (unfold-single-defined-constant-globally a%cosets) simplify (backchain"with(g:gg,xx_0:sets[gg],xx_0=right%trans(a,g))") (instantiate-existential ("g mul xx_1")) (apply-macete-with-minor-premises lct-macete) (apply-macete-with-minor-premises simplify-set-translations) simplify )))

(def-theorem lct-obligation-4"forall(x:b%sort,inv(x) in b)"lemma (theory lct-theory) (proof ( (apply-macete-with-minor-premises lct-macete) )))

(def-theorem lct-obligation-5"forall(x,y:b%sort,(x mul y) in b)"lemma (theory lct-theory) (proof ( (apply-macete-with-minor-premises lct-macete) )))

(def-theorem lct-obligation-6"forall(g,h:b%sort,(g mul h) in b) and (forall(alpha:a%cosets%sort,g:b%sort, right%trans(alpha,g) in a%cosets) and forall(alpha:a%cosets%sort,g,h:b%sort, right%trans(alpha,g mul h)=right%trans(right%trans(alpha,g),h)))"lemma (theory lct-theory) (proof ( (apply-macete-with-minor-premises lct-macete) direct-and-antecedent-inference-strategy (block (script-comment"node added by `direct-and-antecedent-inference-strategy' at (0 0)") (unfold-single-defined-constant-globally a%cosets) simplify (cut-with-single-formula"alpha in a%cosets") (block (script-comment"node added by `cut-with-single-formula' at (0)") (incorporate-antecedent"with(p:prop,p);") (unfold-single-defined-constant-globally a%cosets) simplify direct-and-antecedent-inference-strategy (backchain"with(f:sets[gg],alpha:a%cosets%sort,alpha=f);") (instantiate-existential ("g_$0 mul g")) (block (script-comment"node added by `instantiate-existential' at (0 0)") (apply-macete-with-minor-premises lct-macete) (apply-macete-with-minor-premises b%sort-members-are-in-b)) (apply-macete-with-minor-premises simplify-set-translations)) (apply-macete-with-minor-premises a%cosets%sort-members-are-in-a%cosets)) (apply-macete-with-minor-premises simplify-set-translations) )))