diff --git a/server/testgame/TestGame/Levels/Contradiction.lean b/server/testgame/TestGame/Levels/Contradiction.lean index b62ccb7..fd52d01 100644 --- a/server/testgame/TestGame/Levels/Contradiction.lean +++ b/server/testgame/TestGame/Levels/Contradiction.lean @@ -4,3 +4,7 @@ import TestGame.Levels.Contradiction.L03_ByContra import TestGame.Levels.Contradiction.L04_ByContra import TestGame.Levels.Contradiction.L05_Contrapose import TestGame.Levels.Contradiction.L06_Summary + +Game "TestGame" +World "Predicate" +Title "Widerspruch" diff --git a/server/testgame/TestGame/Levels/Implication.lean b/server/testgame/TestGame/Levels/Implication.lean index d88d75a..9c69a80 100644 --- a/server/testgame/TestGame/Levels/Implication.lean +++ b/server/testgame/TestGame/Levels/Implication.lean @@ -13,4 +13,4 @@ import TestGame.Levels.Implication.L12_Summary Game "TestGame" World "Implication" -Title "Meer der Implikationen" +Title "Aussagenlogik 2" diff --git a/server/testgame/TestGame/Levels/Induction.lean b/server/testgame/TestGame/Levels/Induction.lean index 88d12a3..cf07e3e 100644 --- a/server/testgame/TestGame/Levels/Induction.lean +++ b/server/testgame/TestGame/Levels/Induction.lean @@ -2,3 +2,7 @@ import TestGame.Levels.Induction.L01_Simp import TestGame.Levels.Induction.L02_Sum import TestGame.Levels.Induction.L03_Induction import TestGame.Levels.Induction.L04_SumOdd + +Game "TestGame" +World "Predicate" +Title "Induktion" diff --git a/server/testgame/TestGame/Levels/Predicate.lean b/server/testgame/TestGame/Levels/Predicate.lean index 43bcc35..c12c91a 100644 --- a/server/testgame/TestGame/Levels/Predicate.lean +++ b/server/testgame/TestGame/Levels/Predicate.lean @@ -10,4 +10,4 @@ import TestGame.Levels.Predicate.L09_Summary Game "TestGame" World "Predicate" -Title "Reich der Prädikate" +Title "Prädikate" diff --git a/server/testgame/TestGame/Levels/Proposition.lean b/server/testgame/TestGame/Levels/Proposition.lean index b458a31..9e1b736 100644 --- a/server/testgame/TestGame/Levels/Proposition.lean +++ b/server/testgame/TestGame/Levels/Proposition.lean @@ -14,4 +14,4 @@ import TestGame.Levels.Proposition.L13_Summary Game "TestGame" World "Proposition" -Title "Land der Proposititionen" +Title "Aussagenlogik 1" diff --git a/server/testgame/TestGame/ToBePorted.lean b/server/testgame/TestGame/ToBePorted.lean index 226d5c7..ed519cc 100644 --- a/server/testgame/TestGame/ToBePorted.lean +++ b/server/testgame/TestGame/ToBePorted.lean @@ -1,8 +1,10 @@ import Mathlib -lemma not_odd {n : ℕ} : ¬ Odd n ↔ Even n := by sorry +lemma not_odd {n : ℕ} : ¬ Odd n ↔ Even n := by + sorry -lemma not_even {n : ℕ} : ¬ Even n ↔ Odd n := by sorry +lemma not_even {n : ℕ} : ¬ Even n ↔ Odd n := by + sorry lemma even_square (n : ℕ) : Even n → Even (n ^ 2) := by intro ⟨x, hx⟩