Update De_Rham_Cohomology_of_smooth_manifolds.cpp

De_Rham_Cohomology_of_smooth_manifolds.cpp

@@ -26,30 +26,30 @@ int main (/* implementation-defined */)
     Suppose_literal (for_all_p_there_is_an_open_neighbourhood_U, true);
     Suppose_literal (U_is_homeomorphic_to_an_open_subset_V, true);
 
-    auto manifold_of_dimension_n = M_is_Hausdorff. And (points_can_be_seperated_by_open_sets). And (M_is_second_countable). And (M_has_a_countable_topological_base). And (p_is_element_of_M). And (U_is_proper_subset_of_M). And (V_is_subset_of_real_coordinate_space_of_dimension_n). And (for_all_p_there_is_an_open_neighbourhood_U). And (U_is_homeomorphic_to_an_open_subset_V). Implying (a_topological_space_M);
-
-    bool M_is_a_manifold_of_dimension_n = manifold_of_dimension_n. Value (/* truth value */);
-    Suppose_literal (let_M_be_a_manifold_of_dimension_n, M_is_a_manifold_of_dimension_n);
-
-    // like the supposed literal a_topological_space_M, you may introduce a function for each literal below
-    Suppose_literal (U_is_element_of_M, true);
-    Suppose_literal (a_pair_U_psi_where_U_is_open, true);
-    Suppose_literal (psi_maps_U_to_V_a_homeomorphism_to_some_open_V, true);
-
-    auto chart = let_M_be_a_manifold_of_dimension_n. And (U_is_element_of_M). And (a_pair_U_psi_where_U_is_open). And (psi_maps_U_to_V_a_homeomorphism_to_some_open_V);
-
-    Suppose_literal (the_pair_U_phi_is_a_chart_M, chart. Value(/* truth value */));
-
-    // like the supposed literal a_topological_space_M, you may introduce a function for each literal below
-    Suppose_literal (p_is_element_of_the_pair_U_phi, true);
-    Suppose_literal (p_is_element_of_U, true);
-    Suppose_literal (for_all_p_for_some_chart, true);
-
-    auto remark_2_1 = the_pair_U_phi_is_a_chart_M. And (p_is_element_of_U). Implying (p_is_element_of_the_pair_U_phi);
-
-    auto third_condition_from_definition_2_1 = for_all_p_there_is_an_open_neighbourhood_U. And (U_is_element_of_M). And (U_is_homeomorphic_to_an_open_subset_V). And (V_is_subset_of_real_coordinate_space_of_dimension_n);
-
-    auto rewrite_third_condition_from_definition_2_1 = for_all_p_for_some_chart. Implying (third_condition_from_definition_2_1);
+    Satisfy::Formula manifold_of_dimension_n = M_is_Hausdorff. And (points_can_be_seperated_by_open_sets). And (M_is_second_countable). And (M_has_a_countable_topological_base). And (p_is_element_of_M). And (U_is_proper_subset_of_M). And (V_is_subset_of_real_coordinate_space_of_dimension_n). And (for_all_p_there_is_an_open_neighbourhood_U). And (U_is_homeomorphic_to_an_open_subset_V). Implying (a_topological_space_M);
+
+    bool M_is_a_manifold_of_dimension_n = manifold_of_dimension_n. Value (/* truth value */);
+    Suppose_literal (let_M_be_a_manifold_of_dimension_n, M_is_a_manifold_of_dimension_n);
+
+    // like the supposed literal a_topological_space_M, you may introduce a function for each literal below
+    Suppose_literal (U_is_element_of_M, true);
+    Suppose_literal (a_pair_U_psi_where_U_is_open, true);
+    Suppose_literal (psi_maps_U_to_V_a_homeomorphism_to_some_open_V, true);
+
+    auto chart = let_M_be_a_manifold_of_dimension_n. And (U_is_element_of_M). And (a_pair_U_psi_where_U_is_open). And (psi_maps_U_to_V_a_homeomorphism_to_some_open_V);
+
+    Suppose_literal (the_pair_U_phi_is_a_chart_M, chart. Value(/* truth value */));
+
+    // like the supposed literal a_topological_space_M, you may introduce a function for each literal below
+    Suppose_literal (p_is_element_of_the_pair_U_phi, true);
+    Suppose_literal (p_is_element_of_U, true);
+    Suppose_literal (for_all_p_for_some_chart, true);
+
+    Satisfy::Formula remark_2_1 = the_pair_U_phi_is_a_chart_M. And (p_is_element_of_U). Implying (p_is_element_of_the_pair_U_phi);
+
+    auto third_condition_from_definition_2_1 = for_all_p_there_is_an_open_neighbourhood_U. And (U_is_element_of_M). And (U_is_homeomorphic_to_an_open_subset_V). And (V_is_subset_of_real_coordinate_space_of_dimension_n);
+
+    Satisfy::Formula rewrite_third_condition_from_definition_2_1 = for_all_p_for_some_chart. Implying (third_condition_from_definition_2_1);
 
     return 0;
 }