-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathrmorphism.txt
1 lines (1 loc) · 14.1 KB
/
rmorphism.txt
1
Compose [Alpha (TensorO (Star (OVar LeftLoop)) (TensorO (OVar LeftLeg) (OVar LeftLoop))) (TensorO (TensorO (TensorO (Star (OVar LeftLoop)) (Star (OVar LeftLeg))) (OVar LeftLoop)) (Star (OVar RightLoop))) (TensorO (OVar RightLeg) (Star (TensorO (TensorO (TensorO (Star (OVar LeftLoop)) (Star (OVar LeftLeg))) (OVar LeftLoop)) (Star (OVar RightLoop))))),TensorM (TensorM (Alpha (Star (OVar LeftLoop)) (OVar LeftLeg) (OVar LeftLoop)) (Id (TensorO (TensorO (TensorO (Star (OVar LeftLoop)) (Star (OVar LeftLeg))) (OVar LeftLoop)) (Star (OVar RightLoop))))) (TensorM (Id (OVar RightLeg)) (Id (Star (TensorO (TensorO (TensorO (Star (OVar LeftLoop)) (Star (OVar LeftLeg))) (OVar LeftLoop)) (Star (OVar RightLoop)))))),TensorM (TensorM (Id (TensorO (TensorO (TensorO (Star (OVar LeftLoop)) (OVar LeftLeg)) (OVar LeftLoop)) (TensorO (TensorO (TensorO (Star (OVar LeftLoop)) (Star (OVar LeftLeg))) (OVar LeftLoop)) (Star (OVar RightLoop))))) (Ev (OVar RightLoop))) (Id (TensorO (OVar RightLeg) (Star (TensorO (TensorO (TensorO (Star (OVar LeftLoop)) (Star (OVar LeftLeg))) (OVar LeftLoop)) (Star (OVar RightLoop)))))),TensorM (Compose [AlphaI (TensorO (TensorO (Star (OVar LeftLoop)) (OVar LeftLeg)) (OVar LeftLoop)) (TensorO (TensorO (TensorO (Star (OVar LeftLoop)) (Star (OVar LeftLeg))) (OVar LeftLoop)) (Star (OVar RightLoop))) (OVar RightLoop),AlphaI (TensorO (Star (OVar LeftLoop)) (OVar LeftLeg)) (OVar LeftLoop) (TensorO (TensorO (TensorO (TensorO (Star (OVar LeftLoop)) (Star (OVar LeftLeg))) (OVar LeftLoop)) (Star (OVar RightLoop))) (OVar RightLoop)),AlphaI (Star (OVar LeftLoop)) (OVar LeftLeg) (TensorO (OVar LeftLoop) (TensorO (TensorO (TensorO (TensorO (Star (OVar LeftLoop)) (Star (OVar LeftLeg))) (OVar LeftLoop)) (Star (OVar RightLoop))) (OVar RightLoop))),TensorM (Id (Star (OVar LeftLoop))) (TensorM (Id (OVar LeftLeg)) (TensorM (Id (OVar LeftLoop)) (AlphaI (TensorO (TensorO (Star (OVar LeftLoop)) (Star (OVar LeftLeg))) (OVar LeftLoop)) (Star (OVar RightLoop)) (OVar RightLoop)))),TensorM (Id (Star (OVar LeftLoop))) (TensorM (Id (OVar LeftLeg)) (Alpha (OVar LeftLoop) (TensorO (TensorO (Star (OVar LeftLoop)) (Star (OVar LeftLeg))) (OVar LeftLoop)) (TensorO (Star (OVar RightLoop)) (OVar RightLoop)))),TensorM (Id (Star (OVar LeftLoop))) (Alpha (OVar LeftLeg) (TensorO (OVar LeftLoop) (TensorO (TensorO (Star (OVar LeftLoop)) (Star (OVar LeftLeg))) (OVar LeftLoop))) (TensorO (Star (OVar RightLoop)) (OVar RightLoop))),Alpha (Star (OVar LeftLoop)) (TensorO (OVar LeftLeg) (TensorO (OVar LeftLoop) (TensorO (TensorO (Star (OVar LeftLoop)) (Star (OVar LeftLeg))) (OVar LeftLoop)))) (TensorO (Star (OVar RightLoop)) (OVar RightLoop)),TensorM (TensorM (Id (Star (OVar LeftLoop))) (TensorM (Id (OVar LeftLeg)) (Alpha (OVar LeftLoop) (TensorO (Star (OVar LeftLoop)) (Star (OVar LeftLeg))) (OVar LeftLoop)))) (TensorM (Id (Star (OVar RightLoop))) (Id (OVar RightLoop))),TensorM (TensorM (Id (Star (OVar LeftLoop))) (Alpha (OVar LeftLeg) (TensorO (OVar LeftLoop) (TensorO (Star (OVar LeftLoop)) (Star (OVar LeftLeg)))) (OVar LeftLoop))) (TensorM (Id (Star (OVar RightLoop))) (Id (OVar RightLoop))),TensorM (Alpha (Star (OVar LeftLoop)) (TensorO (OVar LeftLeg) (TensorO (OVar LeftLoop) (TensorO (Star (OVar LeftLoop)) (Star (OVar LeftLeg))))) (OVar LeftLoop)) (TensorM (Id (Star (OVar RightLoop))) (Id (OVar RightLoop))),TensorM (TensorM (TensorM (Id (Star (OVar LeftLoop))) (TensorM (Id (OVar LeftLeg)) (Alpha (OVar LeftLoop) (Star (OVar LeftLoop)) (Star (OVar LeftLeg))))) (Id (OVar LeftLoop))) (TensorM (Id (Star (OVar RightLoop))) (Id (OVar RightLoop))),TensorM (TensorM (TensorM (Id (Star (OVar LeftLoop))) (Alpha (OVar LeftLeg) (TensorO (OVar LeftLoop) (Star (OVar LeftLoop))) (Star (OVar LeftLeg)))) (Id (OVar LeftLoop))) (TensorM (Id (Star (OVar RightLoop))) (Id (OVar RightLoop))),TensorM (TensorM (Id (TensorO (TensorO (Star (OVar LeftLoop)) (TensorO (TensorO (OVar LeftLeg) (TensorO (OVar LeftLoop) (Star (OVar LeftLoop)))) (Star (OVar LeftLeg)))) (OVar LeftLoop))) (Ev One)) (Id (TensorO (Star (OVar RightLoop)) (OVar RightLoop))),TensorM (Compose [AlphaI (TensorO (Star (OVar LeftLoop)) (TensorO (TensorO (OVar LeftLeg) (TensorO (OVar LeftLoop) (Star (OVar LeftLoop)))) (Star (OVar LeftLeg)))) (OVar LeftLoop) One,AlphaI (Star (OVar LeftLoop)) (TensorO (TensorO (OVar LeftLeg) (TensorO (OVar LeftLoop) (Star (OVar LeftLoop)))) (Star (OVar LeftLeg))) (TensorO (OVar LeftLoop) One),TensorM (Id (Star (OVar LeftLoop))) (Rho (TensorO (TensorO (TensorO (OVar LeftLeg) (TensorO (OVar LeftLoop) (Star (OVar LeftLoop)))) (Star (OVar LeftLeg))) (TensorO (OVar LeftLoop) One))),TensorM (Id (Star (OVar LeftLoop))) (TensorM (Id (TensorO (TensorO (TensorO (OVar LeftLeg) (TensorO (OVar LeftLoop) (Star (OVar LeftLoop)))) (Star (OVar LeftLeg))) (TensorO (OVar LeftLoop) One))) (Ev (OVar LeftLoop))),TensorM (Id (Star (OVar LeftLoop))) (Alpha (TensorO (TensorO (TensorO (OVar LeftLeg) (TensorO (OVar LeftLoop) (Star (OVar LeftLoop)))) (Star (OVar LeftLeg))) (TensorO (OVar LeftLoop) One)) (Star (OVar LeftLoop)) (OVar LeftLoop)),TensorM (Id (Star (OVar LeftLoop))) (TensorM (Compose [AlphaI (TensorO (TensorO (OVar LeftLeg) (TensorO (OVar LeftLoop) (Star (OVar LeftLoop)))) (Star (OVar LeftLeg))) (TensorO (OVar LeftLoop) One) (Star (OVar LeftLoop)),TensorM (TensorM (Id (TensorO (TensorO (OVar LeftLeg) (TensorO (OVar LeftLoop) (Star (OVar LeftLoop)))) (Star (OVar LeftLeg)))) (Ev One)) (Id (TensorO (TensorO (OVar LeftLoop) One) (Star (OVar LeftLoop)))),TensorM (Compose [AlphaI (TensorO (OVar LeftLeg) (TensorO (OVar LeftLoop) (Star (OVar LeftLoop)))) (Star (OVar LeftLeg)) One,AlphaI (OVar LeftLeg) (TensorO (OVar LeftLoop) (Star (OVar LeftLoop))) (TensorO (Star (OVar LeftLeg)) One),TensorM (Id (OVar LeftLeg)) (Rho (TensorO (TensorO (OVar LeftLoop) (Star (OVar LeftLoop))) (TensorO (Star (OVar LeftLeg)) One))),TensorM (Id (OVar LeftLeg)) (TensorM (Id (TensorO (TensorO (OVar LeftLoop) (Star (OVar LeftLoop))) (TensorO (Star (OVar LeftLeg)) One))) (Ev (Star (OVar LeftLeg)))),TensorM (Id (OVar LeftLeg)) (Alpha (TensorO (TensorO (OVar LeftLoop) (Star (OVar LeftLoop))) (TensorO (Star (OVar LeftLeg)) One)) (OVar LeftLeg) (Star (OVar LeftLeg))),TensorM (Id (OVar LeftLeg)) (TensorM (Compose [AlphaI (TensorO (OVar LeftLoop) (Star (OVar LeftLoop))) (TensorO (Star (OVar LeftLeg)) One) (OVar LeftLeg),TensorM (TensorM (Id (TensorO (OVar LeftLoop) (Star (OVar LeftLoop)))) (Ev One)) (Id (TensorO (TensorO (Star (OVar LeftLeg)) One) (OVar LeftLeg))),TensorM (Compose [AlphaI (OVar LeftLoop) (Star (OVar LeftLoop)) One,TensorM (Id (OVar LeftLoop)) (Rho (TensorO (Star (OVar LeftLoop)) One)),TensorM (Id (OVar LeftLoop)) (TensorM (Id (TensorO (Star (OVar LeftLoop)) One)) (Ev (Star (OVar LeftLoop)))),TensorM (Id (OVar LeftLoop)) (Alpha (TensorO (Star (OVar LeftLoop)) One) (OVar LeftLoop) (Star (OVar LeftLoop))),TensorM (Id (OVar LeftLoop)) (TensorM (Compose [TensorM (RhoI (Star (OVar LeftLoop))) (Id (OVar LeftLoop)),Coev (OVar LeftLoop)]) (Id (Star (OVar LeftLoop)))),TensorM (PivotalJI (OVar LeftLoop)) (LambdaI (Star (OVar LeftLoop))),Coev (Star (OVar LeftLoop))]) (Compose [TensorM (Id (Star One)) (Rho (TensorO (TensorO (Star (OVar LeftLeg)) One) (OVar LeftLeg))),TensorM (Id (Star One)) (TensorM (Id (TensorO (TensorO (Star (OVar LeftLeg)) One) (OVar LeftLeg))) (Ev One)),TensorM (Id (Star One)) (Alpha (TensorO (TensorO (Star (OVar LeftLeg)) One) (OVar LeftLeg)) (Star One) One),TensorM (Id (Star One)) (TensorM (Compose [AlphaI (TensorO (Star (OVar LeftLeg)) One) (OVar LeftLeg) (Star One),TensorM (RhoI (Star (OVar LeftLeg))) (TensorM (Id (OVar LeftLeg)) (Id (Star One))),TensorM (Id (Star (OVar LeftLeg))) (RhoI (OVar LeftLeg)),Coev (OVar LeftLeg)]) (Id One)),TensorM (PivotalJI (Star One)) (LambdaI One),Coev One])]) (Id (Star (OVar LeftLeg)))),TensorM (PivotalJI (OVar LeftLeg)) (LambdaI (Star (OVar LeftLeg))),Coev (Star (OVar LeftLeg))]) (Compose [TensorM (Id (Star One)) (Rho (TensorO (TensorO (OVar LeftLoop) One) (Star (OVar LeftLoop)))),TensorM (Id (Star One)) (TensorM (Id (TensorO (TensorO (OVar LeftLoop) One) (Star (OVar LeftLoop)))) (Ev One)),TensorM (Id (Star One)) (Alpha (TensorO (TensorO (OVar LeftLoop) One) (Star (OVar LeftLoop))) (Star One) One),TensorM (Id (Star One)) (TensorM (Compose [AlphaI (TensorO (OVar LeftLoop) One) (Star (OVar LeftLoop)) (Star One),AlphaI (OVar LeftLoop) One (TensorO (Star (OVar LeftLoop)) (Star One)),TensorM (Id (OVar LeftLoop)) (Rho (TensorO One (TensorO (Star (OVar LeftLoop)) (Star One)))),TensorM (Id (OVar LeftLoop)) (TensorM (Id (TensorO One (TensorO (Star (OVar LeftLoop)) (Star One)))) (Ev (Star (OVar LeftLoop)))),TensorM (Id (OVar LeftLoop)) (Alpha (TensorO One (TensorO (Star (OVar LeftLoop)) (Star One))) (OVar LeftLoop) (Star (OVar LeftLoop))),TensorM (Id (OVar LeftLoop)) (TensorM (Compose [AlphaI One (TensorO (Star (OVar LeftLoop)) (Star One)) (OVar LeftLoop),TensorM (Id One) (Rho (TensorO (TensorO (Star (OVar LeftLoop)) (Star One)) (OVar LeftLoop))),TensorM (Id One) (TensorM (Id (TensorO (TensorO (Star (OVar LeftLoop)) (Star One)) (OVar LeftLoop))) (Ev (Star One))),TensorM (Id One) (Alpha (TensorO (TensorO (Star (OVar LeftLoop)) (Star One)) (OVar LeftLoop)) One (Star One)),TensorM (Id One) (TensorM (Compose [AlphaI (TensorO (Star (OVar LeftLoop)) (Star One)) (OVar LeftLoop) One,TensorM (TensorM (Id (Star (OVar LeftLoop))) (Id (Star One))) (RhoI (OVar LeftLoop)),TensorM (RhoI (Star (OVar LeftLoop))) (Id (OVar LeftLoop)),Coev (OVar LeftLoop)]) (Id (Star One))),TensorM (PivotalJI One) (LambdaI (Star One)),Coev (Star One)]) (Id (Star (OVar LeftLoop)))),TensorM (PivotalJI (OVar LeftLoop)) (LambdaI (Star (OVar LeftLoop))),Coev (Star (OVar LeftLoop))]) (Id One)),TensorM (PivotalJI (Star One)) (LambdaI One),Coev One])]) (Id (OVar LeftLoop))),TensorM (PivotalJI (Star (OVar LeftLoop))) (LambdaI (OVar LeftLoop)),Coev (OVar LeftLoop)]) (Compose [TensorM (Id (Star One)) (Rho (TensorO (Star (OVar RightLoop)) (OVar RightLoop))),TensorM (Id (Star One)) (TensorM (Id (TensorO (Star (OVar RightLoop)) (OVar RightLoop))) (Ev One)),TensorM (Id (Star One)) (Alpha (TensorO (Star (OVar RightLoop)) (OVar RightLoop)) (Star One) One),TensorM (Id (Star One)) (TensorM (Compose [AlphaI (Star (OVar RightLoop)) (OVar RightLoop) (Star One),TensorM (Id (Star (OVar RightLoop))) (RhoI (OVar RightLoop)),Coev (OVar RightLoop)]) (Id One)),TensorM (PivotalJI (Star One)) (LambdaI One),Coev One])]) (Compose [TensorM (Id (Star (OVar RightLoop))) (Rho (TensorO (OVar RightLeg) (Star (TensorO (TensorO (TensorO (Star (OVar LeftLoop)) (Star (OVar LeftLeg))) (OVar LeftLoop)) (Star (OVar RightLoop)))))),TensorM (Id (Star (OVar RightLoop))) (TensorM (Id (TensorO (OVar RightLeg) (Star (TensorO (TensorO (TensorO (Star (OVar LeftLoop)) (Star (OVar LeftLeg))) (OVar LeftLoop)) (Star (OVar RightLoop)))))) (Ev (OVar RightLoop))),TensorM (Id (Star (OVar RightLoop))) (Alpha (TensorO (OVar RightLeg) (Star (TensorO (TensorO (TensorO (Star (OVar LeftLoop)) (Star (OVar LeftLeg))) (OVar LeftLoop)) (Star (OVar RightLoop))))) (Star (OVar RightLoop)) (OVar RightLoop)),TensorM (Id (Star (OVar RightLoop))) (TensorM (Compose [AlphaI (OVar RightLeg) (Star (TensorO (TensorO (TensorO (Star (OVar LeftLoop)) (Star (OVar LeftLeg))) (OVar LeftLoop)) (Star (OVar RightLoop)))) (Star (OVar RightLoop)),TensorM (Id (OVar RightLeg)) (Rho (TensorO (Star (TensorO (TensorO (TensorO (Star (OVar LeftLoop)) (Star (OVar LeftLeg))) (OVar LeftLoop)) (Star (OVar RightLoop)))) (Star (OVar RightLoop)))),TensorM (Id (OVar RightLeg)) (TensorM (Id (TensorO (Star (TensorO (TensorO (TensorO (Star (OVar LeftLoop)) (Star (OVar LeftLeg))) (OVar LeftLoop)) (Star (OVar RightLoop)))) (Star (OVar RightLoop)))) (Ev (Star (OVar RightLeg)))),TensorM (Id (OVar RightLeg)) (Alpha (TensorO (Star (TensorO (TensorO (TensorO (Star (OVar LeftLoop)) (Star (OVar LeftLeg))) (OVar LeftLoop)) (Star (OVar RightLoop)))) (Star (OVar RightLoop))) (OVar RightLeg) (Star (OVar RightLeg))),TensorM (Id (OVar RightLeg)) (TensorM (Compose [AlphaI (Star (TensorO (TensorO (TensorO (Star (OVar LeftLoop)) (Star (OVar LeftLeg))) (OVar LeftLoop)) (Star (OVar RightLoop)))) (Star (OVar RightLoop)) (OVar RightLeg),TensorM (Id (Star (TensorO (TensorO (TensorO (Star (OVar LeftLoop)) (Star (OVar LeftLeg))) (OVar LeftLoop)) (Star (OVar RightLoop))))) (Rho (TensorO (Star (OVar RightLoop)) (OVar RightLeg))),TensorM (Id (Star (TensorO (TensorO (TensorO (Star (OVar LeftLoop)) (Star (OVar LeftLeg))) (OVar LeftLoop)) (Star (OVar RightLoop))))) (TensorM (Id (TensorO (Star (OVar RightLoop)) (OVar RightLeg))) (Ev (TensorO (TensorO (TensorO (Star (OVar LeftLoop)) (Star (OVar LeftLeg))) (OVar LeftLoop)) (Star (OVar RightLoop))))),TensorM (Id (Star (TensorO (TensorO (TensorO (Star (OVar LeftLoop)) (Star (OVar LeftLeg))) (OVar LeftLoop)) (Star (OVar RightLoop))))) (Alpha (TensorO (Star (OVar RightLoop)) (OVar RightLeg)) (Star (TensorO (TensorO (TensorO (Star (OVar LeftLoop)) (Star (OVar LeftLeg))) (OVar LeftLoop)) (Star (OVar RightLoop)))) (TensorO (TensorO (TensorO (Star (OVar LeftLoop)) (Star (OVar LeftLeg))) (OVar LeftLoop)) (Star (OVar RightLoop)))),TensorM (Id (Star (TensorO (TensorO (TensorO (Star (OVar LeftLoop)) (Star (OVar LeftLeg))) (OVar LeftLoop)) (Star (OVar RightLoop))))) (TensorM (Compose [AlphaI (Star (OVar RightLoop)) (OVar RightLeg) (Star (TensorO (TensorO (TensorO (Star (OVar LeftLoop)) (Star (OVar LeftLeg))) (OVar LeftLoop)) (Star (OVar RightLoop)))),TensorM (Id (Star (OVar RightLoop))) (Alpha (OVar RightLeg) (OVar RightLoop) (Star (TensorO (TensorO (Star (OVar LeftLoop)) (Star (OVar LeftLeg))) (OVar LeftLoop)))),Alpha (Star (OVar RightLoop)) (TensorO (OVar RightLeg) (OVar RightLoop)) (Star (TensorO (TensorO (Star (OVar LeftLoop)) (Star (OVar LeftLeg))) (OVar LeftLoop))),Phi]) (Id (TensorO (TensorO (TensorO (Star (OVar LeftLoop)) (Star (OVar LeftLeg))) (OVar LeftLoop)) (Star (OVar RightLoop))))),TensorM (PivotalJI (Star (TensorO (TensorO (TensorO (Star (OVar LeftLoop)) (Star (OVar LeftLeg))) (OVar LeftLoop)) (Star (OVar RightLoop))))) (LambdaI (TensorO (TensorO (TensorO (Star (OVar LeftLoop)) (Star (OVar LeftLeg))) (OVar LeftLoop)) (Star (OVar RightLoop)))),Coev (TensorO (TensorO (TensorO (Star (OVar LeftLoop)) (Star (OVar LeftLeg))) (OVar LeftLoop)) (Star (OVar RightLoop)))]) (Id (Star (OVar RightLeg)))),TensorM (PivotalJI (OVar RightLeg)) (LambdaI (Star (OVar RightLeg))),Coev (Star (OVar RightLeg))]) (Id (OVar RightLoop))),TensorM (PivotalJI (Star (OVar RightLoop))) (LambdaI (OVar RightLoop)),Coev (OVar RightLoop)])]