{"formation":[{"steps":0,"faithful":0,"wrapping":0,"saturating":0,"extra":"0"},{"steps":1,"faithful":1,"wrapping":1,"saturating":1,"extra":"1"},{"steps":2,"faithful":2,"wrapping":2,"saturating":1,"extra":"2"},{"steps":3,"faithful":3,"wrapping":0,"saturating":1,"extra":"3"},{"steps":4,"faithful":4,"wrapping":1,"saturating":1,"extra":"4"},{"steps":5,"faithful":5,"wrapping":2,"saturating":1,"extra":"5"},{"steps":6,"faithful":6,"wrapping":0,"saturating":1,"extra":"6"},{"steps":7,"faithful":7,"wrapping":1,"saturating":1,"extra":"7"},{"steps":8,"faithful":8,"wrapping":2,"saturating":1,"extra":"8"},{"steps":9,"faithful":9,"wrapping":0,"saturating":1,"extra":"9"},{"steps":10,"faithful":10,"wrapping":1,"saturating":1,"extra":"10"},{"steps":11,"faithful":11,"wrapping":2,"saturating":1,"extra":"11"},{"steps":12,"faithful":12,"wrapping":0,"saturating":1,"extra":"12"}]} 'ActualMathematics.FormationLesson.faithful_generated_iff_peano' does not depend on any axioms 'ActualMathematics.FormationLesson.unique_faithful_translation' does not depend on any axioms 'ActualMathematics.FormationLesson.wrap_not_faithful' does not depend on any axioms 'ActualMathematics.FormationLesson.extra_fold' does not depend on any axioms 'ActualMathematics.FormationLesson.extra_unreachable' does not depend on any axioms 'ActualMathematics.FormationLesson.three_independent_failures' does not depend on any axioms