Proof: Do Append 15

Let's prove the following theorem:

result of appending (Python object: [ entry "__class_name__": "Dog", [ ] ]) to [ ] = [ Python object: [ entry "__class_name__": "Dog", [ ] ], [ ] ]

Proof:

View as a tree | View dependent proofs | Try proving it

Proof Table

#	Claim	Reason
1	result of appending (Python object: [ entry "__class_name__": "Dog", [ ] ]) to [ ] = reverse of [ Python object: [ entry "__class_name__": "Dog", [ ] ], reverse of [ ] ]	result of appending (Python object: [ entry "__class_name__": "Dog", [ ] ]) to [ ] = reverse of [ Python object: [ entry "__class_name__": "Dog", [ ] ], reverse of [ ] ] (Appending to a List Property)
2	reverse of [ ] = [ ]	reverse of [ ] = [ ] (do_reverse_14_0)
3	[ Python object: [ entry "__class_name__": "Dog", [ ] ], reverse of [ ] ] = [ Python object: [ entry "__class_name__": "Dog", [ ] ], [ ] ]	if reverse of [ ] = [ ], then [ Python object: [ entry "__class_name__": "Dog", [ ] ], reverse of [ ] ] = [ Python object: [ entry "__class_name__": "Dog", [ ] ], [ ] ] (Substitution)
4	reverse of [ Python object: [ entry "__class_name__": "Dog", [ ] ], reverse of [ ] ] = reverse of [ Python object: [ entry "__class_name__": "Dog", [ ] ], [ ] ]	if [ Python object: [ entry "__class_name__": "Dog", [ ] ], reverse of [ ] ] = [ Python object: [ entry "__class_name__": "Dog", [ ] ], [ ] ], then reverse of [ Python object: [ entry "__class_name__": "Dog", [ ] ], reverse of [ ] ] = reverse of [ Python object: [ entry "__class_name__": "Dog", [ ] ], [ ] ] (Substitution)
5	reverse of [ Python object: [ entry "__class_name__": "Dog", [ ] ], [ ] ] = [ Python object: [ entry "__class_name__": "Dog", [ ] ], [ ] ]	reverse of [ Python object: [ entry "__class_name__": "Dog", [ ] ], [ ] ] = [ Python object: [ entry "__class_name__": "Dog", [ ] ], [ ] ] (do_reverse_15_1)
6	reverse of [ Python object: [ entry "__class_name__": "Dog", [ ] ], reverse of [ ] ] = [ Python object: [ entry "__class_name__": "Dog", [ ] ], [ ] ]	if reverse of [ Python object: [ entry "__class_name__": "Dog", [ ] ], reverse of [ ] ] = reverse of [ Python object: [ entry "__class_name__": "Dog", [ ] ], [ ] ] and reverse of [ Python object: [ entry "__class_name__": "Dog", [ ] ], [ ] ] = [ Python object: [ entry "__class_name__": "Dog", [ ] ], [ ] ], then reverse of [ Python object: [ entry "__class_name__": "Dog", [ ] ], reverse of [ ] ] = [ Python object: [ entry "__class_name__": "Dog", [ ] ], [ ] ] (Transitive Property of Equality)
7	result of appending (Python object: [ entry "__class_name__": "Dog", [ ] ]) to [ ] = [ Python object: [ entry "__class_name__": "Dog", [ ] ], [ ] ]	if result of appending (Python object: [ entry "__class_name__": "Dog", [ ] ]) to [ ] = reverse of [ Python object: [ entry "__class_name__": "Dog", [ ] ], reverse of [ ] ] and reverse of [ Python object: [ entry "__class_name__": "Dog", [ ] ], reverse of [ ] ] = [ Python object: [ entry "__class_name__": "Dog", [ ] ], [ ] ], then result of appending (Python object: [ entry "__class_name__": "Dog", [ ] ]) to [ ] = [ Python object: [ entry "__class_name__": "Dog", [ ] ], [ ] ] (Transitive Property of Equality)

Comments

Please log in to add comments